(************************************************************
 *                      IMITATOR MODEL                      
 *
 * CSMA/CD Protocol
 *
 * Description     : Non-probabilistic model deduced from the probabilistic model in "Symbolic Model Checking for Probabilistic Timed Automata" (M. Kwiatkowska, G. Norman, J. Sproston and F. Wang., FORMATS/FTRTFT'2004). See figures on http://www.prismmodelchecker.org/casestudies/csma.php.
	Input by Laurent Fribourg and Étienne André (LSV)
	Renamed actions (May 2012) for taking probabilities into account
	Version with BC=1, i.e., up to waiting time of 3*timeslot
 * Correctness     : Transmission completed
 * Source          : http://www.prismmodelchecker.org/casestudies/csma.php
 * Author          : M. Kwiatkowska, G. Norman, J. Sproston and F. Wang
 * Modeling        : M. Kwiatkowska, G. Norman, J. Sproston and F. Wang
 * Input by        : Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : 2007
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)

var

(* Clocks *)
	x1,
	x2,
	y,
		: clock;

(* Parameters *)
	lambda,    (* length of a message *)
	sigma,     (* propagation time of a message *)
	timeslot,
		: parameter;



(************************************************************)
  automaton medium
(************************************************************)
synclabs: send1, send2, end1, end2, busy1, busy2, cd;

loc Init: invariant True
		when True sync send1 do {y := 0} goto Transmit;
		when True sync send2 do {y := 0} goto Transmit;

loc Transmit: invariant True
		when y <= sigma sync send1 do {y := 0} goto Collide;
		when y <= sigma sync send2 do {y := 0} goto Collide;

		when y >= sigma sync busy1 do {} goto Transmit;
		when y >= sigma sync busy2 do {} goto Transmit;

		when True sync end1 do {y := 0} goto Init;
		when True sync end2 do {y := 0} goto Init;

loc Collide: invariant y <= sigma
		when y <= sigma sync cd do {y := 0} goto Init;

end (* medium *)



(************************************************************)
  automaton sender1
(************************************************************)
synclabs: send1, end1, busy1, cd, prob1;

loc Init1: invariant True
	when True sync send1 do {} goto Transmit1;

loc Transmit1: invariant x1 <= lambda
	when x1 = lambda sync end1 do {x1 := 0} goto Done1;
	when True sync cd do {x1 := 0} goto Collide1;

loc Collide1: invariant x1 <= 0
	when True sync prob1 goto Wait1_0;
	when True sync prob1 goto Wait1_1;
	when True sync prob1 goto Wait1_2;
	when True sync prob1 goto Wait1_3;

loc Wait1_0: invariant x1 <= 0
	when x1 = 0 sync busy1 do {x1 := 0} goto Collide1;
	when x1 = 0 sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_1: invariant x1 <= timeslot
	when x1 = timeslot sync busy1 do {x1 := 0} goto Collide1;
	when x1 = timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_2: invariant x1 <= 2 timeslot
	when x1 = 2 timeslot sync busy1 do {x1 := 0} goto Collide1;
	when x1 = 2 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3: invariant x1 <= 3 timeslot
	when x1 = 3 timeslot sync busy1 do {x1 := 0} goto Collide1;
	when x1 = 3 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Done1: invariant x1 <= 0
 (* when True goto Done1; *)

end (* sender1 *)




(************************************************************)
  automaton sender2
(************************************************************)
synclabs: send2, end2, busy2, cd, prob2;

loc Init2: invariant x2 = 0
	when x2 = 0 sync send2 do {} goto Transmit2;

loc Transmit2: invariant x2 <= lambda
	when x2 = lambda sync end2 do {x2 := 0} goto Done2;
	when True sync cd do {x2 := 0} goto Collide2;

loc Collide2: invariant x2 <= 0
	when True sync prob2 goto Wait2_0;
	when True sync prob2 goto Wait2_1;
	when True sync prob2 goto Wait2_2;
	when True sync prob2 goto Wait2_3;

loc Wait2_0: invariant x2 <= 0
	when x2 = 0 sync busy2 do {x2 := 0} goto Collide2;
	when x2 = 0 sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_1: invariant x2 <= timeslot
	when x2 = timeslot sync busy2 do {x2 := 0} goto Collide2;
	when x2 = timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_2: invariant x2 <= 2 timeslot
	when x2 = 2 timeslot sync busy2 do {x2 := 0} goto Collide2;
	when x2 = 2 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3: invariant x2 <= 3 timeslot
	when x2 = 3 timeslot sync busy2 do {x2 := 0} goto Collide2;
	when x2 = 3 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Done2: invariant x2 <= 0
	(* when True goto Done2; *)

end (* sender2 *)




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

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[medium]  = Init
	& loc[sender1] = Init1
	& loc[sender2] = Init2

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

	(*------------------------------------------------------------*)
	(* Parameter constraints *)
	(*------------------------------------------------------------*)
	& lambda >=0
	& sigma >= 0
	& timeslot >= 0
;


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