#define N 4 byte garray[N]; inline forall(i, from, to, array, result) { result = true; i = from; do :: i < to -> if :: array[i] == false -> result = false; break; :: else -> skip; fi; i = i+1; :: else -> break; od; } inline forallExcept(i, from, to, except, array, result) { result = true; i = from; do :: i < to -> if :: i != except && array[i] == false -> result = false; break; :: else -> skip; fi; i = i+1; :: else -> break; od; } proctype proc(byte id) { byte larray[N]; byte i, lall, gall; // evaluate all conditions atomically atomic { forall(i, 0, N, larray, lall); forall(i, 0, N, garray, gall); } // use conditions in program if :: lall -> printf("AAA%d\n", id); :: gall -> printf("BBB%d\n", id); :: else -> printf("CCC%d\n", id); fi } init { atomic { int i = 0; do :: i < N -> run proc(i); i = i+1; :: else -> break; od; } }