module Generator[StateSpace, EventSet]

-- Usual definition of a generator
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

open Automaton[StateSpace, EventSet, NoEvent]


abstract sig NoEvent { }

fact
{
 no NoEvent
 no SilentEvents
}


abstract sig Generator extends Automaton
{
 events           : set EventSet,
 ctrlEvents       : set EventSet,
 markedStates     : set StateSpace
}
{
 events = labels
 markedStates = finalStates
 ctrlEvents in events
 this.isDeterministic
}


pred lastStepIsCtrl[w: one Walk]
{
 last[w.edges] in w.stg.ctrlEvents
}