(* schedule operators  *)

\* Notice:  cardinality of +steps+ sequence elements is 1, change in future?
ProcessStep( stepdefs ) ==  (CHOOSE s \in Head( stepdefs ): TRUE )
ProcessRunning( stepdefs ) ==  ProcessStep( stepdefs ).process
ProcessEnabled( stepdefs, s ) == Len( stepdefs ) # 0 /\ s =  ProcessRunning( stepdefs )
ProcessesToRun( stepdefs ) == Tail( stepdefs )
ProcessParameter( stepdefs ) == ProcessStep( stepdefs )

TickNext( t )   == t + 1                \* advance time (when process start)
InTransaction   == FALSE                \* TRUE when application service running, FALSE when not