Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
-#define queue_has_entry (queue == 1)
+#define queue_has_entry (queue[0] == 1 || queue[1] == 1)
* Copyright (c) 2009 Mathieu Desnoyers
*/
* Copyright (c) 2009 Mathieu Desnoyers
*/
+#define get_pid() (_pid)
+
+int queue[2] = 0;
+active [2] proctype waker()
+ assert(get_pid() < 2);
+
+ queue[get_pid()] = 1;
fi;
#ifdef INJ_QUEUE_NO_WAKE
fi;
#ifdef INJ_QUEUE_NO_WAKE
+ :: (queue[0] == 1 || queue[1] == 1) ->
#ifndef INJ_LATE_DEC
fut = 0;
#endif
#ifndef INJ_LATE_DEC
fut = 0;
#endif
+ if
+ :: queue[0] == 1 ->
+ queue[0] = 0;
+ fi;
+ if
+ :: queue[1] == 1 ->
+ queue[1] = 0;
+ fi;