feat(learning-spin): add counter.pml and printer.pml

Author: nojima

learning-spin/counter.pml

@@ -0,0 +1,22 @@
+// グローバル変数はプロセス間で共有される。
+// 初期値が指定されていない場合はゼロで初期化される。
+byte count;
+bool finished[2];
+
+// カウンタの値をインクリメントする
+proctype Increment(byte index) {
+    // read-modify-write
+    count = count + 1;
+
+    finished[index] = true;
+}
+
+init {
+    run Increment(0);
+    run Increment(1);
+
+    // 条件文を書いた場合、trueになるまでブロックするという意味になる。
+    (finished[0] && finished[1]);  
+    // assert を使って検証したい条件を書く。
+    assert(count == 2);
+}

learning-spin/printer.pml

@@ -0,0 +1,23 @@
+bool printer_locked;
+bool scanner_locked;
+
+proctype User() {
+    if
+    :: atomic { (!printer_locked) -> printer_locked = true };
+       atomic { (!scanner_locked) -> scanner_locked = true };
+       skip;    // use printer and scanner
+       scanner_locked = false;
+       printer_locked = false;
+
+    :: atomic { (!scanner_locked) -> scanner_locked = true };
+       atomic { (!printer_locked) -> printer_locked = true };
+       skip;    // use scanner and printer
+       printer_locked = false;
+       scanner_locked = false;
+    fi
+}
+
+init {
+    run User();
+    run User();
+}