const
	MININT	:	-32768;
	MAXINT	:	32767;
var
	z	:	BOOLEAN;
	y	:	MININT..MAXINT;
	x	:	MININT..MAXINT;
	shared	:	MININT..MAXINT;
	can_change_shared	:	BOOLEAN;
	can_change_shared_B	:	BOOLEAN;

Rule "ENTER_CRITIC1_EXIT_CRITIC2"
can_change_shared & !can_change_shared_B
==>
begin
  can_change_shared_B:=TRUE;
  shared:=shared + 1;
  can_change_shared:=FALSE;
end;

Rule "EXIT_CRITIC1_ENTER_CRITIC2"
!can_change_shared & can_change_shared_B
==>
begin
  can_change_shared_B:=FALSE;
  shared:=shared - 1;
  can_change_shared:=TRUE;
end;

Rule "NON_CRITIC1"
z
==>
begin
  x:=10;
end;

Rule "NON_CRITIC2"
z
==>
begin
  y:=11;
end;

startstate
begin
  can_change_shared_B:=FALSE;
  can_change_shared:=TRUE;
  shared:=6;
  x:=0;
  y:=0;
  z:=TRUE;
end;