UPPAALまたはNuSMVを使用したエレベーター制御

Question

NuSMVおよびUPPAALを初めて使用しています。この問題の解決に取り組んでいます。 誰でも次の質問に対する解決策を提供できますか？

モデル及び（5 4言うか）と
LIXSの数の（例えば2または3）と数とフロアの数にサービスを提供あなた
独自設計のエレベータシステムの制御系を解析ユーザーが
個々のフロアにあり、別のものにgelngするための個別の希望があります
フロア。システムがあります。•
、ユーザーはLIXが一定の階で必要とされていることを示すことができるよう
および/または上がるか、ダウンする必要があり、および/または
特定の階に
•またはを行くことを要求されますユーザはliX要求の実際の床の中に一度入ることができる。
•ドアを移動するには、ドアを閉じる必要があります。 •フロアはスキップできません。 •すべての椅子の床面は床1です。aエレベーターは、 エレベーターを立てることが可能な1つの支柱によって制御される
です。

Answer 1

私はあなたのためのプログラムを書いていないが、私はあなたにいくつかのヒントを与えることができます。

エンティティを含めるエンティティとエンティティが持つことができる状態を決定します。例：Button、cabin、controller、door ...はエンティティであり、エンティティは状態を持つことができます。ボタンを押したり、キャビンを動かしたり、アイドルにしたり、ドアを開閉することができます。

エンティティをSMVでモジュールとしてモデル化します。あなたがSMVを知らないなら、簡単な例から学んでみてください。

どの仕様を満たすべきかを決定します。例：ドアが開かれている間は、エレベータは階を変えるべきではありません。

他のSMVプログラムの例で練習すると、始めるのが簡単になります。問題を解決するために努力しているコードを投稿すると、私たちはあなたをより多く、より良く助けることができます。