用Python实现一个最简单的LTL解释器

16一/080

用Python实现一个最简单的LTL解释器

昨天在考虑一个问题：能否用LTL (Linear Temporal Logic)表示a*b*，(ab)*这两个正则表达式？前者还好写一点，但后者实在很复杂，在纸上写写画画，后来我自己都搞不清我写的公式是什么意思了。如果有个LTL表达式的解释器作测试会方便得多，但除了SPIN，手边找不到一个轻量级的工具，于是就自己写一个，选择Python是因为它支持lambda表达式，而且比较熟悉。

运行效果：
>>> F(Ischar('a'))("baac")
True
>>> U(Ischar('a'), Ischar('b'))("aaaa")
False
>>> U(Not(Ischar('b')), Ischar('b'))("aaab")
True
>>> G(Imply(Ischar('a'), F(Ischar('b'))))("aaab")
True

存在问题：
1. 只能处理有限长度的串，跟LTL的语义稍有不符，不过也足够用了。
2. 没有做Parse，所以输入必须是前缀表达式。

代码很简单：

def Ischar(ch):
return lambda s: len(s)>0 and s[0]==ch

def X(func):
return lambda s: func(s[1:])

def G(func):
return lambda s: G_impl(func, s)

def G_impl(func, s):
for i in range(len(s)):
if not func(s[i:]): return False
return True

def Not(func):
return lambda s: not func(s)

def And(f1, f2):
return lambda s: f1(s) and f2(s)

def Or(f1, f2):
return lambda s: f1(s) or f2(s)

def Imply(f1, f2):
return lambda s: (not f1(s)) or f2(s)

def F(func):
return lambda s: not G(Not(func))(s)

def U(f1, f2):
return lambda s: U_impl(f1, f2, s)

def U_impl(f1, f2, s):
i=0
while (i<len(s)):
if (f2(s[i:])): break
i += 1
if (i>=len(s)): return False
for j in range(0, i):
if (not f1(s[j:])): return False
return True
# 到此就定义了LTL的各种算子。

# 判定a* b*：
def astar_bstar(a,b):
return lambda s: G(Imply(Ischar(b), G(Not(Ischar(a)))))(s)

# 下面是为定义(ab)*所写的辅助函数，参考了DecSerFlow的定义（所以才用了奇怪的B_always_between_A，而不是定义A_always_between_B）。
def existence(a):
return lambda s: F(Ischar(a))(s)

def response(a, b):
return lambda s: G(Imply(Ischar(a), existence(b)))(s)

def precedence(a, b):
return lambda s: Imply(existence(b), U(Not(Ischar(b)), Ischar(a)))(s)

def B_always_between_A(a,b):
return lambda s: G(Imply(Ischar(a), X(precedence(b, a))))(s)

# 判定(ab)*：
def ab_star(a,b):
return lambda s: And(precedence(a,b), And(response(a,b), And(B_always_between_A(b,a), B_always_between_A(a,b))))(s)

# 测试一下：
if __name__ == "__main__":
assert ab_star('a','b')("")==True
assert ab_star('a','b')("a")==False
assert ab_star('a','b')("b")==False
assert ab_star('a','b')("ba")==False
assert ab_star('a','b')("abab")==True
assert ab_star('a','b')("ababa")==False
assert ab_star('a','b')("ababb")==False
assert ab_star('a','b')("abaab")==False

assert astar_bstar('a','b')("aabb")==True
assert astar_bstar('a','b')("abab")==False
assert astar_bstar('a','b')("bbaa")==False

看起来我的定义似乎是对的，虽然我也无法证明这个正确性。我比较困惑的是LTL和正则表达式的关系，查了一本书说是LTL的表达能力不如正则表达式，LTL的表达能力与star-free regular expression相同？但上面的例子却说明(ab)*, a*b*是可以用LTL表达的？搞不懂。

Update: 原来是我对star-free的理解不对，参照Loop-Free Alternating Finite Automata一文的说法，所谓“star-free的regexp语言”虽然不含有*，却包含negation和intersection，因此它可以表达某些无限长的串，究竟是哪些？不是那么容易说清楚。

如果LTL可以表达(ab)*，那就说明(ab)*一定可以转换为star-free regexp的形式。尝试一下：先定义L=\neg (aa) \intersection \neg (bb)，则L表示ab交错的序列，但不保证a是第一个字母；稍微改进一下，(a L) \intersection L应该就是一个正确的表示吧。