Module System

type state = [0 .. 7]
local input : bool 
local output : bool 
local current_state : state where current_state = 0


Module COUNTER :


Transition SELF_LOOP NoFairness:
enable input=false
assign output := false

Transition GO_TO_NEXT_STATE NoFairness:
enable ((input=true)/\(current_state!=7))
assign current_state := current_state+1,output := false

Transition OUTPUT_IS_1 NoFairness:
enable ((input=true)/\(current_state=7))
assign current_state := 0,output := true
EndModule


Module SYSTEM :

include COUNTER : ( COUNTER )
EndModule