Department of Computing and Information Systems SWEN90004 Modelling Complex Software Systems Some Concurrency Workshop 4 solutions
The exercises
1. The two LTS models are shown below:
Different sequence
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 -> …
b release
a acquire
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, Acquire resources respectively
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).
ERROR
STOP
I Error State
END E
Number
Deadlock State Successful Termination
5. If we run the three models through the LTS safety check, we get the following output:
STOP:
ERROR:
Trace to DEADLOCK:
once
Trace to property violation in ONESHOT:
once
END:
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 di↵erent. Try to apply the Build ! Minimise tool to both processes.
4
1
I
n
ONE THREE Oneresource
Ea Justprefix X
I shared
Two resources with prefixes Hynthesame
4132
A B must allfinish a3 bz to enable start
ABI
AB3
14133