const
	MININT	:	-32768;
	MAXINT	:	32767;
type
	state	:	enum { no_code_digit,first_code_digit,second_code_digit };
	digit	:	0..9;
var
	PC	:	MININT..MAXINT;
	current_state	:	state;
	output	:	BOOLEAN;
	input	:	MININT..MAXINT;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable output */ 
Ruleset i : BOOLEAN Do
Rule 
PC=0
==>
begin
  output:=i;
  if PC=0 then
    PC:=1
  end;
end;
end;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable input */ 
Ruleset i : MININT..MAXINT Do
Rule 
PC=1
==>
begin
  input:=i;
  if PC=1 then
    PC:=2
  end;
end;
end;

Rule "SAFE_IS_OPENED"
PC=2 & ((current_state=second_code_digit) & (input=3))
==>
begin
  output:=TRUE;
  current_state:=no_code_digit;
end;

Rule "SECOND_ARRIVED_NEXT_SPOILED"
PC=2 & ((current_state=second_code_digit) & (input!=3))
==>
begin
  output:=FALSE;
  current_state:=no_code_digit;
end;

Rule "SECOND_CODE_DIGIT_ARRIVED"
PC=2 & ((current_state=first_code_digit) & (input=0))
==>
begin
  output:=FALSE;
  current_state:=second_code_digit;
end;

Rule "FIRST_ARRIVED_NEXT_SPOILED"
PC=2 & ((current_state=first_code_digit) & (input!=0))
==>
begin
  current_state:=no_code_digit;
  output:=FALSE;
end;

Rule "FIRST_CODE_DIGIT_ARRIVED"
PC=2 & ((input=8) & (current_state=no_code_digit))
==>
begin
  output:=FALSE;
  current_state:=first_code_digit;
end;

Rule "NO_DIGIT_SELF_LOOP"
PC=2 & ((current_state=no_code_digit) & (input!=8))
==>
begin
  current_state:=no_code_digit;
  output:=FALSE;
end;

startstate
begin
  input:=0;
  output:=TRUE;
  current_state:=no_code_digit;
  PC:=0;
end;