const
	MININT	:	-32768;
	MAXINT	:	32767;
type
	T#SYSTEM#state	:	enum { ready,busy };
var
	fail_1_1	:	BOOLEAN;
	fail_1	:	BOOLEAN;
	fail	:	BOOLEAN;
	PC	:	MININT..MAXINT;
	__init	:	BOOLEAN;
	request	:	BOOLEAN;
	state	:	T#SYSTEM#state;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable request */ 
Ruleset i : BOOLEAN Do
Rule 
PC=0 | PC=4 | PC=8 | PC=12
==>
begin
  request:=i;
  if PC=12 then
    PC:=13
  end;
  if PC=8 then
    PC:=9
  end;
  if PC=4 then
    PC:=5
  end;
  if PC=0 then
    PC:=1
  end;
end;
end;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable state */ 
Ruleset i : T#SYSTEM#state Do
Rule 
PC=1 | PC=3 | PC=7 | PC=11
==>
begin
  state:=i;
  if PC=11 then
    PC:=12
  end;
  if PC=7 then
    PC:=8
  end;
  if PC=3 then
    PC:=4
  end;
  if PC=1 then
    PC:=2
  end;
end;
end;

/* Ruleset created to simulate non-deterministic assignment to __init that is to take place since HOLD_PREVIOUS is not used in core program */ 
Ruleset i : BOOLEAN Do
Rule 
PC=5 | PC=9 | PC=13
==>
begin
  __init:=i;
  if PC=13 then
    PC:=14
  end;
  if PC=9 then
    PC:=10
  end;
  if PC=5 then
    PC:=6
  end;
end;
end;

/* Rule created during translating relation */ 
Rule 
PC=14 & !((state=ready) & !__init) & !fail_1_1
==>
begin
  fail_1_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=14 & ((state=ready) & !__init) & !fail_1_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=10 & !(state=busy) & !fail_1
==>
begin
  fail_1:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=10 & (state=busy) & !fail_1
==>
begin
  PC:=2;
end;

/* Rule created during translating relation */ 
Rule 
PC=6 & !(state=ready | state=busy) & !fail
==>
begin
  fail:=TRUE;
end;

/* Rule created during translating relation */ 
Rule 
PC=6 & (state=ready | state=busy) & !fail
==>
begin
  PC:=2;
end;

Rule "T_state_2"
PC=2 & !__init & !(state=ready & request)
==>
begin
end;

Rule "T_state_1"
PC=2 & !__init & (state=ready & request)
==>
begin
end;

Rule "T_state_0"
PC=2 & __init
==>
begin
end;

startstate
begin
  state:=ready;
  request:=TRUE;
  __init:=TRUE;
  PC:=0;
  fail:=FALSE;
  fail_1:=FALSE;
  fail_1_1:=FALSE;
end;