in dynamics.maude

omod TRAFFIC-LIGHT is including RUNTIME-APG .

  ops count mode : -> IVarId [ctor] .
  ops trafficLight pedestrian : -> ReactorId [ctor] .
  ops out ped sigR sigY sigG : -> IPortId [ctor] .
  ops startup resetCount : -> IActionId [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 |-> [0]), 
	  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 t --> (sigR ; sigG ; sigY ; resetCount) do {
	          if (mode === [0]) then
		      (if (count >= [60]) then ((sigG <- [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]) ; 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]) ; schedule(resetCount, [0], [0]))
                                  else (count := count + [1]) fi)
			      else (if (count >= [60]) then ((sigY <- [1]) ; 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]),  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 .

eof

*** Comment: In the LF page, they admit that there is a bug: the variable
***   mode is never changed.  Therefore we also improve the example
*** in the file corrected-traffic-light.maude



