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

    op PingPong : -> ReactorId [ctor] .
    op ping : -> ReactorId [ctor] .
    op pong : -> ReactorId [ctor] .
    op ping.sv.pingsLeft : -> RVarId [ctor] .
    op pong.sv.count : -> RVarId [ctor] .
    op pong.sv.expected : -> RVarId [ctor] .
    op ping.in.receive : -> RPortId [ctor] .
    op ping.out.send : -> RPortId [ctor] .
    op pong.in.receive : -> RPortId [ctor] .
    op pong.out.send : -> RPortId [ctor] .
    op ping.la.serve : -> RActionId [ctor] .
    op startup : -> RActionId [ctor] .
    op init : -> Configuration .
    
    eq init = 
        < ping : Reactor |
            inports : 
                < ping.in.receive : Port | value : [0] >,
            outports : 
                < ping.out.send : Port | value : [0] >,
            state : 
                ( ping.sv.pingsLeft |-> [10] ),
            timers : none,
            actions : 
                < ping.la.serve : LogicalAction | minDelay : 1000000, minSpacing : 0, policy : defer, payload : [0] >
                < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >,
            reactions : 
                (reaction when (startup) --> (ping.la.serve) do {
                    schedule(ping.la.serve, [0], [0])
                })
                (reaction when (ping.la.serve) --> (ping.out.send) do {
                    (ping.out.send <- ping.sv.pingsLeft) ;
                    (ping.sv.pingsLeft := (ping.sv.pingsLeft - [1]))
                })
                (reaction when (ping.in.receive) --> (ping.la.serve) do {
                    if ((ping.sv.pingsLeft > [0])) then (schedule(ping.la.serve, [0], [0])) fi
                })
        >
        < pong : Reactor |
            inports : 
                < pong.in.receive : Port | value : [0] >,
            outports : 
                < pong.out.send : Port | value : [0] >,
            state : 
                ( pong.sv.count |-> [0] );
                ( pong.sv.expected |-> [10] ),
            timers : none,
            actions : none,
            reactions : 
                (reaction when (pong.in.receive) --> (pong.out.send) do {
                    (pong.sv.count := (pong.sv.count + [1])) ;
                    (pong.out.send <- pong.in.receive)
                })
        >
    (ping : ping.out.send --> pong : pong.in.receive)
    (pong : pong.out.send --> ping : ping.in.receive)
    .
endom

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

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

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

red in MODELCHECKER-PINGPONG : modelCheck(initSystem timeBound 4000000 , ([] ((ping . 2) invoked  -> O ~ ((ping . 2) invoked ))) ) .

quit
