看 NEWS 的时候看到一个叫 peg.el 的包直接在 Emacs 30 里面内置了。正好最近在玩 LTL ,就写了个 LTL2BA 生成的自动机输出的 parser 玩玩。
Emacs 29 里面可以通过 package-install
来安装 peg 这个包,目前似乎没有太多文档可以参考,peg.el 里面的注释和 peg-test.el 的例子是不错的学习材料。我不打算详细介绍 peg.el 怎么用,这个帖子算是给出一个简单用例。
在 LTL 2 BA (lsv.fr) 输入 F(a1) && F(a2) && F(a3)
可以得到如下输出和图:
never { /* F(a1) && F(a2) && F(a3) */
T0_init : /* init */
if
:: (1) -> goto T0_init
:: (a3) -> goto T0_S2
:: (a2) -> goto T0_S3
:: (a2 && a3) -> goto T0_S4
:: (a1) -> goto T1_S5
:: (a1 && a3) -> goto T1_S6
:: (a1 && a2) -> goto T2_S7
:: (a1 && a2 && a3) -> goto accept_all
fi;
T0_S2 : /* 1 */
if
:: (1) -> goto T0_S2
:: (a2) -> goto T0_S4
:: (a1) -> goto T1_S6
:: (a1 && a2) -> goto accept_all
fi;
T0_S3 : /* 2 */
if
:: (1) -> goto T0_S3
:: (a3) -> goto T0_S4
:: (a1) -> goto T2_S7
:: (a1 && a3) -> goto accept_all
fi;
T0_S4 : /* 3 */
if
:: (1) -> goto T0_S4
:: (a1) -> goto accept_all
fi;
T1_S5 : /* 4 */
if
:: (1) -> goto T1_S5
:: (a3) -> goto T1_S6
:: (a2) -> goto T2_S7
:: (a2 && a3) -> goto accept_all
fi;
T1_S6 : /* 5 */
if
:: (1) -> goto T1_S6
:: (a2) -> goto accept_all
fi;
T2_S7 : /* 6 */
if
:: (1) -> goto T2_S7
:: (a3) -> goto accept_all
fi;
accept_all : /* 7 */
skip
}
上面的输出格式似乎和 Spin - Formal Verification (spinroot.com) 有点关系。不过由于 ltl2ba 的输出并不复杂,这里就写出了如下凑合用的解析代码:
(defun ltl-buchi2list ()
(peg-parse
(translation_unit "never" _ statements)
(statements "{" (+ _ statement _)"}")
(statement state _ ":" _
(or (and "if" (list (+ transform)) "fi;")
(list "skip"))
`(state arrows -- (list state arrows)))
(state (substring [a-z A-Z] (* [a-z A-Z 0-9 "_"])))
(transform (list _ "::" _ condition _ "->" _ "goto" _ state _))
(condition (or (and "(1)" `(-- (list "1")))
(list (and "("_ id _ id-list _")"))))
(id-list (* _ "&&" _ id))
(id (substring (opt "!") identifier))
(identifier [a-z A-Z] (* [a-z A-Z 0-9 "_"]))
(_ (* (or [" \n\t"] comment)))
(comment "/*" (* (not (or "\n" (eob))) (any)))))
对以上文本可以得到如下解析结果:
(("accept_all" nil)
("T2_S7"
((("1") "T2_S7")
(("a3") "accept_all")))
("T1_S6"
((("1") "T1_S6")
(("a2") "accept_all")))
("T1_S5"
((("1") "T1_S5")
(("a3") "T1_S6")
(("a2") "T2_S7")
(("a2" "a3") "accept_all")))
("T0_S4"
((("1") "T0_S4")
(("a1") "accept_all")))
("T0_S3"
((("1") "T0_S3")
(("a3") "T0_S4")
(("a1") "T2_S7")
(("a1" "a3") "accept_all")))
("T0_S2"
((("1") "T0_S2")
(("a2") "T0_S4")
(("a1") "T1_S6")
(("a1" "a2") "accept_all")))
("T0_init"
((("1") "T0_init")
(("a3") "T0_S2")
(("a2") "T0_S3")
(("a2" "a3") "T0_S4")
(("a1") "T1_S5")
(("a1" "a3") "T1_S6")
(("a1" "a2") "T2_S7")
(("a1" "a2" "a3") "accept_all"))))