--- Feb 2025 version of overall interpreter. Adds the set of reactions
--- performed in the "last" step.

in executeStep.maude

(tomod DYNAMICS-WITHOUT-TICK is
  including EXECUTE-STEP .
  including TIMED-PRELUDE .

  subsort Configuration < System .

  --- At the moment, the global state is
  --- < env : Environment | physicalActions : ... >
  --- REACTORS and CONNECTIONS in some state
  --- < q : EventQueue | queue : ... >


  vars REACTORS-AND-CONNECTIONS CONF1 CONF
       PHYSICAL-ACTIONS NEW-NETWORK TIMERS : Configuration .
  var TI : TimeInf .
  vars T1 T T2 : Time .
  vars E Q PA RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  vars QUEUE NEW-QUEUE : EQueue .
  var NZN : NzNat .
  var REACTORID : ReactorId .
  var TIMERID : TimerId .
  var VAL : Value .
  var ACTIONID : ActionId .
  var INVOKED : ReactionIdSet .

  *** We need some initialization, obviously.  DONE


  *** We have some freedom here; IF an event can happen
  *** at the same time when a physical action could happen, we always
  *** make the physical action happen first.
  ---  In reality physical actions and events probably
  ---  will never happen at the same time.


*** NEW Feb'25:
--- We add a new object keeping track of the reactions that were performed
--- in the last step.

  class Invoked | reactions : ReactionIdSet .



 
*** We comment out the following "standard" tick rule, since the user
*** can select below the appropriate tick rule for her analysis purposes
*** by including different modules.
*** Those transformations were previously implemented in the Real-Time Maude
*** tool, which we do not use at the moment.
---(

 crl [tick] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1, N)) :: QUEUE >}
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1 monus T, N))
                                 :: decreaseTags(QUEUE, T) >}
     in time T
     if T := min(T1, smallestTimer(CONF1))
        /\ T > 0 .

)---

  op decreaseTimers : Configuration Time -> Configuration .
  *** decrease timers in out physical action objects:

  eq decreaseTimers(none, T) = none .
  eq decreaseTimers(< PA : PhysAct | leftOfPeriod : TI >   PHYSICAL-ACTIONS, T)
  = < PA : PhysAct | leftOfPeriod : TI monus T >   decreaseTimers(PHYSICAL-ACTIONS, T) .


  op decreaseTags : EQueue Time -> EQueue .
  eq decreaseTags(empty, T) = empty .
  eq decreaseTags((EVENTS at tag(T2, N)) :: QUEUE, T) =
     (EVENTS at tag(T2 monus T, N)) :: decreaseTags(QUEUE, T) .

  op smallestTimer : Configuration -> TimeInf .
  eq smallestTimer(none) = INF .
  eq smallestTimer(< PA : PhysAct | leftOfPeriod : TI >   PHYSICAL-ACTIONS)
   = min(TI, smallestTimer(PHYSICAL-ACTIONS)) .


***(    New version: we remove the tickMicro rule ...
 crl [tickMicro] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(0, NZN)) :: QUEUE >}
     =>
     {< E : Environment | >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(0, 0)) :: QUEUE >} 
     if smallestTimer(CONF1) > 0 .
   --- condition ensures no mess/nondet between generating
   --- physical actions and reducing????
   --- CORRECT????
)***



  crl [step] :
      {< E : Environment | physicalActions : CONF1 >
       REACTORS-AND-CONNECTIONS
       < Q : EventQueue | queue : (EVENTS at tag(0, N)) :: QUEUE >
       < RXNS : Invoked | >} 
    =>
      {< E : Environment | physicalActions : CONF1 >
       NEW-NETWORK
       < Q : EventQueue | queue : NEW-QUEUE >
       < RXNS : Invoked | reactions : INVOKED >} 
     --- NOTE: this could also generate future events that need to be inserted
     ---        into the event queue
   if   smallestTimer(CONF1) > 0
      /\ networkQueueRxns(NEW-NETWORK, NEW-QUEUE, INVOKED) :=
            executeStep(EVENTS, REACTORS-AND-CONNECTIONS, QUEUE) .

   *** Note: condition ensures that physical actions are generated
   ***       before events are processed.


   *** This ends "standard" Lingua Franca interpreter.
   ***    However, we also add the new infrastructure/way of
   ***    treating physical actions.  The "environment" could generate
   ***    new events in the future even when the event queue is empty.
   ***  Therefore, we need an additional tick rule for this case:
   ***   Same thing here as with the main tick rule; for different purposes,
   ***   different modules below should be included. Thereofre commented out.
---(
    crl [extraTickRuleForPhysActs] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >}
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >}
     in time T
     if T := smallestTimer(CONF1)
        /\ T > 0
	/\ CONF1 =/= none .      --- implied by typing of T
)---	
*** Note: this rule should not apply when we do not have
***    physical actions, since T cannot have the value INF.
***    So the last conjunct in condition not really needed.


  --- add initial timer values to event queue:
  op addInitialTimers : Configuration EQueue -> EQueue .

  eq addInitialTimers(< REACTORID : Reactor | timers : TIMERS
                                                       < TIMERID : Timer | offset : T > >
		      REACTORS-AND-CONNECTIONS, QUEUE)
   = addInitialTimers(< REACTORID : Reactor | timers : TIMERS >
		      REACTORS-AND-CONNECTIONS,
		      schedule(event(REACTORID, TIMERID, [0]), T, QUEUE)) .

  eq addInitialTimers(REACTORS-AND-CONNECTIONS, QUEUE) = QUEUE [owise] .




  op addStartup : ActionId Configuration EQueue -> EQueue .
  --- addStartup(startup, init, empty)

  eq addStartup(ACTIONID, < REACTORID : Reactor | actions : CONF
                                                  < ACTIONID : LogicalAction |
						       payload : VAL > >
                REACTORS-AND-CONNECTIONS, QUEUE)
   = addStartup(ACTIONID, < REACTORID : Reactor | actions : CONF >
            REACTORS-AND-CONNECTIONS, schedule(event(REACTORID, ACTIONID, VAL), 0, QUEUE)) .

  eq addStartup(ACTIONID, REACTORS-AND-CONNECTIONS, QUEUE) = QUEUE [owise] .
endtom)



*** We now add the tick rule, which is slightly different for three cases:
---  1. Basic Real-Time Maude model and semantics of LF, with "standard"
---     tick rule, perfect for, e.g., simulation purposes.
---  2. A tick rule for unbounded model checking analysis; this uses
---     the same tick rule, except that we do not carry the global
---     clock in the state. We just remove the "in time T" part of
---     the tick rule.
---  3. Time-bounded analysis: we must modify the tick rule so that
---     time does not advance beyond the bound.

*** For each of these choices, select the appropriate of the below modules:


*** Case 1: standard tick rule for simulation:

(tomod SIMULATION-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 CONF
       PHYSICAL-ACTIONS NEW-NETWORK TIMERS : Configuration .
  var TI : TimeInf .
  vars T1 T T2 : Time .
  vars E Q PA RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  vars QUEUE NEW-QUEUE : EQueue .
  var NZN : NzNat .
  var REACTORID : ReactorId .
  var TIMERID : TimerId .
  var VAL : Value .
  var ACTIONID : ActionId .



   crl [tick] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1, N)) :: QUEUE >
      < RXNS : Invoked | >}
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1 monus T, N))
                                 :: decreaseTags(QUEUE, T) >
      < RXNS : Invoked | reactions : none >}
     in time T
     if T := min(T1, smallestTimer(CONF1))
        /\ T > 0 .



    crl [extraTickRuleForPhysActs] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >
      < RXNS : Invoked | >}
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >
      < RXNS : Invoked | reactions : none >}
     in time T
     if T := smallestTimer(CONF1)
        /\ T > 0
	/\ CONF1 =/= none .      --- implied by typing of T
endtom)


*** Case 2: for unbounded and unclocked analyses:

(tomod UNBOUNDED-ANALYSIS-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 CONF
       PHYSICAL-ACTIONS NEW-NETWORK TIMERS : Configuration .
  var TI : TimeInf .
  vars T1 T T2 : Time .
  vars E Q PA RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  vars QUEUE NEW-QUEUE : EQueue .
  var NZN : NzNat .
  var REACTORID : ReactorId .
  var TIMERID : TimerId .
  var VAL : Value .
  var ACTIONID : ActionId .



   crl [tick] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1, N)) :: QUEUE >
      < RXNS : Invoked | >}
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1 monus T, N))
                                 :: decreaseTags(QUEUE, T) >
      < RXNS : Invoked | reactions : none >}
     if T := min(T1, smallestTimer(CONF1))
        /\ T > 0 .



    crl [extraTickRuleForPhysActs] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >
      < RXNS : Invoked | >}
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >
      < RXNS : Invoked | reactions : none >}
     if T := smallestTimer(CONF1)
        /\ T > 0
	/\ CONF1 =/= none .      --- implied by typing of T
endtom)



*** Case 3: time-bounded analysis.
*** The user must do TWO things:
***    a. start with state {...} in time 0
***    b. set the value of the constant 'timeBound' to the desired value.

(tomod TIME-BOUNDED-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 CONF
       PHYSICAL-ACTIONS NEW-NETWORK TIMERS : Configuration .
  var TI : TimeInf .
  vars T1 T T2 T3 : Time .
  vars E Q PA RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  vars QUEUE NEW-QUEUE : EQueue .
  var NZN : NzNat .
  var REACTORID : ReactorId .
  var TIMERID : TimerId .
  var VAL : Value .
  var ACTIONID : ActionId .


  op timeBound : -> Time .   *** initialized by user

   crl [tick] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1, N)) :: QUEUE >
      < RXNS : Invoked | >} in time T3
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1 monus T, N))
                                 :: decreaseTags(QUEUE, T) >
      < RXNS : Invoked | reactions : none >}
     in time (T3 + T)
     if T := min(T1, smallestTimer(CONF1))
        /\ T > 0
	/\ T3 + T <= timeBound .



    crl [extraTickRuleForPhysActs] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >
      < RXNS : Invoked | >} in time T3 
     =>
     {< E : Environment | physicalActions : decreaseTimers(CONF1, T) >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : empty >
      < RXNS : Invoked | reactions : none >}
     in time (T3 + T)
     if T := smallestTimer(CONF1)
        /\ T > 0
	/\ CONF1 =/= none       --- implied by typing of T
	/\ T3 + T <= timeBound .
endtom)
