values
psize = 5
PIDset = {1,...,psize}
types
PID = nat
inv p == p in set PIDset
channels
create, delete, ready, enter, leave : PID
process Proc = p: PID @
begin
actions
NewProc = create.p -> RunProc
RunProc =
ready.p -> enter.p -> leave.p -> RunProc
[]
delete.p -> NewProc
@
NewProc;
RunProc
end
process Mutex =
begin
@
mu X @ (enter?p -> leave!p -> X)
end
process Scheduler =
( ||| p in set PIDset @ Proc(p) ) [|{|enter,leave|}|] Mutex
process Queue =
begin
state
q: seq of PID := []
inv len(q) <= psize
actions
Q =
[len(q) < psize] & ready?p -> q := q^[p]; Q
[]
[not (q = [])] & enter!(hd(q)) -> q := tl(q); Q
@
Q
end
process Scheduler1 =
Scheduler [|{|ready,enter|}|] Queue
when one has selecetd the events: [create.1, create.2, ready.1, ready.2] one should have both enter.1 and enter.2 as possible choices. Right now it only selects the first one.
Not offering enter.2 is expected on that trace (Queue prevents this), however, related bug with not offering ready.2 after first two events fixed with #242.
With a model such as:
when one has selecetd the events: [create.1, create.2, ready.1, ready.2] one should have both enter.1 and enter.2 as possible choices. Right now it only selects the first one.