#ifdef NO_RMB
PRODUCE_TOKENS(proc_one_produced, P1_RMB);
#endif
+#ifdef NO_SYNC
+ PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
+#endif
do
:: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_WRITE) ->
#ifdef NO_RMB
PRODUCE_TOKENS(proc_two_produced, P2_RMB);
#endif
+#ifdef NO_SYNC
+ PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
+#endif
do
:: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE) ->