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

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