これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド ltsconvert です。
プログラム：
NAME
ltsconvert - LTS を変換し、必要に応じて最小化します
SYNOPSIS
変換します [オプション] ... [インファイル [アウトファイル]]
DESCRIPTION
要求されたファイル内のラベル付き遷移システム (LTS) を INFILE から OUTFILE に変換します。
選択した最小化方法を適用した後の形式 (デフォルトはなし)。 OUTFILE が
提供されない場合は、stdout が使用されます。 INFILE が指定されていない場合は、stdin が使用されます。
出力形式は OUTFILE の拡張子によって決まりますが、入力形式は
INFILE の内容によって決まります。 オプション --in および --out を使用して入力を強制できます。
そして出力形式。 サポートされている形式は次のとおりです。
アルデバラン形式 (CADP) の場合は「aut」、
GraphViz 形式の場合は「dot」 (入力形式としてサポートされなくなりました)、
有限ステート マシン形式の場合は「fsm」、または
mCRL2 LTS 形式の場合は「lts」 (デフォルト)
OPTIONS
オプション 次のいずれかになります。
-D, --決定する
LTSを決定する
-eNAME, - 等価=NAME
同等の LTS を生成し、同等の NAME: 'none' アイデンティティを維持します
等価性 (デフォルト) 'bisim' 強い二重類似性 'bisim-sig' 強い二重類似性
署名改良 'branching-bisim' を使用して分岐双類似性 'branching-
bisim-sig '署名改良'dpbranching-bisim'を使用した分岐双類似性
分岐双類似性を維持する分岐 'dpbranching-bisim-sig' 分岐
シグネチャ改良「weak-bisim」を使用して分岐の双類似性を維持する
双類似性 'weak-bisim-sig' 署名改良を使用した弱い双類似性 'dpweak-
bisim' の発散、弱い双類似性を維持する 'dpweak-bisim-sig' の発散
シグネチャ改良「sim」を使用して弱い二重類似性を維持する強力なシミュレーション
等価性 'trace' 強いトレースの等価性 'weak-trace' 弱いトレースの等価性
「タウスター」タウスターの還元
-iFORMAT, - の=FORMAT
入力形式として FORMAT を使用する
-lFILE, --lps=FILE
入力 LTS の生成元の LPS として FILE を使用します。 これは必要になるかもしれません
fsm 形式で保存するときに状態の正しいパラメータ名を保存し、
非 mCRL2 LTS を mCRL2 LTS に変換する
--到達不能
入力 LTS の到達可能性チェックを実行しません。
-n, -状態なし
ドット形式で保存する場合は状態情報を省略します
-oFORMAT, - アウト=FORMAT
出力形式として FORMAT を使用する
--タウ=行為名
カンマ区切りリスト ACTNAMES 内の名前を持つアクションは内部アクションであるとみなします。
(tau) 入力によって定義されたアクションに加えてアクション
-タイミング[=FILE]
タイミング測定値をFILEに追加します。 次の場合、測定値は標準誤差に書き込まれます
ファイルは提供されません
標準オプション：
-q, - 静かな
警告メッセージを表示しない
-v, -詳細
短い中間メッセージを表示する
-d, - デバッグ
詳細な中間メッセージを表示する
-ログレベル=LEVEL
レベルまでの中間メッセージを表示する
-h, - 助けて
ヘルプ情報を表示する
- バージョン
バージョン情報を表示する
onworks.net サービスを使用してオンラインで ltsconvert を使用する
