HOLD_PREVIOUS

TYPE

state: 0..7;

VAR

input: boolean;
output: boolean;
current_state: state INITVAL 0;



MODULE COUNTER(){
	TRANS SELF_LOOP:
		enable: input = false;
		assign: output' := false;
	
	TRANS GO_TO_NEXT_STATE:
		enable: ((input = true) /\ (current_state != 7));
		assign: current_state' := current_state + 1;
			output' := false;

	TRANS OUTPUT_IS_1:
		enable: ((input = true) /\ (current_state = 7));
		assign: current_state' := 0;
			output' := true;
}

MODULE SYSTEM(){

	COUNTER()
}