問題タブ [transition-systems]

移行システムでいくつかの操作を実行できるツールを作成しており、それらを視覚化する必要もあります。

ruby-gem に関するドキュメントはあまりありませんが (これは私が入手できる最高のものでした: http://www.omninerd.com/articles/Automating_Data_Visualization_with_Ruby_and_Graphviz )、移行システムからグラフを作成することができました。(自由に使用してください。サンプルコードはあまりありません。コメント/質問も大歓迎です)

私ができない唯一のことは、「何もないところから」開始状態に矢印を描くことです。提案は誰ですか？

Z3 の PDR エンジンを使用して、遷移系の不変式を証明します。遷移システムに、特定の状態に到達するために通過する必要があるカウンター ループが含まれている場合、パフォーマンスは低下します。

次のソース コードでは、 Z3 Fixedpoint Homepageの遷移システム Python クラスで実装された 3 つの状態と 3 つの遷移を含む遷移システムの例を示します。最後の行には、状態 L0 から開始して状態 L2 に到達するクエリがあります。したがって、遷移 t2 は y 回通過する必要があります。

y==10 を初期化すると、答えは高速に計算されます。ただし、初期化 y==1000 ではパフォーマンスが低下します。

L0 から L2 へのパスを別の方法で計算し、Z3 のパフォーマンスを向上させる可能性はありますか?

私はプロメラが初めてです。私はpromelaで書かれたプログラミングを持っています:

このプログラムの遷移システムを描く方法を知っている人はいますか?

HTTP インタラクション、つまり HTTPRequest/HTTPResponse のシーケンスをモデル化したいのですが、これをトランジション システムとしてモデル化しようとしています。以下を使用して、クラス State の順序付けを定義しました。

ここで、State は単なるメッセージのセットです。

(HTTPRequest->HTTPResponse) と (HTTPResponse->HTTPRequest) の各ペアは、移行システムのルールとして表されます。ルールは、ある状態から別の状態に移動できるようにする述語として Alloy で表現されます。

たとえば、これは特定の HTTPRequest が受信された後に HTTPResponse を生成するルールです。

残念ながら、作成されたモデルは複雑すぎるようです。多数のルールがあり (上記のものよりも複雑ですが、同じパターンに従います)、実行は非常に遅くなります。

編集:特に、CNF の生成は非常に遅く、解決にはかなりの時間がかかります。

同様の移行システムをモデル化する方法について何か提案はありますか?

どうもありがとうございました！

依存関係パーサーではないパーサーを開発していますが、それでも遷移ベースのシステムです。arc-transition のように SHIFT、REDUCE-LEFT、REDUCE-RIGHT の 3 つのアクションを使用する代わりに、パーサーに独自のアクションを提案しました。Andor らの論文による私の理解として。(2016)、システムが論文で定義されたいくつかのルールに従う限り、遷移ベースのシステムで SyntaxNet をトレーニングできます。しかし、どこから始めればよいか正確にはわかりません。私はコードを見ましたが、それらは主に依存関係パーサーをトレーニングするためのもののようです（3つのアクションSHIFT、REDUCE-LEFT、およびREDUCE-RIGHTを使用）。私の目標を達成するのに役立つコードの一部を強調していただければ幸いです。

また、SyntaxNet が ConNLL データ形式をゴールド トレーニング データに変換する方法がよくわかりません。このタスクを担当するソース ファイルを教えてもらえますか?

事前にどうもありがとうございました