pbes2bool - クラウドでオンライン

プログラム：

NAME

pbes2bool - PBES から BES を生成し、それを解決します。

SYNOPSIS

pbes2bool [オプション] ... [インファイル]

DESCRIPTION

INFILE から (P)BES を解決します。 INFILE が存在しない場合は、stdin が使用されます。

OPTIONS

オプション 次のいずれかになります。

-c, - カウンター
最後に、の左側のインスタンス化でラベル付けされたツリーを出力します。
方程式; このツリーは、pbes2bool がどのようにして有効になったかを示しています。
PBESの無効性

-eLEVEL, --消去=LEVEL
bes 変数を削除するには、削除レベル LEVEL を使用します。 'none' 生成された bes は削除しません
変数。 これにより、メモリが過剰に使用される可能性があります。 (デフォルト) '一部' 削除
生成される変数は使用されない変数です。ただし、その右側が
方程式は真か偽です。 次の場合、変数の右辺を再計算する必要があります。
再び遭遇しましたが、これはごく普通のことです。 'all' は、すべての bes 変数を削除します。
もうどの方程式でも使用されません。 これは非常にメモリ効率が良いですが、
削除された bes 変数の rhss を次のようにする必要があるため、非常に時間がかかります。
かなり頻繁に再計算されます。

-H, --ハッシュテーブル
bes 方程式に代入するときにハッシュテーブルを使用し、内部を変換します。
二分決定図への式 (パフォーマンスのため非推奨)

-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 を使用します (このオプションは非推奨です。ツール pbes2bes を使用します)
代わりに）。

-QNUM, --qlimit=NUM
数量詞の列挙をNUM変数に制限します。 （デフォルトはNUM = 1000、NUM = 0の場合
無制限）。

-rNAME, -リライター=NAME
書き換え戦略を使用するNAME： 'jitty' jitty rewriting（デフォルト） 'jittyc'コンパイル済み
jitty rewriting'jittyp 'jitty rewriting with prover

-z検索, - 探す=検索
検索戦略を使用します。 SEARCH: '幅優先' の右辺を計算します。
ブール変数は先着順で使用されます。 これは、
幅優先検索。 これは反例を生成するのに適しています。 （デフォルト）
'深さ優先' ブール変数の右辺を計算します。
生成された変数が最初に調査されます。 これは深さ優先に対応します
検索。 これは、
式は、より深い深さの後に決定されます。 'b' 幅優先の短縮形。
「d」 深さ優先の短縮形。

-sストラット, - ストラテジー=ストラット
置換戦略 STRAT を使用します: '0' 使用できるすべてのブール方程式を計算します。
最適化を行わずに初期状態から到達しました。 これが最も多くのデータです
生成された方程式ごとの効率的なオプション。 (デフォルト) '1' すぐに最適化します
すでに調査されている真の変数の右辺を代入します。
式を生成する場合は false。 これは 0 と同じくらいメモリ効率が良いです。
1 に加えて、true または false の変数をすでに設定されている変数に置き換えます。
右側が生成されます。 これは、特定の変数が到達不能になることを意味する場合があります
(例: X0 が他に発生しないと仮定して、X0 と X1 の X1、X0 が false になるとき。
どの変数が到達不能になったかは維持されます。
調査されることになる。 PBES によっては、これにより、
BES は大幅に生成されますが、より大きなメモリ フットプリントが必要になります。 「3」イン
2 に加えて、生成された変数がループ上で発生するかどうかを調査します。
固定小数点シンボルに応じて true または false に設定できます。
これにより、方程式の生成に必要な時間が大幅に増加する可能性があります。

-タイミング[=FILE]
タイミング測定値をFILEに追加します。 次の場合、測定値は標準誤差に書き込まれます
ファイルは提供されません

-u, --unused_data
データ仕様の未使用部分を削除しないでください

標準オプション：

-q, - 静かな
警告メッセージを表示しない

-v, -詳細
短い中間メッセージを表示する

-d, - デバッグ
詳細な中間メッセージを表示する

-ログレベル=LEVEL
レベルまでの中間メッセージを表示する

-h, - 助けて
ヘルプ情報を表示する

- バージョン
バージョン情報を表示する

onworks.net サービスを使用してオンラインで pbes2bool を使用する