Basic LOTOS

■Basic LOTOS

1. Labelled Transition System (LTS)

2. toolbox による LTS生成

3. Basic LOTOS による操作の記述例

4. 等価性のチェック

5. 再び自販機の例

練習問題4-1

参考資料・リンク集

 

 

BLAによるプロセス定義を行うと、Basic LOTOSによるプロセス定義ファイルが作成できる。LOTOS独特の記述方法(gate hiding など)も存在する。CADP toolboxを用いて、Basic LOTOSのプロセストレースを行い、Labelled Transition System (LTS)に基づいたプロセスグラフの生成を行うことができる。また、生成したLTS(プロセスグラフ)の等価性チェック、ならびに種々の等価性を利用したグラフ縮約(reduction)ができる。

この章で学習する内容は以下の5つである。最後に演習問題1を与える。

1. Labelled Transition System (LTS)
2. toolbox による LTS生成
3. Basic LOTOS による操作の記述例
4. 等価性のチェック
5. 再び自販機の例

練習問題4-1


●Labelled Transition System (LTS)

通常の有限状態機械(オートマトン)では、状態値間の変化と、各状態に付けられた性質(Atomic Proposition)に基づいて、システムのモデル化を行っている。

プロセスによるモデル化では、"状態値"は、もはや、"その後実行すべきプロセスラベルの列"に過ぎず、プロセスのActionによる遷移、つまり状態間のラベル付きトランジション(Lebelled Transition)の働きが重要となっている。

初期状態からのプロセスモデルの振る舞いをトレースしたものが、プロセスグラフであった。以後、このプロセスグラフを、下記に定義する Labelled Transition System (LTS) で表現することとする。

1.1 LTSの定義
1.2 LTSの例


1.1 LTSの定義

Definition of Labelled Transition System (LTS) (Def-4.1):

A Labelled Transition System (LTS) is a tuple of (S,A,T,s0), where

S : finite, nonempty set of states
A : finite, nonempty set of transition labels (or actions)
T ⊆ S x A x S : transition relation (or arcs)
s0 ∈ S : initial state

L,N をある自然数とし、猫+ をL個のアルファベットの"空でない"列全体とする。このとき、
S = {0, 1, … , N-1}, A ⊆ 猫+, s0 = 0 としても、上記の定義について一般性を失わない。

|*|を 集合* のサイズ とする。このとき、上記のLTSの定義により、
|S|:状態数(=N)、|A|:ラベル数(<|2^L|)、|T|:トランジション数(≦|S|^2 * |A|)
となる。

大雑把な見積もりを行うと、このLTSの初期状態から始まる全てのpathを調べあげる(トレース)アルゴリズムの計算量は、高々 O(|S|+|T|) である。



1.2 LTSの例

<例1>

Process P1 := A;B;$ のプロセスグラフ、LTS(P1) を上記の定義Def-4.1に従って構成してみる。

LTS(P1) = (S,A,T,s0), where

S = {0,1,2},
A = {A,B,exit},
T = {(0,A,1),(1,B,2),(2,exit,3)}, and
s0 = 0 .

※ terminating process '$' は、Basic LOTOS では 'exit' である。

Aldebaran-automaton形式では、LTS(P1) は以下のように記述される。

時に、第1行目は des (s0, |T|, |S|) という意味である。
第2行目以降、transition relations : T が |T|行、列挙される。

LTS(P1)
----------------
des (0, 3, 4)
(0, A, 1)
(1, B, 2)
(2, exit, 3)
----------------

<例2>

Process P2 := A;B;$ [] A;C;$

LTS(P2) = (S,A,T,s0), where

S = {0,1,2,3,4,5},
A = {A,B,C,exit},
T = {(0,A,1),(1,B,3),(3,exit,5),
(0,A,2),(2,C,4),(4,exit,5)}, and
s0 = 0 .

LTS(P2)
----------------
des (0, 6, 6)
(0, A, 1)
(0, A, 2)
(1, B, 3)
(2, C, 4)
(3, exit, 5)
(4, exit, 5)
----------------


●toolbox による LTS生成

LOTOS仕様に基づいたプロセスグラフであるLTSを、計算機を用いて生成する。
LTS生成には、CADP toolbox のアプリケーションである "caesar" を使用する。

※caesarのon-line manual pageはここからどうぞ

(いまのところBasic-)LOTOS仕様のファイルは、通常のテキストファイル形式で、拡張子が .lotos あるいは .lot なものである。
caesar が処理可能なLOTOSファイルの形式は、これまでに説明してきたBLA記法に殆ど準じている。以下の解説記事などのドキュメントを先に読んでおこう。

Introduction to the ISO Specification Language LOTOS ←お勧め!(local copy)
Tommaso Bolognesi and Ed Brinksma
Computer Networks and ISDN Systems 14(1) 25-59
January 1987, 66 pages

An Introduction to LOTOS: Learning by Examples (local copy)
L. Logrippo, M. Faci, M. Haj-Hussein
Computer Networks and ISDN Systems 23(5) 325-342
Errata in 25(1) 99-100
1999, 34 pages

なお、LOTOS言語仕様書は ISO-8807(1989) として公開されている(有料)

ISO International Standard 8807:1989
Information processing systems - Open Systems Interconnection -
LOTOS - A formal description technique based on the temporal ordering of observational behaviour
Geneva, September 1989
An annex of the LOTOS standard provides a user-friendly tutorial.

2.1 LTSのフォーマット
2.2 caesar による LTS生成 の例


2.1 LTSのフォーマット

LTSのファイルフォーマットとしては、以下の2つを取り上げる。
他に様々なファイル交換形式が存在するが、これは bcg_ioアプリケーションを用いて相互変換することができる。

(1)Aldebaran automaton形式(.aut)
(2)Binary Coded Graph(BCG)形式 (.bcg)

automaton形式はテキストファイルのため人間にとって可読性が良いが、1トランジションあたり10バイト程度を要するため、ファイルシステム上での容量が大きい。また、各種処理プログラムでLTSとして読み込みを行う際に、前解析処理が必要で、処理速度上問題となる。

他方、BCG形式は、LTSのプロセスグラフをそのまま、一定のバルク形式で格納していったものであり、人間は直接読むことができない。その代わりに、ファイルシステム上での容量が比較的小さく、また各種プログラムで読み込む際に、用意されているBCG用ライブラリを呼び出すだけでメモリ上へLTSを展開することが可能で、処理上有利である。

 


2.2 caesar による LTS生成 の例

先述の例4-1のプロセス定義を、Basic-LOTOSファイルとして書き、caesarアプリケーションを用いてトレースし、LTS生成を実際に行ってみる。


2.2.1 LOTOSファイルの作成(例4-1)

例4-1のプロセス定義のために、以下のようなLOTOSファイルを作成する。
適当なテキストエディタで作成し、exa4_1.lotos というファイル名で保存する。

exa4_1.lotos (Process P1 := A;B;$)

specification exa4_1[a,b] : exit

behaviour

a; b; exit

endspec

※注意点: CADP toolbox では、全般に渡って、識別子として英大文字と小文字を区別しない。(例: coffee と COFFEE は同じラベルと見なされる。)

LOTOSファイルは、specification 〜 endspec のブロック内部に、その spec が必要なサブプロセスの定義を process 〜 endproc ブロックで定義していく。

第1行目の exa4_1[a,b] のうち、exa4_1 は単なるspec名であり、何か分かり易い名前を書いておけばよい。 [a,b] は、そのspecを外側から見た場合の「入出力インターフェース」のようなものである(正確には gate という)。

続いて : exit という記述があるが、これは、以下の behaviour から定義されるプロセス(のインスタンス)が、正常に終了すること(terminating)を期待している。永遠に処理が終らないことが期待される場合には noexit と書く。

behaviour に続いて、このspecに対する実際の プロセス(のインスタンス)の定義を行う。この例では、サブプロセス定義はないので、そのまま BLA記法の a;b;$ に相当する、 a; b; exit を一行に列挙した。exit の後ろにはセミコロンは不要である。


2.2.2 caesarによるLTS生成(その1)

exa4_1.lotos を、caesarアプリケーションを用いてトレースし、LTS生成を行う。
まず、出力形式として(1)Aldebaran automaton形式(.aut)を指定して生成を行ってみる。

(caesarのコマンドライン引数の詳細についてはon-line manual pageを参照のこと)

LOTOS spec. → automaton形式でLTS生成

$ caesar -aldebaran exa4_1.lotos

-- caesar 6.1 -- Hubert Garavel (INRIA Rhone-Alpes) --

caesar: syntax analysis of ``exa4_1''
caesar: semantic analysis of ``exa4_1''
caesar: - gates binding
caesar: - processes binding
caesar: - types binding
caesar: - signature analysis
caesar: - sorts binding
caesar: - variables binding
caesar: - operations binding
caesar: - functionality analysis
caesar: restriction of ``exa4_1''
caesar: expansion of ``exa4_1''
caesar: type survey of ``exa4_1''
caesar: generation of ``exa4_1''
caesar: optimization of ``exa4_1''
caesar: simulation of ``exa4_1''
caesar: - simulator production
caesar: - simulator compilation
caesar: - simulator execution
caesar: - graph dump for ``exa4_1'' using ``aldebaran'' format

正常にLTS生成が終了すると、exa4_1.aut というファイル名で、automaton形式のプロセスグラフが出力されている。これはテキストファイルなので、catコマンドなどで容易に観察することができる。前節の例1、LTS(P1)と同等の結果が得られていることが判る。

$ cat exa4_1.aut

des (0, 3, 4)
(0, A, 1)
(1, B, 2)
(2, exit, 3)


2.2.3 caesarによるLTS生成(その2)

次に、exa4_1.lotos を、caesarによってトレースし、出力形式として (2)BCG形式(.bcg)を指定して生成を行ってみる。

LOTOS spec. → BCG形式でLTS生成

$ caesar -bcg exa4_1.lotos

-- caesar 6.1 -- Hubert Garavel (INRIA Rhone-Alpes) --

caesar: syntax analysis of ``exa4_1''
caesar: semantic analysis of ``exa4_1''
caesar: - gates binding
caesar: - processes binding
caesar: - types binding
caesar: - signature analysis
caesar: - sorts binding
caesar: - variables binding
caesar: - operations binding
caesar: - functionality analysis
caesar: restriction of ``exa4_1''
caesar: expansion of ``exa4_1''
caesar: type survey of ``exa4_1''
caesar: generation of ``exa4_1''
caesar: optimization of ``exa4_1''
caesar: simulation of ``exa4_1''
caesar: - simulator production
caesar: - simulator compilation
caesar: - simulator execution
caesar: - graph dump for ``exa4_1'' using ``bcg'' format

正常にLTS生成が終了すると、exa4_1.bcg というファイル名で、BCG形式のプロセスグラフが出力されている。これはバイナリファイルなので、直接読むことはできない。

プロセストレースグラフとして了解性の高い表示を得るために、bcg_drawアプリケーションを用いて観察してみる。これは、BCG形式ファイルを解析し、下→上側に向かって、state番号の若い順→トランジションの遷移の状況に応じて、"プロセス木"を現出させるためのものである。グラフの解析後、中間的なPostscriptファイルを出力し、内部で ghostview を起動してGUIへ表示する。

$ bcg_draw exa4_1.bcg

※PDFファイルはここをクリック!

図4-1: exa4_1.bcg を bcg_draw で表示した例

前節の例4-1、LTS(P1)のプロセスグラフと同等の結果が得られている。

トランジションラベルが重なって判読しにくい場合には、bcg_editアプリケーションによってBCGファイルを読み込み、分かり易いように整形しながら観測すると良い

※bcg_editにより、出力されたPostscriptファイルの「編集」が可能である。しかし、これは人間が綺麗に見たいことが目的であり、元のLTSが変化している訳ではないので注意。


2.2.4 プロセスのインスタンスを有するLOTOSファイルの作成(例4-1a)

例4-1のプロセス定義について、プロセス P1 を定義し、そのインスタンスを spec として保持するような、LOTOSファイルを作成してみる。

適当なテキストエディタで作成し、exa4_1a.lotos というファイル名で保存する。

exa4_1a.lotos (Process P1 := A;B;$)

specification exa4_1a[a,b] : exit

behaviour

P1[a,b]

where

process P1 [one, two] : exit :=

one; two; exit

endproc

endspec

process 〜 endproc ブロックにより、Process P1 の"定義"を行う。Process P1 [one,two] ではプロセス名として P1 、このプロセスの外から見たインターフェース(正確には gate)として one, two を有することを定義している。これはまだ定義をおこなっただけで、実際のインスタンスは、後述の behaviour セクション内で行う。

次の : exit は、このプロセスが正常に終了することが期待されていることを示す。(後に見るように、プロセスを呼び出して正常終了した後、何らかの"返り値"を得られるようにすることも可能である。これはプロセスを"関数"のように扱う方法である。この場合、gate列とは別に、内部で生成したgate(例えば VAL )によって、exit(VAL) のように書く)。

最後の := は、プロセス名 P1 は、:= 以下のプロセス列によって定義されることを示している。

specification 〜 endproc ブロックの、behaviour セクションでは、プロセスP1のインスタンス化を行う。インスタンス化のためには、実際にspecの外側から観測可能なgateを"引数"にして、spec内に現出させる。


●Basic LOTOS による操作の記述例

以下に、3種のプロセス操作に関するLOTOSによる記述例について取り挙げる。
caesar が処理可能なLOTOSファイルの形式は、これまでに説明してきたBLA記法に殆ど準じている。

ここでLOTOSの文法の全てを取り扱うのは容易でないので、このドキュメントなどを先に読んでおこう。

3.1 (非決定的)選択動作(Choice / P [] Q)
3.2 再帰(Recursion / Y := T >> Y)
3.3 並列化構成(Parallel Composition / P|[G]|Q)


3.1 (非決定的)選択動作(Choice / P [] Q)

2つのプロセスP,Qのchoice P [] Q は、LOTOSにおいても同様に書けばよい。

<例4-2>

coffeeかteaを選択すると、それが販売されて終了するようなプロセス VMa をLOTOSで作成してみる。coffeeとteaの間で優先順位はない。また、この2つしか販売しない。

Process VMa := coffee;dispence;$ [] tea;dispence;$

specification VMa [coffee,tea,dispence] : exit

behaviour

coffee; dispence; exit
[]
tea; dispence; exit

endspec

<例4-3>

Process P2 := a;b;$ [] a;c;$ について、これを P2 := P1[a,b] [] P1[a,c] の2つのプロセスのchoice であると見做す。このLOTOSファイルについて、例4-1aのプロセス P1 の定義を再利用し、そのインスタンスをchoiceによって結合した spec として保持するような、LOTOSファイルを作成してみよう。

例4-1aのプロセスP1の定義を利用して、それをchoiceで結合した。

exa4_3.lotos (Process P2 := a;b;$ [] a;c;$)

specification exa4_3[a,b,c] : exit

behaviour

P1[a,b]
[]
P1[a,c]

where

process P1 [one, two] : exit :=

one; two; exit

endproc

endspec


3.2 再帰(Recursion / Y := T >> Y)

プロセスTのterminating後、ラベルYへ戻るようなRecursion Y := T >> Y は、LOTOSにおいても同様に書けばよい。

<例4-3>

1.3節で取り挙げた、プッシュボタンを押すと出力がon/offされるプロセス PBL を定義してみる。最初にpushされる以前の出力は不定である。永遠に繰り返すことが期待されているので、spec は noexit である。

Process PBL := *[push;on;push;off]

specification PBL [push,on,off] : noexit

behaviour

PBL_BODY[push,on,off]

where

process PBL_BODY [push,out1,out2] : noexit :=

push; out1; push; out2;
PBL_BODY[push,out1,out2]

endproc

endspec

<例4-4>

2.4節・例2-7で取り挙げた、coinが挿入された後、candy か toffeeの商品選択を行うと、その商品が販売され、最初に戻る、というようなプロセス VMb について、そのLOTOSファイルを作成してみよう。

P1 := coin;(candy;$ [] toffee;$)
P2 := dispence; P1

VMb := P1>>P2
= (coin;(candy;$ [] toffee;$)) >> (dispence; VMb)
= coin;(candy;dispence;VMb [] toffee;dispence;VMb)

いくつかの書き方が存在するが、以下の記述例では、P1 と P2 の逐次合成を用いたRecusionを行った。当然のことながら、spec は noexit である。

Process VMb

specification VMb [coin,candy,toffee,dispence] : noexit

behaviour

VM_BODY[coin,candy,toffee,dispence]

where

process VM_BODY [coin,item1,item2,dispence] : noexit :=

(
coin;
(
item1; exit
[]
item2; exit
)
)
>> ( dispence; VM_BODY[coin,item1,item2,dispence] )

endproc

endspec

 


3.3 並列化構成(Parallel Composition / P|[G]|Q)

プロセス P,Q の gate G による並列化構成 P|[G]|Q の記法は、LOTOSにおいても同様である。

3.3.1 同期化ラベル gate G の列を用いた例 P |[g1,g2,...]| Q

<例4-5>
Process P := a;b;d;$ |[a,d]| a;c;d;$ のような 同期化ラベル L={a,d} による並列化構成をLOTOSで記述してみよう。

exa4_5.lotos (Process P := a;b;d;$ |[a,d]| a;c;d;$)

specification exa4_5[a,b,c,d] : exit

behaviour

a; b; d; exit
|[a,d]|
a; c; d; exit

endspec
3.3.2 Full-Synchronizationの例 P || Q

不可観測のinternal action i を含むプロセスの並列化構成について、Full-Synchronizationを用いて以下のような構成が考えられる。

<例4-6>

exa4_6.lotos (Process P := a;i;i;b;$ || i;a;i;b;$)

specification exa4_6[a,b] : exit

behaviour

a; i; i; b; exit
||
i; a; i; b; exit

endspec

internal action i を hiding すると(obs. reduction)、Process P == a;b;$ である。

3.3.2 Interleave(同期化ラベルがない場合) P ||| Q

プロセス木の並列化構成(第3章)の定義では、同期化ラベル L は空ではないことを要求していた。
しかしながら、LOTOSでは同期化ラベル L が空であるようなプロセスの並列化も記述できる。

各プロセスのactionが同期せずに並列動作する、という意味で、これを interleave(=互い違い)と呼ぶ。
オペレータとしては P ||| Q のように書く。

<例4-7>
Process P := a;b;$ ||| c;d;$ のような interleave をLOTOSで記述してみよう。

exa4_7.lotos (Process P := a;b;$ ||| c;d;$)

specification exa4_7[a,b,c,d] : exit

behaviour

a; b; exit
|||
c; d; exit

endspec

プロセスPのトレースは、合計6通りの組み合わせが存在する(LTSを確認せよ)。

この結果について理解することは、非同期で相互に動作しているようなシステムは、如何にその振る舞いが複雑になっているか、ということを知る手がかりになる。


●等価性のチェック

2.3節・木の等価性(Tree Equivalences)で説明したプロセス間の等価性チェックについて、CADP toolboxでは、bcg_cmpアプリケーションが執り行う。bcg_minは、種々の等価性に基づいて、プロセスグラフを縮約(reduction)して出力する機能を有する。

(bcg_cmpのコマンドライン引数の詳細についてはon-line manual pageを参照のこと)

4.1 等価性チェック・グラフ縮約
4.2 等価性チェックの例
4.3 グラフ縮約の例


4.1 等価性チェック・グラフ縮約

等価性チェックでは、主に以下の2つを用いる。入力は2つのプロセスグラフのファイル(BCG形式 *.bcg)

強い挙動の等価性(strong bisimulation equivalent)のチェック
$bcg_cmp -strong
src1.bcg src2.bcg 

観測値挙動の等価性(observational equivalent)のチェック
$bcg_cmp -observational
src1.bcg src2.bcg 

グラフ縮約では、主に以下の2つを用いる。入力は縮約元のプロセスグラフのファイル、出力は縮約後のグラフファイルを指定する(BCG形式 *.bcg)

強い挙動の等価性(strong bisimulation equivalent)による縮約
$bcg_min -strong
src.bcg dst.bcg 

観測値挙動の等価性(observational equivalent)による縮約
$bcg_min -observational
src.bcg dst.bcg  


4.2 等価性チェックの例

4.2.1 strong bisimulation equivalent

<例4-8>
以下の2つのプロセス P1, P2 の、強い挙動の等価性(strong bisimulation equivalent)のチェックを行ってみよう。つまり、
(P1 = P2) → TRUE or FALSE
検査することに他ならない。

Process P1 := a;b;$ [ ] a;b;$
Process P2 := a;(b;$ [ ] b;$)

LOTOSによって、各々のプロセス定義を別々のファイルに作成する。

exa4_8_P1.lotos
exa4_8_P2.lotos

各々のプロセスのトレースグラフを得るために、をcaesarによってLTS生成する。
(下の実行例では、BCG形式のグラフファイルを生成している)

$ caesar -bcg exa4_8_P1.lotos
$ caesar -bcg exa4_8_P2.lotos

正常にLTS生成が終了したならば、exa4_8_P1.bcg, exa4_8_P2.bcg という2つのグラフファイルが存在しているはずである。

それでは、bcg_cmp によって、strong bisimulation equivalentの検査を実行する。実行時オプションは -strong である。

$ bcg_cmp -strong exa4_8_P1.bcg exa4_8_P2.bcg

TRUE

2.3節にも示したように、bisimulation equivalentであれば、observational equivalent であるから、上記の -strong を -observational に取り替えても、結果はTRUEになる(確認してみよ)。

4.2.2 observational equivalent

<例4-9>
以下の2つのプロセス P1, P2 の、観測値挙動の等価性(observation equivalent)のチェックを行ってみよう。つまり、
(P1 == P2) → TRUE or FALSE
検査することに他ならない。

Process P1 := a;(b;$ [ ] i;c;$) [ ] a;c;$
Process P2 := a;(b;$ [ ] i;c;$)

LOTOSによって、各々のプロセス定義を作成し、BCG形式でのLTS生成を行う。
※各自で作成・生成してみよ.
exa4_9_P1.lotos → exa4_9_P1.bcg
exa4_9_P2.lotos → exa4_9_P2.bcg

bcg_cmp によって、observational equivalentの検査を実行する。
実行時オプションは -observational である。

$ bcg_cmp -observational exa4_9_P1.bcg exa4_9_P2.bcg

TRUE

observational equivalentであっても、bisimulation equivalentであるとは限らない。
上記の -observational を -strong に取り替えた場合、bisimilar R の反例が表示され、検査が停止する。(確認してみよ)。


4.3 グラフ縮約の例

<例4-10>
以下のプロセス P1について、観測値挙動の等価性(observational equivalent)を用いたグラフ縮約を行ってみよう。

Process P1 := a;(b;$ [ ] i;c;$) [ ] a;c;$

exa4_10_P1.lotos → exa4_10_P1.bcg

bcg_min によって、observational equivalentによるグラフ縮約を実行する。
実行時オプションは -observational である。

$ bcg_min -observational exa4_10_P1.bcg exa4_10_P1_omin.bcg

縮約した結果は、プロセス a;(b;$ [ ] c;$)のグラフと等価である(各自で確認せよ)。


<例4-11>
以下のLOTOSファイルは、gate hiding を行って、サブプロセス内の一部のgate(act1,act2,act3)について不可観測値として取り扱っている。

一部のgateを不可観測とするには、 hide g1,g2,... in をプロセス定義の前に記述する。通常のLTS生成を行った後には、これらのgate hiding を施したラベルは internal action i として出力される。後にobservational reductionを行うと、これらの不可観測のラベルが "hide"(隠し)され、LTSとして見えない状態になる。システム内部のactionの非同期的な振る舞いは気にしないで、システムを外から見た時の挙動だけを観測したい場合、有効な手法である。

exa4_11.lotos

specification exa4_11[req,done] : noexit

behaviour

hide act1,act2,act3 in

P1[req,act1,done]
|[req,done]|
P1[req,act2,done]
|[req,done]|
P1[req,act3,done]

where

process P1 [req, act, done] : noexit :=
req; act; done;
P1[req,act,done]
endproc

endspec

caesarによってLTS生成した状態のグラフは、このようになる(bcg_editにより整形)。

※プロセスグラフ exa4_11.bcg はこちらから参照

bcg_min によって、observational equivalentによるグラフ縮約を実行する。
実行時オプションは -observational である。

$ bcg_min -observational exa4_11.bcg exa4_11_omin.bcg

縮約した結果は、プロセスの外から見た req <--> done という振る舞いしか見えなくなる(bcg_editにより整形)。

※プロセスグラフ exa4_11_omin.bcg はこちらから参照


●再び自販機の例

1.2.3節にて取り挙げた、自動販売機(コイン返却機能付き)のプロセスモデルについて、Basic-LOTOSで記述し、CADP toolbox によってLTS生成を行ってみよう。

5.1 ペトリネットモデル、マーキンググラフ
5.2 LOTOSによる自販機のプロセスモデル
5.3 caesar/bcg_minによるLTS生成とグラフ縮約


5.1 ペトリネットモデル、マーキンググラフ

この自販機のモデルは、基本的な機能(コイン挿入、コイン返却、商品販売)を有するものである。

まず復習として、この自販機のペトリネットモデルと、そのマーキンググラフを再掲する。(LOTOSによるプロセス定義を行って、LTS生成した結果は、以下のマーキンググラフと等価なbehaviour となるはずである)

図4.2(a) 自動販売機のモデルその1

図4.2(b) (a)のmarking graph


5.2 LOTOSによる自販機のプロセスモデル

プロセス Basic は、自販機の基本機能(コイン挿入、コイン返却、商品販売)を実現したものとする。
並列性はないので、自販機プロセス VM2 は、

VM2 := Basic

と書ける。それでは、VM2のLOTOSによる具体的な定義を行ってみよう。

VM2.lotos

specification VM2[coin,accepted,reject,dispence] : noexit

behaviour

Basic [coin,accepted,reject,dispence]

where

process Basic [coin,accepted,reject,dispence] : noexit :=
coin;
(
accepted; dispence; exit
[]
reject; exit
)
>> Basic [coin,accepted,reject,dispence]
endproc

endspec


5.3 LOTOSによる自販機のプロセスモデル

caesarによってLTS生成した状態のグラフは、以下のようになる(bcg_editにより整形)。

PDFファイルは画像をクリック!

図4.3 プロセスVM2のトレースグラフ(VM2.bcg)

逐次合成に伴う internal action i が存在するので、bcg_min によって、observational equivalentによるグラフ縮約を実行する。 縮約した結果は、先の図4.2(b)marking graphと等価である。(bcg_editにより整形)。

PDFファイルは画像をクリック!

図4.4 プロセスVM2のobs. reducedなトレースグラフ(VM2_omin.bcg)

 


練習問題4-1

[1] 例4-2: プロセス VM について、LOTOSファイルを作成し、caesarを用いてLTS生成を行え。automaton形式、BCG形式の両方で出力すること。BCG形式による出力は、bcg_drawアプリケーションによって、プロセスグラフを観察すること。

[2] 例4-3: Process P2 について、LOTOSファイルを作成し、caesarを用いてLTS生成を行え。例4-1aのプロセスP1のインスタンスを2つのchoiceとして結合・操作しただけで、P2の結果を得たことを、理解せよ。

[3] 例4-4 〜 例4-7 について、LOTOSファイルを作成し、caesarを用いてLTS生成を行い、プロセスグラフを観察せよ。(トランジションラベルが重なって判読しにくい場合には、bcg_editアプリケーションによってBCGファイルを読み込み、分かり易いように整形しながら観測すると良い)

[4] 以下の2つのプロセスがbisimulation equivalentであることをcaesar+bcg_cmpを用いてチェックしてみよ。

Process P1 := a;(b;$ [ ] i;c;$) [ ] a;i;c;$
Process P2 := a;(b;$ [ ] i;c;$)

(P1 = P2) → TRUE

[5] 以下の2つのプロセスはobservational equivalentでは"ない"ことを、caesar+bcg_cmpを用いてチェックしてみよ。

Process P1 := a;(b;$ [ ] c;$)
Process P2 := (a;b;$ [ ] a;c;$)

(P1 == P2) → FALSE

[6] 以下のプロセス P の obs. reduced なプロセスグラフを bcg_min を用いて生成し、obs. reduced( P ) = a;b;$ となることを確かめよ。

Process P := a;i;i;b;$ || i;a;i;b;$

 


★レポート課題1

<課題>
1.2.7節にて取り挙げた、自動販売機(コイン返却機能付き、在庫数=1)のプロセスモデルについて、Basic-LOTOSで記述し、CADP toolbox によってLTS生成を行いなさい。
また、生成したLTSのobs. reduced を行いなさい。

提出するファイルは以下の通り(tar+gzipでアーカイブした後、提出)。

・LOTOSファイル:VM3.lotos
・プロセスグラフ生成に必要な他のファイル(*.lib, *.tなど)
・LTSプロセスグラフファイル:VM3.bcg
・obs. reducedしたプロセスグラフファイル:VM3_omin.bcg


<演習手順>
(1)参考のため、自販機のペトリネットモデルと、そのマーキンググラフを以下に再掲する。

図4.5(a) 自動販売機のモデルその2:在庫数=1

図4.5(b) (a)のmarking graph


(2)プロセス Basic,Strageは、各々、自販機の基本機能、商品在庫の資源と補充の動作、とする。

(3)各々のプロセスのaction集合は以下の通り。

Act(Basic) = {coin,accepted,reject,dispence}
Act(Strage) = {dispence,refill}

(4)自販機プロセスVM3 は、プロセスBasicとStrageの並列化構成をとる。

(5)LOTOSファイル VM3.lotos を作成しなさい。

(6)LTSプロセスグラフファイル:VM3.bcg を caesar を用いて生成しなさい。bcg_drawを用いてグラフを観察しなさい。

(7)obs. reducedしたプロセスグラフファイル:VM3_omin.bcg を bcg_min を用いて生成しなさい。bcg_drawを用いてグラフを観察しなさい。


(8)(6)で生成したプロセスグラフが、図4.5(b)と観測値挙動の等価性(observation equivalence)において同等であることを、bcg_cmp を用いてチェックしなさい。

※図4.5(b)のトレースグラフのBCG形式ファイルはここからダウンロード(VM3_correct.bcg)

※図4.5(b)のトレースグラフのAUT形式ファイルはここからダウンロード(VM3_correct.aut)

※トレースグラフVM3_correct.bcgを可視化・整形したもの(参考)(VM3_correct.pdf)


<レポート提出の手順>
(1)提出するファイルは以下の通り。

・LOTOSファイル:VM3.lotos
・プロセスグラフ生成に必要な他のファイル(*.lib, *.tなど)
・LTSプロセスグラフファイル:VM3.bcg
・obs. reducedしたプロセスグラフファイル:VM3_omin.bcg

(2)以下のいずれかの形式でarchiveし、一本のファイルにまとめなさい。
アーカイブのファイル名は VM3.zip あるいは VM3.tar.gz とする。

※提出可能形式
(a) tar+gzip形式 (*.tar.gz) 例:UNIXコマンドの tar + gzip を用いる
(b) ZIP圧縮形式 (*.zip) 例:WinZipなど


(3)eALPSの、レポート提出システムからアップロードし、提出しなさい。 

wasaki@cs.shinshu-u.ac.jp
Copyright(c) Katsumi Wasaki. All rights reserved.