discrete;
-- Fishers's mutual exclusion algorithm
-- The algorithm works under some timing constraints
 
var atl1p1, atl2p1, atl3p1, atl4p1, atl5p1,
    t1p1, t2p1, t3p1, t4p1, t5p1, t6p1,
    atl1p2, atl2p2, atl3p2, atl4p2, atl5p2,
    t1p2, t2p2, t3p2, t4p2, t5p2, t6p2,
    xeq0, xeq1, xeq2 ;
    
const bigdel = 8, smalldel = 7 ;
	-- these are timing constants. The algorithm achieves
	-- mutual exclusion iff bigdel < smalldel.


-- variable x can have exactly one value at a time. 
define prop1 as
[[	!(xeq0&&xeq1 || xeq0&&xeq2 || xeq1&&xeq2) && (xeq0 || xeq1 || xeq2)	
]]
;

-- Description of PROCESS P1

-- process p1 can be at exactly one location at a time. 
define prop2 as
[[ 
	!(atl1p1&&atl2p1 || atl1p1&&atl3p1 || atl1p1&&atl4p1 || atl1p1&&atl5p1 
	 || atl2p1&&atl3p1 || atl2p1&&atl4p1 || atl2p1&&atl5p1 
	 || atl3p1&&atl4p1 || atl3p1&&atl5p1 || atl4p1&&atl5p1 ) 
	&&	
	(atl1p1 || atl2p1 || atl3p1 || atl4p1 || atl5p1)
]]
;

-- in p1 atmost one transition can occur at a time.
-- if there are no transitions,  the process idles.
define prop3 as
[[
	!(t1p1&&t2p1 || t1p1&&t3p1 || t1p1&&t4p1 || t1p1&&t5p1 || t1p1&&t6p1 
	 || t2p1&&t3p1 || t2p1&&t4p1 || t2p1&&t5p1 || t2p1&&t6p1
	 || t3p1&&t4p1 || t3p1&&t5p1 || t3p1&&t6p1 
	 || t4p1&&t5p1 || t4p1&&t6p1 || t5p1&&t6p1 
         ) 
]]
;

--  initial conditions
define prop4 as
          ( <atl1p1 && xeq0> ^ true)
;

define prop5 as
 	[] (< t1p1> => <atl1p1 && xeq0 >)
 	&&
 	[] (< t1p1 > ^ slen=1 => slen=1^<atl2p1> )
;
 
define prop6 as
 	[] ( <t2p1> => <atl2p1> )
 	&&
 	[] ( <t2p1>^slen=1 => slen=1^<atl3p1 && xeq1> )
 	&&
-- the next formula asserts an upper time bound of bigdel on t2p1 
	[] ( [[atl2p1 && !(t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1) ]] 
	      =>  slen < bigdel || slen = bigdel )
;

define prop7 as
	[] ( <t3p1> => <atl3p1> )
	&&
	[] ( <t3p1>^slen=1 => slen=1^<atl4p1>)
	&&
-- the next two formulae assert a lower bound of smalldel on t3p1
 	(slen < smalldel => [[ !t3p1 ]])
 	&&
	[]( <t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1>^slen=1^
               (slen< smalldel)
		 => slen=1^[[!t3p1 ]] )
;

define prop8 as
	[] ( <t4p1> => <atl4p1 && xeq1 > )
	&&
	[] ( <t4p1>^slen=1 => slen=1^<atl5p1> ) 	 
;

define prop9 as
	[] ( <t5p1> => <atl4p1 && !xeq1 > )
	&&
	[] ( <t5p1>^slen=1 => slen=1^<atl1p1 > ) 	 
;

define prop10 as
 	[] ( <t6p1> => <atl5p1> )
 	&&
 	[] ( <t6p1>^ slen=1 => slen=1^<atl1p1 && xeq0> )
;
 	
-- The following formuale assert that state does not change during idling. 

define prop11 as
	[] ( <atl1p1>^[!(t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1) ]
		=> [[ atl1p1 ]] )
	&&
 	[] ( <atl2p1>^[!(t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1) ]
		=> [[ atl2p1 ]] )
	&&
 	[] ( <atl3p1>^[!(t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1) ]
		=> [[ atl3p1 ]] )
	&&
 	[] ( <atl4p1>^[!(t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1) ]
		=> [[ atl4p1 ]] )
	&&
 	[] ( <atl5p1>^[!(t1p1 || t2p1 || t3p1 || t4p1 || t5p1 || t6p1) ]
		=> [[ atl5p1 ]] )
;

-- description of PROCESS P2

define prop12 as
[[ 
	!(atl1p2&&atl2p2 || atl1p2&&atl3p2 || atl1p2&&atl4p2 || atl1p2&&atl5p2 
	 || atl2p2&&atl3p2 || atl2p2&&atl4p2 || atl2p2&&atl5p2 
	 || atl3p2&&atl4p2 || atl3p2&&atl5p2 || atl4p2&&atl5p2 ) 
	&&	
	(atl1p2 || atl2p2 || atl3p2 || atl4p2 || atl5p2)
]]
;

define prop13 as
[[
	!(t1p2&&t2p2 || t1p2&&t3p2 || t1p2&&t4p2 || t1p2&&t5p2 || t1p2&&t6p2 
	 || t2p2&&t3p2 || t2p2&&t4p2 || t2p2&&t5p2 || t2p2&&t6p2
	 || t3p2&&t4p2 || t3p2&&t5p2 || t3p2&&t6p2 
	 || t4p2&&t5p2 || t4p2&&t6p2 || t5p2&&t6p2 ) 
]]
;

define prop14 as
          ( <atl1p2 && xeq0> ^true)
;

define prop15 as
 	[] (< t1p2> => <atl1p2 && xeq0 >)
 	&&
 	[] (< t1p2 > ^ slen=1 => slen=1^<atl2p2> )
 ;

define prop16 as 
 	[] ( <t2p2> => <atl2p2> )
 	&&
 	[] ( <t2p2>^slen=1 => slen=1^<atl3p2 && xeq2> )
 	&&
	[] ( [[atl2p2 && !(t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2) ]] => 
	slen < bigdel || slen = bigdel )
;

define prop17 as
	[] ( <t3p2> => <atl3p2> )
	&&
	[] ( <t3p2>^slen=1 => slen=1^<atl4p2>)
	&&
 	(slen < smalldel => [[ !t3p2 ]])
 	&&
	[]( <t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2>^slen=1^
               (slen< smalldel )
		 => slen=1^[[!t3p2 ]] )
;

define prop18 as
	[] ( <t4p2> => <atl4p2 && xeq2 > )
	&&
	[] ( <t4p2>^slen=1 => slen=1^<atl5p2> ) 	 
;

define prop19 as
	[] ( <t5p2> => <atl4p2 && !xeq2 > )
	&&
	[] ( <t5p2>^slen=1 => slen=1^<atl1p2 > ) 	 
;

define prop20 as
 	[] ( <t6p2> => <atl5p2> )
 	&&
 	[] ( <t6p2>^ slen=1 => slen=1^<atl1p2 && xeq0> )
;
 	

define prop21 as
	[] ( <atl1p2>^[!(t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2) ]
		=> [[ atl1p2 ]] )
	&&
 	[] ( <atl2p2>^[!(t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2) ]
		=> [[ atl2p2 ]] )
	&&
 	[] ( <atl3p2>^[!(t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2) ]
		=> [[ atl3p2 ]] )
	&&
 	[] ( <atl4p2>^[!(t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2) ]
		=> [[ atl4p2 ]] )
	&&
 	[] ( <atl5p2>^[!(t1p2 || t2p2 || t3p2 || t4p2 || t5p2 || t6p2) ]
		=> [[ atl5p2 ]] )
;



-- The following formulae assert that value of x can change only
-- if transitions t2p1, t6p1, t2p2 and t6p2 take place. 
		
define prop22 as 
 	[] ( <xeq0>^[!(t2p1 || t6p1 || t2p2 || t6p2 )] => [[ xeq0 ]] )
	&& 	
	[] ( <xeq1>^[!(t2p1 || t6p1 || t2p2 || t6p2 )] => [[ xeq1 ]] )
	&& 	
	[] ( <xeq2>^[!(t2p1 || t6p1  || t2p2 || t6p2)] => [[ xeq2 ]] ) 
;


infer

-- process is in critical region at location l5
-- both p1 and p2 cannot be in critical region at same time.
(
prop1 && prop2 && prop3 && prop4 && prop5 && prop6 && prop7 &&
prop8 && prop9 && prop10 && prop11 && prop12 && prop13 && prop14 &&
prop15 && prop16 && prop17 && prop18 && prop19 && prop20 && prop21 &&
prop22
)     
    =>    ! <> (<atl5p1 && atl5p2>)  
.