これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなど、複数の無料オンライン ワークステーションのいずれかを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド lpssuminst です。
プログラム:
NAME
lpssuminst - LPS の合計変数をインスタンス化する
SYNOPSIS
lpsuminst [オプション] ... [インファイル [アウトファイル]]
DESCRIPTION
INFILE で線形プロセス仕様 (LPS) の合計変数をインスタンス化する
結果を OUTFILE に書き込みます。 INFILE が存在しない場合は、stdin が使用されます。 OUTFILE が
存在しない場合、stdout が使用されます。
OPTIONS
オプション 次のいずれかになります。
-f, - 有限の
ソートが有限である変数のみをインスタンス化する
-QNUM, --qlimit=NUM
数量詞の列挙をNUM変数に制限します。 (デフォルトはNUM = 1000、NUM = 0の場合
無制限)。
-rNAME, -リライター=NAME
書き換え戦略を使用するNAME: 'jitty' jitty rewriting(デフォルト) 'jittyc'コンパイル済み
jitty rewriting'jittyp 'jitty rewriting with prover
-s[NAME], --並べ替え[=NAME]
展開する必要がある並べ替えを選択します (カンマ区切りのリスト)
例: ブール; ブール、リスト(Nat)
-t, --タウ
タウ加数でのみ変数をインスタンス化する
-タイミング[=FILE]
タイミング測定値をFILEに追加します。 次の場合、測定値は標準誤差に書き込まれます
ファイルは提供されません
標準オプション:
-q, - 静かな
警告メッセージを表示しない
-v, -詳細
短い中間メッセージを表示する
-d, - デバッグ
詳細な中間メッセージを表示する
-ログレベル=LEVEL
レベルまでの中間メッセージを表示する
-h, - 助けて
ヘルプ情報を表示する
- バージョン
バージョン情報を表示する
onworks.net サービスを使用してオンラインで lpssuminst を使用する
