+bit init_done = 0;
+
+bit sighand_exec = 0;
+
+inline wait_init_done()
+{
+ do
+ :: init_done == 0 -> skip;
+ :: else -> break;
+ od;
+}
+
+#ifdef TEST_SIGNAL
+
+inline wait_for_sighand_exec()
+{
+ sighand_exec = 0;
+ do
+ :: sighand_exec == 0 -> skip;
+ :: else -> break;
+ od;
+}
+
+#ifdef TOO_BIG_STATE_SPACE
+inline wait_for_sighand_exec()
+{
+ sighand_exec = 0;
+ do
+ :: sighand_exec == 0 -> skip;
+ :: else ->
+ if
+ :: 1 -> break;
+ :: 1 -> sighand_exec = 0;
+ skip;
+ fi;
+ od;
+}
+#endif
+
+#else
+
+inline wait_for_sighand_exec()
+{
+ skip;
+}
+
+#endif
+
+#ifdef TEST_SIGNAL_ON_WRITE
+/* Block on signal handler execution */
+inline dispatch_sighand_write_exec()
+{
+ sighand_exec = 1;
+ do
+ :: sighand_exec == 1 ->
+ skip;
+ :: else ->
+ break;
+ od;
+}
+
+#else
+
+inline dispatch_sighand_write_exec()
+{
+ skip;
+}
+
+#endif
+
+#ifdef TEST_SIGNAL_ON_READ
+/* Block on signal handler execution */
+inline dispatch_sighand_read_exec()
+{
+ sighand_exec = 1;
+ do
+ :: sighand_exec == 1 ->
+ skip;
+ :: else ->
+ break;
+ od;
+}
+
+#else
+
+inline dispatch_sighand_read_exec()
+{
+ skip;
+}
+
+#endif
+
+