導入

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