*** We fix the LF version of the traffic light by also updating the 'mode' variable.

*** Note 2: The LF spec checks isPresent(ped) even when ped is NOT a trigger.
***   We think that in general, you cannot check 'isPresent' for something
***   that the reaction has NOT declared as trigger.  Why?  A reaction can execute
***   when we know the status of all TRIGGERS.  But if ped is NOT a trigger for reaction X,
***   reaction X can execute, but the status of ped can still be unknown.

***  We therefore make the obvious assumption that all isPresent checks can only be done
***   on triggers.


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

  ops count mode : -> RVarId [ctor] .
  ops trafficLight pedestrian : -> ReactorId [ctor] .
  ops out ped sigR sigY sigG : -> RPortId [ctor] .
  ops startup resetCount : -> RActionId [ctor] .
  op t : -> TimerId [ctor] .

  --- 0 is red, 1 is green, 2 is yellow, and 3 is pending, for "mode"

  op init : -> Configuration .

  eq init
   = < trafficLight : Reactor |
          inports : < ped : Port | value : [0] >,
	  outports :  < sigR : Port | value : [0] >
	              < sigY : Port | value : [0] >
		      < sigG : Port | value : [0] >,
	  state : (count |-> [0]) ; (mode |-> [3]), 
	  timers : < t : Timer | offset : 0, period : 1 >,
	  actions : < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >
                    < resetCount : LogicalAction | minDelay : 0, 
                                                   minSpacing : 0, 
                                                   policy : defer, 
                                                   payload : [0] >,
	  reactions :
	     (reaction when startup do {(mode := [0]) ; (count := [58])})
             (reaction when (ped ; t) --> (sigR ; sigG ; sigY ; resetCount) do {
	          if (mode === [0]) then
		      (if (count >= [60]) then ((sigG <- [1]) ; (mode := [1]) ; schedule(resetCount, [0], [0]))
		       else (count := count + [1]) fi)
                  else (if (mode === [1]) then
		            (if isPresent(ped) then      *** isPresent(ped)
			       (if (count >= [60]) then ((sigY <- [1]) ; (mode := [2]) ;
			                                 schedule(resetCount, [0], [0]))
                                else (count := count + [1]) fi)
                             else (count := count + [1]) fi)
                        else (if (mode === [2]) then 
                                 (if (count >= [5]) then ((sigR <- [1]) ; (mode := [0]) ;
				                          schedule(resetCount, [0], [0]))
                                  else (count := count + [1]) fi)
			      else (if (count >= [60]) then ((sigY <- [1]) ; (mode := [2]) ;
			                                     schedule(resetCount, [0], [0]))
		                    else (count := count + [1]) fi)  	  
                              fi)
                         fi)
                   fi})     		 
             (reaction when resetCount do {count := [0]})   >
     
    < pedestrian : Reactor |
          inports : none,
	  outports : < out : Port | value : [0] >,
	  state : empty,
	  timers : < t : Timer | offset : 1, period : 10 >,
	  actions : none,
	  reactions : reaction when t --> out do {out <- [1]} > 

    (pedestrian : out --> trafficLight : ped)  .
endom

red generateAPG(event(trafficLight, startup, [0]) event(trafficLight, t, [0]),  addReactionIndices(init)) .

red generateAPG(event(pedestrian, t, [0]),  addReactionIndices(init)) .



omod TEST-TRAFFIC-LIGHT is
  including TRAFFIC-LIGHT .
  including DYNAMICS-WITHOUT-TICK .

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

  op initSystem : -> GlobalSystem .
  eq initSystem =
      {< env : Environment | physicalActions : none >
       addReactionIndices(init)
       < queue : EventQueue | queue : addInitialTimers(init, addStartup(startup, init, empty)) >
       < rxns : Invoked | reactions : none >} .
endom

omod SIMULATE-TRAFFIC-LIGHT is
  including TEST-TRAFFIC-LIGHT .
  including SIMULATION-DYNAMICS .
endom  

rew [100] initSystem .


*** Desired property, which supposedly does not hold: Within 5 seconds the light will be green
***   in all possible behaviors:

*** Time-bounded analysis:

omod TIME-BOUNDED-TRAFFIC-LIGHT is
  including TEST-TRAFFIC-LIGHT .
  including TIME-BOUNDED-DYNAMICS  .
  eq timeBound = 5 .
endom  

rew initSystem in time 0 .

omod UNBOUNDED-TRAFFIC-LIGHT is
  including TEST-TRAFFIC-LIGHT .
  including UNBOUNDED-ANALYSIS-DYNAMICS  .
endom  

search initSystem =>* {none} .   --- benchmarking

omod MODEL-CHECK-TRAFFIC-LIGHT is
  including MODEL-CHECKER .
  including TIME-BOUNDED-TRAFFIC-LIGHT .
  including LF-PROP .
endom

red modelCheck(initSystem in time 0,
               <> (mode in trafficLight == [1])) .


*** return true for bound 5.




omod UNBOUNDED-MODEL-CHECK-TRAFFIC-LIGHT is
  including MODEL-CHECKER .
  including UNBOUNDED-TRAFFIC-LIGHT .
  including LF-PROP .

endom

*** The traffic light is infinitely often in RED AND infinitely often in GREEN!!!

red modelCheck(initSystem in time 0,
               ([] <> (mode in trafficLight == [1])) /\ ([] <> (mode in trafficLight == [0]))) .


*** retuens true!!!

***(   Main property in LF directory:

spec="F[0, 5 sec](TrafficLight_t__mode == 1)", expect=false

)***

--- This has already been checked above!
