これは、Ubuntu Online、Fedora Online、Windowsオンラインエミュレーター、MACOSオンラインエミュレーターなどの複数の無料オンラインワークステーションのXNUMXつを使用してOnWorks無料ホスティングプロバイダーで実行できるコマンドマリアです。
プログラム：
NAME
maria-高レベルのペトリネット用のモジュラー到達可能性アナライザー
SYNOPSIS
マリア [オプション] ファイル...
DESCRIPTION
このマニュアルページでは、 マリア 指図。 より完全なドキュメントは
GNU情報形式で利用可能。 下記参照。
マリア は、入力で説明されている同時システムのモデルを分析するプログラムです。
代数システムネットに基づく言語。 形式主義はEkkartによって提示されました
ICATPN'98でのKindlerとHagenVölzer、 柔軟性 in 代数的 ネッツ.
代数システムネットは、データ型や代数を定義しないフレームワークです。
オペレーション。 マリアのデータ型システムと操作は、高レベルで設計されています
プログラミングと仕様言語を念頭に置いてください。 それにもかかわらず、各マリアモデルには
有限の展開。
低レベルのペトリネットツールとの相互運用性を確保するために、Mariaは識別子を次のように変換します。
展開されたネットを英数字とアンダースコアの文字列に変換します。 フィルター
フォルダ名.pl 識別子の読みやすさを向上させるために使用または適合させることができます。
OPTIONS
Mariaは通常のGNUコマンドライン構文に従い、XNUMXで始まる長いオプションを使用します
ダッシュ（ `-'）。 オプションの概要は以下に含まれています。 完全な説明については、を参照してください。
情報ファイル。
-a 制限, --array-limit =制限
配列インデックスタイプのサイズをに制限する 制限 可能な値。 0の制限
チェックを無効にします。
-b , --幅優先探索=
の到達可能性グラフを生成します 幅優先探索を使用します。
-C ディレクトリにジョブを開始します。, --compile =ディレクトリにジョブを開始します。
でCコードを生成する ディレクトリにジョブを開始します。 式の評価と低レベルの
遷移インスタンス分析アルゴリズムのルーチン。 このオプションを使用すると、
評価エラーは、わずかに異なる方法で報告されます。 通訳
状態の最初のエラーの原因となった評価と式を表示します。 the
コンパイルされたコードはエラーの数を表示します。 パフォーマンス上の理由から、
生成されたコードは、マルチセットにアイテムを追加するときにオーバーフローエラーをチェックしません。
-NS、 --no-コンパイル
の反対 -C。 組み込みのインタープリターですべての式を評価します。 これは
デフォルトの動作。
-D シンボル, --define =シンボル
プリプロセッサシンボルを定義する シンボル.
-d , --深さ優先探索=
の到達可能性グラフを生成します 深さ優先探索を使用します。
-E インターバル, --edges =インターバル
到達可能性グラフを生成するときは、毎回グラフのサイズを報告してください
インターバル 生成されたエッジ。
-e 文字列, --execute =文字列
実行する 文字列.
-g グラフファイル, --グラフ=グラフファイル
以前に生成された到達可能性グラフをからロードします グラフファイル.rgh.
-H h[,f[,t]], --hashes =h[,f[,t]]
確率的検証用のパラメーターを構成します（-P）。 割り当てる t ユニバーサル
のハッシュ関数 f の要素と対応するハッシュテーブル h 各ビット。 両方 h
& f 次の適切な値に切り上げられます。
-?、 -NS、 - 助けて
コマンドラインオプションの概要をMariaに出力して、終了します。
-I ディレクトリにジョブを開始します。, --include =ディレクトリにジョブを開始します。
追加 ディレクトリにジョブを開始します。 インクルードファイルを検索するディレクトリのリストに移動します。
-i コラム, -幅=コラム
出力の右マージンをに設定します コラム。 デフォルトは80です。
-j ラボレーション, --jobs =ラボレーション
安全性を確認する場合（オプション -L, -M & -P）、この多くの労働者を使用してください
マルチプロセッサコンピュータでの分析を高速化するプロセス。 も参照してください -k &
-Z.
-k ポート[/host], --connect =ポート[/host]
安全モデル検査を配布する（オプション -L, -M & -P）TCP/IPネットワーク内。 にとって
サーバーのみ ポート 16ビットの符号なし整数として指定されます。通常は
1024および65535。ワーカープロセスの場合、 ポート/host ポートとを指定します
サーバーのアドレス。 も参照してください -j.
-L , --lossless =
負荷 到達可能な状態のセットを構築することにより、それを分析する準備をします
ディスクファイルで。 も参照してください -M, -P, -j & -k.
-m , --model =
負荷 到達可能性グラフをクリアします。
-M , --md5-compacted =
負荷 の過剰近似を構築することにより、それを分析する準備をします
メインメモリ内の到達可能な状態のセット。 も参照してください -P, -L, -j & -k.
-N クレグエクスプ, --name =クレグエクスプ
コンテキストで許可される名前を指定します c 拡張正規表現として 正規表現.
コンテキストは、パラメータ文字列の最初の文字で識別されます。 the
後続の文字は、許可された名前がしなければならない正規表現を構成します
一致しています。
-n クレグエクスプ, --no-name =クレグエクスプ
コンテキストで許可されていない名前を指定してください c 拡張正規表現として
正規表現.
両方の場合 -N および -n コンテキストに指定されています c、その後、許可マッチがかかります
優先順位。 たとえば、すべてのユーザー定義の型名が
で終了 _t、指定する -nt -Nt'_t $'。 後者のパラメーターの引用符は次のとおりです。
から特別な意味を取り除くために必要 $ コマンドラインシェルでは、
おそらくマリアを呼び出すために使用します。
-P , --確率的=
負荷 到達可能な状態のセットを構築することにより、それを分析する準備をします
と呼ばれる手法を使用してメインメモリに ビットステート ハッシュ.
-p command, --property-translator = command
プロパティオートマトンの変換に使用するコマンドを指定します。 コマンドは
標準入力から数式を読み取り、対応するオートマトンを書き込みます
標準出力への説明。 翻訳者 百万ポンド これと互換性があります
オプションを選択します。
-q 制限, --定量限界=制限
を超えるタイプの定量化（マルチセット合計）を防止します 制限 可能
値。 制限が0の場合、チェックは無効になります。
-U シンボル, --undefine =シンボル
プリプロセッサシンボルの定義を解除します シンボル.
-u [a][f[アウトファイル]], --展開=[a][f[アウトファイル]]
アルゴリズムを使用してネットを展開する a そしてそれをフォーマットで書く f 〜へ アウトファイル。 場合 アウトファイル
指定されていない場合は、展開されたネットを標準出力にダンプします。 可能なフォーマット
m （マリア（人間が読める形式）、デフォルト）、 l （LoLA）、 p （PEP）、および r （PROD）。 三
XNUMXつのアルゴリズムがあります：従来の（デフォルト）と構築することによって削減された カバー可能
マーキング (M).
-V、 - バージョン
マリアのバージョン番号を印刷して終了します。
-v、 -詳細
分析のさまざまな段階に関する詳細な情報を表示します。
-W、 -警告
疑わしいネット構造に関する警告を有効にします。 これがデフォルトの動作です。
-w、 -警告なし
の反対 -W。 すべての警告を無効にします。
-x ナンバーベース, -基数=ナンバーベース
診断出力の基数を指定します。 の許容値 ナンバーベース
10月, 8進数, 8, 16進法, 16進数, 16, 12月, 10進数 & 10。 デフォルトでは使用します
XNUMX進数。
-Y、 --圧縮-非表示
の継承状態を保存しないことにより、到達可能な状態のセットを減らします。
遷移するインスタンス 隠す 条件が成立します。 隠された後継者は
別の状態セットに保存されます。 このオプションはメモリを節約する可能性があります（-L or -m）または削減
状態が省略される確率（-M or -P）、そしてそれは改善するかもしれません
並列分析の効率（-j or -k）、しかしそれはまたかなり増加するかもしれません
プロセッサ時間の要件。 このオプションは、活性モデルでも機能します
チェックしますが、活力特性の真理値が保証されるわけではありません
変更されません。 このオプションは、 -Z.
-y、 --圧縮なし-非表示
の反対 -Y。 これがデフォルトの動作です。
-Z、 --圧縮パス
にある中間状態を保存しないことにより、到達可能な状態のセットを減らします。
ほとんどの後継者。 このオプションはメモリを節約する可能性があります（-L or -m）または削減
状態が省略される確率（-M or -P）、そしてそれは効率を改善するかもしれません
並列分析の-j or -k）、しかしそれはまたかなり増加するかもしれません
プロセッサ時間の要件。 このオプションは、活性モデル検査でも機能します。
しかし、活力特性の真理値が残るという保証はありません
変更なし。 このオプションは、 -Y.
-z、 --no-compress-paths
の反対 -Z。 これがデフォルトの動作です。
onworks.netサービスを使用してオンラインでmariaを使用する
