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

    op TrainDoor : -> ReactorId [ctor] .
    op c : -> ReactorId [ctor] .
    op t : -> ReactorId [ctor] .
    op d : -> ReactorId [ctor] .
    op t.sv.received : -> RVarId [ctor] .
    op d.sv.received : -> RVarId [ctor] .
    op c.out.out1 : -> RPortId [ctor] .
    op c.out.out2 : -> RPortId [ctor] .
    op t.in.in : -> RPortId [ctor] .
    op d.in.in : -> RPortId [ctor] .
    op startup : -> RActionId [ctor] .
    op init : -> Configuration .
    
    eq init = 
        < c : Reactor |
            inports : none,
            outports : 
                < c.out.out1 : Port | value : [0] >
                < c.out.out2 : Port | value : [0] >,
            state : empty,
            timers : none,
            actions : 
                < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >,
            reactions : 
                (reaction when (startup) --> (c.out.out1 ; c.out.out2) do {
                    (c.out.out1 <- [1]) ;
                    (c.out.out2 <- [2])
                })
        >
        < t : Reactor |
            inports : 
                < t.in.in : Port | value : [0] >,
            outports : none,
            state : 
                ( t.sv.received |-> [0] ),
            timers : none,
            actions : none,
            reactions : 
                (reaction when (t.in.in) do {
                    (t.sv.received := t.in.in)
                })
        >
        < d : Reactor |
            inports : 
                < d.in.in : Port | value : [0] >,
            outports : none,
            state : 
                ( d.sv.received |-> [0] ),
            timers : none,
            actions : none,
            reactions : 
                (reaction when (d.in.in) do {
                    (d.sv.received := d.in.in)
                })
        >
    (c : c.out.out1 -- 1000000 --> t : t.in.in)
    (c : c.out.out2 -- 1000000 --> d : d.in.in)
    .
endom

omod TEST-TRAINDOOR is
    including TRAINDOOR .
    including DYNAMICS-WITHOUT-TICK .

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

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

omod ANALYSIS-TRAINDOOR is
    including TEST-TRAINDOOR .
    including LF-PROP-EXT .
    including SEARCH-GOAL .
endom

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

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

red in MODELCHECKER-TRAINDOOR : modelCheck(initSystem timeBound 1000000 , ((~ ((t . 1) invoked )) U ((d . 1) invoked )) ) .

quit
