Model Base
A.2.1 電話のスイッチング接続
最終更新:
modelbase
更新日2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計/付録 A 練習問題 解答例 ]
( a ) 述語を1つ追加してコマンドを起動することで、モデルをシミュレーションせよ
通話と接続に関する基本的なルールを 述語basic で定義し、 つまらないインスタンスを避けるための環境設定を 述語environment で定義した。
sig Phone { requests: set Phone, connects: lone Phone } pred basic{ -- 通話に関する根本的な制約 -- 非反射的 no iden & connects -- 接続要求に関する根本的な制約 -- 非反射的 no iden & requests } pred environment{ -- 接続要求が存在する some requests -- 通話が存在する some connects } fact system{ basic and environment } run a{}
この程度のしばりでインスタンスを探せば、何でもありな感じになる。。。
接続要求してないのに通話が確立したり、かなりフリーダムな感じになった。
( b ) 次の2つの不変条件を追加せよ。1つは、全ての接続には対応する要求があること。もう1つは、会議通話はないこと。
2つの不変条件を、述語calling と 述語conncection として定義する。
--呼び出しに関する制約 pred calling{ --全ての接続には対応する要求があること(ただし、要求は接続が切れるまで消えないとする) all p: Phone | p.connects in p.requests } --接続に関する制約 pred connection{ --会議通話(1つの電話が複数の接続を持つ通話)はないこと --同時に接続の要求元と要求受けになる電話はない no (univ.connects & connects.univ) --複数の接続の要求受けになる電話はない #connects = #univ.connects } run b{ calling and connection } for 4
設問で要請された制約条件を入れると、ありがちなシステムの様子が見られる。
( c ) 通話転送機能を組み込んでみよ
上記のシステムの上に通話転送機能を構築してみる。
不変条件 fact system はそのまま引き継ぎ、通話転送機能を拡張した電話 PhoneF を導入する。
さらに、通話転送機能を持つシステムの基本的なルールを 述語basic2 で追加定義し、 つまらないインスタンスを避けるための環境設定を 述語environment2 で追加定義した。
sig PhoneF extends Phone{ forward: set Phone } pred basic2{ -- 転送に関する根本的な制約 -- 非反射的 no iden & forward } pred environment2{ -- 全ての電話は電話回線システムが提供する転送機能を活用できる Phone in PhoneF -- 誰かは転送機能を利用する some forward } fact system2{ basic2 and environment2 }
次に、転送による接続に関する不変条件を 述語forwarding で定義する。
--転送による接続に関する制約 pred forwarding{ -- p.forward は、空でないならば、p への通話が転送されるべき電話を表す all disj p,q: Phone | some p.forward =>(p.forward in q.connects => p in q.requests) }
最後に、通話転送機能を構築するために 前述の2つの不変条件、述語calling と 述語conncection を改訂する。
--呼び出しに関する制約 改定版 pred calling'{ --全ての接続には対応する要求があること(ただし、要求は接続が切れるまで消えないとする) all p: Phone | --転送機能を利用している電話と接続する場合の制約 (p.connects not in p.requests and some q: p.requests | p.connects in q.forward) or --転送機能を利用しない電話と接続する場合は、従来と同じ (p.connects in p.requests and no p.connects.forward) } --接続に関する制約 改定版 pred connection'{ connection forwarding }
面白そうな通話転送の例
calling' と connection' を満たすインスタンスを観察してみる。
ビジュアライザでどの電話が転送元になったかが分かる(転送元の電話に$FWがマークされる)ように、関数FWを定義しておく。
--ビジュアライザ観察用 --転送元 fun FW: set Phone{ {src: Phone | let dst = src.forward{ some dst some p: Phone | src in p.requests and some p.connects & dst } } } run c{ calling' and connection'}for 4
Fig A.2.1.c-1
電話1から電話2へかけて、転送先の電話0と通話が成立している。
。。。
退屈なインスタンスが多いので、
#connects > 1
を 述語environment2 に追加すると、やや複雑な例が出てくる
Fig A.2.1.c-2
電話0から(電話0の転送先の)電話3へかけて、通話が成立している。
Fig A.2.1.c-3
電話0と電話3は通話中であるが、
電話1から(通話中の)電話0へかけて、電話0の転送の電話2と電話1で通話が成立している。
仮に電話0に$FWの表示が無かったならば、転送でなく電話1が直接電話2へ電話をかけたことを意味する。
さらに複雑ななインスタンスを見たいので、
#FW > 1
を 述語environment2 に追加する。
Fig A.2.1.c-4
電話1から電話0にかけて電話3へ転送され、電話1と電話3の通話が成立。
電話2から電話3にかけて電話0へ転送され、電話2と電話0の通話が成立。
Fig A.2.1.c-5
電話3からの呼び出しが転送され、電話3と電話2の通話が成立しているのだが、 電話0、電話1のどちらが転送したかは特定されない。
転送先で転送されるパターンの述語を用意して、環境述語にセットしてみると、
pred doubleForwarding{ #connects = 1 #forward = 2 #FW = 2 one f,f': FW | f->f' in forward }
インスタンスは発見できなかった。