(************************************************************
 *                      IMITATOR MODEL                      
 *
 * IEEE 1394 Root Contention Protocol
 *
 * Description     : Protocol described in "Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX" Collomb-Annichini, Sighireanu (RTTOOLS 2001)
 * Correctness     : see paper
 * Source          : "Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX"
 * Author          : Collomb-Annichini, Sighireanu
 * Modeling        : Collomb-Annichini, Sighireanu
 * Input by        : Étienne André
 *
 * Created         : 2015/07/31
 * Last modified   : 2020/08/18
 *
 * IMITATOR version: 3
 ************************************************************)


var 	x1, x2, x12, y12, x21, y21
		: clock;

(*	rc_fast_min, rc_fast_max,
	rc_slow_min, rc_slow_max,
	delay
			: parameter;*)

	rc_fast_min (*= 76*), rc_fast_max (*= 85*),
	rc_slow_min, rc_slow_max (*= 167*),
	delay
		: parameter;
	
	s1, s2,
	s12, sprime12,
	s21, sprime21,
		: discrete;

	ack  = 0,
	idle = 1,
	req  = 2,
		: constant;


(************************************************************)
  automaton node1
(************************************************************)
synclabs: snd_ack12, rcv_ack21, snd_idle12, rcv_idle21, snd_req12, rcv_req21, root1, child1;

urgent loc rcont1: invariant True
	when True sync snd_idle12 do {x1 := 0} goto fast1;
	when True sync snd_idle12 do {x1 := 0} goto slow1;
	(* Simulate message passing using three actions and global variables *)
	when True sync rcv_ack21 do {s1 := ack} goto rcont1;
	when True sync rcv_idle21 do {s1 := idle} goto rcont1;
	when True sync rcv_req21 do {s1 := req} goto rcont1;


loc fast1: invariant x1 <= rc_fast_max
	when x1 >= rc_fast_min goto sample1;
	(* Simulate message passing using three actions and global variables *)
	when True sync rcv_ack21 do {s1 := ack} goto fast1;
	when True sync rcv_idle21 do {s1 := idle} goto fast1;
	when True sync rcv_req21 do {s1 := req} goto fast1;
	

loc slow1: invariant x1 <= rc_slow_max
	when x1 >= rc_slow_min goto sample1;
	(* Simulate message passing using three actions and global variables *)
	when True sync rcv_ack21 do {s1 := ack} goto slow1;
	when True sync rcv_idle21 do {s1 := idle} goto slow1;
	when True sync rcv_req21 do {s1 := req} goto slow1;
	

urgent loc sample1: invariant True
	when s1 = idle sync snd_req12 goto snt_req1;
	when s1 = req sync snd_ack12 goto almost_root1;

loc snt_req1: invariant True
	when True sync rcv_req21 do {s1 := req} goto rcont1;
	when True sync rcv_ack21 do {s1 := ack} goto almost_child1;

urgent loc almost_child1: invariant True
	when True sync child1 goto child1;

loc child1: invariant True

urgent loc almost_root1: invariant True
	when True sync root1 goto root1;

loc root1: invariant True

end



(************************************************************)
  automaton node2
(************************************************************)
synclabs: snd_ack21, rcv_ack12, snd_idle21, rcv_idle12, snd_req21, rcv_req12, root2, child2;

urgent loc rcont2: invariant True
	when True sync snd_idle21 do {x2 := 0} goto fast2;
	when True sync snd_idle21 do {x2 := 0} goto slow2;
	(* Simulate message passing using three actions and global variables *)
	when True sync rcv_ack12 do {s2 := ack} goto rcont2;
	when True sync rcv_idle12 do {s2 := idle} goto rcont2;
	when True sync rcv_req12 do {s2 := req} goto rcont2;


loc fast2: invariant x2 <= rc_fast_max
	when x2 >= rc_fast_min goto sample2;
	(* Simulate message passing using three actions and global variables *)
	when True sync rcv_ack12 do {s2 := ack} goto fast2;
	when True sync rcv_idle12 do {s2 := idle} goto fast2;
	when True sync rcv_req12 do {s2 := req} goto fast2;
	

loc slow2: invariant x2 <= rc_slow_max
	when x2 >= rc_slow_min goto sample2;
	(* Simulate message passing using three actions and global variables *)
	when True sync rcv_ack12 do {s2 := ack} goto slow2;
	when True sync rcv_idle12 do {s2 := idle} goto slow2;
	when True sync rcv_req12 do {s2 := req} goto slow2;
	

urgent loc sample2: invariant True
	when s2 = idle sync snd_req21 goto snt_req2;
	when s2 = req sync snd_ack21 goto almost_root2;

loc snt_req2: invariant True
	when True sync rcv_req12 do {s2 := req} goto rcont2;
	when True sync rcv_ack12 do {s2 := ack} goto almost_child2;

urgent loc almost_child2: invariant True
	when True sync child2 goto child2;

loc child2: invariant True

urgent loc almost_root2: invariant True
	when True sync root2 goto root2;

loc root2: invariant True

end



(************************************************************)
  automaton wire12
(************************************************************)
synclabs: snd_ack12, rcv_ack12,
	snd_idle12, rcv_idle12,
	snd_req12, rcv_req12;

loc empty12: invariant True
	when True sync snd_ack12 do {x12 := 0, y12 := 0, s12 := ack} goto bufone12;
	when True sync snd_idle12 do {x12 := 0, y12 := 0, s12 := idle} goto bufone12;
	when True sync snd_req12 do {x12 := 0, y12 := 0, s12 := req} goto bufone12;


loc bufone12: invariant y12 <= delay
	when s12 = ack sync snd_ack12 goto bufone12;
	when s12 = idle sync snd_idle12 goto bufone12;
	when s12 = req sync snd_req12 goto bufone12;
	
	when True sync snd_ack12 do {y12 := 0, sprime12 := ack} goto buftwo12;
	when True sync snd_idle12 do {y12 := 0, sprime12 := idle} goto buftwo12;
	when True sync snd_req12 do {y12 := 0, sprime12 := req} goto buftwo12;

	when y12 > 0 & s12 = ack sync rcv_ack12 goto empty12;
	when y12 > 0 & s12 = idle sync rcv_idle12 goto empty12;
	when y12 > 0 & s12 = req sync rcv_req12 goto empty12;

	
loc buftwo12: invariant x12 <= delay
	when sprime12 = ack sync snd_ack12 goto buftwo12;
	when sprime12 = idle sync snd_idle12 goto buftwo12;
	when sprime12 = req sync snd_req12 goto buftwo12;

	when x12 > 0 sync rcv_ack12 do {sprime12 := s12} goto bufone12;
	when x12 > 0 sync rcv_idle12 do {sprime12 := s12} goto bufone12;
	when x12 > 0 sync rcv_req12 do {sprime12 := s12} goto bufone12;

end 



(************************************************************)
  automaton wire21
(************************************************************)
synclabs: snd_ack21, rcv_ack21,
	snd_idle21, rcv_idle21,
	snd_req21, rcv_req21;

loc empty21: invariant True
	when True sync snd_ack21 do {x21 := 0, y21 := 0, s21 := ack} goto bufone21;
	when True sync snd_idle21 do {x21 := 0, y21 := 0, s21 := idle} goto bufone21;
	when True sync snd_req21 do {x21 := 0, y21 := 0, s21 := req} goto bufone21;


loc bufone21: invariant y21 <= delay
	when s21 = ack sync snd_ack21 goto bufone21;
	when s21 = idle sync snd_idle21 goto bufone21;
	when s21 = req sync snd_req21 goto bufone21;
	
	when True sync snd_ack21 do {y21 := 0, sprime21 := ack} goto buftwo21;
	when True sync snd_idle21 do {y21 := 0, sprime21 := idle} goto buftwo21;
	when True sync snd_req21 do {y21 := 0, sprime21 := req} goto buftwo21;

	when y21 > 0 & s21 = ack sync rcv_ack21 goto empty21;
	when y21 > 0 & s21 = idle sync rcv_idle21 goto empty21;
	when y21 > 0 & s21 = req sync rcv_req21 goto empty21;

	
loc buftwo21: invariant x21 <= delay
	when sprime21 = ack sync snd_ack21 goto buftwo21;
	when sprime21 = idle sync snd_idle21 goto buftwo21;
	when sprime21 = req sync snd_req21 goto buftwo21;

	when x21 > 0 sync rcv_ack21 do {sprime21 := s21} goto bufone21;
	when x21 > 0 sync rcv_idle21 do {sprime21 := s21} goto bufone21;
	when x21 > 0 sync rcv_req21 do {sprime21 := s21} goto bufone21;

end 


(************************************************************)
  automaton s1o (*Safety 1 Observer*)
(************************************************************)
synclabs: child1, child2,
	root1, root2;

loc S1oStart: invariant True
	when True sync root1 do {} goto S1o1;
	when True sync child1 do {} goto S1o2;
	when True sync child2 do {} goto S1o3;
	when True sync root2 do {} goto S1o4;

loc S1o1: invariant True
	when True sync child2 do {} goto S1oEnd;

loc S1o2: invariant True
	when True sync root2 do {} goto S1oEnd;

loc S1o3: invariant True
	when True sync root1 do {} goto S1oEnd;

loc S1o4: invariant True
	when True sync child1 do {} goto S1oEnd;

loc S1oEnd: invariant True
end (*s1o*)



(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[node1]  = rcont1
	& loc[node2]  = rcont2
	& loc[wire12] = empty12
	& loc[wire21] = empty21
	& loc[s1o]    = S1oStart

	(*------------------------------------------------------------*)
	(* Initial discrete assignments *)
	(*------------------------------------------------------------*)
		(* It seems these values are not relevant in the beginning *)
	& s1 = 0
	
	& s2 = 0
	
	& s12 = 0
	& sprime12 = 0

	& s21 = 0
	& sprime21 = 0

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
	& x1 = 0
	
	& x2 = 0
	
	& x12 = 0
	& y12 = 0

	& x21 = 0
	& y21 = 0

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& delay >= 0 
	& rc_fast_min >= 0
	& rc_fast_max >= 0
	& rc_slow_max >= 0
	& rc_slow_min >= 0

	(* Constraint given in [CS01] *)
	& delay > 0
	& rc_fast_min <= rc_fast_max
	& rc_fast_max < rc_slow_min
	& rc_slow_min <= rc_slow_max

;


(************************************************************)
(* The end *)
(************************************************************)
end