「Promelaメモ1」の編集履歴（バックアップ）一覧はこちら

「Promelaメモ1」(2011/02/07 (月) 12:06:14) の最新版変更点

追加された行は緑色になります。

削除された行は赤色になります。

----
エラーが出て30秒以上なやんだところを覚え書き
----
その1
ガード条件内のinline展開は括弧をつけるとエラー？
|追記|ガード条件に副作用がある文は使えないとあるので、理由はそれ(多分)|
#highlight(linenumber,promela){{byte n = 0;

inline under1(){
  n < 1
}

active proctype P1(){
  if
    ::(under1()) -> printf("pass");
  fi;
} }}

エラー
#aa(blockquote){{spin: e1.pml:9, Error: syntax error	saw 'inline name' near 'under1'
}}

直る
#highlight(linenumber,promela){{byte n = 0;

inline under1(){
  n < 1
}

active proctype P1(){
  if
    ::under1() -> printf("pass");
  fi;
} }}

これは通る
#highlight(linenumber,promela){{byte n = 0;

active proctype P1(){
  if
    ::(n < 1) -> printf("pass");
  fi;
} }}

----
その2
大域変数への代入はプロセスの中で宣言しなければならない？
#highlight(linenumber,promela){{byte a;
a = 1;

active proctype P1(){
  true
} }}

エラー
#aa(blockquote){{spin: e1.pml:2, Error: syntax error	saw 'an identifier' }}

直す
#highlight(linenumber,promela){{byte a;

active proctype P1(){
  a = 1;
} }}

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

初期化は大域変数宣言と同時に
#highlight(linenumber,promela){{byte a = 1;

active proctype P1(){
  true;
} }}

----
エラーが出て30秒以上なやんだところを覚え書き
----
その1
ガード条件内のinline展開は括弧をつけるとエラー？
-追記
--ガード条件に副作用がある文は使えないとあるので、理由はそれ(多分)
#highlight(linenumber,promela){{byte n = 0;

inline under1(){
  n < 1
}

active proctype P1(){
  if
    ::(under1()) -> printf("pass");
  fi;
} }}

エラー
#aa(blockquote){{spin: e1.pml:9, Error: syntax error	saw 'inline name' near 'under1'
}}

直る
#highlight(linenumber,promela){{byte n = 0;

inline under1(){
  n < 1
}

active proctype P1(){
  if
    ::under1() -> printf("pass");
  fi;
} }}

これは通る
#highlight(linenumber,promela){{byte n = 0;

active proctype P1(){
  if
    ::(n < 1) -> printf("pass");
  fi;
} }}

----
その2
大域変数への代入はプロセスの中で宣言しなければならない？
#highlight(linenumber,promela){{byte a;
a = 1;

active proctype P1(){
  true
} }}

エラー
#aa(blockquote){{spin: e1.pml:2, Error: syntax error	saw 'an identifier' }}

直す
#highlight(linenumber,promela){{byte a;

active proctype P1(){
  a = 1;
} }}

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

初期化は大域変数宣言と同時に
#highlight(linenumber,promela){{byte a = 1;

active proctype P1(){
  true;
} }}