これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド pbesrewr です。
プログラム：
NAME
pbesrewr - PBES を書き換えて簡素化する
SYNOPSIS
ペベスレワー [オプション] ... [インファイル [アウトファイル]]
DESCRIPTION
INFILE 内の PBES を書き換え、数量化された変数を削除し、結果の PBES を次のように書き込みます。
アウトファイル。 INFILE が存在しない場合は、stdin が使用されます。 OUTFILE が存在しない場合、stdout は
中古。
OPTIONS
オプション 次のいずれかになります。
-iFORMAT, - の=FORMAT
入力形式を使用するFORMAT： 'pbes'内部形式のPBES'pbes_text 'PBES in
内部テキスト形式 'テキスト'テキスト（mCRL2）形式のPBES 'bes'内部のBES
形式 'bes_text'内部テキスト形式のBES'cwi'CWI形式のBES'pgsolver '
PGSolver形式のBES
-oFORMAT, - アウト=FORMAT
出力形式 FORMAT を使用します: 内部形式 'pbes_text' PBES の 'pbes' PBES
内部テキスト形式 'text' テキスト (mCRL2) 形式の PBES
-pNAME, --pbes-リライター=NAME
PBES 書き換え戦略を使用します。 名前: 単純化するために 'simplify' (デフォルト)
'quantifier-all' はすべての量指定子を削除します。 'quantifier-finite' は次のとおりです。
XNUMX 点ルールの有限量子変数「quantifier-one-point」を削除します
量指定子消去 'pfnf' PFNF 標準形式に書き換える場合 'ppg'
書き換え用のパラメータ化パリティ ゲーム フォーム「bqnf-quantifier」に書き換えます
結合子上の量指定子から量指定子の結合子へ (実験的)
-QNUM, --qlimit=NUM
数量詞の列挙をNUM変数に制限します。 （デフォルトはNUM = 1000、NUM = 0の場合
無制限）。
-rNAME, -リライター=NAME
書き換え戦略を使用するNAME： 'jitty' jitty rewriting（デフォルト） 'jittyc'コンパイル済み
jitty rewriting'jittyp 'jitty rewriting with prover
-タイミング[=FILE]
タイミング測定値をFILEに追加します。 次の場合、測定値は標準誤差に書き込まれます
ファイルは提供されません
標準オプション：
-q, - 静かな
警告メッセージを表示しない
-v, -詳細
短い中間メッセージを表示する
-d, - デバッグ
詳細な中間メッセージを表示する
-ログレベル=LEVEL
レベルまでの中間メッセージを表示する
-h, - 助けて
ヘルプ情報を表示する
- バージョン
バージョン情報を表示する
onworks.net サービスを使用してオンラインで pbesrewr を使用する
