• List of Backups
• View the diff.
• View the diff current.
• View the source.
• Go to システム検証例.
  • 1 (2009-12-30 (Wed) 17:32:33)

単純化エレベーターモデルの検証 †

pn(1).//乗客の数
fn(2).//フロアの数


//フロアの生成
fn(F) :- F0=F-1,F>0 | fn(F0),
{ f(F0),btn(false).
 //乗客の出入り
 p,elv{open(1),$p} :- elv{p,open(1),$p}.
 elv{p,open(1),$p} :- p,elv{open(1),$p}.
}.

//乗客の生成
pn(P),{ f(F),$p,@p } :- P0=P-1,P>0,int(F) | pn(P0),{ p,f(F),$p,@p }.

//エレベーターの生成
pn(0),fn(0),{ f(F),$p,@p } :- int(F) | { elv{open(1),act(null),to(0)},f(F),$p,@p }.



//乗客の動作

//フロアにいる乗客がボタンを押す
{ p,btn(false),$p,@p } :- { p,btn(true),$p,@p }.

//エレベーター中にいる乗客がボタンを押す
{ elv{p,to(0),$q[]},$p1[],@p1 },{ f(F),$p2[],@p2 }
 :- int(F) | { elv{p,to(F),$q[]},$p1[],@p1 },{ f(F),$p2[],@p2 }.


//エレベーターの動作

//エレベーターのドアを閉める
{ elv{open(Op),act(close),$q},$p,@p } :- int(Op) | { elv{open(0),act(null),$q},$p,@p }.

//エレベーターのドアをあける
{ elv{open(Op),act(open),$q},$p,@p } :- int(Op) | { elv{open(1),act(null),$q},$p,@p }.

//エレベーターの移動
{ elv{act(move(M)),$q[] },$p1[],@p1 },{ f(F),$p2[],@p2 }
 :- M=:=F | { $p1[],@p1 },{ elv{act(null),$q[]},f(F),$p2[],@p2 }.

//エレベーターの不移動
{ f(F),elv{act(move(M)),$q[] },$p[],@p }
 :- F=:=M | { f(F),elv{act(null),$q[]},$p[],@p }.


//コントローラー
cnt(null).

//ドアを閉じる命令を送信(エレベーター内から受信)
cnt(null),{ elv{act(null),to(T),$q[]},$p[],@p }
 :- int(T) | cnt(move(T)),{ elv{act(close),to(T),$q[]},$p[],@p }.

//ドアを閉じる命令を送信(フロアのボタンから受信)
cnt(null),{ f(F),btn(true),$p1[],@p1 },{ elv{act(null),$q[]},$p2[],@p2 }
 :- int(F) | cnt(move(F)),{ f(F),btn(true),$p1[],@p1 },{ elv{act(close),$q[]},$p2[],@p2 }.

//移動命令を送信
cnt(move(F)),{ elv{act(null),$q[]},$p[],@p }
 :- int(F) | cnt(end),{ elv{act(move(F)),$q[]},$p[],@p }.

//ドアを開く命令を送信
cnt(end),{ btn(B),elv{act(null),to(T),$q[]},$p[],@p }
 :- unary(B),int(T) | cnt(null),{ btn(false),elv{act(open),to(0),$q[]},$p[],@p }.

検証項目 †

エレベーターはドアを開けたまま動くことはない

シンボル定義：p = { elv{open(1),act(move(M)),$q},$p,@p } :- int(M)
仕様：!<>p

これを調べてみるとこのモデルではそのようなことがないことが分かる