updates

korg-examples/test.pml

@@ -0,0 +1,12 @@
+chan msgs = [4] of { bit };
+int count = 0;
+
+active [1] proctype Producer() { // one producer
+  do :: atomic { count++; msgs ! 1; } od
+}
+
+active [4] proctype Consumer() { // four consumers
+  do :: atomic { msgs ? 1 -> count--; } od
+}
+
+ltl always_positive { always (count >= 0) }