/* Run instructions:
 * prom2lts-seq --ltl="! <> (state != 1 && <> (state == 1))" --trace=trace.gcf race-condition.prm
 * ltsmin-printtrace trace.gcf -a | grep state | grep -v end
 */

#define __instances_A 1
#define __instances_B 1

byte state = 1;

proctype A() {
    byte tmp;
    (state==1) -> tmp = state; tmp = tmp+1; state = tmp
}

proctype B() {
    byte tmp;
    (state==1) -> tmp = state; tmp = tmp-1; state = tmp
}

init {
    atomic { run A(); run B() }
}