SPIN(simple promela interpreter)は、Promela(process meta language)システムです。
４日で学ぶモデル検査 初級編
https://www.amazon.co.jp/dp/4860431197/
モデル検査 初級編―基礎から実践まで4日で学べる (CVS教程)
https://www.amazon.co.jp/dp/4764955059/
NuSMVとSPINで記述している。
導入
brew install spin
Updating Homebrew...
==> Auto-updated Homebrew!
** snip **
==> Downloading https://homebrew.bintray.com/bottles/spin-6.4.8.high_sierra.bottle.tar.gz
######################################################################## 100.0%
==> Pouring spin-6.4.8.high_sierra.bottle.tar.gz
🍺 /usr/local/Cellar/spin/6.4.8: 5 files, 1MB
$ brew install xspin
Updating Homebrew...
==> Auto-updated Homebrew!
** snip **
==> Downloading https://homebrew.bintray.com/bottles/xspin-5.2.5.high_sierra.bottle.tar.gz
######################################################################## 100.0%
==> Pouring xspin-5.2.5.high_sierra.bottle.tar.gz
🍺 /usr/local/Cellar/xspin/5.2.5: 3 files, 192.2KB
SPINインストール手順
https://qiita.com/kannkyo/items/f2cc2c763f38bcbb4392
例 p18
systemalpha.pml
// systemalpha.pml
mtype ={on, off}
int a, b;
type sw;
int Na, Nb;
mtype New;
active prototype alpha(){
a = 0;
b = 0;
sw = off;
do
::true ->
if
::(b==1) -> Na = a
::else ->
if
::(a==0) -> Na = 1
::(a==1) -> Na = 2
::(a==2) -> Na = 0
fi
fi;
if
::(a==b) -> Nb = b
::else ->
if
::(b==0) -> Nb = 1
::(b==1) -> Nb = 2
::(b==2) -> Nb = 0
fi
fi;
if
::(a==2&&b==2) -> Nsw = on
::(a==1&&b==1) -> Nsw = off
::else -> Nsw = sw
fi;
atomic {
a = Na;
b = Nb;
sw = Nsw
}
od
}
$ spin systemalpha.pml
spin: systemalpha.pml:4, Error: syntax error saw 'an identifier' near 'type'
spin: systemalpha.pml:8, Error: syntax error saw 'an identifier' near 'prototype'
0 processes created
[](p -> <>q)
$ spin -f "[](p -> <>q)" systemalpha.pml
spin: systemalpha.pml.nvr:5, Error: undeclared variable: p saw '')' = 41'
$ xspin &
Run syntax check
Xspin Version 5.2.5 -- 17 April 2010
TclTk Version 8.5/8.5
spin -a -v pan_in
no syntax errors
"run LTL property parameter"
/*
* Formula As Typed:
* The Never Claim Below Corresponds
* To The Negated Formula !()
* (formalizing violations of the original)
*/
never { /* !() */
accept_init:
T0_init:
do
:: atomic { (! (())) -> assert(!(! (()))) }
od;
accept_all:
skip
}
"Run"
<starting verification>
spin -a -X -N pan.ltl pan_in
spin: pan.ltl:1, Error: syntax error saw ''[' = 91'
spin: pan.ltl:13, Error: syntax error saw '')' = 41'
spin: pan.ltl:13, Error: syntax error saw '')' = 41'
spin: pan_in.nvr:2, Error: aborting (ana_stmnt)
spin: 1 error(s) - aborting
child process exited abnormally
$ spin --h
use: spin [-option] ... [-option] file
Note: file must always be the last argument
-A apply slicing algorithm
-a generate a verifier in pan.c
-B no final state details in simulations
-b don't execute printfs in simulation
-C print channel access info (combine with -g etc.)
-c columnated -s -r simulation output
-d produce symbol-table information
-Dyyy pass -Dyyy to the preprocessor
-Eyyy pass yyy to the preprocessor
-e compute synchronous product of multiple never claims (modified by -L)
-f "..formula.." translate LTL into never claim
-F file like -f, but with the LTL formula stored in a 1-line file
-g print all global variables
-h at end of run, print value of seed for random nr generator used
-i interactive (random simulation)
-I show result of inlining and preprocessing
-J reverse eval order of nested unlesses
-jN skip the first N steps in simulation trail
-k fname use the trailfile stored in file fname, see also -t
-L when using -e, use strict language intersection
-l print all local variables
-M generate msc-flow in tcl/tk format
-m lose msgs sent to full queues
-N fname use never claim stored in file fname
-nN seed for random nr generator
-O use old scope rules (pre 5.3.0)
-o1 turn off dataflow-optimizations in verifier
-o2 don't hide write-only variables in verifier
-o3 turn off statement merging in verifier
-o4 turn on rendezvous optiomizations in verifier
-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)
-o6 revert to the old rules for interpreting priority tags (pre version 6.2)
-o7 revert to the old rules for semi-colon usage (pre version 6.3)
-Pxxx use xxx for preprocessing
-p print all statements
-pp pretty-print (reformat) stdin, write stdout
-qN suppress io for queue N in printouts
-r print receive events
-replay replay an error trail-file found earlier
if the model contains embedded c-code, the ./pan executable is used
otherwise spin itself is used to replay the trailfile
note that pan recognizes different runtime options than spin itself
-run (or -search) generate a verifier, and compile and run it
options before -search are interpreted by spin to parse the input
options following a -search are used to compile and run the verifier pan
valid options that can follow a -search argument include:
-bfs perform a breadth-first search
-bfspar perform a parallel breadth-first search
-dfspar perform a parallel depth-first search, same as -DNCORE=4
-bcs use the bounded-context-switching algorithm
-bitstate or -bit, use bitstate storage
-biterateN,M use bitstate with iterative search refinement (-w18..-w35)
perform N randomized runs and increment -w every M runs
default value for N is 10, default for M is 1
(use N,N to keep -w fixed for all runs)
(add -w to see which commands will be executed)
(add -W if ./pan exists and need not be recompiled)
-swarmN,M like -biterate, but running all iterations in parallel
-link file.c link executable pan to file.c
-collapse use collapse state compression
-noreduce do not use partial order reduction
-hc use hash-compact storage
-noclaim ignore all ltl and never claims
-p_permute use process scheduling order random permutation
-p_rotateN use process scheduling order rotation by N
-p_reverse use process scheduling order reversal
-rhash randomly pick one of the -p_... options
-ltl p verify the ltl property named p
-safety compile for safety properties only
-i use the dfs iterative shortening algorithm
-a search for acceptance cycles
-l search for non-progress cycles
similarly, a -D... parameter can be specified to modify the compilation
and any valid runtime pan argument can be specified for the verification
-S1 and -S2 separate pan source for claim and model
-s print send events
-T do not indent printf output
-t[N] follow [Nth] simulation trail, see also -k
-Uyyy pass -Uyyy to the preprocessor
-uN stop a simulation run after N steps
-v verbose, more warnings
-w very verbose (when combined with -l or -g)
-[XYZ] reserved for use by xspin interface
-V print version number and exit
参考文献
SPINインストール手順
https://qiita.com/kannkyo/items/f2cc2c763f38bcbb4392
モデル検査SPINと統合環境jSpinとispinの導入
https://qiita.com/nt_tn/items/60752a314392140e621a
仮想環境でSpinモデル検査
https://qiita.com/tokikaze0604/items/2a167ff54e2b9576b233
Is Parallel Programming Hard, And, If So, What Can You Do About It?
https://qiita.com/yohhoy/items/bf6cd447fe4964f95d3e
プログラミング言語教育のXYZ
https://qiita.com/kaizen_nagoya/items/1950c5810fb5c0b07be4
SWESTまとめ
https://qiita.com/kaizen_nagoya/items/62e56ae151554d6200c0
文書履歴
ver 0.10 初稿 20180318
ver 0.11 参考文献・文書履歴追記 20180411
ver. 0.12 ありがとう追記 20230508
最後までおよみいただきありがとうございました。
いいね 💚、フォローをお願いします。
Thank you very much for reading to the last sentence.
Please press the like icon 💚 and follow me for your happy life.