日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

階層グラフ書換え言語 LMNtal の否定表現の拡張と全称量化の実現
齋藤 諒人

上田 和紀

LMNtal は，階層構造と接続構造を表現する階層グラフ構造の書換えを非決定的に行う計算モデルである．実行は部分グラフのパターンマッチとその書換えによって構成される．既存の LMNtal では，部分グラフが存在しない場合に成功するパターンマッチは記述できなかったため，これまでの研究で，部分グラフの不存在を表現する存在否定構文およびその操作的意味論を設計し，導入した．本論文では，存在否定構文の拡張による表現力の強化について述べる．また，存在否定構文の重要な応用に全称量化の表現があり，それについても具体例とともに述べる．

め，存在量化の論理積に相当する．全称量化は否定と

1 はじめに存在量化を用いて表現できることから，新たに否定表

LMNtal は接続構造と階層構造を表現することので現の導入を行うことによる全称量化の実現も期待できるグラフ書換え言語であり [6]，グラフと書換え規きる．現在の LMNtal で複数のプロセスのパターン

則をテキストで簡潔に記述できる特徴を持つ．

マッチを行うためには，具体的なプロセスの数を明記

LMNtal の書換えは非決定性を有しており，並行プ

する必要があった．全称量化表現の導入により，よりロセス計算の記述に適する並行言語の側面も持つ．し汎用性の高い書換え規則の記述が可能になり，モデリ

かし，並行言語の多くはプロセスの存在に基づく計算

ング能力の向上につながる．

を行うため，プロセスの不存在を表現する構文がな

これまでの研究で部分グラフの不存在を表現する存く，現状の LMNtal も同様にグラフ要素の不存在を

在否定構文とその意味論の設計を行ったが，LMNtal

表現できない．計算や通信がプロセスの存在によってのグラフ表現と否定表現を同時に記述する設計によ成立するプロセス計算とは異なり，グラフ書換えの側り十分な表現力が得られなかった．本研究では，グラ面を有する LMNtal において，指定の構造を有してフ表現と否定表現を独立に記述するように設計し，否いるかの判定を行うことができる否定表現は重要で定表現能力の拡張を行う．また，これまでの構文ではある．

記述できなかった例題を記述できることを確認する．

書換えはパターンマッチングによって取得した部分グラフを規則に従って変換する操作である．パターン
マッチングは部分グラフの各要素の存在判定を行うた

2 LMNtal
本節では階層グラフ書換え言語 LMNtal について簡単に述べる．詳細は文献 [6] を参照されたい．

∗ An enhancement of negative expression and realiza-tion of universal quantification for LMNtal, a hierarchical graph rewriting language
This is an unrefereed paper. Copyrights belong to
the Author(s).
Ryoto Saito, Kazunori Ueda, 早稲田大学基幹理工学
研究科情報理工・情報通信専攻, Dept. of Computer
Science and Engineering, Waseda University.

2. 1 構文
LMNtal はリンク（無向辺）でグラフを構成する言語である．また，膜を用いることで階層構造を表現できる．LMNtal の構文を図 1 に示す． P をプロセス，

T をプロセステンプレートと呼ぶ．

ルールのマッチングが非決定的であり，グラフがいず（空）れのルールによっても簡約不可能になるまで適用が繰（アトム）

り返される．LMNtal ではルールを任意の膜に記述す| P, P（分子）ることができ，その膜より外側で実行されることはな| {P }（膜）

い．これにより計算の局所化ができる．

| T :- T（ルール）

P ::= 0| p(X1 , . . . , Xm )(m ≥ 0)

プロセス文脈はアトムと膜の抽象表現であり，膜内（空）のプロセステンプレートで明示されなかったすべて（アトム）のプロセスを指す．例えばルール mem{a,$p} :- $p| T, T（分子）は，「ある mem 膜に a アトムが存在するなら，mem 膜| {T }（膜）内に存在するそれ以外のアトムと膜を外に取り出す」| T :- T（ルール）というルールである．このとき $p は mem 膜の中にあ| @p（ルール文脈）る a 以外のすべての膜とアトムを指す．プロセス文

T ::= 0| p(X1 , ..., Xm )(m ≥ 0)| $p[X1 , . . . , Xm |A](m ≥ 0)（プロセス文脈）

脈が記述されなかった場合，a 以外のプロセスが存在| p(∗X1 , . . . , ∗Xm )(m ≥ 0) （アトム集団）

してはいけないことに注意する．ここで，プロセス文

A ::= [ ]
| ∗X

（空）

脈の [X1 , . . . , Xm ] は自由リンクであり，プロセス文（リンク束）

脈に記述された数とちょうど同じ自由リンク数であ図 1: LMNtal 構文

るときにマッチングが成功する．リンク束 ∗X は自由リンクの数を任意とする．$p と省略された場合は，アトムはグラフの節点に相当し，小文字から始ま$p[∗X] と同値である．

る．アトム名に続く括弧はリンク（グラフの辺に相ルール文脈はプロセス文脈と同様に，膜に存在する

当する）が存在するときのみ記述し，リンクは大文

ルールのうち，プロセステンプレートによって明示さ字から始まる．同名のリンクはグラフ中にたかだか 2

れないものを指す．

回出現し，対応するリンクが接続されることを意味

LMNtal の処理系では拡張構文として，制約条件をする．アトム p(X1 , . . . , Xm ) の引数 X1 , . . . , Xm は

Guard に記述することができる．Guard を記述する

順序づけられている．このリンク名はアトムにつな際の記法を以下に示す．

がるリンクの端点である．アトム p(X1 , . . . , Xm ) は
リンクの個数が m 個であり，m 価アトムという．ア
トム名が + または − かつ，リンクを 1 つ持つ場合，+X ，−X といった略記法が認められている．プロセ
ス P に 1 回だけ出現するリンク名を P の自由リンクと呼び，P の外部に接続されることを意味する．2 回出現するリンク名を局所リンクと呼ぶ．
膜はプロセスの階層化を実現する．膜がリンクを持
つことはなく，膜の中にあるアトムがリンクを持つことで膜内外の接続を行う．また，膜には名前をつけることができ，その場合は name{P } や name{T } と記述する．
ルールは LMNtal の書換え規則である．T :- T の
うち，左辺を Head，右辺を Body と呼ぶ．Head でのマッチングは存在量化に相当する．LMNtal は各

Head :- Guard | Body
LMNtal は数値や文字列をアトムとして記述できる．Guard には Head でマッチしたプロセスの型検査を記述できる．検査可能な型は int（整数），float（浮動小数点），string（文字列），unary（1 価アトム），ground（膜を持たず，すべてのアトムが連結されたグラフ）である．また，int 型，float 型の大小比
較，演算を行うことができる．int，float，string 型
はそれぞれ unary 型の真部分集合であり，互いに独立している．さらに unary 型は ground 型の真部分集合である．

造を表現することはできない．

(T :- U ), T θ → (T :- U ), U θ

グラフは host graph と呼ばれる初期グラフと rule

図 2: LMNtal のルールによる遷移規則と呼ばれる書換え規則に分けられる．Rule のグラフ
では節点および辺に分類を示す色がつけられ，黒は適2. 2 操作的意味論

用の存在条件，青は書換えによって削除されるもの，

LMNtal の操作的意味論は，プロセスの合同関係を

緑は書換えによって作成されるもの，赤は適用の不存示す 10 個の構造合同規則と，書換えの遷移関係を示

在条件を意味する．また，rule グラフには量化子を示す 6 つの遷移規則で構成される．このうち書換え規

す疑似節点を扱うことができ，量化子の節点を辺で参則による遷移規則を図 2 に示す．ここで θ は代入で照することにより全称量化と存在量化ができる．

あり，プロセステンプレート T のプロセス文脈およ

各 rule には名前が付けられる．これにより非決定びルール文脈にそれぞれ具体的なプロセスとルールを実行だけでなく，手続き型プログラミング言語のよう付値することを意味する．書換え時はその代入 θ をに rule の適用順序や条件分岐，ループの制御を指定

U に対して適用する．

することができる．

2. 3 処理系とモデル検査

3. 2 VIATRA [1]LMNtal の処理系はコンパイラと実行時処理系に分VIATRA はソフトウェア工学におけるモデル駆動

類され，コンパイラは LMNtal プログラムから実行

開発を支援するモデル変換フレームワークである．モ

時処理系が解釈する中間言語に変換する．

デル駆動開発は主にオブジェクト指向プログラミング

実行時処理系 SLIM [8] には通常実行モードに加えによる開発方法であり，コーディングに先立ってモデ

非決定実行モードが存在する．非決定実行モードは適ル設計を行うものである．モデル変換とグラフ書換え用できる遷移をすべて行い，最終的な状態空間を返す

は厳密には分類が異なるが，接続構造や階層構造を操モードである．また，LTL 式によるモデル検査にも作する点において類似している．VIATRA の書換え

対応しており，パターンマッチングを原子命題としたはドメインの制約下でのみ行われ，これはグラフ書換検査が行える．具体的には LMNtal のルール形式でえ系との相違点である．

記述し，そのルールが適用できる場合を真とする．

VIATRA は統合開発環境 Eclipse 上で動作するパッケージとして提供され，複数の言語およびフレーム

3 関連研究ワークで構成される．対象となるモデルは Eclipse

本節では関連する書換え系について述べる．

Modeling Framework によって構成され，パターン
マッチングには独自言語の Viatra Query Language

3. 1 GROOVE [2](VQL) が用いられる．パターンマッチは要素（インGROOVE は動的システムを視覚的にモデリングスタンス）単位で行われ，要素の型（ドメインのクするグラフ書換え系およびそのツールセットであり，ラスに相当）や属性（フィールド），要素間の関係にプログラムの仕様と挙動を自動で検証するモデル検よって判断される．VIATRA では否定マッチングが査を実行できる．モデル検査器は LTL，CTL 式に対可能であり，二重否定によって全称量化の表現が可能応している．LMNtal は無向グラフを表現するのに対である他，後継言語である VIATRA2 では forall 構

して GROOVE は有向グラフを対象とし，節点と辺文が用意されている．

いずれも名前付きである．また，節点には名前の他に任意の型（type）やラベル（flag）をつけ，書換えや3. 3 CPN [4]モデル検査のマッチングに利用できる．接続構造や非CPN (Coloured Petri Net) は Petri net [3] の拡張

連結グラフを表現できるが，LMNtal のような階層構

であり，多重集合書換え系という点で類似してい![P ]![P, ![P ], . . . , ![P ]]図 3: 存在否定構文（旧）Rule ::= T :- [N eg |] T.
N eg ::= ![N eg] | ![In] | N eg, N eg
In::= P ∈ $p | In, In
図 4: 存在否定構文

る．Petri net は離散システムを数学的に記述するモデルであり，place, transition，arc，token から構要があり，膜や否定条件が複数存在するような複雑な成される．Place と transition は有向 2 部グラフをHead 部の記述が困難であることがわかった．この構構成し，place と transition の遷移関係 arc は有向辺

文では記述できなかったが，本研究により記述可能にに相当する．Place は必ず transition と，transition

なった例題については後述する．プロセスと否定条件

は必ず place と隣接する．つまり arc は place 同士，は直交しており，同時に記述しないのが妥当である．

transition 同士の関係を認めない．
Place は任意個数の token を保有し，状態遷移は

4. 2 プログラムルート膜とプロセス文脈

token の移動によって表現される．Transition に向新たな構文設計に必要な概念と構文について示す．

かうすべての place に 1 つ以上の token が存在する

LMNtal は膜を用いた階層グラフを扱う言語であとき，それらの place から token を 1 つ削除し，同り，現行の LMNtal では最上位の膜を世界的ルート

transition から出るすべての place に token を 1 つ付膜と呼ぶ．世界的ルート膜は無限の広さを持つ膜であ与する．Petri net の状態遷移はこの規則のみに従っ

り，全体集合が有限であることを前提とした否定表現て行われる．

は世界的ルート膜に記述できない．そこで，プログラ

CPN は token への色（型）付けと具体的な値を与えることができる．Place に保有できる token の色がムの実行範囲として有限の膜を定義する．これをプロ
グラムルート膜と呼ぶことにする．

制限され，arc にも色指定を施すことで token の流れ

ここで，自己参照プロセス文脈を定義する．自己参を制御することができる．したがって複数の place が照プロセス文脈は$self と記述され，ルールの Guard

ある transition と隣接するとき，状態遷移をするた部のみに記述可能である．ルール中の最上位膜にプ

めにはそれらすべての place に同色かつ同値の token

ロセス文脈を記述できない代わりに，Head 部に出現が存在する必要がある．また，遷移の際に token のしないプロセス全体を$self として参照することを値による場合分けや不定値によるランダム実行が可認める．これにより，ルールが記述された膜において能である．

も否定マッチングが実現できる．拡張された LMNtal

CPN は LMNtal の膜を持たないサブセットで表現

では，$self は予約語となる．

可能であることが文献 [7] で示されている．

4. 3 存在否定構文の拡張

4 構文設計新たに設計した存在否定構文を図 4 に示す．ここ4. 1 これまでの研究

で，構文中に現れるプロセス文脈 $p は，全て Head

これまでの研究 [9] では，プロセスの不存在を表す部に出現するものとする．

構文として存在否定構文を設計した．その構文を図 3に示す．

書換え時には $p に具体的なプロセスが代入されているため，$p をプロセスの多重集合と考えるのは自

この構文はルールの Head 部のみに記述可能であ然である．したがって，構文では集合の要素を示す ∈り，![ ] 内に囲まれたプロセスが存在しないときにマッを記述することでプロセス文脈に含まれるという意

チングが成功するものであった．しかし，これはマッ味を表し，プログラム中では LATEX 記法に基づき\in

チングするプロセスと否定条件を同時に記述する必と記述することにした．

ここでの依存性とは，コンポーネントを状態遷移¬∃Q($p ≡ (P, Q))(T :- ![P ∈ $p] | U ), T θ → (T :- ![P ∈ $p] | U ), U θ系とみなしたとき，あるコンポーネントの状態遷移

図 5: シンプルな存在否定構文の操作的意味論

例えば，サーバの設定ファイルの更新を反映するためが別のコンポーネントの状態に依存する性質を指す．

にはサーバプログラムを一度終了させる必要がある．
新たな操作的意味論の基本的な構造を図 5 に示す．

このような依存性を持つシステムの構成を安全に![P ∈ $p] はプロセス文脈 $p にプロセス P が含まれ変更するプランニング問題の解決のために，適切なないことを意味する．したがって $p が P とそれ以外構成のモデリングが要求される．文献 [5] では stateのプロセス（Q）によって構成される分子と構造合同

model と呼ばれるモデルが利用されているが，これでない必要がある．

を LMNtal のモデル検査によって解決する．

一般化した操作的意味論を図 6 に示す．ここで，LMNtal によってモデリングされた依存性システム

CVT は否定節から意味論への変換関数である．\inを図 7 に示す．コンポーネントは element 膜によっはプロセスとプロセス文脈の要素関係，![] は否定とて表される．element 膜は起動や停止と行った状態を対応し，条件の連結は論理積を意味する．さらに多重示す state 膜と state 間の遷移を示す transition 膜に否定の記述を許容することにより，後述する全称量化

よって構成される．現在状態は current アトムを持つを実現した．

state 膜であり，current アトムは element 膜においプログラム例を以下に示す．

てある state 膜に 1 つしか存在しない．同時に目的{$p} :- ![a \in $self], ![b \in $p] | .

状態を示す desired アトムも存在し，制限は current

これは，このルールが記述された膜（$self）に a ア

アトムと同様である．すべての element 膜においてトムが存在しないとき，かつルールが記述された膜内

current アトムと desired アトムが同じ state 膜に存在に存在する膜（{$p}）に b アトムが存在しないときすることを目的とする．current アトムは state 膜の +にマッチングが成功する．

アトムから transition 膜の − アトム方向，transition
膜の + アトムから state 膜の − アトム方向に従っ

4. 4 全称量化て移動する．つまり図中の矢印方向に従って current

全称量化 ∀xP (x) は ¬∃x¬P (x) と同値である．LM-

アトムの移動が行われる．この際，transition 膜に

Ntal のパターンマッチングはプロセスの存在量化にcurrent アトムは含めず，1 ステップで別の state 膜

相当することを踏まえると，二重否定によって全称量に移動する．

化を表現することができる．

図 7 のモデルは図左の element 膜内の current ア:- ![a(X) \in $self, ![b(X) \in $self]] |トムが右上の transition 膜経由で移動しようとする．

a(X), c(X).

この transition 膜は dep アトムを有し，dependency

このルールはすべての 1 価（リンクを 1 つ持つ）a ア

膜と接続する．dep アトムを持つ transition 膜を経由

トムが，1 価の b アトムと接続されている（≡ 1 価のする場合，dependency 膜とつながるすべての stateb アトムと接続されないような 1 価の a アトムは存

膜が current アトムを有する必要がある．この制約

在しない）場合に適用できるルールである．

が依存性を表現する．ここでは依存性制約をすべて満たすため，図 8 に遷移することが可能である．反

5 例題：依存性システム

対に，左下の transition 膜経由で図 7 に戻る場合は，大規模なソフトウェアシステムの構成変更は，コン

dep アトムを有さないため，制約なしで状態遷移可能

ポーネント間に依存性を有するケースが多く，簡単ではない．このシステムの依存性を考慮した構成変更のプランニング問題が文献 [5] で提案されている．

である．
状態遷移を実現する LMNtal ルール（遷移規則）を図 9 に示す．1 つ目のルールは dep アトムが存在

CV T (Cond)(T :- Cond | U ), T θ → (T :- Cond | U ), U θ∃Q($p ≡ (P, Q))






¬CV T (Cond1 )CV T (Cond) = ∧nCV T (Condi )

i=1




true

(Cond = P ∈ $p)(Cond = ![Cond1 ])(Cond = Cond1 , . . . , Condn )(Cond = 0)

図 6: 存在否定構文の操作的意味論（一般形）

図 7: 依存性システムの LMNtal モデリング（遷移前）

図 8: 依存性システムの LMNtal モデリング（遷移後）しないとき，2 つ目のルールは dep アトムが存在し，かつすべての依存制約を満たすときのルールである．

図 9 に対する中間言語を手動で記述し，その動作を確認している．中間言語は付録 A 節に示す．

dependency 膜とつながるすべての state 膜が current
アトムを有する制約を，Guard 部の二重否定による6 まとめと今後の課題

全称量化で記述できた．これまでの研究による旧存在

本論文では，LMNtal のパターンマッチングで否定

否定構文では記述できなかった制約である．図 9 のを表現するための存在否定構文を拡張し，複雑なグラ

ルールはモデルの element 数，state 数，dependency

フ構造における否定や全称量化にたえうる構文としの複雑度に依存しない．つまりシステムの構成にかかた．それに伴い，無限の広さを持つ世界的ルート膜のわらずすべての遷移を同じルールセットで記述できる

代わりにプログラム実行単位を示す有限のプログラ特徴がある．

ムルート膜を定義した．さらに，5 節では拡張されたelement {state {+ SRC , current , $p } ,transition { - SRC , + DST , $q } ,state { - DST , $r } ,$s }.
: - ![ dep ( DEP ) \ in $q ]| element {state {+ SRC , $p } ,transition { - SRC , + DST , $q } ,state { - DST , current , $r } ,$s }.
element {state {+ SRC , current , $p } ,transition { - SRC , + DST , dep ( DEP ) , $q } ,state { - DST , $r } ,$s } ,
dependency {+ DEP , $p1 }: - ![+ REF \ in $p1 ,![ element { state { current , ref ( REF ) , $t } , $u } \ in $self ]]| element {state {+ SRC , $p } ,transition { - SRC , + DST , dep ( DEP ) , $q } ,state { - DST , current , $r } ,$s } ,
dependency {+ DEP , $p1 }
図 9: 依存性システム問題の拡張 LMNtal エンコード（ルール）
存在否定構文で記述できるようになった複雑な例題を示し，拡張の有用性を示した．拡張した構文を中間言語に変換するためのコンパイラ拡張が必要であるこ必要がある．
謝 辞 本 研 究 の 一 部 は ，科 学 研 究 費 基 盤 研 究(B)18H03223 の助成を受けて実施した．

とは言うまでもないが，さらなる課題として以下のものが考えられる．

A 5 節 LMNtal エンコードの中間言語

LMNtal のパターンマッチングにおける否定は，指5 節で示した依存性システム問題の遷移規則を表す

定された部分グラフが存在しないことを意味する．し図 9 の LMNtal プログラムに対して出力が期待されたがって通常の書換えと異なり，存在しない部分グラる中間言語を Listing 1 に示す．Compiled Rule で区フを参照しながら別のグラフに書き換えることはで切られる単位が一つの書換え規則である．

きない．これは二重否定を用いた全称量化表現に不都合である．全称量化は本来「指定したすべての部分グラフが条件を満たす」というパターンマッチングであるため，成功した場合は部分グラフが存在することを意味する．しかし存在否定構文による記述では二重否定を用いるため，「条件を満たさない部分グラフが存在しない」という解釈により，条件を満たすすべての部分グラフを参照することはできない．全称量化パターンへの参照を書換えで利用する仕様を検討する

Listing 1: 図 9 のプログラムに対応する中間言語
Compiled Ruleset@602
Compiled Rule-- atommatch :spec[2 , 2]-- memmatch :spec[1 , 19]anymem[1 , 0 , 0 , " element "]norules[1][2 , 1 , 0 , " state "]anymemfindatom[3 , 2 , ’ current ’ _0 ]findatom[4 , 2 , ’+ ’ _1 ]deref
[5 , 4 , 0 , 1]
func
[5 , $in_2 ]deref[6 , 5 , 0 , 0]

func
[6 , $out_2 ]deref[7 , 6 , 1 , 1]
func
[7 , $out_2 ]deref[8 , 7 , 0 , 0]func
[8 , $in_2 ]deref[9 , 8 , 1 , 0]func
[9 , ’-’ _1 ]lockmem[10 , 8 , " transition "]norules[10]
findatom[11 , 10 , ’+ ’ _1 ]deref
[12 , 11 , 0 , 1]
func
[12 , $in_2 ]deref[13 , 12 , 0 , 0]
func
[13 , $out_2 ]deref[14 , 13 , 1 , 1]
func
[14 , $out_2 ]deref[15 , 14 , 0 , 0]
func
[15 , $in_2 ]deref[16 , 15 , 1 , 0]func
[16 , ’-’ _1 ]lockmem[17 , 15 , " state "]norules[17]
neqmem[17 , 10]
not [[
findatom[18 , 10 , ’dep ’ _1 ]proceed[]]]commit[" test " , 0]removeatom [3 , 2 , ’ current ’ _0 ]dequeueatom [3]newatom[19 , 17 , ’ current ’ _0 ]enqueueatom [19]freeatom[3]
unlockmem [17]unlockmem [10]unlockmem [2]unlockmem [1]proceed[]Compiled Rule-- atommatch :spec-- memmatch :specanymemnorulesanymemfindatomfindatom
deref
func
deref
func
deref
func
deref
func
deref
func
lockmem
norulesfindatom
deref
func
deref
func
deref
func
deref
func
deref
func

[2 , 2][1 , 37][1 , 0 , 0 , " element "][1][2 , 1 , 0 , " state "][3 , 2 , ’ current ’ _0 ][4 , 2 , ’+ ’ _1 ][5 , 4 , 0 , 1]
[5 , $in_2 ][6 , 5 , 0 , 0]
[6 , $out_2 ][7 , 6 , 1 , 1]
[7 , $out_2 ][8 , 7 , 0 , 0]
[8 , $in_2 ][9 , 8 , 1 , 0]
[9 , ’-’ _1 ][10 , 8 , " transition "][10][11 , 10 , ’+ ’ _1 ][12 , 11 , 0 , 1]
[12 , $in_2 ][13 , 12 , 0 , 0]
[13 , $out_2 ][14 , 13 , 1 , 1]
[14 , $out_2 ][15 , 14 , 0 , 0]
[15 , $in_2 ][16 , 15 , 1 , 0]
[16 , ’-’ _1 ]lockmem[17 , 15 , " state "]norules[17]
neqmem[17 , 10]findatom[18 , 10 , ’dep ’ _1 ]not [[
deref[19 , 18 , 0 , 1]
func
[19 , $in_2 ]deref[20 , 19 , 0 , 0]
func
[20 , $out_2 ]
deref[21 , 20 , 1 , 1]func
[21 , $in_2 ]
deref[22 , 21 , 0 , 0]
func
[22 , $out_2 ]deref[23 , 22 , 1 , 1]
func
[23 , $out_2 ]deref[24 , 23 , 0 , 0]
func
[24 , $in_2 ]
deref[25 , 24 , 1 , 0]func
[25 , ’+ ’ _1 ]lockmem[26 , 24 , " dependency "]norules[26]
findatom[27 , 26 , ’+ ’ _1 ]neqatom[27 , 25]deref
[28 , 27 , 0 , 1]func
[28 , $in_2 ]deref[29 , 28 , 0 , 0]
[29 , $out_2 ]
func
deref
[30 , 29 , 1 , 1]func
[30 , $out_2 ]deref[31 , 30 , 0 , 0]
func
[31 , $in_2 ]deref[32 , 31 , 1 , 1]func
[32 , $out_2 ]deref[33 , 32 , 0 , 0]func
[33 , $in_2 ]
deref[34 , 33 , 1 , 0]
func
[34 , ’ ref ’ _1 ]lockmem[35 , 33 , " state "]neqmem[35 , 42]not [[
findatom[36 , 35 , ’ current ’ _0 ]proceed[]]]unlockmem [26]unlockmem [35]proceed[]]]commit[" test " , 0]removeatom [3 , 2 , ’ current ’ _0 ]dequeueatom [3]newatom[37 , 17 , ’ current ’ _0 ]enqueueatom [37]freeatom[3]
unlockmem [17]unlockmem [10]unlockmem [2]unlockmem [1]proceed[]Inline参 考 文 献[1] András, B. and Dániel, V.: Advanced Model
Transformation Language Constructs in the VIATRA2 Framework, ACM Symposium on Applied
Computing — Model Transformation Track, ACM
Press, 2006.
[2] Arend, R., Iovka, B., Harmen, K., and Tom, S.:

User Manual for the GROOVE Tool Set, Department of Computer Science, University of Twente,
2014.
[3] Desel, J. and Reisig, W.: Place/transition PetriNets, Springer, 1998, pp. 122–173.
[4] Jensen, K. and Kristensen, L. M.: Colored PetriNets: A Graphical Language for Formal Modelingand Validation of Concurrent Systems, Commun.
ACM, Vol. 58, No. 6(2015), pp. 61–70.
[5] Kuroda, T., Nakanoya, M., Kitano, A., andGokhale, A.: The configuration-oriented planningfor fully declarative IT system provisioning automation, NOMS 2016 - 2016 IEEE/IFIP Network Operations and Management Symposium, April 2016,

pp. 808–811.
[6] Ueda, K.: LMNtal as a hierarchical logic programming language, Theoretical Computer Science,Vol. 410, No. 46(2009), pp. 4784–4800.
[7] 綾野貴之, 堀泰祐, 岩澤宏希, 小川誠司, 上田和紀: 統
合開発環境による LMNtal モデル検査, コンピュータ
ソフトウェア, Vol. 27, No. 4(2010), pp. 4 197–4 214.
[8] 後町将人, 堀泰祐, 上田和紀: LMNtal 実行時処理系の並列モデル検査器への発展, コンピュータ ソフトウェ
ア, Vol. 28, No. 4(2011), pp. 137–157.
[9] 齋藤諒人, 上田和紀: 階層グラフ書換え言語 LMNtalの表現力向上に向けたパターンマッチングモデルとその実現, 情報処理学会全国大会講演論文集, Vol. 80,
No. 1(2018), pp. 1-259–1-260.