const
	MININT	:	-32768;
	MAXINT	:	32767;
type
	state	:	enum { idle,entering,critical,exiting };
var
	arr_1	:	array [0..2-1] of state;
	arr	:	array [0..2-1] of state;
	PC	:	MININT..MAXINT;
	semaphore	:	BOOLEAN;
	user_state	:	state;
	user_state_USER	:	state;

/* Ruleset created to simulate non-deterministic assignment to  */ 
Ruleset i : 0..1 Do
Rule 
PC=1 | PC=2
==>
begin
  user_state:=arr [ i ] ;
  if PC=2 then
    PC:=0
  end;
  if PC=1 then
    PC:=0
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to  */ 
Ruleset i : 0..1 Do
Rule 
PC=3 | PC=4
==>
begin
  user_state_USER:=arr_1 [ i ] ;
  if PC=4 then
    PC:=0
  end;
  if PC=3 then
    PC:=0
  end;
end;
end;

Rule "RETURN_TO_IDLE_AND_FREE_SEMAPHORE"
PC=0 & user_state=exiting
==>
begin
  user_state:=idle;
  semaphore:=FALSE;
end;

Rule "NON_DETERMINISTIC_CRITICAL_OR_EXITING"
PC=0 & user_state=critical
==>
begin
  PC:=1;
end;

Rule "ENTERING_BUT_SEMAPHOR_IS_TRUE"
PC=0 & ((user_state=entering) & (semaphore=TRUE))
==>
begin
  user_state:=entering;
end;

Rule "ENTERING_AND_SEMAPHOR_IS_FALSE"
PC=0 & ((user_state=entering) & (semaphore=FALSE))
==>
begin
  user_state:=critical;
  semaphore:=TRUE;
end;

Rule "NON_DETERMINISTIC_IDLE_OR_ENTERING"
PC=0 & user_state=idle
==>
begin
  PC:=2;
end;

Rule "NON_DETERMINISTIC_IDLE_OR_ENTERING_USER"
PC=0 & user_state_USER=idle
==>
begin
  PC:=3;
end;

Rule "ENTERING_AND_SEMAPHOR_IS_FALSE_USER"
PC=0 & ((user_state_USER=entering) & (semaphore=FALSE))
==>
begin
  user_state_USER:=critical;
  semaphore:=TRUE;
end;

Rule "ENTERING_BUT_SEMAPHOR_IS_TRUE_USER"
PC=0 & ((user_state_USER=entering) & (semaphore=TRUE))
==>
begin
  user_state_USER:=entering;
end;

Rule "NON_DETERMINISTIC_CRITICAL_OR_EXITING_USER"
PC=0 & user_state_USER=critical
==>
begin
  PC:=4;
end;

Rule "RETURN_TO_IDLE_AND_FREE_SEMAPHORE_USER"
PC=0 & user_state_USER=exiting
==>
begin
  user_state_USER:=idle;
  semaphore:=FALSE;
end;

startstate
begin
  user_state_USER:=idle;
  user_state:=idle;
  semaphore:=FALSE;
  PC:=0;
  arr[0]:= critical;
  arr[1]:= exiting;
  arr_1[0]:= idle;
  arr_1[1]:= entering;
end;