-- Fischer's mutual exclusion protocol

var	a,		-- max delay time to register intent
	b		-- min time to delay before rechecking
	: parameter;

--const a = 1;
--const b = 2;

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

automaton p1
var x: analog;

synclabs : leave_1, leave_2, claim_1, claim_2, attempt_1, enter_1, fail_1;

loc loc_1_k0: while True wait {x' >= 4/5 & x' <= 1}
    when True sync attempt_1 do {x' =0} goto loc_2_k0;
    when True sync leave_2 goto loc_1_k0;
    when True sync claim_2 goto loc_1_k2;

loc loc_1_k2: while True wait {x' >= 4/5 & x' <= 1}
    when True sync leave_2 goto loc_1_k0;
    when True sync claim_2 goto loc_1_k2;
	
loc loc_2_k0: while x<=a wait {x' >= 4/5 & x' <= 1}
    when True sync claim_1 do {x' = 0} goto loc_3_k1;
    when True sync claim_2 do {x' = x} goto loc_2_k2;
    when True sync leave_2 do {x' = x} goto loc_2_k0;

loc loc_2_k2: while x<=a wait {x' >= 4/5 & x' <= 1}
    when True sync claim_1 do {x' = 0} goto loc_3_k1;
    when True sync claim_2 do {x' = x} goto loc_2_k2;
    when True sync leave_2 do {x' = x} goto loc_2_k0;    

loc loc_3_k1: while True wait {x' >= 4/5 & x' <= 1}
    when x>=b sync enter_1 goto cs;
    when True sync claim_2 do {x' = x} goto loc_3_k2;
    when True sync leave_2 do {x' = x} goto loc_3_k0;

loc loc_3_k2: while True wait {x' >= 4/5 & x' <= 1}
    when x>=b sync fail_1 goto loc_1_k2;
    when True sync claim_2 do {x' = x} goto loc_3_k2;
    when True sync leave_2 do {x' = x} goto loc_3_k0;

loc loc_3_k0: while True wait {x' >= 4/5 & x' <= 1}
    when x>=b sync fail_1 goto loc_1_k0;
    when True sync claim_2 do {x' = x} goto loc_3_k2;
    when True sync leave_2 do {x' = x} goto loc_3_k0;

loc cs: while True wait {x' >= 4/5 & x' <= 1}
    when True sync leave_1 goto loc_1_k0;
    when True sync claim_2 goto cs;
    when True sync leave_2 goto cs;

end

--

automaton p2
var y: analog;

synclabs : leave_1, leave_2, claim_1, claim_2, attempt_2, enter_2, fail_2;

loc loc_1_k0: while True wait {y' >= 1 & y' <= 11/10}
    when True sync attempt_2 do {y' =0} goto loc_2_k0;
    when True sync leave_1 goto loc_1_k0;
    when True sync claim_1 goto loc_1_k1;

loc loc_1_k1: while True wait {y' >= 1 & y' <= 11/10}
    when True sync leave_1 goto loc_1_k0;
    when True sync claim_1 goto loc_1_k1;
	
loc loc_2_k0: while y<=a wait {y' >= 1 & y' <= 11/10}
    when True sync claim_2 do {y' = 0} goto loc_3_k2;
    when True sync claim_1 do {y' = y} goto loc_2_k1;
    when True sync leave_1 do {y' = y} goto loc_2_k0;

loc loc_2_k1: while y<=a wait {y' >= 1 & y' <= 11/10}
    when True sync claim_2 do {y' = 0} goto loc_3_k2;
    when True sync claim_1 do {y' = y} goto loc_2_k1;
    when True sync leave_1 do {y' = y} goto loc_2_k0;    

loc loc_3_k2: while True wait {y' >= 1 & y' <= 11/10}
    when y>=b sync enter_2 goto cs;
    when True sync claim_1 do {y' = y} goto loc_3_k1;
    when True sync leave_1 do {y' = y} goto loc_3_k0;

loc loc_3_k1: while True wait {y' >= 1 & y' <= 11/10}
    when y>=b sync fail_2 goto loc_1_k1;
    when True sync claim_1 do {y' = y} goto loc_3_k1;
    when True sync leave_1 do {y' = y} goto loc_3_k0;

loc loc_3_k0: while True wait {y' >= 1 & y' <= 11/10}
    when y>=b sync fail_2 goto loc_1_k0;
    when True sync claim_1 do {y' = y} goto loc_3_k1;
    when True sync leave_1 do {y' = y} goto loc_3_k0;

loc cs: while True wait {y' >= 1 & y' <= 11/10}
    when True sync leave_2 goto loc_1_k0;
    when True sync claim_1 goto cs;
    when True sync leave_1 goto cs;
end

var init: region;
init := loc[p1] = loc_1_k0 & loc[p2] = loc_1_k0 & x = 1 & y = 2;

--  constraint obtained by CEGAR
--   10 >= b
-- & 2*b > 1 + 2*a
-- & a >= 0
-- & 80*b > 25 + 110*a;

var bad: region;
bad := loc[p1] = cs & loc[p2] = cs;

-- predicates : ;
domain: x in [0,100] & y in [0,100] & a in [0, 10] & b in [0, 10];