-- ==========================================================
--> verificationBySearchWithObEq.cafe
-- ==========================================================

in qlockTrans
in qlockObEq
in mex

-- %%%%%%%%%%%%%
-- 2 agents case
-- %%%%%%%%%%%%%

-- verification of non existence of counter examples
-- for 2 agents case
open (QLOCKijTrans + QLOCKobEq + MEX)

-- defining observational/behavioral equivalence
pred _=ob=_ : Config Config {memo} .
vars S1 S2 : Sys .
eq (< S1 > =ob= < S2 >) = (S1 =ob= S2 with (i j)) .

-- check that the number of 
-- the classes of observational equivlant states is finite 
red < init > =(*,*)=>* < S:Sys > 
       withStateEq (C1:Config =ob= C2:Config) .

-- proof of non-existence of counter examples
-- for 2 agents/processes case
red < init > =(*,*)=>* < S:Sys > 
       suchThat (not mutualEx(S,i,j))
       withStateEq (C1:Config =ob= C2:Config) .

-- proof of other properties
-- for 2 agents/processes case
red < init > =(*,*)=>* < S:Sys > 
       suchThat 
         (not (((pc(S,i) = wt) implies (i in queue(S))) and
               ((pc(S,j) = wt) implies (j in queue(S)))))
       withStateEq (C1:Config =ob= C2:Config) .
red < init > =(*,*)=>* < S:Sys > 
       suchThat 
         (not (((top(queue(S)) = i) implies 
                    ((pc(S,i) = wt) or (pc(S,i) = cs))) and
               ((top(queue(S)) = j) implies 
                    ((pc(S,j) = wt) or (pc(S,j) = cs))))) 
       withStateEq (C1:Config =ob= C2:Config) .
red < init > =(*,*)=>* < S:Sys > 
       suchThat 
         (not (((pc(S,i) = cs) implies (top(queue(S)) = i)) and
               ((pc(S,j) = cs) implies (top(queue(S)) = j))))
       withStateEq (C1:Config =ob= C2:Config) .

close