(*******************************************************************************
 *                                IMITATOR MODEL                               
 * 
 * Title            : CSMACD-bc5
 * 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.
 * Correctness      : Transmission completed
 * Scalable         : yes
 * Generated        : yes
 * Categories       : Academic ; Industrial ; Protocol ; RTS
 * Source           : http://www.prismmodelchecker.org/casestudies/csma.php
 * bibkey           : KNSW07
 * 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
 * Model version    : 
 * 
 * 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_1;

(* STARTING AUTOMATED PROGRAM FOR CSMA/CD FOR STATION 1 WITH BCMAX = 5 *)

(* Considering case with bc = 1, hence from 0 to 3 (i.e., 2^(bc+1) - 1) *)
loc Collide1_1: invariant x1 <= 0
	when True sync prob1 goto Wait1_1_0;
	when True sync prob1 goto Wait1_1_1;
	when True sync prob1 goto Wait1_1_2;
	when True sync prob1 goto Wait1_1_3;

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

loc Wait1_1_1: invariant x1 <= 1 timeslot
	when x1 = 1 timeslot sync busy1 do {x1 := 0} goto Collide1_2;
	when x1 = 1 timeslot sync send1 do {x1 := 0} goto Transmit1;

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

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

(* Considering case with bc = 2, hence from 0 to 7 (i.e., 2^(bc+1) - 1) *)
loc Collide1_2: invariant x1 <= 0
	when True sync prob1 goto Wait1_2_0;
	when True sync prob1 goto Wait1_2_1;
	when True sync prob1 goto Wait1_2_2;
	when True sync prob1 goto Wait1_2_3;
	when True sync prob1 goto Wait1_2_4;
	when True sync prob1 goto Wait1_2_5;
	when True sync prob1 goto Wait1_2_6;
	when True sync prob1 goto Wait1_2_7;

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

loc Wait1_2_1: invariant x1 <= 1 timeslot
	when x1 = 1 timeslot sync busy1 do {x1 := 0} goto Collide1_3;
	when x1 = 1 timeslot sync send1 do {x1 := 0} goto Transmit1;

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

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

loc Wait1_2_4: invariant x1 <= 4 timeslot
	when x1 = 4 timeslot sync busy1 do {x1 := 0} goto Collide1_3;
	when x1 = 4 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_2_5: invariant x1 <= 5 timeslot
	when x1 = 5 timeslot sync busy1 do {x1 := 0} goto Collide1_3;
	when x1 = 5 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_2_6: invariant x1 <= 6 timeslot
	when x1 = 6 timeslot sync busy1 do {x1 := 0} goto Collide1_3;
	when x1 = 6 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_2_7: invariant x1 <= 7 timeslot
	when x1 = 7 timeslot sync busy1 do {x1 := 0} goto Collide1_3;
	when x1 = 7 timeslot sync send1 do {x1 := 0} goto Transmit1;

(* Considering case with bc = 3, hence from 0 to 15 (i.e., 2^(bc+1) - 1) *)
loc Collide1_3: invariant x1 <= 0
	when True sync prob1 goto Wait1_3_0;
	when True sync prob1 goto Wait1_3_1;
	when True sync prob1 goto Wait1_3_2;
	when True sync prob1 goto Wait1_3_3;
	when True sync prob1 goto Wait1_3_4;
	when True sync prob1 goto Wait1_3_5;
	when True sync prob1 goto Wait1_3_6;
	when True sync prob1 goto Wait1_3_7;
	when True sync prob1 goto Wait1_3_8;
	when True sync prob1 goto Wait1_3_9;
	when True sync prob1 goto Wait1_3_10;
	when True sync prob1 goto Wait1_3_11;
	when True sync prob1 goto Wait1_3_12;
	when True sync prob1 goto Wait1_3_13;
	when True sync prob1 goto Wait1_3_14;
	when True sync prob1 goto Wait1_3_15;

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

loc Wait1_3_1: invariant x1 <= 1 timeslot
	when x1 = 1 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 1 timeslot sync send1 do {x1 := 0} goto Transmit1;

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

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

loc Wait1_3_4: invariant x1 <= 4 timeslot
	when x1 = 4 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 4 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_5: invariant x1 <= 5 timeslot
	when x1 = 5 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 5 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_6: invariant x1 <= 6 timeslot
	when x1 = 6 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 6 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_7: invariant x1 <= 7 timeslot
	when x1 = 7 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 7 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_8: invariant x1 <= 8 timeslot
	when x1 = 8 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 8 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_9: invariant x1 <= 9 timeslot
	when x1 = 9 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 9 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_10: invariant x1 <= 10 timeslot
	when x1 = 10 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 10 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_11: invariant x1 <= 11 timeslot
	when x1 = 11 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 11 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_12: invariant x1 <= 12 timeslot
	when x1 = 12 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 12 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_13: invariant x1 <= 13 timeslot
	when x1 = 13 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 13 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_14: invariant x1 <= 14 timeslot
	when x1 = 14 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 14 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_3_15: invariant x1 <= 15 timeslot
	when x1 = 15 timeslot sync busy1 do {x1 := 0} goto Collide1_4;
	when x1 = 15 timeslot sync send1 do {x1 := 0} goto Transmit1;

(* Considering case with bc = 4, hence from 0 to 31 (i.e., 2^(bc+1) - 1) *)
loc Collide1_4: invariant x1 <= 0
	when True sync prob1 goto Wait1_4_0;
	when True sync prob1 goto Wait1_4_1;
	when True sync prob1 goto Wait1_4_2;
	when True sync prob1 goto Wait1_4_3;
	when True sync prob1 goto Wait1_4_4;
	when True sync prob1 goto Wait1_4_5;
	when True sync prob1 goto Wait1_4_6;
	when True sync prob1 goto Wait1_4_7;
	when True sync prob1 goto Wait1_4_8;
	when True sync prob1 goto Wait1_4_9;
	when True sync prob1 goto Wait1_4_10;
	when True sync prob1 goto Wait1_4_11;
	when True sync prob1 goto Wait1_4_12;
	when True sync prob1 goto Wait1_4_13;
	when True sync prob1 goto Wait1_4_14;
	when True sync prob1 goto Wait1_4_15;
	when True sync prob1 goto Wait1_4_16;
	when True sync prob1 goto Wait1_4_17;
	when True sync prob1 goto Wait1_4_18;
	when True sync prob1 goto Wait1_4_19;
	when True sync prob1 goto Wait1_4_20;
	when True sync prob1 goto Wait1_4_21;
	when True sync prob1 goto Wait1_4_22;
	when True sync prob1 goto Wait1_4_23;
	when True sync prob1 goto Wait1_4_24;
	when True sync prob1 goto Wait1_4_25;
	when True sync prob1 goto Wait1_4_26;
	when True sync prob1 goto Wait1_4_27;
	when True sync prob1 goto Wait1_4_28;
	when True sync prob1 goto Wait1_4_29;
	when True sync prob1 goto Wait1_4_30;
	when True sync prob1 goto Wait1_4_31;

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

loc Wait1_4_1: invariant x1 <= 1 timeslot
	when x1 = 1 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 1 timeslot sync send1 do {x1 := 0} goto Transmit1;

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

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

loc Wait1_4_4: invariant x1 <= 4 timeslot
	when x1 = 4 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 4 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_5: invariant x1 <= 5 timeslot
	when x1 = 5 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 5 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_6: invariant x1 <= 6 timeslot
	when x1 = 6 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 6 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_7: invariant x1 <= 7 timeslot
	when x1 = 7 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 7 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_8: invariant x1 <= 8 timeslot
	when x1 = 8 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 8 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_9: invariant x1 <= 9 timeslot
	when x1 = 9 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 9 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_10: invariant x1 <= 10 timeslot
	when x1 = 10 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 10 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_11: invariant x1 <= 11 timeslot
	when x1 = 11 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 11 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_12: invariant x1 <= 12 timeslot
	when x1 = 12 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 12 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_13: invariant x1 <= 13 timeslot
	when x1 = 13 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 13 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_14: invariant x1 <= 14 timeslot
	when x1 = 14 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 14 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_15: invariant x1 <= 15 timeslot
	when x1 = 15 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 15 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_16: invariant x1 <= 16 timeslot
	when x1 = 16 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 16 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_17: invariant x1 <= 17 timeslot
	when x1 = 17 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 17 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_18: invariant x1 <= 18 timeslot
	when x1 = 18 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 18 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_19: invariant x1 <= 19 timeslot
	when x1 = 19 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 19 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_20: invariant x1 <= 20 timeslot
	when x1 = 20 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 20 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_21: invariant x1 <= 21 timeslot
	when x1 = 21 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 21 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_22: invariant x1 <= 22 timeslot
	when x1 = 22 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 22 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_23: invariant x1 <= 23 timeslot
	when x1 = 23 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 23 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_24: invariant x1 <= 24 timeslot
	when x1 = 24 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 24 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_25: invariant x1 <= 25 timeslot
	when x1 = 25 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 25 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_26: invariant x1 <= 26 timeslot
	when x1 = 26 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 26 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_27: invariant x1 <= 27 timeslot
	when x1 = 27 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 27 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_28: invariant x1 <= 28 timeslot
	when x1 = 28 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 28 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_29: invariant x1 <= 29 timeslot
	when x1 = 29 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 29 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_30: invariant x1 <= 30 timeslot
	when x1 = 30 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 30 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_4_31: invariant x1 <= 31 timeslot
	when x1 = 31 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 31 timeslot sync send1 do {x1 := 0} goto Transmit1;

(* Considering case with bc = 5, hence from 0 to 63 (i.e., 2^(bc+1) - 1) *)
loc Collide1_5: invariant x1 <= 0
	when True sync prob1 goto Wait1_5_0;
	when True sync prob1 goto Wait1_5_1;
	when True sync prob1 goto Wait1_5_2;
	when True sync prob1 goto Wait1_5_3;
	when True sync prob1 goto Wait1_5_4;
	when True sync prob1 goto Wait1_5_5;
	when True sync prob1 goto Wait1_5_6;
	when True sync prob1 goto Wait1_5_7;
	when True sync prob1 goto Wait1_5_8;
	when True sync prob1 goto Wait1_5_9;
	when True sync prob1 goto Wait1_5_10;
	when True sync prob1 goto Wait1_5_11;
	when True sync prob1 goto Wait1_5_12;
	when True sync prob1 goto Wait1_5_13;
	when True sync prob1 goto Wait1_5_14;
	when True sync prob1 goto Wait1_5_15;
	when True sync prob1 goto Wait1_5_16;
	when True sync prob1 goto Wait1_5_17;
	when True sync prob1 goto Wait1_5_18;
	when True sync prob1 goto Wait1_5_19;
	when True sync prob1 goto Wait1_5_20;
	when True sync prob1 goto Wait1_5_21;
	when True sync prob1 goto Wait1_5_22;
	when True sync prob1 goto Wait1_5_23;
	when True sync prob1 goto Wait1_5_24;
	when True sync prob1 goto Wait1_5_25;
	when True sync prob1 goto Wait1_5_26;
	when True sync prob1 goto Wait1_5_27;
	when True sync prob1 goto Wait1_5_28;
	when True sync prob1 goto Wait1_5_29;
	when True sync prob1 goto Wait1_5_30;
	when True sync prob1 goto Wait1_5_31;
	when True sync prob1 goto Wait1_5_32;
	when True sync prob1 goto Wait1_5_33;
	when True sync prob1 goto Wait1_5_34;
	when True sync prob1 goto Wait1_5_35;
	when True sync prob1 goto Wait1_5_36;
	when True sync prob1 goto Wait1_5_37;
	when True sync prob1 goto Wait1_5_38;
	when True sync prob1 goto Wait1_5_39;
	when True sync prob1 goto Wait1_5_40;
	when True sync prob1 goto Wait1_5_41;
	when True sync prob1 goto Wait1_5_42;
	when True sync prob1 goto Wait1_5_43;
	when True sync prob1 goto Wait1_5_44;
	when True sync prob1 goto Wait1_5_45;
	when True sync prob1 goto Wait1_5_46;
	when True sync prob1 goto Wait1_5_47;
	when True sync prob1 goto Wait1_5_48;
	when True sync prob1 goto Wait1_5_49;
	when True sync prob1 goto Wait1_5_50;
	when True sync prob1 goto Wait1_5_51;
	when True sync prob1 goto Wait1_5_52;
	when True sync prob1 goto Wait1_5_53;
	when True sync prob1 goto Wait1_5_54;
	when True sync prob1 goto Wait1_5_55;
	when True sync prob1 goto Wait1_5_56;
	when True sync prob1 goto Wait1_5_57;
	when True sync prob1 goto Wait1_5_58;
	when True sync prob1 goto Wait1_5_59;
	when True sync prob1 goto Wait1_5_60;
	when True sync prob1 goto Wait1_5_61;
	when True sync prob1 goto Wait1_5_62;
	when True sync prob1 goto Wait1_5_63;

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

loc Wait1_5_1: invariant x1 <= 1 timeslot
	when x1 = 1 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 1 timeslot sync send1 do {x1 := 0} goto Transmit1;

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

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

loc Wait1_5_4: invariant x1 <= 4 timeslot
	when x1 = 4 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 4 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_5: invariant x1 <= 5 timeslot
	when x1 = 5 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 5 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_6: invariant x1 <= 6 timeslot
	when x1 = 6 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 6 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_7: invariant x1 <= 7 timeslot
	when x1 = 7 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 7 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_8: invariant x1 <= 8 timeslot
	when x1 = 8 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 8 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_9: invariant x1 <= 9 timeslot
	when x1 = 9 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 9 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_10: invariant x1 <= 10 timeslot
	when x1 = 10 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 10 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_11: invariant x1 <= 11 timeslot
	when x1 = 11 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 11 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_12: invariant x1 <= 12 timeslot
	when x1 = 12 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 12 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_13: invariant x1 <= 13 timeslot
	when x1 = 13 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 13 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_14: invariant x1 <= 14 timeslot
	when x1 = 14 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 14 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_15: invariant x1 <= 15 timeslot
	when x1 = 15 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 15 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_16: invariant x1 <= 16 timeslot
	when x1 = 16 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 16 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_17: invariant x1 <= 17 timeslot
	when x1 = 17 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 17 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_18: invariant x1 <= 18 timeslot
	when x1 = 18 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 18 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_19: invariant x1 <= 19 timeslot
	when x1 = 19 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 19 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_20: invariant x1 <= 20 timeslot
	when x1 = 20 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 20 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_21: invariant x1 <= 21 timeslot
	when x1 = 21 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 21 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_22: invariant x1 <= 22 timeslot
	when x1 = 22 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 22 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_23: invariant x1 <= 23 timeslot
	when x1 = 23 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 23 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_24: invariant x1 <= 24 timeslot
	when x1 = 24 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 24 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_25: invariant x1 <= 25 timeslot
	when x1 = 25 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 25 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_26: invariant x1 <= 26 timeslot
	when x1 = 26 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 26 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_27: invariant x1 <= 27 timeslot
	when x1 = 27 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 27 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_28: invariant x1 <= 28 timeslot
	when x1 = 28 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 28 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_29: invariant x1 <= 29 timeslot
	when x1 = 29 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 29 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_30: invariant x1 <= 30 timeslot
	when x1 = 30 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 30 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_31: invariant x1 <= 31 timeslot
	when x1 = 31 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 31 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_32: invariant x1 <= 32 timeslot
	when x1 = 32 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 32 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_33: invariant x1 <= 33 timeslot
	when x1 = 33 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 33 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_34: invariant x1 <= 34 timeslot
	when x1 = 34 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 34 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_35: invariant x1 <= 35 timeslot
	when x1 = 35 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 35 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_36: invariant x1 <= 36 timeslot
	when x1 = 36 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 36 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_37: invariant x1 <= 37 timeslot
	when x1 = 37 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 37 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_38: invariant x1 <= 38 timeslot
	when x1 = 38 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 38 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_39: invariant x1 <= 39 timeslot
	when x1 = 39 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 39 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_40: invariant x1 <= 40 timeslot
	when x1 = 40 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 40 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_41: invariant x1 <= 41 timeslot
	when x1 = 41 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 41 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_42: invariant x1 <= 42 timeslot
	when x1 = 42 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 42 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_43: invariant x1 <= 43 timeslot
	when x1 = 43 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 43 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_44: invariant x1 <= 44 timeslot
	when x1 = 44 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 44 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_45: invariant x1 <= 45 timeslot
	when x1 = 45 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 45 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_46: invariant x1 <= 46 timeslot
	when x1 = 46 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 46 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_47: invariant x1 <= 47 timeslot
	when x1 = 47 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 47 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_48: invariant x1 <= 48 timeslot
	when x1 = 48 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 48 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_49: invariant x1 <= 49 timeslot
	when x1 = 49 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 49 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_50: invariant x1 <= 50 timeslot
	when x1 = 50 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 50 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_51: invariant x1 <= 51 timeslot
	when x1 = 51 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 51 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_52: invariant x1 <= 52 timeslot
	when x1 = 52 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 52 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_53: invariant x1 <= 53 timeslot
	when x1 = 53 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 53 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_54: invariant x1 <= 54 timeslot
	when x1 = 54 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 54 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_55: invariant x1 <= 55 timeslot
	when x1 = 55 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 55 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_56: invariant x1 <= 56 timeslot
	when x1 = 56 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 56 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_57: invariant x1 <= 57 timeslot
	when x1 = 57 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 57 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_58: invariant x1 <= 58 timeslot
	when x1 = 58 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 58 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_59: invariant x1 <= 59 timeslot
	when x1 = 59 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 59 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_60: invariant x1 <= 60 timeslot
	when x1 = 60 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 60 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_61: invariant x1 <= 61 timeslot
	when x1 = 61 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 61 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_62: invariant x1 <= 62 timeslot
	when x1 = 62 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 62 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_5_63: invariant x1 <= 63 timeslot
	when x1 = 63 timeslot sync busy1 do {x1 := 0} goto Collide1_5;
	when x1 = 63 timeslot sync send1 do {x1 := 0} goto Transmit1;

(* END OF AUTOMATED PROGRAM FOR CSMA/CD *)

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_1;

(* STARTING AUTOMATED PROGRAM FOR CSMA/CD FOR STATION 2 WITH BCMAX = 5 *)

(* Considering case with bc = 1, hence from 0 to 3 (i.e., 2^(bc+1) - 1) *)
loc Collide2_1: invariant x2 <= 0
	when True sync prob2 goto Wait2_1_0;
	when True sync prob2 goto Wait2_1_1;
	when True sync prob2 goto Wait2_1_2;
	when True sync prob2 goto Wait2_1_3;

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

loc Wait2_1_1: invariant x2 <= 1 timeslot
	when x2 = 1 timeslot sync busy2 do {x2 := 0} goto Collide2_2;
	when x2 = 1 timeslot sync send2 do {x2 := 0} goto Transmit2;

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

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

(* Considering case with bc = 2, hence from 0 to 7 (i.e., 2^(bc+1) - 1) *)
loc Collide2_2: invariant x2 <= 0
	when True sync prob2 goto Wait2_2_0;
	when True sync prob2 goto Wait2_2_1;
	when True sync prob2 goto Wait2_2_2;
	when True sync prob2 goto Wait2_2_3;
	when True sync prob2 goto Wait2_2_4;
	when True sync prob2 goto Wait2_2_5;
	when True sync prob2 goto Wait2_2_6;
	when True sync prob2 goto Wait2_2_7;

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

loc Wait2_2_1: invariant x2 <= 1 timeslot
	when x2 = 1 timeslot sync busy2 do {x2 := 0} goto Collide2_3;
	when x2 = 1 timeslot sync send2 do {x2 := 0} goto Transmit2;

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

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

loc Wait2_2_4: invariant x2 <= 4 timeslot
	when x2 = 4 timeslot sync busy2 do {x2 := 0} goto Collide2_3;
	when x2 = 4 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_2_5: invariant x2 <= 5 timeslot
	when x2 = 5 timeslot sync busy2 do {x2 := 0} goto Collide2_3;
	when x2 = 5 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_2_6: invariant x2 <= 6 timeslot
	when x2 = 6 timeslot sync busy2 do {x2 := 0} goto Collide2_3;
	when x2 = 6 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_2_7: invariant x2 <= 7 timeslot
	when x2 = 7 timeslot sync busy2 do {x2 := 0} goto Collide2_3;
	when x2 = 7 timeslot sync send2 do {x2 := 0} goto Transmit2;

(* Considering case with bc = 3, hence from 0 to 15 (i.e., 2^(bc+1) - 1) *)
loc Collide2_3: invariant x2 <= 0
	when True sync prob2 goto Wait2_3_0;
	when True sync prob2 goto Wait2_3_1;
	when True sync prob2 goto Wait2_3_2;
	when True sync prob2 goto Wait2_3_3;
	when True sync prob2 goto Wait2_3_4;
	when True sync prob2 goto Wait2_3_5;
	when True sync prob2 goto Wait2_3_6;
	when True sync prob2 goto Wait2_3_7;
	when True sync prob2 goto Wait2_3_8;
	when True sync prob2 goto Wait2_3_9;
	when True sync prob2 goto Wait2_3_10;
	when True sync prob2 goto Wait2_3_11;
	when True sync prob2 goto Wait2_3_12;
	when True sync prob2 goto Wait2_3_13;
	when True sync prob2 goto Wait2_3_14;
	when True sync prob2 goto Wait2_3_15;

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

loc Wait2_3_1: invariant x2 <= 1 timeslot
	when x2 = 1 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 1 timeslot sync send2 do {x2 := 0} goto Transmit2;

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

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

loc Wait2_3_4: invariant x2 <= 4 timeslot
	when x2 = 4 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 4 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_5: invariant x2 <= 5 timeslot
	when x2 = 5 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 5 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_6: invariant x2 <= 6 timeslot
	when x2 = 6 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 6 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_7: invariant x2 <= 7 timeslot
	when x2 = 7 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 7 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_8: invariant x2 <= 8 timeslot
	when x2 = 8 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 8 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_9: invariant x2 <= 9 timeslot
	when x2 = 9 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 9 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_10: invariant x2 <= 10 timeslot
	when x2 = 10 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 10 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_11: invariant x2 <= 11 timeslot
	when x2 = 11 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 11 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_12: invariant x2 <= 12 timeslot
	when x2 = 12 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 12 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_13: invariant x2 <= 13 timeslot
	when x2 = 13 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 13 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_14: invariant x2 <= 14 timeslot
	when x2 = 14 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 14 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_3_15: invariant x2 <= 15 timeslot
	when x2 = 15 timeslot sync busy2 do {x2 := 0} goto Collide2_4;
	when x2 = 15 timeslot sync send2 do {x2 := 0} goto Transmit2;

(* Considering case with bc = 4, hence from 0 to 31 (i.e., 2^(bc+1) - 1) *)
loc Collide2_4: invariant x2 <= 0
	when True sync prob2 goto Wait2_4_0;
	when True sync prob2 goto Wait2_4_1;
	when True sync prob2 goto Wait2_4_2;
	when True sync prob2 goto Wait2_4_3;
	when True sync prob2 goto Wait2_4_4;
	when True sync prob2 goto Wait2_4_5;
	when True sync prob2 goto Wait2_4_6;
	when True sync prob2 goto Wait2_4_7;
	when True sync prob2 goto Wait2_4_8;
	when True sync prob2 goto Wait2_4_9;
	when True sync prob2 goto Wait2_4_10;
	when True sync prob2 goto Wait2_4_11;
	when True sync prob2 goto Wait2_4_12;
	when True sync prob2 goto Wait2_4_13;
	when True sync prob2 goto Wait2_4_14;
	when True sync prob2 goto Wait2_4_15;
	when True sync prob2 goto Wait2_4_16;
	when True sync prob2 goto Wait2_4_17;
	when True sync prob2 goto Wait2_4_18;
	when True sync prob2 goto Wait2_4_19;
	when True sync prob2 goto Wait2_4_20;
	when True sync prob2 goto Wait2_4_21;
	when True sync prob2 goto Wait2_4_22;
	when True sync prob2 goto Wait2_4_23;
	when True sync prob2 goto Wait2_4_24;
	when True sync prob2 goto Wait2_4_25;
	when True sync prob2 goto Wait2_4_26;
	when True sync prob2 goto Wait2_4_27;
	when True sync prob2 goto Wait2_4_28;
	when True sync prob2 goto Wait2_4_29;
	when True sync prob2 goto Wait2_4_30;
	when True sync prob2 goto Wait2_4_31;

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

loc Wait2_4_1: invariant x2 <= 1 timeslot
	when x2 = 1 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 1 timeslot sync send2 do {x2 := 0} goto Transmit2;

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

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

loc Wait2_4_4: invariant x2 <= 4 timeslot
	when x2 = 4 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 4 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_5: invariant x2 <= 5 timeslot
	when x2 = 5 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 5 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_6: invariant x2 <= 6 timeslot
	when x2 = 6 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 6 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_7: invariant x2 <= 7 timeslot
	when x2 = 7 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 7 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_8: invariant x2 <= 8 timeslot
	when x2 = 8 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 8 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_9: invariant x2 <= 9 timeslot
	when x2 = 9 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 9 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_10: invariant x2 <= 10 timeslot
	when x2 = 10 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 10 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_11: invariant x2 <= 11 timeslot
	when x2 = 11 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 11 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_12: invariant x2 <= 12 timeslot
	when x2 = 12 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 12 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_13: invariant x2 <= 13 timeslot
	when x2 = 13 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 13 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_14: invariant x2 <= 14 timeslot
	when x2 = 14 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 14 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_15: invariant x2 <= 15 timeslot
	when x2 = 15 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 15 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_16: invariant x2 <= 16 timeslot
	when x2 = 16 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 16 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_17: invariant x2 <= 17 timeslot
	when x2 = 17 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 17 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_18: invariant x2 <= 18 timeslot
	when x2 = 18 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 18 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_19: invariant x2 <= 19 timeslot
	when x2 = 19 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 19 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_20: invariant x2 <= 20 timeslot
	when x2 = 20 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 20 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_21: invariant x2 <= 21 timeslot
	when x2 = 21 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 21 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_22: invariant x2 <= 22 timeslot
	when x2 = 22 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 22 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_23: invariant x2 <= 23 timeslot
	when x2 = 23 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 23 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_24: invariant x2 <= 24 timeslot
	when x2 = 24 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 24 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_25: invariant x2 <= 25 timeslot
	when x2 = 25 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 25 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_26: invariant x2 <= 26 timeslot
	when x2 = 26 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 26 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_27: invariant x2 <= 27 timeslot
	when x2 = 27 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 27 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_28: invariant x2 <= 28 timeslot
	when x2 = 28 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 28 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_29: invariant x2 <= 29 timeslot
	when x2 = 29 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 29 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_30: invariant x2 <= 30 timeslot
	when x2 = 30 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 30 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_4_31: invariant x2 <= 31 timeslot
	when x2 = 31 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 31 timeslot sync send2 do {x2 := 0} goto Transmit2;

(* Considering case with bc = 5, hence from 0 to 63 (i.e., 2^(bc+1) - 1) *)
loc Collide2_5: invariant x2 <= 0
	when True sync prob2 goto Wait2_5_0;
	when True sync prob2 goto Wait2_5_1;
	when True sync prob2 goto Wait2_5_2;
	when True sync prob2 goto Wait2_5_3;
	when True sync prob2 goto Wait2_5_4;
	when True sync prob2 goto Wait2_5_5;
	when True sync prob2 goto Wait2_5_6;
	when True sync prob2 goto Wait2_5_7;
	when True sync prob2 goto Wait2_5_8;
	when True sync prob2 goto Wait2_5_9;
	when True sync prob2 goto Wait2_5_10;
	when True sync prob2 goto Wait2_5_11;
	when True sync prob2 goto Wait2_5_12;
	when True sync prob2 goto Wait2_5_13;
	when True sync prob2 goto Wait2_5_14;
	when True sync prob2 goto Wait2_5_15;
	when True sync prob2 goto Wait2_5_16;
	when True sync prob2 goto Wait2_5_17;
	when True sync prob2 goto Wait2_5_18;
	when True sync prob2 goto Wait2_5_19;
	when True sync prob2 goto Wait2_5_20;
	when True sync prob2 goto Wait2_5_21;
	when True sync prob2 goto Wait2_5_22;
	when True sync prob2 goto Wait2_5_23;
	when True sync prob2 goto Wait2_5_24;
	when True sync prob2 goto Wait2_5_25;
	when True sync prob2 goto Wait2_5_26;
	when True sync prob2 goto Wait2_5_27;
	when True sync prob2 goto Wait2_5_28;
	when True sync prob2 goto Wait2_5_29;
	when True sync prob2 goto Wait2_5_30;
	when True sync prob2 goto Wait2_5_31;
	when True sync prob2 goto Wait2_5_32;
	when True sync prob2 goto Wait2_5_33;
	when True sync prob2 goto Wait2_5_34;
	when True sync prob2 goto Wait2_5_35;
	when True sync prob2 goto Wait2_5_36;
	when True sync prob2 goto Wait2_5_37;
	when True sync prob2 goto Wait2_5_38;
	when True sync prob2 goto Wait2_5_39;
	when True sync prob2 goto Wait2_5_40;
	when True sync prob2 goto Wait2_5_41;
	when True sync prob2 goto Wait2_5_42;
	when True sync prob2 goto Wait2_5_43;
	when True sync prob2 goto Wait2_5_44;
	when True sync prob2 goto Wait2_5_45;
	when True sync prob2 goto Wait2_5_46;
	when True sync prob2 goto Wait2_5_47;
	when True sync prob2 goto Wait2_5_48;
	when True sync prob2 goto Wait2_5_49;
	when True sync prob2 goto Wait2_5_50;
	when True sync prob2 goto Wait2_5_51;
	when True sync prob2 goto Wait2_5_52;
	when True sync prob2 goto Wait2_5_53;
	when True sync prob2 goto Wait2_5_54;
	when True sync prob2 goto Wait2_5_55;
	when True sync prob2 goto Wait2_5_56;
	when True sync prob2 goto Wait2_5_57;
	when True sync prob2 goto Wait2_5_58;
	when True sync prob2 goto Wait2_5_59;
	when True sync prob2 goto Wait2_5_60;
	when True sync prob2 goto Wait2_5_61;
	when True sync prob2 goto Wait2_5_62;
	when True sync prob2 goto Wait2_5_63;

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

loc Wait2_5_1: invariant x2 <= 1 timeslot
	when x2 = 1 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 1 timeslot sync send2 do {x2 := 0} goto Transmit2;

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

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

loc Wait2_5_4: invariant x2 <= 4 timeslot
	when x2 = 4 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 4 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_5: invariant x2 <= 5 timeslot
	when x2 = 5 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 5 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_6: invariant x2 <= 6 timeslot
	when x2 = 6 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 6 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_7: invariant x2 <= 7 timeslot
	when x2 = 7 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 7 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_8: invariant x2 <= 8 timeslot
	when x2 = 8 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 8 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_9: invariant x2 <= 9 timeslot
	when x2 = 9 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 9 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_10: invariant x2 <= 10 timeslot
	when x2 = 10 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 10 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_11: invariant x2 <= 11 timeslot
	when x2 = 11 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 11 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_12: invariant x2 <= 12 timeslot
	when x2 = 12 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 12 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_13: invariant x2 <= 13 timeslot
	when x2 = 13 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 13 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_14: invariant x2 <= 14 timeslot
	when x2 = 14 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 14 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_15: invariant x2 <= 15 timeslot
	when x2 = 15 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 15 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_16: invariant x2 <= 16 timeslot
	when x2 = 16 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 16 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_17: invariant x2 <= 17 timeslot
	when x2 = 17 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 17 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_18: invariant x2 <= 18 timeslot
	when x2 = 18 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 18 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_19: invariant x2 <= 19 timeslot
	when x2 = 19 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 19 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_20: invariant x2 <= 20 timeslot
	when x2 = 20 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 20 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_21: invariant x2 <= 21 timeslot
	when x2 = 21 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 21 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_22: invariant x2 <= 22 timeslot
	when x2 = 22 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 22 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_23: invariant x2 <= 23 timeslot
	when x2 = 23 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 23 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_24: invariant x2 <= 24 timeslot
	when x2 = 24 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 24 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_25: invariant x2 <= 25 timeslot
	when x2 = 25 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 25 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_26: invariant x2 <= 26 timeslot
	when x2 = 26 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 26 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_27: invariant x2 <= 27 timeslot
	when x2 = 27 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 27 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_28: invariant x2 <= 28 timeslot
	when x2 = 28 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 28 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_29: invariant x2 <= 29 timeslot
	when x2 = 29 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 29 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_30: invariant x2 <= 30 timeslot
	when x2 = 30 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 30 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_31: invariant x2 <= 31 timeslot
	when x2 = 31 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 31 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_32: invariant x2 <= 32 timeslot
	when x2 = 32 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 32 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_33: invariant x2 <= 33 timeslot
	when x2 = 33 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 33 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_34: invariant x2 <= 34 timeslot
	when x2 = 34 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 34 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_35: invariant x2 <= 35 timeslot
	when x2 = 35 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 35 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_36: invariant x2 <= 36 timeslot
	when x2 = 36 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 36 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_37: invariant x2 <= 37 timeslot
	when x2 = 37 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 37 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_38: invariant x2 <= 38 timeslot
	when x2 = 38 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 38 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_39: invariant x2 <= 39 timeslot
	when x2 = 39 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 39 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_40: invariant x2 <= 40 timeslot
	when x2 = 40 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 40 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_41: invariant x2 <= 41 timeslot
	when x2 = 41 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 41 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_42: invariant x2 <= 42 timeslot
	when x2 = 42 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 42 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_43: invariant x2 <= 43 timeslot
	when x2 = 43 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 43 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_44: invariant x2 <= 44 timeslot
	when x2 = 44 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 44 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_45: invariant x2 <= 45 timeslot
	when x2 = 45 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 45 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_46: invariant x2 <= 46 timeslot
	when x2 = 46 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 46 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_47: invariant x2 <= 47 timeslot
	when x2 = 47 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 47 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_48: invariant x2 <= 48 timeslot
	when x2 = 48 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 48 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_49: invariant x2 <= 49 timeslot
	when x2 = 49 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 49 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_50: invariant x2 <= 50 timeslot
	when x2 = 50 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 50 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_51: invariant x2 <= 51 timeslot
	when x2 = 51 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 51 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_52: invariant x2 <= 52 timeslot
	when x2 = 52 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 52 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_53: invariant x2 <= 53 timeslot
	when x2 = 53 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 53 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_54: invariant x2 <= 54 timeslot
	when x2 = 54 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 54 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_55: invariant x2 <= 55 timeslot
	when x2 = 55 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 55 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_56: invariant x2 <= 56 timeslot
	when x2 = 56 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 56 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_57: invariant x2 <= 57 timeslot
	when x2 = 57 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 57 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_58: invariant x2 <= 58 timeslot
	when x2 = 58 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 58 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_59: invariant x2 <= 59 timeslot
	when x2 = 59 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 59 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_60: invariant x2 <= 60 timeslot
	when x2 = 60 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 60 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_61: invariant x2 <= 61 timeslot
	when x2 = 61 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 61 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_62: invariant x2 <= 62 timeslot
	when x2 = 62 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 62 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_5_63: invariant x2 <= 63 timeslot
	when x2 = 63 timeslot sync busy2 do {x2 := 0} goto Collide2_5;
	when x2 = 63 timeslot sync send2 do {x2 := 0} goto Transmit2;

(* END OF AUTOMATED PROGRAM FOR CSMA/CD *)
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