-- TICKET protocol, 2 processes
-- MP 26/11/2007

-- Liveness for P1: (AG loc[p1] = s_wait -> (AF loc[p1] = s_use))


var 
	a,      	-- P1's counter
	b,     		-- P2's counter
	c,		-- ticket number
	d		-- served number
	: discrete; 

-- -------------------------------------------------------------- *)

automaton p1
synclabs : ;

initially s_think & True;

loc s_think:
	while a>=0 & b>=0 & c>=0 & d>=0 wait {}
	when True do {a' = c, c'=c+1} goto s_wait;
	
loc s_wait: while a>=0 & b>=0 & c>=0 & d>=0 wait {}
	when d>=a goto s_use;

loc s_use: while a>=0 & b>=0 & c>=0 & d>=0 wait {}
	when True do {d' =d+1} goto s_think;
end


automaton p2
synclabs : ;

initially s_think & True;

loc s_think: while a>=0 & b>=0 & c>=0 & d>=0 wait {}
	when True do {b' = c, c'=c+1} goto s_wait;
	
loc s_wait: while a>=0 & b>=0 & c>=0 & d>=0 wait {}
	when d>=b goto s_use;

loc s_use: while a>=0 & b>=0 & c>=0 & d>=0 wait {}
	when True do {d' =d+1} goto s_think;

end

--

var 
   init_reg, final_reg, reached : region;

init_reg:= loc[p1] = s_think & loc[p2] = s_think & a=0 & b=0 & c=d;

final_reg:= loc[p1] = s_use & loc[p2] = s_use;

reached:= reach backward from final_reg endreach;

if empty(reached & init_reg)
  then prints "mutual exclusion holds!";
       print reached;
  else prints "mutual exclusion does NOT hold!";

-- reached:= reach forward from init_reg endreach;
--
-- if empty(reached & final_reg)
--   then prints "mutual exclusion holds!";
--        print reached;
--  else prints "mutual exclusion does NOT hold!";

endif;