CVS教程(1) 4日で学ぶモデル検査 初級編 (著:産業技術総合研究所システム検証研究センター

正誤表

Updated: 2006/10/03
ページ 該当箇所
i 1行目 在化したため” 在化したため”
iv 下から4行目 6.例題:並行システムと排他制御 6.例題:並行システムと排他制御
22 10行目 OKボタンをクリックすると” Runボタンをクリックすると”
46 1行目 (d1+d2=0,3 のとき) (d1+d2=0 のとき)
48-50 モデルのコードの変数
”a”をすべて”d”に置き換える

---- MiniLifeGame
MODULE main

VAR	         ---- 変数宣言部
 a1:{0,1};
 a2:{0,1};
 a3:{0,1};
 a4:{0,1};
 a5:{0,1};
 a6:{0,1};
 a7:{0,1};
 a8:{0,1};

DEFINE	         ----「御近所さん」のようす
 b1:=a1+a2;
 b2:=a1+a2+a3;
 b3:=   a2+a3+a4;
 b4:=      a3+a4+a5;
 b5:=         a4+a5+a6;
 b6:=            a5+a6+a7;
 b7:=               a6+a7+a8;
 b8:=                  a7+a8;

ASSIGN		         ---- 遷移系記述部
		     ---- 初期値
 init(a1):=1;
 init(a2):=0;
 init(a3):=0;
 init(a4):=0;
 init(a5):=0;
 init(a6):=0;
 init(a7):=0;
 init(a8):=0;

		         ---- 遷移
 next(a1) := case
              b1=0: 0;
              b1=1: 1;
              b1=2: {0,1};
              b1=3: 0;
              1: a1;
            esac;

 next(a2) := case
             b2=0: 0;
             b2=1: 1;
             b2=2: {0,1};
             b2=3: 0;
             1: a2;
           esac;

 next(a3) := case
             b3=0: 0;
             b3=1: 1;
             b3=2: {0,1};
             b3=3: 0;
             1: a3;
           esac;

 next(a4) := case
             b4=0: 0;
             b4=1: 1;
             b4=2: {0,1};
             b4=3: 0;
             1: a4;
           esac;

 next(a5) := case
             b5=0: 0;
             b5=1: 1;
             b5=2: {0,1};
             b5=3: 0;
             1: a5;
           esac;

 next(a6) := case
             b6=0: 0;
             b6=1: 1;
             b6=2: {0,1};
             b6=3: 0;
             1: a6;
           esac;

 next(a7) := case
             b7=0: 0;
             b7=1: 1;
             b7=2: {0,1};
             b7=3: 0;
             1: a7;
           esac;

 next(a8) := case
             b8=0: 0;
             b8=1: 1;
             b8=2: {0,1};
             b8=3: 0;
             1: a8;
           esac;

---- MiniLifeGame
MODULE main

VAR	         ---- 変数宣言部
 d1:{0,1};
 d2:{0,1};
 d3:{0,1};
 d4:{0,1};
 d5:{0,1};
 d6:{0,1};
 d7:{0,1};
 d8:{0,1};

DEFINE	         ----「御近所さん」のようす
 b1:=d1+d2;
 b2:=d1+d2+d3;
 b3:=   d2+d3+d4;
 b4:=      d3+d4+d5;
 b5:=         d4+d5+d6;
 b6:=            d5+d6+d7;
 b7:=               d6+d7+d8;
 b8:=                  d7+d8;

ASSIGN		         ---- 遷移系記述部
		     ---- 初期値
 init(d1):=1;
 init(d2):=0;
 init(d3):=0;
 init(d4):=0;
 init(d5):=0;
 init(d6):=0;
 init(d7):=0;
 init(d8):=0;

		         ---- 遷移
 next(d1) := case
              b1=0: 0;
              b1=1: 1;
              b1=2: {0,1};
              b1=3: 0;
              1: d1;
            esac;

 next(d2) := case
             b2=0: 0;
             b2=1: 1;
             b2=2: {0,1};
             b2=3: 0;
             1: d2;
           esac;

 next(d3) := case
             b3=0: 0;
             b3=1: 1;
             b3=2: {0,1};
             b3=3: 0;
             1: d3;
           esac;

 next(d4) := case
             b4=0: 0;
             b4=1: 1;
             b4=2: {0,1};
             b4=3: 0;
             1: d4;
           esac;

 next(d5) := case
             b5=0: 0;
             b5=1: 1;
             b5=2: {0,1};
             b5=3: 0;
             1: d5;
           esac;

 next(d6) := case
             b6=0: 0;
             b6=1: 1;
             b6=2: {0,1};
             b6=3: 0;
             1: d6;
           esac;

 next(d7) := case
             b7=0: 0;
             b7=1: 1;
             b7=2: {0,1};
             b7=3: 0;
             1: d7;
           esac;

 next(d8) := case
             b8=0: 0;
             b8=1: 1;
             b8=2: {0,1};
             b8=3: 0;
             1: d8;
           esac;
50-51 4.4 検査項目 NuSMVとSpinに共通のため、NuSMVであることを示すページ脇の飾り線を削除。
58 5.3コード【NuSMV版】
モデルのコード上の文字部分
”モデル部分のコードは以下のようになります。”
”モデル部分のコードは以下のようになります。

追記↓

(注)
NuSMVのモデルには、P57,58で説明していない変数として RbSMとWoSMが使われています。これらの変数は、船が岸にいるときに次に船に乗ろうとするウサギちゃんとオオカミくんの数をそれぞれ表しています。” 

76-77 6.5 コード【NuSMV版】
モデルのコードの中の変数
			----セマフォ
MODULE main

VAR
  run         : {1,2};
  semaphore   : boolean;
  proc1_state :{idle, entering,critical, exiting};
  proc2_state :{idle, entering,critical, exiting};


ASSIGN
  init(run) :={1,2};
  next(run) :={1,2};

  init(proc1_state) := idle;
  next(proc1_state) :=
    case
      run = 1 & proc1_state = idle : {idle, entering};
      run = 1 & proc1_state = entering & !semaphore : critical;
      run = 1 & proc1_state = critical : {critical, exiting};
      run = 1 & proc1_state = exiting : idle;
      1                                         : proc1_state;
    esac;

  init(proc2_state) := idle;
  next(proc2_state) :=
    case
      run = 2 & proc2_state = idle: {idle, entering};
      run = 2 & proc2_state = entering &!semaphore : critical;
      run = 2 & proc2_state = critical : {critical, exiting};
      run = 2 & proc2_state = exiting : idle;
      1                                          : proc2_state;
    esac;

  init(semaphore) := 0;
  next(semaphore) :=
    case
      run = 1 & proc1_state = entering : 1;
      run = 1 & proc1_state = entering : 0;
      run = 2 & proc2_state = entering : 1;
      run = 2 & proc2_state = entering : 0;
      1                                : semaphore;
    esac;			
			----セマフォ
MODULE main

VAR
  run         : {1,2};
  semaphore   : boolean;
  state_p1 :{idle, entering,critical, exiting};
  state_p2 :{idle, entering,critical, exiting};


ASSIGN
  init(run) :={1,2};
  next(run) :={1,2};

  init(state_p1) := idle;
  next(state_p1) :=
    case
      run = 1 & state_p1 = idle : {idle, entering};
      run = 1 & state_p1 = entering & ; !semaphore : critical;
      run = 1 & state_p1 = critical : {critical, exiting};
      run = 1 & state_p1 = exiting : idle;
      1                                         : state_p1;
    esac;

  init(state_p2) := idle;
  next(state_p2) :=
    case
      run = 2 & state_p2 = idle: {idle, entering};
      run = 2 & state_p2 = entering & !semaphore : critical;
      run = 2 & state_p2 = critical : {critical, exiting};
      run = 2 & state_p2 = exiting : idle;
      1                                          : state_p2;
    esac;

  init(semaphore) := 0;
  next(semaphore) :=
    case
      run = 1 & state_p1 = entering : 1;
      run = 1 & state_p1 = exiting : 0;
      run = 2 & state_p2 = entering : 1;
      run = 2 & state_p2 = exiting : 0;
      1                                : semaphore;
    esac;
96 コード中17行目 init(W3) : =a; init(W3) : =a;
init(S_Place) : =a; ←追記
101 11行目 ”●σでPUQが成り立つ⇔0以上のある自然数iでσ(i)でPが成り立つ、かつ0≦j<iのすべての自然数jでσ(j)でQが成り立つ ”●σでPUQが成り立つ⇔0以上のある自然数iに対して、σ(i)でQが成り立つ、かつ0≦j<iのすべての自然数jに対してσ(j)でPが成り立つ
107 表の第一列ラベル 記号 様相記号
113 下から6行目 ”σ(6)の先頭ではp=0が真にならないので(正)” ”σ(4)の先頭ではp=0が真にならないので(正)”
114 13行目 ”σ(6)の先頭ではp=1が真になるので(正)” ”σ(4)の先頭ではp=1が真になるので(正)”
116 下段「P115の課題の解答」の4行目 ”時点6で初めて・・・、時点7からはずっと・・・” ”時点4で初めて・・・、時点5からはずっと・・・”
116 下段「P115の課題の解答」の最後の行 ”i=6とすると” ”i=4とすると”
121 コード中5行目 ”bool err;” 削除

(独)産業技術総合研究所 システム検証研究センター
Copyrights (C) 2005-2006 AIST Research Center for Verification and Semantics, All Rights Reserved.