*** This treats ADAS as is, WITH multiple triggers for the ADAS-controller.
*** We can now handle this case.

*** This is a version to run on Lepri's Maude 2.7 TCTL model checker for
***     good old Real-Time Maude ...

*** Now WITH action predicates, Feb 2025.

*** Note that, as is, ADAS is an infinite-state system, since the frame variable
***  increase beyond any bound. We therefore change it to rest frame when it reaches 10.
*** Furthermore, the ADAS processor couldn't care less about these values ...

--- in rtm-tctl.maude

in dynamics

--- load REAL-TIME-MAUDE


(tomod ADAS-WITH-CAMERA is 
 including RUNTIME-APG .

 ops frame received brakesApplied requestStop counter1 counter2 counter3 : -> IVarId [ctor] .
 ops lidar camera adasProcessor dashboard pedal brakes : -> ReactorId [ctor] .
 op t : -> TimerId [ctor] .
 ops in in1 in2 out out1 out2 inAdas inPedal : -> IPortId [ctor] .
 op a : -> IActionId .
 op init : -> Configuration .
 
 eq init = 
    < lidar : Reactor | 
      inports : none,
      outports : < out : Port | value : [0] >, 
      state : (frame |-> [0]),
      timers : < t : Timer | offset : 0, period : 34 >, --- 0 and 34 originally
          --- change above values to 11 and 17 for error number 3 in p19
      actions : none,
      reactions : 
      reaction when t --> out do { if (frame === [10]) then (frame := [1]) else (frame := frame + [1]) fi ;
                                   (out <- frame)} >

   < camera : Reactor | 
      inports : none,
      outports : < out : Port | value : [0] >, 
      state : frame |-> [0],
      timers : < t : Timer | offset : 0, period : 17 >,	
      actions : none,
      reactions : 
      reaction when t --> out do { if (frame === [10]) then (frame := [1]) else (frame := frame + [1]) fi
                                  ; (out <- frame) } >


    < adasProcessor : Reactor | 
      inports : < in1 : Port | value : [0] >   < in2 : Port | value : [0] >,
      outports : < out1 : Port | value : [0] >
                 < out2 : Port | value : [0] >, 
      state : requestStop |-> [0],
      timers : none,
      actions : < a : LogicalAction | minDelay : 50, --- change to 51 for error 4
                               minSpacing : 0, 
                               policy : defer, 
                               payload : [0] >,
      reactions : 
         (reaction when (in1 ; in2) --> a do
	    { (requestStop := [1]) ;  schedule(a, [0], [0]) } )
         reaction when a --> out1 ; out2 do { 
          if requestStop === [1] then
              (out1 <- [1]) fi     *** CORRECT!
*** ERROR     (out2 <- [1])     --- ERROR CASE 1, page 19
         }
    >

    < dashboard : Reactor | 
        inports : < in : Port | value : [0] >,
        outports : none,
        state : received |-> [0],
        timers : none,
        actions : none,
        reactions : reaction when in do { received := in }       
    >
    
    < pedal : Reactor |
      inports : none,
      outports : < out : Port | value : [0] >,
      timers : none, 
      state : empty,
      actions : < a : PhysicalAction | 
                               minDelay : 0, 
                               minSpacing : 0, 
                               policy : defer, 
                               payload : [0] >,
      reactions : reaction when a --> out do { out <- [1] }
    >

    < brakes : Reactor |
      inports : < inAdas : Port | value : [0] > 
                < inPedal : Port | value : [0] >,
      outports : none,
      timers : none,
      actions : none,
      state : (brakesApplied |-> [0]),
      reactions : (reaction when inAdas do { (brakesApplied := inAdas)})
                  (reaction when inPedal do { (brakesApplied := inPedal) })

    >

    (camera : out --> adasProcessor : in2)
    (lidar : out --> adasProcessor : in1)     *** CORRECT; comment out line for
                                              ***   error 2 on p19
    (adasProcessor : out1 -- 5 --> brakes : inAdas)  --- change to 6 error 5
    (adasProcessor : out2 --> dashboard : in)
    pedal : out --> brakes : inPedal .
endtom)



(tomod TEST-ADAS is
  including ADAS-WITH-CAMERA .
  including DYNAMICS-WITHOUT-TICK .
  including SIMULATION-DYNAMICS .

  ops env queue rxns : -> Oid [ctor] .

  op initSystem : -> GlobalSystem .
  eq initSystem =
     { < env : Environment |
           physicalActions : < (pedal . a) : PhysAct |
                                   leftOfPeriod : 5,
                                   period : 5,
                                   possibleValues : [69] : [71],
                                   timeNonDet : true > >
       addReactionIndices(init)
       < queue : EventQueue | queue : addInitialTimers(init, empty) >
       < rxns : Invoked | reactions : none >} .
endtom)



(tomod TCTL-CHECK-ADAS is
   including TEST-ADAS .
   including TCTL-MODEL-CHECKER  .

   ops brakeApplied stopRequested pedalPressed : -> Prop [ctor] .

   var REST : Configuration .  var N : Nat .  vars EQ1 EQ2 : EQueue .  var EVENTS : Events .
   var TAG : Tag .
   var RID : ReactionId .
   var RIDS : ReactionIdSet .
   var T : Time .
   var O : Oid .
   

   eq {REST <  brakes : Reactor | state : (brakesApplied |-> [ N ]) >} |= brakeApplied = (N == 1) .

   eq {REST <  adasProcessor : Reactor | state : (requestStop |-> [ N ]) >} |= stopRequested = (N == 1) .

   eq {REST  < queue : EventQueue | queue : (EQ1 :: ((event(pedal, a, [ N ]) EVENTS) at TAG) :: EQ2) >}
       |=  pedalPressed = true .

   eq {REST  < queue : EventQueue | queue : EQ2 >}
       |=  pedalPressed = false [owise] .
   

  --- NEW Feb25: a reaction is/was invoken in this/last step:
  op reaction_invoked : ReactionId -> Prop [ctor] .

  eq {REST
      < O : Invoked | reactions : (RID ; RIDS) >}
     |=  reaction RID invoked = true .

  eq {REST}
     |=  reaction RID invoked = false [owise] .



  eq {REST
      < O : Invoked | reactions : (RID ; RIDS) >}  in time T
     |=  reaction RID invoked = true .

  eq {REST}  in time T
     |=  reaction RID invoked = false [owise] .

  op stopRequestedAndLidarInvoked : -> Prop [ctor] .
  eq {REST <  adasProcessor : Reactor | state : (requestStop |-> [ 1 ]) >
           < rxns : Invoked | reactions : ((lidar . 1) ; RIDS) >} |= stopRequestedAndLidarInvoked = true .

  eq {REST} |= stopRequestedAndLidarInvoked = false [owise] .


endtom)



(set tick det .)

(trew initSystem in time < 178 .)

(tsearch [1] initSystem  =>* {REST:Configuration
                < brakes : Reactor | state : (brakesApplied |-> [1]) ; RS:ReactorState,
		                     AS:AttributeSet >} in time <= 10 .)

(tsearch [1] initSystem  =>* {REST:Configuration
                < queue : EventQueue | queue : (EQ1 ::
		((event(pedal, a, [ N ]) EVENTS) at TAG) :: EQ2) >} in time <= 10 .)





--- we will always apply the brakes within time 55:
--- (mc-tctl initSystem |= AF[<= than 55] brakeApplied .)


***(   in  12 seconds ...
Check
mc-tctl_|=_. initSystem |= AF[<= than 55] brakeApplied .
in TCTL-CHECK-ADAS with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E not brakeApplied U[o 55,INF o] tt) .

Property satisfied
)***




--- When requestStop is 1 then within time 55 the brakeApplied


(mc-tctl initSystem |= AG[<= than 10] (stopRequested implies (AF[<= than 55] brakeApplied)) .)

***(  Output:
rewrites: 1544021 in 13496ms cpu (13718ms real) (114399 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG (stopRequested implies AF[<= than 55] brakeApplied) .
in TCTL-CHECK-ADAS with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,INF o] stopRequested and (E not brakeApplied U[o 55,INF o] tt)) .

Property satisfied
)***

*** Property not satisfied for bound 54 ...


*** What we are really interested in in this nondeterministic model is
***   that each time the driver presses the pedal, within time 0, the brakes will
***   apply.

--- In our interpreter, when a physical action happens, the even is entered into
---    the event queue with delay 0.

--- (mc-tctl initSystem |=   AG  (pedalPressed implies AF[<= than 0] brakeApplied) .)


***(   Result:

rewrites: 1538850 in 13938ms cpu (14090ms real) (110403 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG (pedalPressed implies AF[<= than 0] brakeApplied) .
in TCTL-CHECK-ADAS with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,INF o] pedalPressed and (E not brakeApplied U[o 0,INF o] tt)) .

Property satisfied
)***



*** New commands Feb 2025, with 'mixed' dataflow + state-based properties!

---(mc-tctl initSystem |= AG ((reaction (lidar . 1) invoked) implies (AF[<= than 55] brakeApplied)) .)

***(   Result:
rewrites: 1809832 in 14648ms cpu (14787ms real) (123554 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG (reaction lidar . 1 invoked implies AF[<= than 55] brakeApplied) .
in TCTL-CHECK-ADAS with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,INF o] reaction lidar . 1 invoked and (E not brakeApplied U[o 55,INF o]
    tt)) .

Property satisfied
)***

--- (mc-tctl initSystem |= AG[<= than 10] ((reaction (lidar . 1) invoked) implies (AF[<= than 54] brakeApplied)) .)

***(   Result:
rewrites: 1816041 in 14422ms cpu (14528ms real) (125914 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG[<= than 10] (reaction lidar . 1 invoked implies AF[<= than 55] brakeApplied) .
in TCTL-CHECK-ADAS with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,10 c] reaction lidar . 1 invoked and (E not brakeApplied U[o 55,INF o] tt))
    .

Property satisfied
)***


(mc-tctl initSystem |= AG[<= than 10] (stopRequestedAndLidarInvoked
                                       implies (AF[<= than 55] brakeApplied)) .)

***(   Result:
rewrites: 1815558 in 14688ms cpu (14754ms real) (123602 rewrites/second)

Check
mc-tctl_|=_. initSystem |= AG[<= than 10] (stopRequestedAndLidarInvoked implies AF[<= than 55] brakeApplied) .
in TCTL-CHECK-ADAS with mode deterministic time increase


Checking equivalent property:
mc-tctl_|=_. initSystem |= not (E tt U[c 0,10 c] stopRequestedAndLidarInvoked and (E not brakeApplied U[o 55,INF o]
    tt)) .

Property satisfied
)***
--- Property NOT satisfied for bound 54



***( Two things worth remarking:
1. Because of Lin et al have an event-based semantics, they must have a much trickier timed temporal
   logic formula to formalize the simple thing that
   "when the LIDAR reaction invokes and the ADAS processor requests stop at the same tag, ..."
   In our case, of course all the reactions at the same tag are performed in the same step,
   and therefore we can just look at single states and can therefore define this desired
   coincidence in a very simple way:

  op stopRequestedAndLidarInvoked : -> Prop [ctor] .
  eq {REST <  adasProcessor : Reactor | state : (requestStop |-> [ 1 ]) >
           < rxns : Invoked | reactions : ((lidar . 1) ; RIDS) >} |= stopRequestedAndLidarInvoked = true .

  eq {REST} |= stopRequestedAndLidarInvoked = false [owise] .

2. The TCTL model checker seems to have some porblems in some formulas.  For examples, above,
(mc-tctl initSystem |= AG[<= than 10] ((stopRequested and (reaction (lidar . 1) invoked))
                                       implies (AF[<= than 55] brakeApplied)) .)

does not work.   We are currently debugging the TCTL model checker,
which works for most formulas.
The answer, when we get one, is correct, but some times, there is no answer,
and no answer quickly.
)***


--- NOTICE: In general, our states are tuples
--- (newState, reactionInvokedToReachNewState)
--- 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.
