これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド lpsinvelm です。
プログラム：
NAME
lpsinvelm - 不変式をチェックし、これらを使用して LPS の加数を単純化または削除します
SYNOPSIS
lpsinvelm [オプション]... --invfile=INVFILE [インファイル [アウトファイル]]
DESCRIPTION
ブール式 (Bool ソートの mCRL2 データ式) が次のように指定されているかどうかを確認します。
invariant は、INFILE の線形プロセス仕様 (LPS) の不変式です。 これなら
この場合、ツールは条件に違反する LPS の加数をすべて削除します。
不変であり、結果を OUTFILE に書き込みます。 INFILE が存在する場合は、stdin が使用されます。 もし
OUTFILEは存在せず、stdoutが使用されます。
このツールは、指定された LPS の加数の条件を簡素化するために使用することもできます。
OPTIONS
オプション 次のいずれかになります。
-y, --すべての違反
不変条件の違反が XNUMX つ見つかってもすぐに終了するのではなく、
代わりにすべての違反を報告してください
-c, -反例
不変式が違反される可能性がある理由を示す評価を表示します。
被加数が不変式に違反するかどうかが不確かである
-o, - 誘導
リストに誘導を適用する
-iINVファイル, -不変=INVファイル
INVFILEでブール式（BoolソートのmCRL2データ式）を次のように使用します。
不変
-n, -いいえ-チェック
到達不可能な加数を削除する前に不変式が成立するかどうかをチェックしない
-e, --消去なし
加数を削除または単純化せず、各条件に不変式を追加します。
-pプレフィックス, --print-dot=プレフィックス
かどうかを判断できない場合は、結果の BDD の .dot ファイルを保存します。
summand は不変条件に違反します。 PREFIX は出力ファイルのプレフィックスとして使用されます
-QNUM, --qlimit=NUM
数量詞の列挙をNUM変数に制限します。 （デフォルトはNUM = 1000、NUM = 0の場合
無制限）。
-rNAME, -リライター=NAME
書き換え戦略を使用するNAME： 'jitty' jitty rewriting（デフォルト） 'jittyc'コンパイル済み
jitty rewriting'jittyp 'jitty rewriting with prover
-l, --単純化-すべて
加数を単に削除するのではなく、すべての加数の条件を単純化します。
不変式と結合した条件は矛盾します
-zソルバー, --smt-ソルバー=ソルバー
SOLVERを使用して、内部で使用されるBDDから一貫性のないパスを削除します（デフォルトでは、
パス除去は適用されません）： 'cvc'SMTソルバーCVC3
-tLIMIT, - 制限時間=LIMIT
単一の式の証明に最大でLIMIT秒を費やします
-タイミング[=FILE]
タイミング測定値をFILEに追加します。 次の場合、測定値は標準誤差に書き込まれます
ファイルは提供されません
標準オプション：
-q, - 静かな
警告メッセージを表示しない
-v, -詳細
短い中間メッセージを表示する
-d, - デバッグ
詳細な中間メッセージを表示する
-ログレベル=LEVEL
レベルまでの中間メッセージを表示する
-h, - 助けて
ヘルプ情報を表示する
- バージョン
バージョン情報を表示する
onworks.net サービスを使用してオンラインで lpsinvelm を使用する
