The Transitions of The Flattened Core Program:
Transition number 6, original name: SAFE_IS_OPENED
	vars changed by assign: output current_state 
	vars changed by relation: 

Transition number 5, original name: SECOND_ARRIVED_NEXT_SPOILED
	vars changed by assign: output current_state 
	vars changed by relation: 

Transition number 4, original name: SECOND_CODE_DIGIT_ARRIVED
	vars changed by assign: output current_state 
	vars changed by relation: 

Transition number 3, original name: FIRST_ARRIVED_NEXT_SPOILED
	vars changed by assign: current_state output 
	vars changed by relation: 

Transition number 2, original name: FIRST_CODE_DIGIT_ARRIVED
	vars changed by assign: output current_state 
	vars changed by relation: 

Transition number 1, original name: NO_DIGIT_SELF_LOOP
	vars changed by assign: current_state output 
	vars changed by relation: 



New types in core program:
state with definition of enum
digit with definition of Range from 0 to 9

Variable current_state is of type state.

The Variables of the Flattened Program:
Variable name: current_state
	Transitions that change variable by assign: 1 2 3 4 5 6 
	Transitions that change variable by relation: 

Variable name: output
	Transitions that change variable by assign: 1 2 3 4 5 6 
	Transitions that change variable by relation: 

Variable name: input
	Transitions that change variable by assign: 
	Transitions that change variable by relation: