target C;

reactor Controller {
    input in:int
    output out1:int
    output out2:int
    output out3:int
    logical action another(5 ms)
    reaction(startup, another) -> out1, out2, out3 {=
        lf_set(out1, 1);
        lf_set(out2, 2);
        lf_set(out3, 3);
    =}
    reaction(in) -> another {=
        lf_schedule(another, 0);
    =}
}

reactor Train {
    input in:int
    output out:int
    state received:int
    reaction(in) -> out {=
        self->received = in->value;
        lf_set(out, self->received);
    =}
}

reactor Door {
    input in:int
    output out:int
    state received:int
    reaction(in) -> out {=
        self->received = in->value;
        lf_set(out, self->received);
    =}
}

reactor Sink {
    input in1:int
    input in2:int
    input in3:int
    output out:int
    state sum:int = 0
    reaction(in1, in2, in3) -> out {=
        self->sum = in1->value + in2->value + in3->value;
        lf_set(out, self->sum);
    =}
}

// @property(name="train_does_not_move_until_door_closes", tactic="bmc", spec="(!TrainDoor_t_reaction_0)U[0, 1 msec](TrainDoor_d_reaction_0)", expect=false)
@maude(analysis="ltl", timeBound=1, goal="(! (t.1 invoked)) U (d.1 invoked)")
main reactor {
    c = new Controller()
    t = new Train()
    d = new Door()
    d2 = new Door()
    s = new Sink()
    c.out1 -> t.in after 1 msec
    c.out2 -> d.in after 1 msec
    c.out3 -> d2.in after 1 msec
    t.out -> s.in1
    d.out -> s.in2
    d2.out -> s.in3
    s.out -> c.in
}
