target C

reactor Node0 {
    input in:int
    output out:int
    state id:int
    state elected:int = 0
        
    reaction(startup) -> out {=
        self->id = 0;
        lf_set(out, self->id);
    =}
    reaction(in) -> out {=
        if (in->value > self->id) {
            lf_set(out, in->value);
        } else if (in->value == self->id) {
            self->elected = 1;
        }
    =}
}

reactor Node1 {
    input in:int
    output out:int
    state id:int
    state elected:int = 0
        
    reaction(startup) -> out {=
        self->id = 1;
        lf_set(out, self->id);
    =}
    reaction(in) -> out {=
        if (in->value > self->id) {
            lf_set(out, in->value);
        } else if (in->value == self->id) {
            self->elected = 1;
        }
    =}
}

reactor Node2 {
    input in:int
    output out:int
    state id:int
    state elected:int = 0
        
    reaction(startup) -> out {=
        self->id = 2;
        lf_set(out, self->id);
    =}
    reaction(in) -> out {=
        if (in->value > self->id) {
            lf_set(out, in->value);
        } else if (in->value == self->id) {
            self->elected = 1;
        }
    =}
}

// This property being checked does not hold. A valid property is F[0, 30 msec]((Election2_i0_elected + Election2_i1_elected + Election2_i2_elected) == 1)
// @property(name="exactly_one_elected", tactic="bmc", spec="F[0, 20 msec]((Election2_i0_elected + Election2_i1_elected + Election2_i2_elected) == 1)", expect=false)
@maude(analysis="ltl", goal="<> (elected in i0 + elected in i1 + elected in i2 == 1)", timeBound=20)
main reactor {
    i0 = new Node0()
    i1 = new Node1()
    i2 = new Node2()
    i0.out -> i1.in after 10 msec
    i1.out -> i2.in after 10 msec
    i2.out -> i0.in after 10 msec
}
