読者です 読者をやめる 読者になる 読者になる

cloverrose's blog

Python, Machine learning, Emacs, CI/CD, Webアプリなど

SPINをinstall

UbuntuとMacでSPINをビルドした時のメモ ポイント SPINのビルドにはyaccが必要なのでBisonをインストール 手順 sudo apt-get install bison wget http://spinroot.com/spin/Src/src624.tar.gz gunzip *.tar.gz tar -xf *.tar cd Src* make

SPINの基本 初期値を指定した配列の定義の仕方

SPINは配列が使えます。 int requests[100];定義時に初期値を指定しないと、型によって決まった初期値が設定されます。intやboolは0。 これは『requests[idx]が0にはならないはず』というモデルを作ると最初に0に設定されているので破綻します。配列の要素全…

Readers/Writers Algorithm2でReaderが永遠に待ち続ける欠陥をSPINで検証

前回に引き続きSPINでReaders/Writers Algorithmを検証してみました。 今回はAlgorithm2で、Algorithm1とは反対にReaderが永遠に待ち続けるという問題があります。 ソース #define NR 1 #define NW 2 int m1=0; int m2=0; int m3=0; int r=0; int w=0; int r…

Readers/Writers Algorithm1でWriterが永遠に待ち続ける欠陥をSPINで検証

Readers/Writers Algorithmについて Readers-writers problem - Wikipedia, the free encyclopediaこのアルゴリズムの中で一番シンプルなAlgorithm1は、誰かが読込中なら書き込みはしないとか書き込み中なら読み込みはしないという安全性は満たしているんだ…

例題:うさぎとおおかみ解いてみた

ソース mtype = {A, AtoB, B, BtoA}; int RbA, RbB, RbS, WoA, WoB, WoS; mtype Splace; inline toBank(RbX, WoX){ atomic{ RbX=RbX+RbS;RbS=0; WoX=WoX+WoS;WoS=0; } } inline fromBank(RbX, WoX){ atomic{ if ::(RbX>=2) -> RbX = RbX-2; RbS = RbS+2; ::(…

プロセスのローカル変数Nx系に注意

SPINのNx系の変数をプロセスのローカル変数として定義するときは気をつけましょうという話 同時代入とNuSMVとSPINの違いについて 同時代入 x=0 y=0 x=1 y=1 書いた場合、xは1だけどyは0の状態が存在します。 一方、 x=0 y=0 x, y = (1, 1) と書けばxが1にな…