
omod EXECUTE-REACTION is
  including ABS-EXECUTE-REACTION .

  var REACTOR : ReactorId .
  var TSTATUS : TriggerStatus .
  vars RB RB1 RB2 : ReactionBody .
  var OUTPUTS : Events .
  var QUEUE : EQueue .
  var VALUATION : ReactorState .
  vars ACTIONS INPORTS : Configuration .
  var BEXP : BoolExpr .
  var CONST : BoolValue .

  --- the semantics of if-then-else-fi for the concrete case
  eq executeReactionBody(
        < REACTOR : Reactor | state :  VALUATION,
                              inports : INPORTS, actions : ACTIONS >,
        (if BEXP then RB1 else RB2 fi) ; RB, OUTPUTS, QUEUE, TSTATUS, CONST)
   =                                         
      executeReactionBody(< REACTOR : Reactor | >,
        if eval(BEXP, VALUATION, INPORTS ACTIONS, TSTATUS) == trueVal 
        then (RB1 ; RB) else (RB2 ; RB) fi,  
        OUTPUTS, QUEUE, TSTATUS, CONST) .
endom


omod EXECUTE-STEP is
  including EXECUTE-REACTION .
  including ABS-EXECUTE-STEP .

  vars REACTORID : ReactorId .
  vars PRE INVOKED : ReactionIdSet .
  vars OS TRIGGERIDS : OidSet .
  vars NETWORK GRAPH : Configuration .
  var OBJECT : Object .
  var TSTATUS : TriggerStatus .
  vars REACTIONS1 REACTIONS2 : ReactionList .
  var OUTPUTS : Events .
  vars QUEUE RESULT-QUEUE : EQueue .
  var RB : ReactionBody .
  vars CONST CONST' : BoolValue .
  var N : Nat .

  ceq executeStep(
        < (REACTORID . N) : APGNode | 
            triggers : TSTATUS, status : present, pre : PRE > 
        GRAPH,
        NETWORK
        < REACTORID : Reactor | 
            reactions : REACTIONS1 (reaction N when TRIGGERIDS --> OS do {RB}) REACTIONS2 >,
        QUEUE,
        INVOKED, CONST)
   =
      executeStep(
        < (REACTORID . N) : APGNode | status : executed >
        updateGraph(GRAPH, REACTORID, OS, NETWORK < REACTORID : Reactor | >, OUTPUTS),
        propagateImmediateOutputs(OUTPUTS, NETWORK OBJECT),    --- updated reactor
        scheduleDelayedInputs(OUTPUTS, NETWORK, RESULT-QUEUE),
        INVOKED ; (REACTORID . N), CONST && CONST')
   if presetOK(PRE, GRAPH)   
   /\ allTriggersDecided(TSTATUS)  
   /\ result(OBJECT, OUTPUTS, RESULT-QUEUE, CONST') := 
         executeReaction(< REACTORID : Reactor | reactions : REACTIONS1
                                                 reaction N when TRIGGERIDS --> OS do {RB}
                                                 REACTIONS2 >, N, TSTATUS, QUEUE) .

 *** Comment out for debugging with APG graph:
 ceq executeStep(GRAPH, NETWORK, QUEUE, INVOKED, CONST) 
   = networkQueueRxns(NETWORK, QUEUE, INVOKED, CONST) 
  if CONST == trueVal [owise] . --- for the concrete case, CONST must be true

 --- non-owise version
---(
 ceq executeStep(GRAPH, NETWORK, QUEUE, INVOKED, CONST) 
   = networkQueueRxns(NETWORK, QUEUE, INVOKED, CONST) 
  if noMoreReaction(GRAPH, none)
  /\ CONST == trueVal . --- for the concrete case, CONST must be true
)---
endom
