slim runtime option

SLIM実行時オプション

• -O3を標準で使います
• モデル検査器の出力結果のdefaultは, "状態数", "停止状態数", "反例パス"のみとし, 状態遷移グラフは出力しない
• defaultで様々な性能最適化フラグを立てて実行しているため, 必要に応じて--disable-*オプションを使用して最適化を無効にしてください

option	description
--nd	実行モードをRuntimeからModel Checkerへ切り替える
--translate	実行モードをRuntimeからLMNtal2C Translatorへ切り替える
-p	経過時間と消費したCPU時間(スレッド単位)を出力.
-p2	各ルールのTrial, Apply, Backtrack, 消費CPU時間を計測(実行性能にちょびっと影響, 要--enable-profile)状態空間探索終了後に, 状態数, メモリ, ハッシュ値を数え上げ出力
-p3	ボトルネックやピークメモリなどのon-the-flyなプロファイルをoとる (実行性能に影響. 要--enable-profile)
-t	実行パスを出力。状態遷移グラフを出力
--dump-lavit	状態遷移グラフの出力フォーマットをLaViT形式に指定
--dump-dot	LMNtalプロセスの出力フォーマットをGraphViz形式に指定。状態遷移グラフの出力フォーマットをGraphViz形式に指定
--dump-fsm	状態遷移グラフの出力フォーマットをFSM形式に指定(状態データ出力は工事中)
--dump-inc	状態空間の構築と状態出力を同時に行う(実行性能に影響)
--dump-lmn	LMNtalプロセスをLMNtal Syntaxで出力。反例出力をLMNtal Syntaxで出力
--help	オプションの使い方を出力
--version	バージョン
--hide-ruleset	ルールセットを表示しない
--show-proxy	proxyアトムを表示する
--show-chr	Uniq RuleSetを出力する際に, 履歴も出力する. (seijiのつけたオプション名から変更)
--show-ends	全ての最終状態を出力する
--show-transition	遷移オブジェクトを保持し, ルール名などの情報を出力可能にする(メモリ使用量が爆発するため注意)
--use-builtin-rule	システムルールセットやライブラリをロードして使用する
--ltl	LTLモデル検査を行う. 反例が1つ見つかった時点で打ち切る
--ltl-all	LTLモデル検査を全状態空間に対して行う.
--ltl-f <"formula">	入力したLTL式formulaを, 環境変数LTL2BAからltl2baに渡して性質Buchiオートマトンを取得する
--nc	性質Buchiオートマトンを記述したファイルを入力する
--psym	入力した性質オートマトンに対応する原始命題記号の定義を記述したファイル を入力する
--bfs	ポリシーを幅優先探索に切り替える(liveness未対応)
--use-Ncore=	スレッドによる並列実行を行う. defaultはStack-Slicing Algorithm. --bfsと併用すると, オープンノードリストを共有して並列処理.
--mem-enc	通常計算するバイト列(binary string)とは違い, 一意なidとなるバイト列を計算する
--delta-mem	膜の差分表現による状態生成手法を有効にする
--z-compress	バイト列をzlibを用いて更に圧縮する. (zlibがinstallされている環境ならば利用可能)
--d-compress	バイト列をzdelta libを用いて更に圧縮する.
--cutoff-depth=	並列実行時にDFS Stackの分割の閾値をに変更する. (default=7)
--disable-compress	バイト列エンコードを無効にする
--disable-compact	オープンノードを生成した際に直ちにmembraneを破棄する--compact-stackモードを無効にする
--disable-loadbalancer	並列実行時のDynamic Load Balancerを無効にする
--disable-opt-hash	膜のハッシュ関数から膜のIDへのrehash処理を無効にする
--benchmark	出力系統を全て落とし, プロファイル出力をCSV形式で吐く. 実験用
--no-dump	Profilerを除いた全ての出力系統を落とす. 実験用

開発用オプション

• 開発/debug用のオプションなど, より詳細は直接ソースコード(main.c)を見てください. 以下に示すオプションは開発用の裏オプションの一部です.

option	必要なconfigure flag	description
--debug-mc	--enable-debug	LTLモデル検査の探索アルゴリズムの実行をチェックする. とりあえずOWCTYアルゴリズムの反復状況をプリントするようにしている
--prof-nomemeq	--enable-profile	ハッシュ値が等しかったら等価な状態と判定してしまう(グラフ同形成判定をskip). 時間以外のプロファイルを取りたくて, ハッシュ値が完全に散らばることが既に分かっている場合, データ収集を円滑に行うために使う
--property-dump	なし	入力したNCファイル (*.nc) をLaViT形式で出力した後, 実行を打ち切る. --ndと併せて入力する必要あり. てきとうにlmnファイルも与える必要あり. 性質オートマトンがどんなものかを目視したいときに使う. 現在動くかは不明.