HOLD_PREVIOUS

VAR 
shared: integer INITVAL 6;
 
x: integer INITVAL 0;
 
y: integer INITVAL 0;

z: boolean INITVAL true;



MODULE A() {
	VAR
	can_change_shared: boolean INITVAL true;	

	TRANS NON_CRITIC1:
		enable: z;
		assign: x' := 10;
	
	TRANS ENTER_CRITIC1:
		enable: can_change_shared;
		assign: shared' := shared + 1;
			can_change_shared' := false;

	TRANS EXIT_CRITIC1:
		enable: !can_change_shared;
		assign: can_change_shared' := true;
}

MODULE B() {
	VAR
	can_change_shared: boolean INITVAL false;
	TRANS NON_CRITIC2:
		enable: z;
		assign: y' := 11;
	
	TRANS ENTER_CRITIC2:
		enable: can_change_shared;
		assign: shared' := shared - 1;
			can_change_shared' := false;

	TRANS EXIT_CRITIC2:
		enable: !can_change_shared;
		assign: can_change_shared' := true;
}

MODULE SYSTEM () {
     	(A() |(ENTER_CRITIC1,EXIT_CRITIC2),(EXIT_CRITIC1,ENTER_CRITIC2)| B()) 
	
}