ペトリネット展開プレフィックスをJavaに保存するためのmciファイル形式を解析して、それを使用してSAT式を生成できるようにしたい
以下のテキストは、ペトリネット展開プレフィックスを保存するための MCI ファイル形式を説明しています。
以下では、CHAR は 1 バイトの char であり、UINT4 はリトル エンディアンです (つまり、最下位バイトは最下位アドレスにあり、他のバイトは重要度の昇順で続きます)。 -エンディアン)。
条件の総数 (UINT4)
イベントの総数 (UINT4)
各イベント (最初から最後まで): -- 元のトランジションの番号 (UINT4)
各条件について (最初から最後まで): -- 元の場所の番号 (UINT4) -- プリセット イベントの番号 (UINT4); 条件が初期の場合は 0 -- ポストセット イベント番号 (UINT4) の NULL(UINT4) で終了するリスト
各カットオフ イベントの数 -- カットオフ イベントの数 (UINT4) -- 対応するイベントの数 (UINT4) または対応するイベントが仮想初期イベントの場合は NULL(UINT4)
NULL(UINT4)の分離
各構成について: -- NULL(UINT4) で終わるイベント番号のリスト。(これは一部の古いモデル チェッカーで使用されます。PUNF はそれを作成せず、終端の NULL(UINT4) を出力するだけです。)
NULL(UINT4)の分離
元のネットの合計桁数 (UINT4)
元のネットの遷移の総数 (UINT4)
場所/トランジション名の最大文字列長 (UINT4) (パーサーでのメモリ割り当てに役立ちます)
元のネットの各場所: -- 名前 (NULL(CHAR) で終わる文字列)
NULL(UINT4)の分離
元のネットの各遷移: -- 名前 (NULL(CHAR) で終わる文字列)
NULL(UINT4) を終了します。
注：C ++で実装しましたが、Javaで実装したいです。ご参考までに。私は非常に多くのツールを使用してJavaに変換しましたが、どれも完全に機能しませんでした. ですから、皆さんからの助けに感謝します。さらに、必要に応じてコードを C++ に入れます。