---(****************************
 * Auto-generated Maude model *
 ******************************)---
omod TRAFFICLIGHT is
    including LF-REPR .
    protecting LF-VALUE-TIME .

    op TrafficLight : -> ReactorId [ctor] .
    op t : -> ReactorId [ctor] .
    op p : -> ReactorId [ctor] .
    op t.sv.count : -> RVarId [ctor] .
    op t.sv.mode : -> RVarId [ctor] .
    op t.in.pedestrian : -> RPortId [ctor] .
    op t.out.sigR : -> RPortId [ctor] .
    op t.out.sigG : -> RPortId [ctor] .
    op t.out.sigY : -> RPortId [ctor] .
    op p.out.out : -> RPortId [ctor] .
    op t.t.t : -> TimerId [ctor] .
    op p.t.t : -> TimerId [ctor] .
    op t.la.resetCount : -> RActionId [ctor] .
    op startup : -> RActionId [ctor] .
    op init : -> Configuration .
    
    eq init = 
        < t : Reactor |
            inports : 
                < t.in.pedestrian : Port | value : [0] >,
            outports : 
                < t.out.sigR : Port | value : [0] >
                < t.out.sigG : Port | value : [0] >
                < t.out.sigY : Port | value : [0] >,
            state : 
                ( t.sv.count |-> [0] );
                ( t.sv.mode |-> [0] ),
            timers : 
                < t.t.t : Timer | offset : 0, period : 1000000 >,
            actions : 
                < t.la.resetCount : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >
                < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >,
            reactions : 
                (reaction when (startup) do {
                    (t.sv.mode := [0]) ;
                    (t.sv.count := [58])
                })
                (reaction when (t.in.pedestrian ; t.t.t) --> (t.out.sigR ; t.out.sigG ; t.out.sigY ; t.la.resetCount) do {
                    if ((t.sv.mode === [0])) then (if ((t.sv.count >= [60])) then ((t.out.sigG <- [1]) ;
                    schedule(t.la.resetCount, [0], [0]) ;
                    (t.sv.mode := [1])) else ((t.sv.count := (t.sv.count + [1]))) fi) else (if ((t.sv.mode === [1])) then (if ((isPresent(t.in.pedestrian))) then (if ((t.sv.count >= [60])) then ((t.out.sigY <- [1]) ;
                    (t.sv.mode := [2]) ;
                    schedule(t.la.resetCount, [0], [0])) else ((t.sv.count := (t.sv.count + [1]))) fi) else ((t.sv.count := (t.sv.count + [1]))) fi) else (if ((t.sv.mode === [2])) then (if ((t.sv.count >= [5])) then ((t.out.sigR <- [1]) ;
                    schedule(t.la.resetCount, [0], [0])) else ((t.sv.count := (t.sv.count + [1]))) fi) else (if ((t.sv.count >= [60])) then ((t.out.sigY <- [1]) ;
                    schedule(t.la.resetCount, [0], [0])) else ((t.sv.count := (t.sv.count + [1]))) fi) fi) fi) fi
                })
                (reaction when (t.la.resetCount) do {
                    (t.sv.count := [0])
                })
        >
        < p : Reactor |
            inports : none,
            outports : 
                < p.out.out : Port | value : [0] >,
            state : empty,
            timers : 
                < p.t.t : Timer | offset : 1000000, period : 10000000 >,
            actions : none,
            reactions : 
                (reaction when (p.t.t) --> (p.out.out) do {
                    (p.out.out <- [1])
                })
        >
    (p : p.out.out --> t : t.in.pedestrian)
    .
endom

omod TEST-TRAFFICLIGHT is
    including TRAFFICLIGHT .
    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 ANALYSIS-TRAFFICLIGHT is
    including TEST-TRAFFICLIGHT .
    including LF-PROP-EXT .
    including SEARCH-GOAL .
endom

omod MODELCHECKER-TRAFFICLIGHT is
    including TEST-TRAFFICLIGHT .
    including LF-OUTPUT-COUNTEREXAMPLE .
    including LF-PROP-EXT .
    including MODEL-CHECKER .
endom

omod SIMULATION-TRAFFICLIGHT is
    including TEST-TRAFFICLIGHT .
    including TIMED-SIMULATION-DYNAMICS .
endom

red in MODELCHECKER-TRAFFICLIGHT : modelCheck(initSystem timeBound 5000000 , (<> (( (@ t.sv.mode in t) === @ [1] ))) ) .

quit
