夜雨聆风
LTL2BA在线使用说明
转化
高效可靠
基于 CAV ’01 顶会论文实现
深度兼容 Spin 模型检验器
适配
复杂公式
输出
全面实用
可输出标准 /广义Büchi 自动机
该自动机所对应的LTL公式：
F ( ( pi_2_1_2_1&& ! pi_2_1_3 )&& F pi_2_1_3_1 ) && F pi_1_2_4 && ! pi_2_1_3 U pi_1_2_4
大家可以看到，该自动机主要由图的顶点V和有向边E组成，每个顶点代表一个状态，相应的边则代表状态转移的条件即输入的语言。下面我将为大家介绍如何将抽象的LTL公式语言转化为自动机图的直观形式，大家可以跟着手动操作一遍。
核心功能：快速将线性时序逻辑（LTL）公式转换为Büchi自动机，适配模型检验场景，可直接生成Spin模型检验器兼容的never claim，支持自动机图形化展示与性能统计。
开发维护：由Denis Oddoux编写初版，Paul Gastin迭代优化至v1.3版本，基于CAV ’01会议论文《Fast LTL to Büchi Automata Translation》实现。（该文章非常经典，建议阅读）
运行限制：服务器内存限制1GB，单公式转换最长时限2小时。
2.1 基础书写规则
-
所有符号、运算符、原子命题之间必须加空格分隔，无空格会直接触发语法报错
-
原子命题仅支持小写字符串，禁止使用大写字母、特殊符号（除下划线外）
-
否定运算符禁止使用!，统一改用大写NOT，避免服务器安全策略触发403禁止访问错误
-
所有布尔、时序运算符无默认优先级，必须用括号()明确运算顺序，禁止省略括号
2.2可用符号与运算符对照表
（1）命题常量
true（真）、false（假）
（2）布尔运算符
| 运算符 | 含义 | 示例 |
|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
（3）时序运算符
| 标准运算符 | Spin兼容语法 | 含义 | 示例 |
|---|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2.3合法公式示例（直接复制可用）
-
G ( req -> F ack )
-
NOT ( F ( p && NOT q ) )
-
[] ( safe -> <> live )
-
( p U q ) || X r
网页功能选项说明
页面选项分为兼容设置、输出设置、化简优化三类，可按需勾选，下方标注推荐必选选项。
|
|
|
|
|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-
打开工具官网链接，进入操作页面
-
在页面上方LTL formula输入框内，按照语法规范填写目标公式
-
根据需求勾选功能选项，新手直接勾选推荐必选选项即可
-
点击输入框下方的Convert按钮，启动公式转换
-
等待转换完成后，页面会展示自动机图形、never claim代码、转换统计三类结果
-
复制never claim代码至Spin工具，或保存自动机图形与统计数据用于分析
1. 403 Forbidden错误 原因：使用了!作为否定运算符，触发服务器安全拦截 解决：将所有!替换为大写NOT，严格遵守语法规范
2. Syntax Error语法报错 原因：符号间缺少空格、原子命题大写、括号不匹配、运算符拼写错误 解决：逐一检查空格、大小写、括号完整性，修正拼写错误
3. 自动机图形无法显示 原因：网络加载异常、公式过于复杂导致渲染失败 解决：刷新页面重试，简化公式后重新转换
4. 转换超时/内存超限 原因：公式过于复杂，触发服务器内存或时长限制 解决：开启全部化简选项，拆分复杂公式，简化逻辑结构
排版：三十六画生
文字：三十六画生
图片：来源LTL2BA在线网站