*** First attempt; Luxembourg meeting


omod ADAS is 
  including LF-REPR .
  protecting LF-VALUE-TIME .
  protecting RUNTIME-APG .

  ops frame received brakesApplied requestStop : -> RVarId [ctor] .
  ops lidar camera adasProcessor dashboard pedal brakes : -> ReactorId [ctor] .
  op t : -> TimerId [ctor] .
  ops in in1 in2 out out1 out2 inAdas inPedal : -> RPortId [ctor] .
  op a : -> RActionId .
  op init : -> Configuration .
  
  eq init = 
     < lidar : Reactor | 
       inports : none,
       outports : < out : Port | value : [0] >, 
       state : frame |-> [0],
       timers : < t : Timer | offset : 0, period : 34 >,
       actions : none,
       reactions : 
       reaction when t --> out do { (frame := frame + [1]) ; (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 { (frame := frame + [1]) ; (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, 
                                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
          }
     >
 
     < dashboard : Reactor | 
         inports : < in : Port | value : [0] >,
         outports : none,
         state : received |-> [0],
         timers : none,
         actions : none,
         reactions : reaction when in do { received := [1] }       
     >
     
     < 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 ; inPedal do { brakesApplied := [1] }
     >
 
     (lidar : out --> adasProcessor : in1)
     (camera : out --> adasProcessor : in2)
     (adasProcessor : out1 -- 5 --> brakes : inAdas)
     (adasProcessor : out2 --> dashboard : in)
     pedal : out --> brakes : inPedal .
endom


red generateAPG(event(camera, t, [165]), addReactionIndices(init)) .
