Idf_intf.DSM_SIGRepresentation of a symbolically decomposible (potentially infinite) state machine
module State_machine : SM_SIGState machine to decompose
module Template :
TPL_SIG
with type c = State_machine.event
with type state = State_machine.stateSymbolic template of events