uppaal

    0

    1答えて

    私はオートマトンを走らせ、epsファイルをエクスポートしました。しかし、さらに分析し、epsファイルから情報を得るにはどうすればよいですか? 変数値を外部ログファイルに書き込むことはできますか? ありがとうございます

    0

    1答えて

    テンプレートセクション内にチャネルを宣言すると、UPPAALコンパイラでエラーがスローされないのはなぜですか? もし私が正しいとすれば、他のテンプレートはこれらのチャンネルにアクセスすることができないので、チャンネル宣言は宣言セクション全体で意味をなさないように見えます。 または何か見落としていますか? ありがとうございます! PS私は同期チャネルを介して "内部"テンプレート通信をモデル化したい

    0

    1答えて

    すべての状態が指定された時間より長くならないように指定したいと思います。私はそれを州ごとに指定することでそれをすることができますが、人間はそれを忘れることができます。私はグローバルな解決策が必要です。私は、「各州の最大時間」のようなものを意味します。

    0

    1答えて

    私はUPPAALでモデルを設定しました。私はデベロッパーがデッドロックをチェックするために検証を使用しました。答えは:プロパティが満たされていない。したがって、デッドロックが存在します。 UPPAALでは、特定の状況のすべての変数の状態や現在の値など、デッドロックに関する詳細な情報を報告する方法はありますか?

    -2

    1答えて

    NuSMVおよびUPPAALを初めて使用しています。この問題の解決に取り組んでいます。 誰でも次の質問に対する解決策を提供できますか? モデル及び(5 4言うか)と LIXSの数の(例えば2または3)と数とフロアの数にサービスを提供あなた 独自設計のエレベータシステムの制御系を解析ユーザーが 個々のフロアにあり、別のものにgelngするための個別の希望があります フロア。システムがあります。• 、