heptagon/test/good/alloc.ept
2010-06-21 12:11:06 +02:00

33 lines
No EOL
765 B
Text

(* Ressource allocator for two clients, 0 and 1 *)
(* ri means that client i asks for the resource. *)
(* gi means that client i was granted the resource. *)
(* Security property: not (r0 & r1) *)
(* Liveness property (expressed in LTL): G (ri => F gi) *)
node alloc(r0 : bool; r1 : bool) returns (g0 : bool; g1 : bool)
let
automaton
state IDLE0
do g0 = false;
g1 = false;
unless r0 then ALLOC0 | (r1 & not r0) then ALLOC1
state IDLE1
do g0 = false;
g1 = false;
unless r1 then ALLOC1 | (r0 & not r1) then ALLOC0
state ALLOC0
do g0 = true;
g1 = false;
unless (not r0) then IDLE1
state ALLOC1
do g0 = false;
g1 = true;
unless (not r1) then IDLE0
end;
tel