cloverrose's blog

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

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

SPINは配列が使えます。

int requests[100];

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

配列の要素全てを同じ値で初期化する方法は次のとおりです。

int requests[100] = -1;

初期化の挙動を確かめてみる

初期値を指定して定義した場合にも、実は最初に0が設定されて、それから指定した値(NONE)に設定しているのかも?
という疑惑を振り払うために以下のプログラムで検証。

requests[0]=0;

という式を追加しなければ反例は出ないので、疑惑は晴れた。

#define SIZE 100
#define NONE -1
int requests[SIZE] = NONE;

init{
  int i=0;
  do
  ::(i<SIZE) -> printf("requests[%d]: %d\n", i, requests[i]);i++;
  ::else -> break;
  od;
  /* requests[0]=0; */ /* add this statement to check */
}

never  {    /* <>(requests[0]==0) */
T0_init:
	if
	:: ((requests[0]==0)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}