ソフトウェア関連の個人的備忘録
ソフトウェア関連の個人的備忘録

Promelaメモ1

エラーが出て30秒以上なやんだところを覚え書き
その1
ガード条件内のinline展開は括弧をつけるとエラー？
  • 追記
    • ガード条件に副作用がある文は使えないとあるので、理由はそれ(多分)
  1. byte n = 0;
  2.  
  3. inline under1(){
  4.   n < 1
  5. }
  6.  
  7. active proctype P1(){
  8.   if
  9.     ::(under1()) -> printf("pass");
  10.   fi;
  11. }

エラー
spin: e1.pml:9, Error: syntax error saw 'inline name' near 'under1'

直る 
  1. byte n = 0;
  2.  
  3. inline under1(){
  4.   n < 1
  5. }
  6.  
  7. active proctype P1(){
  8.   if
  9.     ::under1() -> printf("pass");
  10.   fi;
  11. }

これは通る 
  1. byte n = 0;
  2.  
  3. active proctype P1(){
  4.   if
  5.     ::(n < 1) -> printf("pass");
  6.   fi;
  7. }

その2
大域変数への代入はプロセスの中で宣言しなければならない？ 
  1. byte a;
  2. a = 1;
  3.  
  4. active proctype P1(){
  5.   true
  6. }

エラー
spin: e1.pml:2, Error: syntax error saw 'an identifier'

直す 
  1. byte a;
  2.  
  3. active proctype P1(){
  4.   a = 1;
  5. }

大域変数への代入という動作はプロセスの状態を変えるのでプロセス内に記述する。
大域変数の初期化に関してはプロセスの状態を変えないので大域変数宣言と同時に設定できる。
ということだと思う。

初期化は大域変数宣言と同時に 
  1. byte a = 1;
  2.  
  3. active proctype P1(){
  4.   true;
  5. }
「Promelaメモ1」をウィキ内検索
最終更新：2011年02月07日 12:06