python - 是否有可以对有限状态机进行时间逻辑模型检查的 Python 包?
问题描述
我希望能够将系统建模为有限状态机,并根据时间逻辑规范测试模型的属性。
我知道 StateFlow 的模型检查功能,但如果可能的话,我更喜欢使用 Python,因为它是开源的。我也知道 TuLiP 是设计和模拟有限状态机的可靠选择,但据我所知,它不进行模型检查。Python wiki 上的 FSM 包列表似乎充满了类似的以实现为中心的包。
有谁知道一个不同的 Python 包,它能够根据时间逻辑设计规范进行模型检查?
解决方案
有很多免费的模型检查器,例如 NuSMV 和 Spin https://en.wikipedia.org/wiki/List_of_model_checking_tools
https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md
我怀疑你找到了很多基于 python 的工具,但是有一些可用的
PyNuSMV - NuSMV 的 python 前端,工业强度免费模型检查器https://github.com/sbusard/pynusmv
Spot - 一个 LTL-omega-automata 库,用于使用 python 绑定进行模型检查https://spot.lrde.epita.fr/
小型 CTL、CTL* 和 LTL Buchi 自动机模型检查器https://github.com/albertocasagrande/pyModelChecking
PyBoolNet NuSMV 的前端https://github.com/hklarner/PyBoolNet以及 misc bool net
Intrepyd https://github.com/formalmethods/intrepyd
硬件 LTL 模型检查器https://github.com/cristian-mattarei/CoSA
HyLaa 混合系统模型检查器https://github.com/stanleybak/hylaa
推荐阅读
- python - Python:格式化控制台输入
- batch-file - 计算某些字符的数量
- angular - “typeof ActivatedRoute”类型上不存在属性“快照”
- java - 如何将此递归深度优先搜索转换为深度受限搜索?
- json - ImportError:无法导入名称“maketrans”
- python - 熊猫将函数应用于每列的第二行
- pandas - 每个示例使用多个类别编码分类特征 - sklearn
- react-native - 设备上的 React Native 导致“未处理的 JS 异常:new.target”
- java - 在 Springboot 中测试 JdbcTemplete.BatchUpdate 方法
- python - Wagtail CMS 在没有模板标签的模板中渲染图像