(************************************************************
 *                      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=6, i.e., up to waiting time of 127*timeslot
	(partially generated file!)
 * 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   : 2018/08/13
 *
 * IMITATOR version: 2.10.2
 ************************************************************)

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 = 6 *)

(* 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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	when x1 = 63 timeslot sync send1 do {x1 := 0} goto Transmit1;

(* Considering case with bc = 6, hence from 0 to 127 (i.e., 2^(bc+1) - 1) *)
loc Collide1_6: invariant x1 <= 0
	when True sync prob1 goto Wait1_6_0;
	when True sync prob1 goto Wait1_6_1;
	when True sync prob1 goto Wait1_6_2;
	when True sync prob1 goto Wait1_6_3;
	when True sync prob1 goto Wait1_6_4;
	when True sync prob1 goto Wait1_6_5;
	when True sync prob1 goto Wait1_6_6;
	when True sync prob1 goto Wait1_6_7;
	when True sync prob1 goto Wait1_6_8;
	when True sync prob1 goto Wait1_6_9;
	when True sync prob1 goto Wait1_6_10;
	when True sync prob1 goto Wait1_6_11;
	when True sync prob1 goto Wait1_6_12;
	when True sync prob1 goto Wait1_6_13;
	when True sync prob1 goto Wait1_6_14;
	when True sync prob1 goto Wait1_6_15;
	when True sync prob1 goto Wait1_6_16;
	when True sync prob1 goto Wait1_6_17;
	when True sync prob1 goto Wait1_6_18;
	when True sync prob1 goto Wait1_6_19;
	when True sync prob1 goto Wait1_6_20;
	when True sync prob1 goto Wait1_6_21;
	when True sync prob1 goto Wait1_6_22;
	when True sync prob1 goto Wait1_6_23;
	when True sync prob1 goto Wait1_6_24;
	when True sync prob1 goto Wait1_6_25;
	when True sync prob1 goto Wait1_6_26;
	when True sync prob1 goto Wait1_6_27;
	when True sync prob1 goto Wait1_6_28;
	when True sync prob1 goto Wait1_6_29;
	when True sync prob1 goto Wait1_6_30;
	when True sync prob1 goto Wait1_6_31;
	when True sync prob1 goto Wait1_6_32;
	when True sync prob1 goto Wait1_6_33;
	when True sync prob1 goto Wait1_6_34;
	when True sync prob1 goto Wait1_6_35;
	when True sync prob1 goto Wait1_6_36;
	when True sync prob1 goto Wait1_6_37;
	when True sync prob1 goto Wait1_6_38;
	when True sync prob1 goto Wait1_6_39;
	when True sync prob1 goto Wait1_6_40;
	when True sync prob1 goto Wait1_6_41;
	when True sync prob1 goto Wait1_6_42;
	when True sync prob1 goto Wait1_6_43;
	when True sync prob1 goto Wait1_6_44;
	when True sync prob1 goto Wait1_6_45;
	when True sync prob1 goto Wait1_6_46;
	when True sync prob1 goto Wait1_6_47;
	when True sync prob1 goto Wait1_6_48;
	when True sync prob1 goto Wait1_6_49;
	when True sync prob1 goto Wait1_6_50;
	when True sync prob1 goto Wait1_6_51;
	when True sync prob1 goto Wait1_6_52;
	when True sync prob1 goto Wait1_6_53;
	when True sync prob1 goto Wait1_6_54;
	when True sync prob1 goto Wait1_6_55;
	when True sync prob1 goto Wait1_6_56;
	when True sync prob1 goto Wait1_6_57;
	when True sync prob1 goto Wait1_6_58;
	when True sync prob1 goto Wait1_6_59;
	when True sync prob1 goto Wait1_6_60;
	when True sync prob1 goto Wait1_6_61;
	when True sync prob1 goto Wait1_6_62;
	when True sync prob1 goto Wait1_6_63;
	when True sync prob1 goto Wait1_6_64;
	when True sync prob1 goto Wait1_6_65;
	when True sync prob1 goto Wait1_6_66;
	when True sync prob1 goto Wait1_6_67;
	when True sync prob1 goto Wait1_6_68;
	when True sync prob1 goto Wait1_6_69;
	when True sync prob1 goto Wait1_6_70;
	when True sync prob1 goto Wait1_6_71;
	when True sync prob1 goto Wait1_6_72;
	when True sync prob1 goto Wait1_6_73;
	when True sync prob1 goto Wait1_6_74;
	when True sync prob1 goto Wait1_6_75;
	when True sync prob1 goto Wait1_6_76;
	when True sync prob1 goto Wait1_6_77;
	when True sync prob1 goto Wait1_6_78;
	when True sync prob1 goto Wait1_6_79;
	when True sync prob1 goto Wait1_6_80;
	when True sync prob1 goto Wait1_6_81;
	when True sync prob1 goto Wait1_6_82;
	when True sync prob1 goto Wait1_6_83;
	when True sync prob1 goto Wait1_6_84;
	when True sync prob1 goto Wait1_6_85;
	when True sync prob1 goto Wait1_6_86;
	when True sync prob1 goto Wait1_6_87;
	when True sync prob1 goto Wait1_6_88;
	when True sync prob1 goto Wait1_6_89;
	when True sync prob1 goto Wait1_6_90;
	when True sync prob1 goto Wait1_6_91;
	when True sync prob1 goto Wait1_6_92;
	when True sync prob1 goto Wait1_6_93;
	when True sync prob1 goto Wait1_6_94;
	when True sync prob1 goto Wait1_6_95;
	when True sync prob1 goto Wait1_6_96;
	when True sync prob1 goto Wait1_6_97;
	when True sync prob1 goto Wait1_6_98;
	when True sync prob1 goto Wait1_6_99;
	when True sync prob1 goto Wait1_6_100;
	when True sync prob1 goto Wait1_6_101;
	when True sync prob1 goto Wait1_6_102;
	when True sync prob1 goto Wait1_6_103;
	when True sync prob1 goto Wait1_6_104;
	when True sync prob1 goto Wait1_6_105;
	when True sync prob1 goto Wait1_6_106;
	when True sync prob1 goto Wait1_6_107;
	when True sync prob1 goto Wait1_6_108;
	when True sync prob1 goto Wait1_6_109;
	when True sync prob1 goto Wait1_6_110;
	when True sync prob1 goto Wait1_6_111;
	when True sync prob1 goto Wait1_6_112;
	when True sync prob1 goto Wait1_6_113;
	when True sync prob1 goto Wait1_6_114;
	when True sync prob1 goto Wait1_6_115;
	when True sync prob1 goto Wait1_6_116;
	when True sync prob1 goto Wait1_6_117;
	when True sync prob1 goto Wait1_6_118;
	when True sync prob1 goto Wait1_6_119;
	when True sync prob1 goto Wait1_6_120;
	when True sync prob1 goto Wait1_6_121;
	when True sync prob1 goto Wait1_6_122;
	when True sync prob1 goto Wait1_6_123;
	when True sync prob1 goto Wait1_6_124;
	when True sync prob1 goto Wait1_6_125;
	when True sync prob1 goto Wait1_6_126;
	when True sync prob1 goto Wait1_6_127;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

loc Wait1_6_64: invariant x1 <= 64 timeslot
	when x1 = 64 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 64 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_65: invariant x1 <= 65 timeslot
	when x1 = 65 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 65 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_66: invariant x1 <= 66 timeslot
	when x1 = 66 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 66 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_67: invariant x1 <= 67 timeslot
	when x1 = 67 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 67 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_68: invariant x1 <= 68 timeslot
	when x1 = 68 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 68 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_69: invariant x1 <= 69 timeslot
	when x1 = 69 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 69 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_70: invariant x1 <= 70 timeslot
	when x1 = 70 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 70 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_71: invariant x1 <= 71 timeslot
	when x1 = 71 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 71 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_72: invariant x1 <= 72 timeslot
	when x1 = 72 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 72 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_73: invariant x1 <= 73 timeslot
	when x1 = 73 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 73 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_74: invariant x1 <= 74 timeslot
	when x1 = 74 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 74 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_75: invariant x1 <= 75 timeslot
	when x1 = 75 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 75 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_76: invariant x1 <= 76 timeslot
	when x1 = 76 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 76 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_77: invariant x1 <= 77 timeslot
	when x1 = 77 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 77 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_78: invariant x1 <= 78 timeslot
	when x1 = 78 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 78 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_79: invariant x1 <= 79 timeslot
	when x1 = 79 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 79 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_80: invariant x1 <= 80 timeslot
	when x1 = 80 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 80 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_81: invariant x1 <= 81 timeslot
	when x1 = 81 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 81 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_82: invariant x1 <= 82 timeslot
	when x1 = 82 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 82 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_83: invariant x1 <= 83 timeslot
	when x1 = 83 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 83 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_84: invariant x1 <= 84 timeslot
	when x1 = 84 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 84 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_85: invariant x1 <= 85 timeslot
	when x1 = 85 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 85 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_86: invariant x1 <= 86 timeslot
	when x1 = 86 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 86 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_87: invariant x1 <= 87 timeslot
	when x1 = 87 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 87 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_88: invariant x1 <= 88 timeslot
	when x1 = 88 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 88 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_89: invariant x1 <= 89 timeslot
	when x1 = 89 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 89 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_90: invariant x1 <= 90 timeslot
	when x1 = 90 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 90 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_91: invariant x1 <= 91 timeslot
	when x1 = 91 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 91 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_92: invariant x1 <= 92 timeslot
	when x1 = 92 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 92 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_93: invariant x1 <= 93 timeslot
	when x1 = 93 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 93 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_94: invariant x1 <= 94 timeslot
	when x1 = 94 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 94 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_95: invariant x1 <= 95 timeslot
	when x1 = 95 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 95 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_96: invariant x1 <= 96 timeslot
	when x1 = 96 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 96 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_97: invariant x1 <= 97 timeslot
	when x1 = 97 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 97 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_98: invariant x1 <= 98 timeslot
	when x1 = 98 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 98 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_99: invariant x1 <= 99 timeslot
	when x1 = 99 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 99 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_100: invariant x1 <= 100 timeslot
	when x1 = 100 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 100 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_101: invariant x1 <= 101 timeslot
	when x1 = 101 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 101 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_102: invariant x1 <= 102 timeslot
	when x1 = 102 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 102 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_103: invariant x1 <= 103 timeslot
	when x1 = 103 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 103 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_104: invariant x1 <= 104 timeslot
	when x1 = 104 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 104 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_105: invariant x1 <= 105 timeslot
	when x1 = 105 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 105 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_106: invariant x1 <= 106 timeslot
	when x1 = 106 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 106 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_107: invariant x1 <= 107 timeslot
	when x1 = 107 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 107 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_108: invariant x1 <= 108 timeslot
	when x1 = 108 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 108 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_109: invariant x1 <= 109 timeslot
	when x1 = 109 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 109 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_110: invariant x1 <= 110 timeslot
	when x1 = 110 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 110 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_111: invariant x1 <= 111 timeslot
	when x1 = 111 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 111 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_112: invariant x1 <= 112 timeslot
	when x1 = 112 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 112 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_113: invariant x1 <= 113 timeslot
	when x1 = 113 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 113 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_114: invariant x1 <= 114 timeslot
	when x1 = 114 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 114 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_115: invariant x1 <= 115 timeslot
	when x1 = 115 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 115 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_116: invariant x1 <= 116 timeslot
	when x1 = 116 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 116 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_117: invariant x1 <= 117 timeslot
	when x1 = 117 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 117 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_118: invariant x1 <= 118 timeslot
	when x1 = 118 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 118 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_119: invariant x1 <= 119 timeslot
	when x1 = 119 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 119 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_120: invariant x1 <= 120 timeslot
	when x1 = 120 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 120 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_121: invariant x1 <= 121 timeslot
	when x1 = 121 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 121 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_122: invariant x1 <= 122 timeslot
	when x1 = 122 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 122 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_123: invariant x1 <= 123 timeslot
	when x1 = 123 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 123 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_124: invariant x1 <= 124 timeslot
	when x1 = 124 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 124 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_125: invariant x1 <= 125 timeslot
	when x1 = 125 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 125 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_126: invariant x1 <= 126 timeslot
	when x1 = 126 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 126 timeslot sync send1 do {x1 := 0} goto Transmit1;

loc Wait1_6_127: invariant x1 <= 127 timeslot
	when x1 = 127 timeslot sync busy1 do {x1 := 0} goto Collide1_6;
	when x1 = 127 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 = 6 *)

(* 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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	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_6;
	when x2 = 63 timeslot sync send2 do {x2 := 0} goto Transmit2;

(* Considering case with bc = 6, hence from 0 to 127 (i.e., 2^(bc+1) - 1) *)
loc Collide2_6: invariant x2 <= 0
	when True sync prob2 goto Wait2_6_0;
	when True sync prob2 goto Wait2_6_1;
	when True sync prob2 goto Wait2_6_2;
	when True sync prob2 goto Wait2_6_3;
	when True sync prob2 goto Wait2_6_4;
	when True sync prob2 goto Wait2_6_5;
	when True sync prob2 goto Wait2_6_6;
	when True sync prob2 goto Wait2_6_7;
	when True sync prob2 goto Wait2_6_8;
	when True sync prob2 goto Wait2_6_9;
	when True sync prob2 goto Wait2_6_10;
	when True sync prob2 goto Wait2_6_11;
	when True sync prob2 goto Wait2_6_12;
	when True sync prob2 goto Wait2_6_13;
	when True sync prob2 goto Wait2_6_14;
	when True sync prob2 goto Wait2_6_15;
	when True sync prob2 goto Wait2_6_16;
	when True sync prob2 goto Wait2_6_17;
	when True sync prob2 goto Wait2_6_18;
	when True sync prob2 goto Wait2_6_19;
	when True sync prob2 goto Wait2_6_20;
	when True sync prob2 goto Wait2_6_21;
	when True sync prob2 goto Wait2_6_22;
	when True sync prob2 goto Wait2_6_23;
	when True sync prob2 goto Wait2_6_24;
	when True sync prob2 goto Wait2_6_25;
	when True sync prob2 goto Wait2_6_26;
	when True sync prob2 goto Wait2_6_27;
	when True sync prob2 goto Wait2_6_28;
	when True sync prob2 goto Wait2_6_29;
	when True sync prob2 goto Wait2_6_30;
	when True sync prob2 goto Wait2_6_31;
	when True sync prob2 goto Wait2_6_32;
	when True sync prob2 goto Wait2_6_33;
	when True sync prob2 goto Wait2_6_34;
	when True sync prob2 goto Wait2_6_35;
	when True sync prob2 goto Wait2_6_36;
	when True sync prob2 goto Wait2_6_37;
	when True sync prob2 goto Wait2_6_38;
	when True sync prob2 goto Wait2_6_39;
	when True sync prob2 goto Wait2_6_40;
	when True sync prob2 goto Wait2_6_41;
	when True sync prob2 goto Wait2_6_42;
	when True sync prob2 goto Wait2_6_43;
	when True sync prob2 goto Wait2_6_44;
	when True sync prob2 goto Wait2_6_45;
	when True sync prob2 goto Wait2_6_46;
	when True sync prob2 goto Wait2_6_47;
	when True sync prob2 goto Wait2_6_48;
	when True sync prob2 goto Wait2_6_49;
	when True sync prob2 goto Wait2_6_50;
	when True sync prob2 goto Wait2_6_51;
	when True sync prob2 goto Wait2_6_52;
	when True sync prob2 goto Wait2_6_53;
	when True sync prob2 goto Wait2_6_54;
	when True sync prob2 goto Wait2_6_55;
	when True sync prob2 goto Wait2_6_56;
	when True sync prob2 goto Wait2_6_57;
	when True sync prob2 goto Wait2_6_58;
	when True sync prob2 goto Wait2_6_59;
	when True sync prob2 goto Wait2_6_60;
	when True sync prob2 goto Wait2_6_61;
	when True sync prob2 goto Wait2_6_62;
	when True sync prob2 goto Wait2_6_63;
	when True sync prob2 goto Wait2_6_64;
	when True sync prob2 goto Wait2_6_65;
	when True sync prob2 goto Wait2_6_66;
	when True sync prob2 goto Wait2_6_67;
	when True sync prob2 goto Wait2_6_68;
	when True sync prob2 goto Wait2_6_69;
	when True sync prob2 goto Wait2_6_70;
	when True sync prob2 goto Wait2_6_71;
	when True sync prob2 goto Wait2_6_72;
	when True sync prob2 goto Wait2_6_73;
	when True sync prob2 goto Wait2_6_74;
	when True sync prob2 goto Wait2_6_75;
	when True sync prob2 goto Wait2_6_76;
	when True sync prob2 goto Wait2_6_77;
	when True sync prob2 goto Wait2_6_78;
	when True sync prob2 goto Wait2_6_79;
	when True sync prob2 goto Wait2_6_80;
	when True sync prob2 goto Wait2_6_81;
	when True sync prob2 goto Wait2_6_82;
	when True sync prob2 goto Wait2_6_83;
	when True sync prob2 goto Wait2_6_84;
	when True sync prob2 goto Wait2_6_85;
	when True sync prob2 goto Wait2_6_86;
	when True sync prob2 goto Wait2_6_87;
	when True sync prob2 goto Wait2_6_88;
	when True sync prob2 goto Wait2_6_89;
	when True sync prob2 goto Wait2_6_90;
	when True sync prob2 goto Wait2_6_91;
	when True sync prob2 goto Wait2_6_92;
	when True sync prob2 goto Wait2_6_93;
	when True sync prob2 goto Wait2_6_94;
	when True sync prob2 goto Wait2_6_95;
	when True sync prob2 goto Wait2_6_96;
	when True sync prob2 goto Wait2_6_97;
	when True sync prob2 goto Wait2_6_98;
	when True sync prob2 goto Wait2_6_99;
	when True sync prob2 goto Wait2_6_100;
	when True sync prob2 goto Wait2_6_101;
	when True sync prob2 goto Wait2_6_102;
	when True sync prob2 goto Wait2_6_103;
	when True sync prob2 goto Wait2_6_104;
	when True sync prob2 goto Wait2_6_105;
	when True sync prob2 goto Wait2_6_106;
	when True sync prob2 goto Wait2_6_107;
	when True sync prob2 goto Wait2_6_108;
	when True sync prob2 goto Wait2_6_109;
	when True sync prob2 goto Wait2_6_110;
	when True sync prob2 goto Wait2_6_111;
	when True sync prob2 goto Wait2_6_112;
	when True sync prob2 goto Wait2_6_113;
	when True sync prob2 goto Wait2_6_114;
	when True sync prob2 goto Wait2_6_115;
	when True sync prob2 goto Wait2_6_116;
	when True sync prob2 goto Wait2_6_117;
	when True sync prob2 goto Wait2_6_118;
	when True sync prob2 goto Wait2_6_119;
	when True sync prob2 goto Wait2_6_120;
	when True sync prob2 goto Wait2_6_121;
	when True sync prob2 goto Wait2_6_122;
	when True sync prob2 goto Wait2_6_123;
	when True sync prob2 goto Wait2_6_124;
	when True sync prob2 goto Wait2_6_125;
	when True sync prob2 goto Wait2_6_126;
	when True sync prob2 goto Wait2_6_127;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

loc Wait2_6_64: invariant x2 <= 64 timeslot
	when x2 = 64 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 64 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_65: invariant x2 <= 65 timeslot
	when x2 = 65 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 65 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_66: invariant x2 <= 66 timeslot
	when x2 = 66 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 66 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_67: invariant x2 <= 67 timeslot
	when x2 = 67 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 67 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_68: invariant x2 <= 68 timeslot
	when x2 = 68 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 68 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_69: invariant x2 <= 69 timeslot
	when x2 = 69 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 69 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_70: invariant x2 <= 70 timeslot
	when x2 = 70 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 70 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_71: invariant x2 <= 71 timeslot
	when x2 = 71 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 71 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_72: invariant x2 <= 72 timeslot
	when x2 = 72 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 72 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_73: invariant x2 <= 73 timeslot
	when x2 = 73 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 73 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_74: invariant x2 <= 74 timeslot
	when x2 = 74 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 74 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_75: invariant x2 <= 75 timeslot
	when x2 = 75 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 75 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_76: invariant x2 <= 76 timeslot
	when x2 = 76 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 76 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_77: invariant x2 <= 77 timeslot
	when x2 = 77 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 77 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_78: invariant x2 <= 78 timeslot
	when x2 = 78 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 78 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_79: invariant x2 <= 79 timeslot
	when x2 = 79 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 79 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_80: invariant x2 <= 80 timeslot
	when x2 = 80 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 80 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_81: invariant x2 <= 81 timeslot
	when x2 = 81 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 81 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_82: invariant x2 <= 82 timeslot
	when x2 = 82 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 82 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_83: invariant x2 <= 83 timeslot
	when x2 = 83 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 83 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_84: invariant x2 <= 84 timeslot
	when x2 = 84 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 84 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_85: invariant x2 <= 85 timeslot
	when x2 = 85 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 85 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_86: invariant x2 <= 86 timeslot
	when x2 = 86 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 86 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_87: invariant x2 <= 87 timeslot
	when x2 = 87 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 87 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_88: invariant x2 <= 88 timeslot
	when x2 = 88 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 88 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_89: invariant x2 <= 89 timeslot
	when x2 = 89 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 89 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_90: invariant x2 <= 90 timeslot
	when x2 = 90 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 90 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_91: invariant x2 <= 91 timeslot
	when x2 = 91 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 91 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_92: invariant x2 <= 92 timeslot
	when x2 = 92 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 92 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_93: invariant x2 <= 93 timeslot
	when x2 = 93 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 93 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_94: invariant x2 <= 94 timeslot
	when x2 = 94 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 94 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_95: invariant x2 <= 95 timeslot
	when x2 = 95 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 95 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_96: invariant x2 <= 96 timeslot
	when x2 = 96 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 96 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_97: invariant x2 <= 97 timeslot
	when x2 = 97 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 97 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_98: invariant x2 <= 98 timeslot
	when x2 = 98 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 98 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_99: invariant x2 <= 99 timeslot
	when x2 = 99 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 99 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_100: invariant x2 <= 100 timeslot
	when x2 = 100 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 100 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_101: invariant x2 <= 101 timeslot
	when x2 = 101 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 101 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_102: invariant x2 <= 102 timeslot
	when x2 = 102 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 102 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_103: invariant x2 <= 103 timeslot
	when x2 = 103 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 103 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_104: invariant x2 <= 104 timeslot
	when x2 = 104 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 104 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_105: invariant x2 <= 105 timeslot
	when x2 = 105 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 105 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_106: invariant x2 <= 106 timeslot
	when x2 = 106 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 106 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_107: invariant x2 <= 107 timeslot
	when x2 = 107 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 107 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_108: invariant x2 <= 108 timeslot
	when x2 = 108 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 108 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_109: invariant x2 <= 109 timeslot
	when x2 = 109 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 109 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_110: invariant x2 <= 110 timeslot
	when x2 = 110 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 110 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_111: invariant x2 <= 111 timeslot
	when x2 = 111 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 111 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_112: invariant x2 <= 112 timeslot
	when x2 = 112 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 112 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_113: invariant x2 <= 113 timeslot
	when x2 = 113 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 113 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_114: invariant x2 <= 114 timeslot
	when x2 = 114 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 114 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_115: invariant x2 <= 115 timeslot
	when x2 = 115 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 115 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_116: invariant x2 <= 116 timeslot
	when x2 = 116 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 116 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_117: invariant x2 <= 117 timeslot
	when x2 = 117 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 117 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_118: invariant x2 <= 118 timeslot
	when x2 = 118 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 118 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_119: invariant x2 <= 119 timeslot
	when x2 = 119 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 119 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_120: invariant x2 <= 120 timeslot
	when x2 = 120 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 120 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_121: invariant x2 <= 121 timeslot
	when x2 = 121 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 121 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_122: invariant x2 <= 122 timeslot
	when x2 = 122 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 122 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_123: invariant x2 <= 123 timeslot
	when x2 = 123 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 123 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_124: invariant x2 <= 124 timeslot
	when x2 = 124 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 124 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_125: invariant x2 <= 125 timeslot
	when x2 = 125 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 125 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_126: invariant x2 <= 126 timeslot
	when x2 = 126 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 126 timeslot sync send2 do {x2 := 0} goto Transmit2;

loc Wait2_6_127: invariant x2 <= 127 timeslot
	when x2 = 127 timeslot sync busy2 do {x2 := 0} goto Collide2_6;
	when x2 = 127 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
;


(************************************************************)
(* Property specification *)
(************************************************************)

property := unreachable loc[sender1] = Done1 & loc[sender2] = Done2;


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