1
1

# SPIN(simple promela interpreter)入門

Last updated at Posted at 2018-03-18

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 **

######################################################################## 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 **

######################################################################## 100.0%
==> Pouring xspin-5.2.5.high_sierra.bottle.tar.gz
🍺  /usr/local/Cellar/xspin/5.2.5: 3 files, 192.2KB

# 例 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
-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:
-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
-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
-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と統合環境jSpinとispinの導入
https://qiita.com/nt_tn/items/60752a314392140e621a

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

# 文書履歴

ver 0.10 初稿 20180318
ver 0.11 参考文献・文書履歴追記 20180411
ver. 0.12 ありがとう追記　20230508

## 最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。