model-checker : test examples for snapshot comparison

[simgrid.git] / examples / msg / mc / test / promela

diff --git a/examples/msg/mc/test/promela b/examples/msg/mc/test/promela
new file mode 100644 (file)
index 0000000..54b9747
--- /dev/null
+++ b/examples/msg/mc/test/promela
@@ -0,0 +1,10 @@
+never { 
+T0_init :    /* init */
+       if
+       :: (1) -> goto accept_S2
+       fi;
+accept_S2 :    /* 1 */
+       if
+  :: (1) -> goto accept_S2
+  fi;      
+}
\ No newline at end of file