Basic LOTOS | ||||||||||||||||||||||||||
■Basic LOTOS 1. Labelled Transition System (LTS)
|
BLAによるプロセス定義を行うと、Basic LOTOSによるプロセス定義ファイルが作成できる。LOTOS独特の記述方法(gate hiding など)も存在する。CADP toolboxを用いて、Basic LOTOSのプロセストレースを行い、Labelled Transition System (LTS)に基づいたプロセスグラフの生成を行うことができる。また、生成したLTS(プロセスグラフ)の等価性チェック、ならびに種々の等価性を利用したグラフ縮約(reduction)ができる。 この章で学習する内容は以下の5つである。最後に演習問題1を与える。 1. Labelled Transition System (LTS) ●Labelled Transition System (LTS)通常の有限状態機械(オートマトン)では、状態値間の変化と、各状態に付けられた性質(Atomic Proposition)に基づいて、システムのモデル化を行っている。 プロセスによるモデル化では、"状態値"は、もはや、"その後実行すべきプロセスラベルの列"に過ぎず、プロセスのActionによる遷移、つまり状態間のラベル付きトランジション(Lebelled Transition)の働きが重要となっている。 初期状態からのプロセスモデルの振る舞いをトレースしたものが、プロセスグラフであった。以後、このプロセスグラフを、下記に定義する Labelled Transition System (LTS) で表現することとする。 1.1 LTSの定義
L,N をある自然数とし、猫+ をL個のアルファベットの"空でない"列全体とする。このとき、 |*|を 集合* のサイズ とする。このとき、上記のLTSの定義により、 大雑把な見積もりを行うと、このLTSの初期状態から始まる全てのpathを調べあげる(トレース)アルゴリズムの計算量は、高々 O(|S|+|T|) である。
1.2 LTSの例<例1> Process P1 := A;B;$ のプロセスグラフ、LTS(P1) を上記の定義Def-4.1に従って構成してみる。
※ terminating process '$' は、Basic LOTOS では 'exit' である。 Aldebaran-automaton形式では、LTS(P1) は以下のように記述される。 時に、第1行目は des (s0, |T|, |S|) という意味である。
<例2> Process P2 := A;B;$ [] A;C;$
●toolbox による LTS生成LOTOS仕様に基づいたプロセスグラフであるLTSを、計算機を用いて生成する。 ※caesarのon-line manual pageはここからどうぞ (いまのところBasic-)LOTOS仕様のファイルは、通常のテキストファイル形式で、拡張子が .lotos あるいは .lot なものである。 Introduction
to the ISO Specification Language LOTOS ←お勧め!(local copy) An
Introduction to LOTOS: Learning by Examples (local copy) なお、LOTOS言語仕様書は ISO-8807(1989) として公開されている(有料) ISO International Standard 8807:1989 2.1 LTSのフォーマット 2.1 LTSのフォーマットLTSのファイルフォーマットとしては、以下の2つを取り上げる。 (1)Aldebaran
automaton形式(.aut) 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ファイルを作成する。
※注意点: 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生成を行う。 (caesarのコマンドライン引数の詳細についてはon-line manual pageを参照のこと)
正常にLTS生成が終了すると、exa4_1.aut というファイル名で、automaton形式のプロセスグラフが出力されている。これはテキストファイルなので、catコマンドなどで容易に観察することができる。前節の例1、LTS(P1)と同等の結果が得られていることが判る。
2.2.3 caesarによるLTS生成(その2)次に、exa4_1.lotos を、caesarによってトレースし、出力形式として (2)BCG形式(.bcg)を指定して生成を行ってみる。
正常にLTS生成が終了すると、exa4_1.bcg というファイル名で、BCG形式のプロセスグラフが出力されている。これはバイナリファイルなので、直接読むことはできない。 プロセストレースグラフとして了解性の高い表示を得るために、bcg_drawアプリケーションを用いて観察してみる。これは、BCG形式ファイルを解析し、下→上側に向かって、state番号の若い順→トランジションの遷移の状況に応じて、"プロセス木"を現出させるためのものである。グラフの解析後、中間的なPostscriptファイルを出力し、内部で ghostview を起動してGUIへ表示する。
図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 というファイル名で保存する。
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による記述例について取り挙げる。 ここでLOTOSの文法の全てを取り扱うのは容易でないので、このドキュメントなどを先に読んでおこう。 3.1 (非決定的)選択動作(Choice / P [] Q) 3.1 (非決定的)選択動作(Choice / P [] Q)2つのプロセスP,Qのchoice P [] Q は、LOTOSにおいても同様に書けばよい。 <例4-2> coffeeかteaを選択すると、それが販売されて終了するようなプロセス VMa をLOTOSで作成してみる。coffeeとteaの間で優先順位はない。また、この2つしか販売しない。
<例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で結合した。
3.2 再帰(Recursion / Y := T >> Y)プロセスTのterminating後、ラベルYへ戻るようなRecursion Y := T >> Y は、LOTOSにおいても同様に書けばよい。 <例4-3> 1.3節で取り挙げた、プッシュボタンを押すと出力がon/offされるプロセス PBL を定義してみる。最初にpushされる以前の出力は不定である。永遠に繰り返すことが期待されているので、spec は noexit である。
<例4-4> 2.4節・例2-7で取り挙げた、coinが挿入された後、candy か toffeeの商品選択を行うと、その商品が販売され、最初に戻る、というようなプロセス VMb について、そのLOTOSファイルを作成してみよう。 P1 := coin;(candy;$ [] toffee;$) VMb := P1>>P2 いくつかの書き方が存在するが、以下の記述例では、P1 と P2 の逐次合成を用いたRecusionを行った。当然のことながら、spec は noexit である。
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>
3.3.2 Full-Synchronizationの例 P || Q不可観測のinternal action i を含むプロセスの並列化構成について、Full-Synchronizationを用いて以下のような構成が考えられる。 <例4-6>
internal action i を hiding すると(obs. reduction)、Process P == a;b;$ である。 3.3.2 Interleave(同期化ラベルがない場合) P ||| Qプロセス木の並列化構成(第3章)の定義では、同期化ラベル L は空ではないことを要求していた。 各プロセスのactionが同期せずに並列動作する、という意味で、これを interleave(=互い違い)と呼ぶ。 <例4-7>
プロセスPのトレースは、合計6通りの組み合わせが存在する(LTSを確認せよ)。 この結果について理解することは、非同期で相互に動作しているようなシステムは、如何にその振る舞いが複雑になっているか、ということを知る手がかりになる。 ●等価性のチェック2.3節・木の等価性(Tree Equivalences)で説明したプロセス間の等価性チェックについて、CADP toolboxでは、bcg_cmpアプリケーションが執り行う。bcg_minは、種々の等価性に基づいて、プロセスグラフを縮約(reduction)して出力する機能を有する。 (bcg_cmpのコマンドライン引数の詳細についてはon-line manual pageを参照のこと) 4.1 等価性チェック・グラフ縮約 4.1 等価性チェック・グラフ縮約等価性チェックでは、主に以下の2つを用いる。入力は2つのプロセスグラフのファイル(BCG形式 *.bcg) 強い挙動の等価性(strong bisimulation equivalent)のチェック グラフ縮約では、主に以下の2つを用いる。入力は縮約元のプロセスグラフのファイル、出力は縮約後のグラフファイルを指定する(BCG形式 *.bcg) 強い挙動の等価性(strong bisimulation equivalent)による縮約 4.2 等価性チェックの例4.2.1 strong bisimulation equivalent<例4-8> Process P1 := a;b;$ [ ] a;b;$ LOTOSによって、各々のプロセス定義を別々のファイルに作成する。 exa4_8_P1.lotos
正常にLTS生成が終了したならば、exa4_8_P1.bcg, exa4_8_P2.bcg という2つのグラフファイルが存在しているはずである。 それでは、bcg_cmp によって、strong bisimulation equivalentの検査を実行する。実行時オプションは -strong である。
2.3節にも示したように、bisimulation equivalentであれば、observational equivalent であるから、上記の -strong を -observational に取り替えても、結果はTRUEになる(確認してみよ)。 4.2.2 observational equivalent<例4-9> Process P1 := a;(b;$ [ ] i;c;$) [ ] a;c;$ LOTOSによって、各々のプロセス定義を作成し、BCG形式でのLTS生成を行う。 bcg_cmp によって、observational equivalentの検査を実行する。
observational equivalentであっても、bisimulation equivalentであるとは限らない。 4.3 グラフ縮約の例<例4-10> Process P1 := a;(b;$ [ ] i;c;$) [ ] a;c;$ exa4_10_P1.lotos → exa4_10_P1.bcg bcg_min によって、observational equivalentによるグラフ縮約を実行する。
縮約した結果は、プロセス a;(b;$ [ ] c;$)のグラフと等価である(各自で確認せよ)。
一部のgateを不可観測とするには、 hide g1,g2,... in をプロセス定義の前に記述する。通常のLTS生成を行った後には、これらのgate hiding を施したラベルは internal action i として出力される。後にobservational reductionを行うと、これらの不可観測のラベルが "hide"(隠し)され、LTSとして見えない状態になる。システム内部のactionの非同期的な振る舞いは気にしないで、システムを外から見た時の挙動だけを観測したい場合、有効な手法である。
caesarによってLTS生成した状態のグラフは、このようになる(bcg_editにより整形)。 bcg_min によって、observational equivalentによるグラフ縮約を実行する。
縮約した結果は、プロセスの外から見た req <--> done という振る舞いしか見えなくなる(bcg_editにより整形)。 ※プロセスグラフ exa4_11_omin.bcg はこちらから参照 ●再び自販機の例1.2.3節にて取り挙げた、自動販売機(コイン返却機能付き)のプロセスモデルについて、Basic-LOTOSで記述し、CADP toolbox によってLTS生成を行ってみよう。 5.1 ペトリネットモデル、マーキンググラフ 5.1 ペトリネットモデル、マーキンググラフこの自販機のモデルは、基本的な機能(コイン挿入、コイン返却、商品販売)を有するものである。 まず復習として、この自販機のペトリネットモデルと、そのマーキンググラフを再掲する。(LOTOSによるプロセス定義を行って、LTS生成した結果は、以下のマーキンググラフと等価なbehaviour となるはずである) 図4.2(a) 自動販売機のモデルその1 図4.2(b) (a)のmarking graph 5.2 LOTOSによる自販機のプロセスモデルプロセス Basic は、自販機の基本機能(コイン挿入、コイン返却、商品販売)を実現したものとする。 VM2 := Basic と書ける。それでは、VM2のLOTOSによる具体的な定義を行ってみよう。
5.3 LOTOSによる自販機のプロセスモデルcaesarによってLTS生成した状態のグラフは、以下のようになる(bcg_editにより整形)。 図4.3 プロセスVM2のトレースグラフ(VM2.bcg) 逐次合成に伴う internal action i が存在するので、bcg_min によって、observational equivalentによるグラフ縮約を実行する。 縮約した結果は、先の図4.2(b)marking graphと等価である。(bcg_editにより整形)。 図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;$ (P1 = P2) → TRUE [5] 以下の2つのプロセスはobservational equivalentでは"ない"ことを、caesar+bcg_cmpを用いてチェックしてみよ。 Process P1 := a;(b;$ [ ] 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<課題> 提出するファイルは以下の通り(tar+gzipでアーカイブした後、提出)。 <演習手順> 図4.5(a) 自動販売機のモデルその2:在庫数=1 図4.5(b) (a)のmarking graph
(3)各々のプロセスのaction集合は以下の通り。 Act(Basic) = {coin,accepted,reject,dispence} (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を用いてグラフを観察しなさい。
※図4.5(b)のトレースグラフのBCG形式ファイルはここからダウンロード(VM3_correct.bcg) ※図4.5(b)のトレースグラフのAUT形式ファイルはここからダウンロード(VM3_correct.aut) ※トレースグラフVM3_correct.bcgを可視化・整形したもの(参考)(VM3_correct.pdf) <レポート提出の手順> ・LOTOSファイル:VM3.lotos (2)以下のいずれかの形式でarchiveし、一本のファイルにまとめなさい。 ※提出可能形式 |
|||||||||||||||||||||||||
wasaki@cs.shinshu-u.ac.jp |