timewinder:适用于Python的时间行为逻辑建模 源码

Timewinder是一个Python 3库,用于构建和运行时态逻辑模型。 该库的目标是将形式化的方法,特别是兰莫特的的带给更多的读者。 尽管受到极大启发,Timewinder试图变得更简单,更具可读性并且更加专注于行业。 也就是说,TLA +是一个令人印象深刻的工具,Timewinder并未尝试涵盖TLA +可以完成的全部工作。 该项目旨在实现以下目标: 向更多开发人员介绍建模和形式化方法 增加使用时间逻辑的人员数量 使用非专家也可以阅读的可测试示例模型来改进设计文档 使运行模型变得容易且可自动化, 。 项目状态 该项目仍为Alpha,因此API可能会更改。 请加入,讨论模型,示例和方向。 绝对希望获得帮助,并感激不已! 例子 从数 高级用法 Timewinder以@timewinder.object和@timewinder.process装饰器@timewinder.process