Contents

(* 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

Version data entries

4 entries across 4 versions & 1 rubygems

Version	Path
tla-sbuilder-0.3.9	mustache/tla/operator_run.mustache
tla-sbuilder-0.3.8	mustache/tla/operator_run.mustache
tla-sbuilder-0.3.7	mustache/tla/operator_run.mustache
tla-sbuilder-0.3.4	mustache/tla/operator_run.mustache