Department of Computing and Information Systems SWEN90004 Modelling Complex Software Systems Some Concurrency Workshop 6 solutions
The exercises
1. (a)
The following assertion says that processes a and b will both eventually acquire the resource:
assert EVENTUALLY_ACQUIRE
= (<>a.acquire && <>b.acquire)
To check this with LTSA, do Check ¡ú LTL Property ¡ú EVENTUALLY ACQUIRE, which will verify that the property holds.
2. (a)
fluent A_HOLDS
=
fluent B_HOLDS
=
assert HOLDS_UNTIL
= []((A_HOLDS U B_HOLDS) && (B_HOLDS U A_HOLDS))
This property does not hold because one process may acquire the resource, use it, release it, and then acquire it again.
The following assertion expresses that, for all of the red cars, it is always the case that each car will eventually enter the bridge:
assert STRONGRED
= forall[i:ID] []<>red[i].enter
This assertion holds for the model.
(b) The following assertion says that it will always be the case that a process which acquires the resource will eventually release it:
assert USE_BEFORE_RELEASE
= []((a.acquire -> <>a.release) && (b.acquire -> <>b.release))
(c) The following assertion says that whenever a process acquires the resource, it holds on to it until the other process acquires it:
(b) For all of the red cars, it is always the case that, if the car enters the bridge, it will eventually exit:
assert REDEXIT
= forall[i:ID] [](red[i].enter -> <>red[i].exit)
(c) There are several ways to specify that there are never both blue and red cars on the bridge at the same time. Below are two different solutions, one that uses fluents, and one that uses the ¡°until¡± operator.
First, using 2N fluents, we specify:
fluent RED[i:ID]
=
fluent BLUE[i:ID]
=
assert SAFE
= []!(exists[i:ID] RED[i] && exists[i:ID] BLUE[i])
This states that it will always be the case that the assertion ¡°there exists some red car and some blue car, both on the bridge¡± is false. In other words, it will never be the case that ¡°there exists a red and a blue car, both on the bridge¡± is true. The latter formulation, which some may find clearer, corresponds to pulling the negation out in front:
assert SAFE
= !<>(exists[i:ID] RED[i] && exists[i:ID] BLUE[i])
Second, using the ¡°until¡± operator:
assert ONEWAY_RED
= forall[i:ID]
[](red[i].enter -> (!blue[j:ID].enter U red[i].exit))
assert ONEWAY_BLUE
= forall[i:ID]
[](blue[i].enter -> (!red[j:ID].enter U blue[i].exit))
assert ALL_ONEWAY
= (ONEWAY_RED && ONEWAY_BLUE)
The first assertion states that, for each red car, once that car enters, no blue car enters, until the red car exits. The second assertion states the same for each blue car, and the third puts these together.
Both assertions (using fluents and using ¡°until¡±) hold on the model.
3. Here is one possible way:
TL
= ([1].red -> TL[0]),
TL[i:0..1]
= ([i].green -> [i].yellow -> [i].red -> TL[(i+1)%2]).
fluent CAN_GO[i:0..1]
= <{[i].green, [i].yellow}, [i].red>
assert SAFE
= []!(CAN_GO[0] && CAN_GO[1])