target C

reactor Trigger {
    output out:int
    timer t(0,1 msec)

    reaction(t) -> out {= 
        lf_set(out, 1);
    =}
}

reactor Task {
    input cnt:int;
    state counter:int = 0;

    reaction(cnt) {=
        self->counter += 2; // Should be 1.
    =}
}

//@property(name="upperbound", tactic="bmc", spec="G[0, 1 msec]((CoopSchedule_task1_counter + CoopSchedule_task2_counter + CoopSchedule_task3_counter + CoopSchedule_task4_counter + CoopSchedule_task5_counter) < 15)", expect=false)
@maude(analysis="reachability", timeBound=1, goal="((counter in task1) + (counter in task2) + (counter in task3) + (counter in task4) + (counter in task5)) >= 15")
main reactor {
    trigger = new Trigger()
    // TODO: Put these reactors in a bank.
    task1 = new Task()
    task2 = new Task()
    task3 = new Task()
    task4 = new Task()
    task5 = new Task()
    trigger.out -> task1.cnt
    trigger.out -> task2.cnt
    trigger.out -> task3.cnt
    trigger.out -> task4.cnt
    trigger.out -> task5.cnt
}
