#######################################
# Fischer's mutual exclusion protocol #
#######################################
#                                     #
# przy setv1, setv2 - duza delta      #
# przy enter1, enter2 - mala delta    #
#                                     #
# wzajemne wykluczanie przy:          #
#                                     #
#   mala delta >= duza delta          #
#                                     #
#######################################

net {
	actions {
		start1;
		setv1;
		enter1;
		setv01;
		
		start2;
		setv2;
		enter2;
		setv02;
		
		start3;
		setv3;
		enter3;
		setv03;

		start4;
		setv4;
		enter4;
		setv04;

		start5;
		setv5;
		enter5;
		setv05;

		start6;
		setv6;
		enter6;
		setv06;

		start7;
		setv7;
		enter7;
		setv07;

		start8;
		setv8;
		enter8;
		setv08;

		start9;
		setv9;
		enter9;
		setv09;

		start10;
		setv10;
		enter10;
		setv010;
	};

	automaton proc1 {
		clocks {
			x1;
		};
		locations {
			idle1 { init; };
			try1;
			wait1;
			crit1;
		};
		trans {
			idle1 -> try1, start1, , { x1; };
			try1 -> wait1, setv1, x1 < 1, { x1; };
			wait1 -> crit1, enter1, x1 > 2, { };
			crit1 -> idle1, setv01, , { };
		};
	};

	automaton proc2 {
		clocks {
			x2;
		};
		locations {
			idle2 { init; };
			try2;
			wait2;
			crit2;
		};
		trans {
			idle2 -> try2, start2, , { x2; };
			try2 -> wait2, setv2, x2 < 1, { x2; };
			wait2 -> crit2, enter2, x2 > 2, { };
			crit2 -> idle2, setv02, , { };
		};
	};
	
	automaton proc3 {
		clocks {
			x3;
		};
		locations {
			idle3 { init; };
			try3;
			wait3;
			crit3;
		};
		trans {
			idle3 -> try3, start3, , { x3; };
			try3 -> wait3, setv3, x3 < 1, { x3; };
			wait3 -> crit3, enter3, x3 > 2, { };
			crit3 -> idle3, setv03, , { };
		};
	};
	
	automaton proc4 {
		clocks {
			x4;
		};
		locations {
			idle4 { init; };
			try4;
			wait4;
			crit4;
		};
		trans {
			idle4 -> try4, start4, , { x4; };
			try4 -> wait4, setv4, x4 < 1, { x4; };
			wait4 -> crit4, enter4, x4 > 2, { };
			crit4 -> idle4, setv04, , { };
		};
	};
	
	automaton proc5 {
		clocks {
			x5;
		};
		locations {
			idle5 { init; };
			try5;
			wait5;
			crit5;
		};
		trans {
			idle5 -> try5, start5, , { x5; };
			try5 -> wait5, setv5, x5 < 1, { x5; };
			wait5 -> crit5, enter5, x5 > 2, { };
			crit5 -> idle5, setv05, , { };
		};
	};
	
	automaton proc6 {
		clocks {
			x6;
		};
		locations {
			idle6 { init; };
			try6;
			wait6;
			crit6;
		};
		trans {
			idle6 -> try6, start6, , { x6; };
			try6 -> wait6, setv6, x6 < 1, { x6; };
			wait6 -> crit6, enter6, x6 > 2, { };
			crit6 -> idle6, setv06, , { };
		};
	};
	
	automaton proc7 {
		clocks {
			x7;
		};
		locations {
			idle7 { init; };
			try7;
			wait7;
			crit7;
		};
		trans {
			idle7 -> try7, start7, , { x7; };
			try7 -> wait7, setv7, x7 < 1, { x7; };
			wait7 -> crit7, enter7, x7 > 2, { };
			crit7 -> idle7, setv07, , { };
		};
	};
	
	automaton proc8 {
		clocks {
			x8;
		};
		locations {
			idle8 { init; };
			try8;
			wait8;
			crit8;
		};
		trans {
			idle8 -> try8, start8, , { x8; };
			try8 -> wait8, setv8, x8 < 1, { x8; };
			wait8 -> crit8, enter8, x8 > 2, { };
			crit8 -> idle8, setv08, , { };
		};
	};
	
	automaton proc9 {
		clocks {
			x9;
		};
		locations {
			idle9 { init; };
			try9;
			wait9;
			crit9;
		};
		trans {
			idle9 -> try9, start9, , { x9; };
			try9 -> wait9, setv9, x9 < 1, { x9; };
			wait9 -> crit9, enter9, x9 > 2, { };
			crit9 -> idle9, setv09, , { };
		};
	};
	
	automaton proc10 {
		clocks {
			x10;
		};
		locations {
			idle10 { init; };
			try10;
			wait10;
			crit10;
		};
		trans {
			idle10 -> try10, start10, , { x10; };
			try10 -> wait10, setv10, x10 < 1, { x10; };
			wait10 -> crit10, enter10, x10 > 2, { };
			crit10 -> idle10, setv010, , { };
		};
	};
	
	automaton varV {
		locations {
			v0 { init; };
			v1;
			v2;
			v3;
			v4;
			v5;
			v6;
			v7;
			v8;
			v9;
			v10;
		};
		trans {
			v0 -> v0, start1, , { };
			v0 -> v0, start2, , { };
			v0 -> v0, start3, , { };
			v0 -> v0, start4, , { };
			v0 -> v0, start5, , { };
			v0 -> v0, start6, , { };
			v0 -> v0, start7, , { };						
			v0 -> v0, start8, , { };
			v0 -> v0, start9, , { };
			v0 -> v0, start10, , { };
			v0 -> v1, setv1, , { };
			v0 -> v2, setv2, , { };
			v0 -> v3, setv3, , { };
			v0 -> v4, setv4, , { };
			v0 -> v5, setv5, , { };
			v0 -> v6, setv6, , { };
			v0 -> v7, setv7, , { };
			v0 -> v8, setv8, , { };
			v0 -> v9, setv9, , { };
			v0 -> v10, setv10, , { };
			
			v1 -> v0, setv01, , { };
			v1 -> v1, enter1, , { };
			v1 -> v1, setv1, , { };
			v1 -> v2, setv2, , { };
			v1 -> v3, setv3, , { };
			v1 -> v4, setv4, , { };
			v1 -> v5, setv5, , { };
			v1 -> v6, setv6, , { };
			v1 -> v7, setv7, , { };
			v1 -> v8, setv8, , { };
			v1 -> v9, setv9, , { };
			v1 -> v10, setv10, , { };
			
			v2 -> v0, setv02, , { };
			v2 -> v1, enter2, , { };
			v2 -> v1, setv1, , { };
			v2 -> v2, setv2, , { };
			v2 -> v3, setv3, , { };
			v2 -> v4, setv4, , { };
			v2 -> v5, setv5, , { };
			v2 -> v6, setv6, , { };
			v2 -> v7, setv7, , { };
			v2 -> v8, setv8, , { };
			v2 -> v9, setv9, , { };
			v2 -> v10, setv10, , { };
		
			v3 -> v0, setv03, , { };
			v3 -> v1, enter3, , { };
			v3 -> v1, setv1, , { };
			v3 -> v2, setv2, , { };
			v3 -> v3, setv3, , { };
			v3 -> v4, setv4, , { };
			v3 -> v5, setv5, , { };
			v3 -> v6, setv6, , { };
			v3 -> v7, setv7, , { };
			v3 -> v8, setv8, , { };
			v3 -> v9, setv9, , { };
			v3 -> v10, setv10, , { };
		
			v4 -> v0, setv04, , { };
			v4 -> v1, enter4, , { };
			v4 -> v1, setv1, , { };
			v4 -> v2, setv2, , { };
			v4 -> v3, setv3, , { };
			v4 -> v4, setv4, , { };
			v4 -> v5, setv5, , { };
			v4 -> v6, setv6, , { };
			v4 -> v7, setv7, , { };
			v4 -> v8, setv8, , { };
			v4 -> v9, setv9, , { };
			v4 -> v10, setv10, , { };
			
			v5 -> v0, setv05, , { };
			v5 -> v1, enter5, , { };
			v5 -> v1, setv1, , { };
			v5 -> v2, setv2, , { };
			v5 -> v3, setv3, , { };
			v5 -> v4, setv4, , { };
			v5 -> v5, setv5, , { };
			v5 -> v6, setv6, , { };
			v5 -> v7, setv7, , { };
			v5 -> v8, setv8, , { };
			v5 -> v9, setv9, , { };
			v5 -> v10, setv10, , { };
			
			v6 -> v0, setv06, , { };
			v6 -> v1, enter6, , { };
			v6 -> v1, setv1, , { };
			v6 -> v2, setv2, , { };
			v6 -> v3, setv3, , { };
			v6 -> v4, setv4, , { };
			v6 -> v5, setv5, , { };
			v6 -> v6, setv6, , { };
			v6 -> v7, setv7, , { };
			v6 -> v8, setv8, , { };
			v6 -> v9, setv9, , { };
			v6 -> v10, setv10, , { };
			
			v7 -> v0, setv07, , { };
			v7 -> v1, enter7, , { };
			v7 -> v1, setv1, , { };
			v7 -> v2, setv2, , { };
			v7 -> v3, setv3, , { };
			v7 -> v4, setv4, , { };
			v7 -> v5, setv5, , { };
			v7 -> v6, setv6, , { };
			v7 -> v7, setv7, , { };
			v7 -> v8, setv8, , { };
			v7 -> v9, setv9, , { };
			v7 -> v10, setv10, , { };
			
			v8 -> v0, setv08, , { };
			v8 -> v1, enter8, , { };
			v8 -> v1, setv1, , { };
			v8 -> v2, setv2, , { };
			v8 -> v3, setv3, , { };
			v8 -> v4, setv4, , { };
			v8 -> v5, setv5, , { };
			v8 -> v6, setv6, , { };
			v8 -> v7, setv7, , { };
			v8 -> v8, setv8, , { };
			v8 -> v9, setv9, , { };
			v8 -> v10, setv10, , { };
			
			v9 -> v0, setv09, , { };
			v9 -> v1, enter9, , { };
			v9 -> v1, setv1, , { };
			v9 -> v2, setv2, , { };
			v9 -> v3, setv3, , { };
			v9 -> v4, setv4, , { };
			v9 -> v5, setv5, , { };
			v9 -> v6, setv6, , { };
			v9 -> v7, setv7, , { };
			v9 -> v8, setv8, , { };
			v9 -> v9, setv9, , { };
			v9 -> v10, setv10, , { };
			
			v10 -> v0, setv010, , { };
			v10 -> v1, enter10, , { };
			v10 -> v1, setv1, , { };
			v10 -> v2, setv2, , { };
			v10 -> v3, setv3, , { };
			v10 -> v4, setv4, , { };
			v10 -> v5, setv5, , { };
			v10 -> v6, setv6, , { };
			v10 -> v7, setv7, , { };
			v10 -> v8, setv8, , { };
			v10 -> v9, setv9, , { };
			v10 -> v10, setv10, , { };
			
		};
	};

};