add formal verif

[lttv.git] / trunk / verif / Spin / Test / priorities

diff --git a/trunk/verif/Spin/Test/priorities b/trunk/verif/Spin/Test/priorities
new file mode 100755 (executable)
index 0000000..bf7a8c4
--- /dev/null
+++ b/trunk/verif/Spin/Test/priorities
@@ -0,0 +1,22 @@
+/* test execution priorities
+   run this as:
+       spin -p -g priorities
+   requires Spin Version 2.5 or later
+*/
+
+int a[5];
+
+proctype A()
+{
+       do
+       :: printf("%d\n", _pid); a[_pid]++
+       od
+}
+
+init {
+       atomic {
+               run A() priority 1;
+               run A() priority 2;
+               run A() priority 3;
+               run A() priority 4;
+}      }