問題タブ [model-checking]

私のモデル チェック コードでは、特定の変数の最大値を見つけることにのみ関心があります。私が今採用している手順は、assert ステートメントを持ちassert( var < MAX_VALUE )、MAX_VALUE を二分探索方式で変更し続けることです。ただし、SPIN が実際に 1 回の実行で変数の最大可能値を与える方法を持っていれば、はるかに優れています。supUPPAALにはそのためのオペレーターがあることを知っています。SPINに同等のものはありますか?

HTTP インタラクション、つまり HTTPRequest/HTTPResponse のシーケンスをモデル化したいのですが、これをトランジション システムとしてモデル化しようとしています。以下を使用して、クラス State の順序付けを定義しました。

ここで、State は単なるメッセージのセットです。

(HTTPRequest->HTTPResponse) と (HTTPResponse->HTTPRequest) の各ペアは、移行システムのルールとして表されます。ルールは、ある状態から別の状態に移動できるようにする述語として Alloy で表現されます。

たとえば、これは特定の HTTPRequest が受信された後に HTTPResponse を生成するルールです。

残念ながら、作成されたモデルは複雑すぎるようです。多数のルールがあり (上記のものよりも複雑ですが、同じパターンに従います)、実行は非常に遅くなります。

編集:特に、CNF の生成は非常に遅く、解決にはかなりの時間がかかります。

同様の移行システムをモデル化する方法について何か提案はありますか?

どうもありがとうございました！

NuSMV で Kripke の構造を作成し、いくつかのプロパティを確認する必要があります。

誰か助けて？構造とプロパティ (LTL、CTL、および CTL*) は写真にあります。

ここに構造とプロパティがあります：

http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%202014-10-16%20at%2016.52.34.png

基本的に、モデル チェックでは、モデル 'm' (システムの動作記述) と、システムが満たすプロパティ 'p' を扱います。どちらのアーティファクトでも、モデル チェッカーはモデルがプロパティを満たすかどうかを判断します。

私の質問は、モデル 'm' を LTL 式として指定し、LTL 'm' としてのモデルがプロパティ 'p' を満たすかどうかを確認できるかどうかです。

理論的には、LTL 式 'p' 用とモデル 'm' を記述する LTL プロパティ用の 2 つの Büchi オートマトンを生成できるため、このアプローチはうまくいくと思います。2 つの非決定性オートマトンの共通部分が空の場合、LTL としてのモデル 'm' はプロパティを満たします。

誰かが私にヒントを与えることができますか？出来ますか？

Promela でオブジェクトの発射体の軌道をモデル化し、モデルのいくつかのプロパティを検証したいと考えています。しかし、Promela には浮動小数点データ型がありません。したがって、たとえば、発射体のモーション パラメータを計算することはできません。たとえば、正弦/余弦などの三角関数を計算できないため、発射体の動きをモデル化できません。

この問題の回避策は何ですか? そのようなシステムを Promela でモデル化するにはどうすればよいでしょうか?

秒によると。The SMT- LIBv2 Language and Tools: A Tutorialの 3.9.3 では、SMT-LIBv2 で次のような複合ソートを宣言できます。

私は CVC4 を使用していますが、この構文を受け入れるようです。しかし、要素にアクセスするにはどうすればよいでしょうか? 私は次のことを試しました（およびそのさまざまなバリエーションと、オンラインで見つけた他のもの）：

しかし、これらの演算子はベクトルと配列でしか機能しないようです。このような複合ソートを使用する例は見つかりませんし、チュートリアルや言語標準でそれらの要素へのアクセスについて何も見つけることができません。それはどのように行われますか？それとも、この機能の目的を完全に誤解していましたか?

私のアプリケーション: 一時的な問題をエンコードし、古い状態を新しい状態に変換する状態遷移関数の形式でそれを実行したいので、システムで実験するときに次のようなものを書くことができます:

UPPAAL を使用してシステムを時限オートマトンとしてモデル化する必要がありますが、UPPAAL が経過時間に応じてクロックとガードを管理する方法に本当に戸惑っています。UPPAAL はクロック ガードを無視しているように見えます! 私の問題は、非常に「物理的な」アプローチからモデリングに取り組んでいることであり、この種の問題に直面していると思います。

ここに簡単なオートマトンがあります。UPPAAL シミュレーションで実行すると、最初の場所と A の場所の間で永久にループし、B に移動することはないと予想されます。 Linux 64 バージョンがないため)。

それで、私は何が欠けていますか？UPPAAL はクロック ガードを実際にどのように扱っていますか?

この問題に最初に遭遇したときに私がやろうとしていたことは、タイムアウトをモデル化することでした。そのため、公称動作のガードが 30 秒前に満たされない場合、オートマトンは別のエッジを取ります。

本当にありがとうございました

私のコーディング アプローチに関するフィードバックをお願いします (つまり、それが適切かどうか、または私が行ったことをより良い方法で行うことができるかどうか)。

コンストラクターが特定の形式を持つ必要があることを文書化するためのインターフェイスを作成したいと思います。もちろん、インターフェイスにコンストラクターしか含まれていない場合 (PHP でコンストラクターをインターフェイスに配置できることに驚きました)、インターフェイスは何の効果もありません (おそらくドキュメントを除いて)。その上、PHP は、呼び出し可能オブジェクトのパラメーターの一致を、数でも型でも強制しません。これは、関数、メソッド、およびコンストラクターにも当てはまります。

私がクラスにどのように名前を付けたかがわかれば、私が何をしようとしているのかがわかるでしょう (: コンストラクターのパラメーターはメッセージのインスタンスでなければならないことを文書化してください。私のアプローチが正しいかどうか、また改善できるかどうか教えてください。

上記の単純なクラスを念頭に置いて、次のようなインターフェイスを作成したいのですが、PHP コンストラクターを扱っているので、これは役に立たないはずですか?

Runner次に、次のようなクラスでインターフェイスを強制したいと考えています。

最後に次のコードを実行します。

出力：