【文件属性】：
文件名称：Coeus:CTL模型检查器
文件大小：561KB
文件格式：ZIP
更新时间：2021-04-10 09:37:25
Ruby
库厄斯
Coeus是计算树逻辑（CTL）模型检查器。 特别是，它支持以下工作流程：
定义状态机模型
解析CTL表达式字符串
根据模型评估CTL表达式
建筑学
Coeus由3个关键组件组成：模型，CTL表达解析器和标签算法
模型
严格来说，CTL模型定义为一组状态，这些状态之间的转换以及标记函数L。在Coeus中，只有状态和转换包含在Model类中：标记是独立实现的。 可以通过YAML文档将模型加载到Coeus中。 您可以在spec/fixtures找到该模式的示例。
CTL表达式解析器
CTL表达式解析器的目标是将CTL表达式的字符串输入转换为解析树，以供标记算法随后使用。 它由2个主要部分组成：一个词法分析器/令牌生成器和解析器，它们与 gem一起实现。 解析器支持所有CTL运算符，尽管在内部将它们转换为较小的适当集合。
【文件预览】：
Coeus-main
----.github()
--------dependabot.yml(503B)
--------workflows()
----coeus.gemspec(1KB)
----lib()
--------coeus.rb(265B)
--------coeus()
----Gemfile(542B)
----spec()
--------test_helper.rb(798B)
--------fixtures()
--------spec_helper.rb(5KB)
--------coeus()
--------support()
----Rakefile(488B)
----README.md(1KB)
----.rubocop.yml(2KB)
----.rspec(30B)
----docs()
--------THINKING.md(549B)
--------mutex_state_machine.png(182KB)
--------ctl_adequate_set.png(41KB)
--------state_adequate_set.png(123KB)
--------labelling_algo.png(233KB)
----Gemfile.lock(2KB)
----.gitignore(1KB)
----bin()
--------coeus(1KB)
--------shell(43B)
----grammar.txt(16KB)