使用 UPPAAL 或 NuSMV 控制电梯

Question

我是 NuSMV 和 UPPAAL 的新手，正在解决这个问题。 任何人都可以提供以下问题的解决方案吗？

对您的电梯系统的控制系统进行建模和分析
自己的设计服务于多个楼层（比如 4 层或 5 层），并带有一个
liX 的数量（比如 2 个或 3 个）并且有许多用户在使用
单独的楼层和不同的凝胶希望
楼层。系统可能：
• 允许用户可以指示在某个楼层需要 liX，
和/或需要上升或下降和/或被要求去一个
某楼层
• 或者用户可以 -- 一旦进入 liX -- 请求实际楼层。
• 为了移动门必须关闭。 • 不能跳过楼层。 • 所有liX 的初始位置是1 楼。a 电梯是
仅由一个 buPon 控制，通过它可以订购 电梯到你站立的楼层。

Answer 1

我不会为你编写程序，但我可以给你一些提示。

决定要包含哪些实体以及实体应该能够具有哪些状态。例如：按钮、客舱、控制器、门……可以是实体，实体可以有状态。按钮可以按下，机舱可以移动或空闲，门可以打开或关闭等。

使用 SMV 将实体建模为模块。如果您不了解 SMV，请尝试从简单的示例中学习。

确定应满足的规范。例如：电梯不应该在开门等情况下换楼层。

如果您使用其他示例 SMV 程序进行练习，那么您会发现它更容易上手。如果您在努力解决问题的地方发布代码，我们可以为您提供更多更好的帮助。