Add no sync_core() test to ooo two writes model

[urcu.git] / formal-model / ooomem-two-writes / mem.spin

diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin
index 4892c5ec333249b74d3b8beab5ff5bee40a268b1..828ff4a5d9245e51c3ba529af0ff4c0189caefc8 100644 (file)
--- a/formal-model/ooomem-two-writes/mem.spin
+++ b/formal-model/ooomem-two-writes/mem.spin
@@ -184,6 +184,9 @@ active proctype test_proc_one()
 #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) ->
@@ -231,6 +234,9 @@ active proctype test_proc_two()
 #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) ->