
omod DYNAMICS-WITHOUT-TICK is
  including ABS-DYNAMICS-WITHOUT-TICK .
  including EXECUTE-STEP .
  including EVENT-QUEUE .
  including PHYSICAL-ACTIONS .

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

  vars REACTORS-AND-CONNECTIONS PHYSICAL-ACTIONS NEW-NETWORK CONF1 : Configuration .
  vars QUEUE NEW-QUEUE : EQueue .
  vars E Q PA RXNS O : Oid .
  var INVOKED : ReactionIdSet .
  var EVENTS : Events .
  var CONST : BoolValue .
  var TI : TimeInf .
  vars T T1 T2 : Time .
  var N : Nat .
  var REST : Configuration .
  var REACTORID : ReactorId .
  var VAR : VarId .
  var VAL : Value .
  var RS : ReactorState .
  var RID : ReactionId .
  var RIDS : ReactionIdSet .
  vars EQ1 EQ2 : EQueue .
  var EVENT : Event .
  var TAG : Tag .
  
  *** 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.

  *** 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 := minimum(T1, smallestTimer(CONF1))
    /\ T gt zero .
  
  )---

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

  *** 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 gt zero
     /\ 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.
   
  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) .

  *** decrease timers in out physical action objects:
  op decreaseTimers : Configuration Time -> Configuration .
  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 smallestTimer : Configuration -> TimeInf .
  eq smallestTimer(none) = INF .
  eq smallestTimer(< PA : PhysAct | leftOfPeriod : TI >   PHYSICAL-ACTIONS)
   = minimum(TI, smallestTimer(PHYSICAL-ACTIONS)) .
   
  *** Here starts helper functions for analysis
  op _._in_ : ReactorId VarId Configuration -> Value .
  op _inQueue_ : Event Configuration -> Bool .
  op _invoked_ : ReactionId Configuration -> Bool .
   
  eq REACTORID . VAR in REST
      < REACTORID : Reactor | state : (VAR |-> VAL) ; RS > = VAL .
      
  eq EVENT inQueue REST
      < O : EventQueue | queue : (EQ1 :: ((EVENT EVENTS) at TAG) :: EQ2) > = true .
  eq EVENT inQueue REST = false [owise] .    
      
  eq RID invoked REST
      < O : Invoked | reactions : (RID ; RIDS) > = true .
  eq RID invoked REST = false [owise] .
endom



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

omod SIMULATION-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 PHYSICAL-ACTIONS : Configuration .
  vars T1 T : Time .
  vars E Q RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  var QUEUE : EQueue .


  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 := minimum(T1, smallestTimer(CONF1))
   /\ T gt zero .


  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 gt zero
   /\ CONF1 =/= none .      --- implied by typing of T
endom


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

omod UNBOUNDED-ANALYSIS-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 PHYSICAL-ACTIONS : Configuration .
  vars T T1 : Time .
  vars E Q RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  var QUEUE : EQueue .


  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 := minimum(T1, smallestTimer(CONF1))
   /\ T gt zero .


  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 gt zero
   /\ CONF1 =/= none .      --- implied by typing of T

endom



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

omod TIME-BOUNDED-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 PHYSICAL-ACTIONS : Configuration .
  vars T1 T T3 : Time .
  vars E Q RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  var QUEUE : EQueue .

  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 plus T)
   if T := minimum(T1, smallestTimer(CONF1))
   /\ T gt zero
   /\ T3 plus T le 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 plus T)
   if T := smallestTimer(CONF1)
   /\ T gt zero
   /\ CONF1 =/= none       --- implied by typing of T
   /\ T3 plus T le timeBound .
endom


*** Case 4: unbounded and time-bounded analysis.
*** The user must do TWO things:
***    a. for unbounded analysis start with state {...} timeBound INF
***    b. for time-bounded analysis set the value after 'timeBound' to the desired value.

omod UNBOUNDED-AND-BOUNDED-ANALYSIS-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 PHYSICAL-ACTIONS : Configuration .
  vars T T1 : Time .
  var T2 : TimeInf .
  vars E Q RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  var QUEUE : EQueue .

   
  op _timeBound_ : ClockedSystem TimeInf -> ClockedSystem [ctor] .


  crl [tick] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1, N)) :: QUEUE >
      < RXNS : Invoked | >} timeBound T2
   =>
     {< 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 >} timeBound (T2 monus T)
   if T := minimum(T1, smallestTimer(CONF1), T2)
   /\ T gt zero .


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


*** Case 5: unbounded and time-bounded analysis.
*** The user must do TWO things:
***    a. for unbounded analysis start with state {...} timeBound INF
***    b. for time-bounded analysis set the value after 'timeBound' to the desired value.

omod TIMED-SIMULATION-DYNAMICS is
  including DYNAMICS-WITHOUT-TICK .

  vars REACTORS-AND-CONNECTIONS CONF1 PHYSICAL-ACTIONS : Configuration .
  vars T T1 T3 : Time .
  vars TI2 TI : TimeInf .
  vars E Q RXNS : Oid .
  var N : Nat .
  var EVENTS : Events .
  var QUEUE : EQueue .

   
  op _timeBound_ : ClockedSystem TimeInf -> ClockedSystem [ctor] .

  eq {C:Configuration} timeBound TI = {C:Configuration} in time 0 timeBound TI .

  crl [tick] :
     {< E : Environment | physicalActions : CONF1 >
      REACTORS-AND-CONNECTIONS
      < Q : EventQueue | queue : (EVENTS at tag(T1, N)) :: QUEUE >
      < RXNS : Invoked | >} in time T3 timeBound TI2
   =>
     {< 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 + T3) timeBound (TI2 monus T)
   if T := minimum(T1, smallestTimer(CONF1), TI2)
   /\ T gt zero .


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

--- NOTICE: In general, our states are tuples
--- (newState, reactionsInvokedToReachNewState)
--- so we should be aware of the order.  If you want
--- something like "if X == 2" then reaction R should fire
--- cannot be checked by just looking at such a (newState, reactionsFired)
--- pair.  However, a property "if R fires then X == 2 [afterwards]" can be
--- checked by just inspecting such a (newState, reactionsFiredToReachNewState)
--- pair.    The latter properties are the ones appearing in the "Towards verifying ..."
--- paper, as well as in the benchmarks repository.
---    Note 2:  Since we handle all reactions at a given tag in one step,
---  we do not need much of the complexity of the LF formulas and stuff, which
---  use interleaving of all the reactions that take place at the same time.
--- The main property for ADAS example has the for us desired form.
--- Of course, we can also check the former, non-existing, properties, since
--- the pre-state is available in the previous state.
