target C

reactor Task {
    /* Define the counters used in the demo application...  */
    state tm_synchronization_processing_counter:int = 0
    timer t(0,1 msec)

    reaction(t) {=
        /* Increment the counter.  */
        self->tm_synchronization_processing_counter += 1;
    =}
}

// @property(name="correctness", tactic="bmc", spec="G[2 msec](ProcessSync_task_tm_synchronization_processing_counter == 3)", expect=true)

// a counterexample found
@maude(analysis="reachability", timeBound=2, goal="(tm_synchronization_processing_counter in task != 3) /\ remainingTime 0")

// no counterexample found
@maude(analysis="reachability", timeBound=2, goal="(tm_synchronization_processing_counter in task != 3) /\ (! (event(task, t)inQueue )) /\ remainingTime 0")

main reactor {
    task = new Task()
}
