A.2.1 電話のスイッチング接続 - Model Base

更新日2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]

---

( a ) 述語を１つ追加してコマンドを起動することで、モデルをシミュレーションせよ

通話と接続に関する基本的なルールを 述語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つの不変条件を、述語calling と 述語conncection として定義する。

 --呼び出しに関する制約
 pred calling{
   --全ての接続には対応する要求があること（ただし、要求は接続が切れるまで消えないとする）
   all p: Phone | p.connects in p.requests
   }
 
 --接続に関する制約
 pred connection{
 --会議通話（１つの電話が複数の接続を持つ通話）はないこと
   --同時に接続の要求元と要求受けになる電話はない
   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
 }

インスタンスは発見できなかった。