target C;

reactor Source {
    output out:int;
    state value:int = 0;
    logical action a(1 msec);
    timer t(0, 2 msec);
    reaction(t) -> a, out {=
        self->value += 1;
        lf_set(out, self->value);
        lf_schedule(a, 0);
    =}
    reaction(a) -> out {=
        lf_set(out, self->value);
    =}
}

reactor Node {
    
    input  in:int;
    output out:int;
    
    state  count:int;
    state  payload:int;

    logical action send_output;

    reaction(in) -> send_output {=
        self->payload = in->value;
        self->count += 1;
        lf_schedule(send_output, 0);
    =}

    reaction(send_output) -> out {=
        lf_set(out, self->payload);
        self->count -= 1;
    =}
}

reactor Sink {
    input in:int;
    state received:int;
    reaction(in) {=
        self->received = in->value;
    =}
}

@maude(analysis="ltl", goal="[] ! ( (count in node1 <= 1) /\ (count in node2 <= 1) /\ (count in node3 <= 1) /\ (count in node4 <= 1) /\ (count in node5 <= 1))", timeBound=1)
//@property(name="count_bounded", tactic="bmc", spec="G[0, 1 msec](!(Pipe_node1_count <= 1 && Pipe_node2_count <= 1 && Pipe_node3_count <= 1 && Pipe_node4_count <= 1 && Pipe_node5_count <= 1))", expect=false)
main reactor {
    
    source = new Source();
    node1 = new Node();
    node2 = new Node();
    node3 = new Node();
    node4 = new Node();
    node5 = new Node();
    sink = new Sink();

    source.out -> node1.in;
    node1.out -> node2.in;
    node2.out -> node3.in;
    node3.out -> node4.in;
    node4.out -> node5.in;
    node5.out -> sink.in;
}
