mtype = { no_code_digit, first_code_digit, second_code_digit };
#define state mtype
#define digit byte

bool Fail = false;
int input;
bool output;
state current_state = no_code_digit;





proctype SAFE() {
do
  ::atomic{
    ((current_state==no_code_digit)&&(input!=8)) ->
    current_state = no_code_digit;
    output = false;
    };
  ::atomic{
    ((input==8)&&(current_state==no_code_digit)) ->
    output = false;
    current_state = first_code_digit;
    };
  ::atomic{
    ((current_state==first_code_digit)&&(input!=0)) ->
    current_state = no_code_digit;
    output = false;
    };
  ::atomic{
    ((current_state==first_code_digit)&&(input==0)) ->
    output = false;
    current_state = second_code_digit;
    };
  ::atomic{
    ((current_state==second_code_digit)&&(input!=3)) ->
    output = false;
    current_state = no_code_digit;
    };
  ::atomic{
    ((current_state==second_code_digit)&&(input==3)) ->
    output = true;
    current_state = no_code_digit;
    };
od;
}

init {

 atomic{
 run SAFE();
 };
}