【发布时间】：2016-11-30 05:41:00
【问题描述】：
我在 UPPAAL 中模拟了两个触发器的定时模型，当我尝试验证一些属性时，我达到了 6M 状态并且我的笔记本电脑内存不足，消耗了大约 5Go，谁能告诉它的近似状态数是多少UPPAAL 可以处理吗？以及在 UPPAAL 中处理状态爆炸的可能技术有哪些？
谢谢你
【问题讨论】：
标签： formal-verification model-checking formal-methods state-space uppaal
【发布时间】：2016-11-30 05:41:00
【问题描述】：
状态数取决于：
可用内存的大小。在 32 位架构上，它被限制为 4GB。
各个州的大小/足迹。
状态空间的形状和探索的顺序。
符号状态的粒度（约束间隔的跨度如何：如果时间离散化，则符号技术的扩展性会很差）。
您可以尝试以下技巧：
应用抽象并删除不必要的变量：将变量设为 const，未使用时将变量设置为零，一次转换通信专用变量可以标记为“元”（不要滥用这个！否则你会得到遇到奇怪的行为）。
通过将状态空间缩减设置为积极优化空间消耗。
应用偏序约简、对称约简。
应用扫线法（在 Uppaal 帮助中查找关键字“progress”）。
查看 Uppaal 教程了解更多信息。
【讨论】：
-
谢谢@mariusm，我现在正在努力了解对称减少和扫描线方法，但是在教程中提到UPPAAL不支持偏序减少！您认为其他版本的 UPPAAL 是否支持它？我使用 4.1.19
-
Uppaal 不支持自动部分降阶，但你仍然可以让你的模型遵循部分降阶方案。
-
感谢@mariusm 的反馈，如果我使用 UPPAAL 的图形界面来构建我的模型，你能告诉一些提示我应该如何遵循 UPPAAL 中的偏序减少方案，比如我应该切换到文本版本 *.xta 并尝试制定算法来优化我的模型，或者我留在 UPPAAL 的图形界面中并遵循特定的方法？谢谢
-
如果您可以自动生成模型，那么 XTA 可能更容易。否则，POR 技术需要在非常抽象的级别应用，即您必须自己推理哪些边缘可以组合为一个，哪些同步可以用广播替换等等。
-
谢谢@mariusm，我没有自动生成 UPPAAL 模型的部分，现在我手动自动编写模型，你的意思是我开发了一个脚本，可以将 VHDL 模型或 C 模型转换为XTA 格式？