HOLD_PREVIOUS

TYPE

state: ENUM {no_code_digit , first_code_digit , second_code_digit};
digit: 0..9;

VAR

input: integer;
output: boolean;
current_state: state INITVAL no_code_digit;

MODULE SAFE(){

	TRANS NO_DIGIT_SELF_LOOP:

		enable: ((current_state = no_code_digit) /\ (input != 8));
		assign: current_state' := no_code_digit;
			output' := false;
	TRANS FIRST_CODE_DIGIT_ARRIVED:

		enable: ((input = 8) /\ (current_state = no_code_digit));
		assign: output' := false;
			current_state' := first_code_digit;
	TRANS FIRST_ARRIVED_NEXT_SPOILED:

		enable: ((current_state = first_code_digit) /\ (input != 0));
		assign: current_state' := no_code_digit;
			output' := false;
	TRANS SECOND_CODE_DIGIT_ARRIVED:

		enable: ((current_state = first_code_digit) /\ (input = 0));
		assign: output' := false;
			current_state' := second_code_digit;
	TRANS SECOND_ARRIVED_NEXT_SPOILED:

		enable: ((current_state = second_code_digit) /\ (input != 3));
		assign: output' := false;
			current_state' := no_code_digit;
	TRANS SAFE_IS_OPENED: 

		enable: ((current_state = second_code_digit) /\ (input = 3));
		assign: output' := true;
			current_state' := no_code_digit;
}

MODULE SYSTEM(){

	SAFE()
}