validation - 使用 UPPAAL 或 NuSMV 控制电梯

Question

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

对您自己设计的电梯系统的控制系统进行建模和分析，该电梯系统
服务于多个楼层（例如 4 或 5 个）并具有
多个 liX（例如 2 或 3 个），并且多个用户位于
各个楼层并具有个人希望凝胶到不同的
楼层。系统可以：
• 允许用户可以指示在某个楼层需要 liX，
和/或需要上或下和/或被要求去
某个楼层
• 或者用户可以 -- 一旦进入liX -- 请求实际楼层。
• 为了移动门必须关闭。• 不能跳过楼层。• 所有liX 的初始位置是1 楼。 a 电梯
仅由一个按钮控制，通过该按钮可以命令电梯到您所在的楼层。

Answer 1

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

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

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

确定应满足的规范。例如：电梯不应该在门打开时改变楼层等。

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