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

set always memo on

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) .

close