School of Computing and Information Systems The University of Melbourne
SWEN90004 Modelling Complex Software Systems
Some Concurrency Workshop 5 solutions
The exercises
Copyright By PowCoder代写 加微信 powcoder
1. The action trace bb violates the safety property PS. 2. const N = 10
range T = 0..N
// The safety property that ensures the number of
// passengers in the lift never exceeds 10
// (or, incidentally, falls below 0!)
property FULL = FULL[0],
FULL[i:T] = (when (i
|when (i>0) exit -> FULL[i-1]
// The following implementation of a lift (v1) will cause a property
// violation when composed with the safety property.
LIFTv1 = LIFTv1[0],
LIFTv1[i:T] =
( enter -> LIFTv1[i+1]
| exit -> LIFTv1[i-1]
// The following implementation of a lift (v2) uses guards to prevent
// the safety property being violated, and hence will not cause a
// property violation when composed with the safety property.
LIFTv2 = LIFTv1[0],
LIFTv1[i:T] =
( when (i
| when (i>0) exit -> LIFTv1[i-1]
||SAFE_LIFTv1 = (LIFTv1 || FULL).
||SAFE_LIFTv2 = (LIFTv2 || FULL).
3. const False = 0 const True = 1
range Bool = False..True
const Nuser = 2
const Nsystem = 2
// As with the reader-writer model, we need to add the full set
// of acquire/release actions to the alphabets of both user and
// system processes
set Actions = {systemAcquire, systemRelease,
userAcquire, userRelease}
// The console acts as a binary semaphore that only allows one
// process access at a time
CONSOLE(N=1) = CONSOLE[0],
CONSOLE[v:0..N] =
( when (v<1) systemAcquire -> CONSOLE[v+1]
| when (v>0) systemRelease -> CONSOLE[v-1]
| when (v<1) userAcquire -> CONSOLE[v+1]
| when (v>0) userRelease -> CONSOLE[v-1]
USER = (userAcquire -> userConsole -> userRelease -> USER)
+ Actions.
SYSTEM = (systemAcquire -> systemConsole -> systemRelease -> SYSTEM)
+ Actions.
||OS = (user[1..Nuser]:USER
||system[1..Nsystem]:SYSTEM
||{user[1..Nuser],
system[1..Nsystem]}::CONSOLE(1)).
// Under fair scheduling assumptions the OS process will provide
// equal access to both user and system processes. However, user
// processes may be denied access to the console if system processes
// have a higher priority when attempting to acquire access,
// as denoted by the action priority operator below.
||OS_PROGRESS = OS <<{system[1..Nsystem].systemAcquire}.
progress USER_PROG = {user[1..Nuser].userAcquire}
progress SYS_PROG = {system[1..Nsystem].systemAcquire}
4. One possible solution:
const True = 1
const False = 0
range Bool = False..True
set BoolActions = {setTrue, setFalse, check[False], check[True]}
BOOLVAR = VAL[False],
VAL[v:Bool] = ( setTrue -> VAL[True]
| setFalse -> VAL[False]
| check[v] -> VAL[v]
||FLAGS = (flag1:BOOLVAR || flag2:BOOLVAR).
FIELD = (enter -> exit -> FIELD).
N1 = (flag1.setTrue -> flag2.check[t:Bool] ->
(when (t == True) flag1.setFalse -> N1
|when (t == False) n1.enter -> n1.pickBerries -> n1.exit ->
flag1.setFalse -> N1)
N2 = (flag2.setTrue -> flag1.check[t:Bool] ->
(when (t == True) flag2.setFalse -> N2
|when (t == False) n2.enter -> n2.pickBerries -> n2.exit ->
flag2.setFalse -> N2)
||WAR = (FLAGS || N1 || N2 || {n1,n2}::FIELD).
// Safety property to ensure mutual exclusion (one neighbour leaves the
// field before the other enters).
property MUTEX = ( n1.enter -> n1.exit -> MUTEX
| n2.enter -> n2.exit -> MUTEX).
||CHECK = (WAR || MUTEX).
// Progress property to ensure that both neighbours are able to pick berries
progress PICK = {{n1,n2}.pickBerries}
// A version of the warring neighbours model with greedy neighbours who refuse
// to lower their flags when trying to access the field.
||WAR_PROGRESS = WAR >>{{flag1,flag2}.setFalse}.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com