*** Second attempt: to avoid too much mess in the first step,
***   we only assume that each reaction is triggered by one port/action/timer

***  It is conceptually trivial to consider the case with
***    multiple input ports, but adds lots of cases, and will
***    treated in the near future.

*** First attempt; Luxembourg meeting

in lf-representation

omod ADAS-WITHOUT-CAMERA is 
 including LF-REPR .

 ops frame received brakesApplied requestStop counter1 counter2 counter3 : -> IVarId [ctor] .
 ops lidar 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]) ; (counter1 |-> [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 { (frame := frame + [1]) ;
                                   (out <- frame) ; (counter1 := counter1 + [1])} >

    < adasProcessor : Reactor | 
      inports : < in1 : 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 --> a do
	    { (requestStop := [1]) ;  schedule(a, [0], [0]) } )
         reaction when a --> out1 ; out2 do { 
          if requestStop === [1] then
	      (out1 <- [1]) fi     *** CORRECT!
*** ERROR       (out2 <- [4])     --- 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]) ; (counter2 |-> [0]) ; (counter3 |-> [0]),
      reactions : (reaction when inAdas do { (brakesApplied := inAdas) ;
                                             (counter3 := counter3 + [1])})
                  (reaction when inPedal do { (brakesApplied := inPedal)  ;
                                             (counter2 := counter2 + [1]) })

    >

    (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 .
endom


--- Property: within time 55, the brakes are applied.
---  Since we know that the timer t has offset 0, it will
--- fire at time 0, then 34, then 68, etc.
--- Therefore, it is enough to verify the time-bounded
--- formula <>_<= 55 (brakesApplied), which is what we will do.

--- We will also show that the other error cases also give errors.
--- While Real-Time Maude has a timed CTL model checker, we only use
--- Maude and "home-made" time-bounded analysis in this case.

