const CAPACITY : nat is 3 const COUNT : nat is 112 type frameid is union NIL | FRAME of nat | MAGIC1 | MAGIC2 | LAST end type mbuff is queue CAPACITY of frameid //---------------------------------------------------------------------- function insertbuff (q: mbuff, f: frameid) : mbuff is var tmp: mbuff := q begin if (full q) then return q end; while not (empty tmp) do if (f = first tmp) then return q end; tmp := dequeue tmp end; return enqueue(q, f) end function contains (q: mbuff, f: frameid) : bool is var tmp: mbuff := q begin while not (empty tmp) do if (f = first tmp) then return true end; tmp := dequeue tmp end; return false end function nextid (v1: frameid, v2: frameid, v3: frameid, reg: frameid, buf: mbuff): nat is var i : nat begin i := 0; while true do if ((contains(buf, FRAME(i))) or (v2 = FRAME(i)) or (v3 = FRAME(i)) or (reg = FRAME(i))) then i := i+1 else return i end end; return 0 // infinite loop not detected end //---------------------------------------------------------------------- process camera (&v1: frameid, &v2: frameid, &v3 : frameid, ®ister: frameid, &buffer: mbuff) is states start, send1, send2, stop var counter : nat := COUNT from start wait [0,0]; v1 := FRAME(0); to send1 from send1 wait [119,119]; select v1 := FRAME(nextid(v1, v2, v3, register, buffer)); to send1 [] v1 := MAGIC1; to send2 end from send2 wait [119,119]; if (counter > 0) then counter := counter - 1; v1 := FRAME(nextid(v1, v2, v3, register, buffer)); to send2 else v1 := MAGIC2; to stop end from stop wait [119,119]; v1 := LAST; to stop process T1 (&v1 : frameid, &v2 : frameid) is states get from get on (v1 <> NIL); wait [84,84]; v2 := v1; v1 := NIL; to get process T2 (&v2 : frameid, ®ister : frameid) is states get from get on (v2 <> NIL); wait [51,57]; register := v2; v2 := NIL; to get process T3 (®ister: frameid, &v3 : frameid, &buffer : mbuff) is states get0, set, get from get0 wait [0,0]; v3 := register; to set from set wait [24,24]; if (v3 <> NIL) then buffer := insertbuff (buffer, v3) end; to get from get wait [16,16]; v3 := register; to set // T4 and display process T4 (&buffer : mbuff) is states get, display, stop init to display from get wait [120,120]; to display from display wait [0, 0]; if (empty buffer) then to get else case first(buffer) of MAGIC1 -> to stop | MAGIC2 -> to stop | LAST -> #twolosses; to stop | any -> buffer := dequeue buffer; to get end end from stop // BLOCK THE WORLD wait [0,0]; to stop //---------------------------------------------------------------------- component C is var v1 : frameid := NIL, v2 : frameid := NIL, v3 : frameid := NIL, register : frameid := NIL, buffer : mbuff := {||} par camera (&v1, &v2, &v3, ®ister, &buffer) || T1 (&v1, &v2) || T2 (&v2, ®ister) || T3 (®ister, &v3, &buffer) || T4 (&buffer) end C //---------------------------------------------------------------------- property looseframe is ltl [] not (C/5/tag twolosses)