School of Computing and Information Systems The University of Melbourne
SWEN90004 Modelling Complex Software Systems
Some Concurrency Workshop 4 solutions
The exercises
Copyright By PowCoder代写 加微信 powcoder
1. The two LTS models are shown below:
Note that the model TWO allows a user to release a resource that has not been acquired, whereas ONE does not. Therefore, a trace that is in TWO but not ONE is
a.acquire -> b.release -> …
2. RESOURCE SHAREv2 models a system comprised of two users and two resources, whereas
RESOURCE SHARE models a system comprised of two users and just one resource. For example, a.acquire -> b.acquire -> b.use -> b.release -> a.use -> a.release -> …
is a trace of RESOURCE SHAREv2, but not of RESOURCE SHARE.
3. Here is an FSP definition of RESOURCE SHAREv3:
RESOURCE = (acquire -> release -> RESOURCE).
USER = (acquire -> use -> release -> USER).
||RESOURCE_SHAREv3(N=5) = (u[1..N]:USER || {u[1..N]}::RESOURCE).
4. The models are equivalent, except for the label on the terminal state. ERROR generates a terminal state labelled ¡°-1¡±to signify an error state. STOP generates a normal terminal state, with no outgoing actions, that is, a deadlock state. END generates a terminate state labelled E. The convention is to use END to capture successful termination, deliberate ending of a process (as opposed to STOP which is associated with premature termination, typically deadlock).
5. If we run the three models through the LTS safety check, we get the following output:
Trace to DEADLOCK:
Trace to property violation in ONESHOT:
As expected, STOP results in what is considered a deadlock, whereas ERROR results in a terminal
No deadlocks/errors
state that is signalled as a ¡°property violation¡±. END yields graceful, intended termination.
When LTSA finds a terminal state, it uses the label on the state to decide what to report. If it is a normal label (a non-negative integer), it reports a deadlock. If it is -1, the error state, it reports it as an error. If it is E, is knows that this is a graceful termination, so it reports nothing.
6. Here are the five dining philosophers, assisted by a butler:
const PHIL_NUMBER = 5
PHIL = (sitdown -> right.get -> left.get -> eat
-> left.put -> right.put -> arise -> PHIL).
FORK = (get -> put -> FORK).
BUTLER = BUTLER[0],
BUTLER[i:0..PHIL_NUMBER-1]
= ( when (i < PHIL_NUMBER-1) sitdown -> BUTLER[i+1]
| when (i > 0) arise -> BUTLER[i-1]
||DINERS(N=PHIL_NUMBER)
= forall [i:0..N-1]
( phil[i]:PHIL
|| {phil[i].left,phil[((i-1)+N)%N].right}::FORK
||DINERS_WITH_BUTLER
= (DINERS || {phil[i:0..PHIL_NUMBER-1]}::BUTLER).
We could have chosen to compose with BUTLER in the definition of DINERS, but it seems more attractive to keep definitions as simple as we can, and to build incrementally on what we had so far.
Note that BUTLER is an indexed process. So is there one butler or five? Technically we have defined five processes, BUTLER[0], BUTLER[1],. . . , BUTLER[4]. BUTLER[i] is the butler who steps in when i philosophers are sitting. Technically, BUTLER[3] is a process that may engage in, say, phil[1].arise, and then proceed to behave like (morph into) the process BUTLER[2]. A more natural way of thinking of this is that there is just one butler, who maintains a count (a local variable i) of how many philosophers are currently sitting.
7. The two processes are strongly equivalent, in spite of the LTSs that LTSA generates being different. Try to apply the Build ¡ú Minimise tool to both processes.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com