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

    op UnsafeSend : -> ReactorId [ctor] .
    op c : -> ReactorId [ctor] .
    op s : -> ReactorId [ctor] .
    op c.sv.req : -> RVarId [ctor] .
    op s.sv.error : -> RVarId [ctor] .
    op c.in.in : -> RPortId [ctor] .
    op c.out.out : -> RPortId [ctor] .
    op s.in.in : -> RPortId [ctor] .
    op s.out.out : -> RPortId [ctor] .
    op startup : -> RActionId [ctor] .
    op s.la.err : -> RActionId [ctor] .
    op init : -> Configuration .
    
    eq init = 
        < c : Reactor |
            inports : 
                < c.in.in : Port | value : [0] >,
            outports : 
                < c.out.out : Port | value : [0] >,
            state : 
                ( c.sv.req |-> [0] ),
            timers : none,
            actions : 
                < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >,
            reactions : 
                (reaction when (startup) --> (c.out.out) do {
                    (c.sv.req := [0]) ;
                    (c.out.out <- c.sv.req)
                })
                (reaction when (c.in.in) do {
                    (c.sv.req := [0])
                })
        >
        < s : Reactor |
            inports : 
                < s.in.in : Port | value : [0] >,
            outports : 
                < s.out.out : Port | value : [0] >,
            state : 
                ( s.sv.error |-> [0] ),
            timers : none,
            actions : 
                < s.la.err : LogicalAction | minDelay : 1000000, minSpacing : 0, policy : defer, payload : [0] >,
            reactions : 
                (reaction when (s.in.in) --> (s.out.out ; s.la.err) do {
                    if ((s.in.in === [0])) then (schedule(s.la.err, [0], [0])) else ((s.out.out <- s.in.in)) fi
                })
                (reaction when (s.la.err) do {
                    (s.sv.error := [1])
                })
        >
    (c : c.out.out -- 2 --> s : s.in.in)
    (s : s.out.out -- 2 --> c : c.in.in)
    .
endom

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

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

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

red in MODELCHECKER-UNSAFESEND : modelCheck(initSystem timeBound 5000000 , (<> ((c . 2) invoked )) ) .

quit
