Module System

type state = {no_code_digit,first_code_digit,second_code_digit}
type digit = [0 .. 9]
local input : int 
local output : bool 
local current_state : state where current_state = no_code_digit


Module SAFE :


Transition NO_DIGIT_SELF_LOOP NoFairness:
enable ((current_state=no_code_digit)/\(input!=8))
assign current_state := no_code_digit,output := false

Transition FIRST_CODE_DIGIT_ARRIVED NoFairness:
enable ((input=8)/\(current_state=no_code_digit))
assign output := false,current_state := first_code_digit

Transition FIRST_ARRIVED_NEXT_SPOILED NoFairness:
enable ((current_state=first_code_digit)/\(input!=0))
assign current_state := no_code_digit,output := false

Transition SECOND_CODE_DIGIT_ARRIVED NoFairness:
enable ((current_state=first_code_digit)/\(input=0))
assign output := false,current_state := second_code_digit

Transition SECOND_ARRIVED_NEXT_SPOILED NoFairness:
enable ((current_state=second_code_digit)/\(input!=3))
assign output := false,current_state := no_code_digit

Transition SAFE_IS_OPENED NoFairness:
enable ((current_state=second_code_digit)/\(input=3))
assign output := true,current_state := no_code_digit
EndModule


Module SYSTEM :

include SAFE : ( SAFE )
EndModule