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

    op ProcessMsg : -> ReactorId [ctor] .
    op task : -> ReactorId [ctor] .
    op task.sv.messageSent : -> RVarId [ctor] .
    op task.sv.counter : -> RVarId [ctor] .
    op task.sv.panic : -> RVarId [ctor] .
    op task.in.in : -> RPortId [ctor] .
    op task.out.out : -> RPortId [ctor] .
    op task.t.t : -> TimerId [ctor] .
    op task.la.updateMessage : -> RActionId [ctor] .
    op startup : -> RActionId [ctor] .
    op init : -> Configuration .
    
    eq init = 
        < task : Reactor |
            inports : 
                < task.in.in : Port | value : [0] >,
            outports : 
                < task.out.out : Port | value : [0] >,
            state : 
                ( task.sv.messageSent |-> [0] );
                ( task.sv.counter |-> [0] );
                ( task.sv.panic |-> [0] ),
            timers : 
                < task.t.t : Timer | offset : 0, period : 1000000 >,
            actions : 
                < task.la.updateMessage : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >
                < startup : LogicalAction | minDelay : 0, minSpacing : 0, policy : defer, payload : [0] >,
            reactions : 
                (reaction when (startup) do {
                    (task.sv.messageSent := [0])
                })
                (reaction when (task.t.t) --> (task.out.out) do {
                    (task.out.out <- task.sv.messageSent)
                })
                (reaction when (task.in.in) --> (task.la.updateMessage) do {
                    if ((task.in.in ==/= task.sv.messageSent)) then ((task.sv.panic := [1])) fi ;
                    schedule(task.la.updateMessage, [0], [0]) ;
                    (task.sv.counter := (task.sv.counter + [1]))
                })
                (reaction when (task.la.updateMessage) do {
                    (task.sv.messageSent := (task.sv.messageSent + [1]))
                })
        >
    (task : task.out.out --> task : task.in.in)
    .
endom

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

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

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

search [1] in ANALYSIS-PROCESSMSG : initSystem timeBound 5000000 =>* CS:ClockedSystem  such that CS:ClockedSystem |= (( (@ task.sv.panic in task) === @ [1] ) /\ remainingTime 0) .

quit
