これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、または MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの 2 つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド lpsXNUMXlts です。
プログラム：
NAME
lps2lts - LPS から LTS を生成します
SYNOPSIS
lps2lts [オプション] ... [インファイル [アウトファイル]]
DESCRIPTION
INFILE の LPS から LTS を生成し、結果を OUTFILE に保存します。 INFILE がそうでない場合
供給されている場合は、stdin が使用されます。 OUTFILE が指定されていない場合、LTS は保存されません。
「jittyc」リライターが使用されている場合、MCRL2_COMPILEREWRITER 環境変数
(デフォルト値: 'mcrl2compilerewriter') リライターをコンパイルするスクリプトを決定します。
MCRL2_COMPILEDIR (デフォルト値: '.') は、一時ファイルの保存場所を決定します。
lps2lts は、任意のペア間で同じラベルを持つ複数の遷移を配信できることに注意してください。
州。 これが望ましくない場合は、強力な効果を適用することでそのような遷移を削除できます。
たとえば ltsconvert ツールを使用したバイシミュレーションの削減。
OUTFILE の形式は、(拡張子で指定されていない限り) 拡張子によって決まります。
オプション）。 サポートされている形式は次のとおりです。
アルデバラン形式 (CADP) の場合は「aut」、
GraphViz 形式の場合は「dot」 (入力形式としてサポートされなくなりました)、
有限ステート マシン形式の場合は「fsm」、または
mCRL2 LTS フォーマットの「lts」 jittyc リライターが使用されている場合、
MCRL2_COMPILEREWRITER 環境変数 (デフォルト値: mcrl2compilerewriter)
リライターをコンパイルするスクリプトと MCRL2_COMPILEDIR (デフォルト値:
'.') は、一時ファイルが保存される場所を決定します。 lps2lts は複数のファイルを配信できることに注意してください。
状態のペア間で同じラベルを持つ遷移。 これが望ましくない場合は、そのような
トランジションは、たとえば次のような強力なバイシミュレーション リダクトンを適用することで削除できます。
ツールは変換します。
OPTIONS
オプション 次のいずれかになります。
-a名前, - アクション=名前
アクション名が次のトランジション システム内のアクションを検出して報告します。
NAMES、カンマ区切りのリスト。 これは、たとえば、
存在しない）アクションエラーがないこと。 次のいずれかが発生するたびにメッセージが出力されます。
これらのアクション名。 -t フラグを使用すると、これらのアクションに対するトレースが生成されます
-b[NUM], --ビットハッシュ[=NUM]
ビット ハッシュを使用して状態を保存し、最大 NUM 個の状態を保存します。 この意味は
訪問したすべての状態の完全な記録を保持する代わりに、ビット配列を使用します。
状態のハッシュが以前に見られたかどうかを示すために使用されます。
これは、このオプションにより州が他の州と誤解される可能性があることを意味しますが、
(同じハッシュにマップされているため)、非常に大規模なデータを探索するのに役立つ場合があります。
それ以外の場合は探索できない LTS。 NUM のデフォルト値はおよそ
2*10^8 (これは約 25MB のメモリに相当します)
-キャッシュ
列挙型キャッシュ技術を使用して、状態空間の生成を高速化します。
-c[NAME], - 合流[=NAME]
アクション ラベル NAME を使用して遷移の優先順位付けを適用します。(NAME が指定されていない場合)
指定された (つまり、「-c」) 優先度は、アクション「ctau」に与えられます。 を優先するには
tau にはフラグ -ctau を使用します。 線形プロセスがタウコンフルエントではない場合、
生成された状態空間は必然的に、次の状態空間と似た形で分岐します。
LP。 使用される生成アルゴリズムは線形プロセスを必要としません
タウが収束すること。
-D, --デッドロック
デッドロックを検出します (つまり、デッドロックごとにメッセージが出力されます)
-F, - 発散
発散を検出します (つまり、発散のあるすべての状態 (= タウ ループ) に対して、メッセージは
印刷されています）。 発散を検出するアルゴリズムはすべての状態に対して線形であるため、
このオプションをオンにすると、状態空間の探索が XNUMX 次になり、状態が発生します。
このオプションを有効にすると、宇宙探査が遅くなります。
-yBOOL, - ダミー=BOOL
LPS 内のフリー変数を BOOL の値に基づいたダミー値に置き換えます。
「はい」(デフォルト) または「いいえ」
--エラートレース
探索中にエラーが発生した場合は、トレースを保存できなかった状態に保存します。
探検した
--init-tsize=NUM
内部で使用されるハッシュ テーブルの初期サイズを設定します (デフォルトは 10000)
-lNUM, --最大=NUM
最大 NUM 個の州を探索する
-m名前, --マルチアクション=名前
カンマ NAMES からのトランジション システム内のマルチアクションを検出して報告します。
区切られたリスト。 複数のアクションが正確に一致することを除いて、-a と同様に機能します。
データパラメータを含む。
-いいえ-情報
状態情報を OUTFILE に追加しません。このオプションを使用しない場合、lps2lts は状態を追加します
LTS へのベクトル。 このオプションを選択すると、この情報が破棄され、次の状態が表示されます。
シーケンス番号のみで示されます。 明示的な状態情報は次の場合に役立ちます。
たとえば視覚化が目的ですが、OUTFILE が大きくなる可能性があります
かなり。 AUT 形式で書き込む場合、このオプションは暗黙的であることに注意してください。
-oFORMAT, - アウト=FORMAT
出力を指定された形式で保存します
- プルーン
サマンド プルーニングを使用して状態空間の生成を高速化します。
-QNUM, --qlimit=NUM
数量詞の列挙をNUM変数に制限します。 （デフォルトはNUM = 1000、NUM = 0の場合
無制限）。
-rNAME, -リライター=NAME
書き換え戦略を使用するNAME： 'jitty' jitty rewriting（デフォルト） 'jittyc'コンパイル済み
jitty rewriting'jittyp 'jitty rewriting with prover
-sNAME, - ストラテジー=NAME
戦略名: 'b', 'breadth' 幅優先探索を使用して状態空間を探索します
(デフォルト) 'd'、'length' 深さ優先検索 'p'、'prioritized' 単一の優先順位
最初の引数のアクションは Nat の種類であり、
このパラメータの最小値が選択されます。 たとえばアクションがある場合 a（3）と
b（4） a(3) 残っているものと b(4)は省略します。 ソートの最初のパラメータを持たないアクション
複数のアクションを持つ Nat およびマルチアクションが常に選択されます (オプションは
実験的) 'q'、'rprioritized' は、最初の引数に基づいてアクションを優先します。
Nat を並べ替え (オプション --prioritized を参照)、これらの XNUMX つをランダムに選択して、
優先順位付きランダム シミュレーション (オプションは実験的) 'r'、'random' ランダム
シミュレーション。 すべての次の状態の中から、次の状態が存在するかどうかに関係なく、ランダムに XNUMX つが選択されます。
この状態はすでに観察されています。 したがって、ランダムなシミュレーションのみ
デッドロック状態になると終了します。
-抑制
詳細モードでは、訪問数を示す進行状況メッセージを出力しません。
状態と遷移。 大規模な状態空間の場合、進行状況メッセージの数は増加します。
かなり恐ろしいことになる。 この機能はそれらを抑制するのに役立ちます。 その他の詳細なメッセージ、
調査された州の総数などは、表示されたままになります。
-タイミング[=FILE]
タイミング測定値をFILEに追加します。 次の場合、測定値は標準誤差に書き込まれます
ファイルは提供されません
--todo-max=NUM
ToDo リストには最大 NUM 個の状態を保持します。 このオプションは幅にのみ関係します。
最初の検索。NUM はレベルごとの最大状態数であり、深さは
最初の検索。NUM は最大深さです。
-t[NUM], - 痕跡[=NUM]
NAMES からのアクションで到達する各状態への最短のトレースを書き込みます。
オプション --action、 --deadlock で検出されたデッドロック、または分岐
ファイルへの --divergence で検出されました。 NUM 個を超えるトレースは書き込まれません。 もしも
NUM が指定されていない場合、トレースの数には制限がありません。各トレースに対して、
拡張子 .trc (トレース) を持つ固有のファイルが作成され、
初期状態からデッドロック状態までの最短のトレース。 痕跡は次のとおりです。
きれいに印刷され、tracepp を使用して他の形式に変換されます。
-u, --未使用データ
データ仕様の未使用部分を削除しないでください
標準オプション：
-q, - 静かな
警告メッセージを表示しない
-v, -詳細
短い中間メッセージを表示する
-d, - デバッグ
詳細な中間メッセージを表示する
-ログレベル=LEVEL
レベルまでの中間メッセージを表示する
-h, - 助けて
ヘルプ情報を表示する
- バージョン
バージョン情報を表示する
onworks.net サービスを使用してオンラインで lps2lts を使用する
