python - 使用 z3 python API 编码线性混合自动机

Question

我正在尝试将线性混合自动机编码为一阶公式的结合，如下所示：

s.add(Or(Or(And(off,Not(on),Not(S1),Not(S2),(10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0,Implies(),
And(Not(off),on,Not(S2),Not(S1),(10*x_next)>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0)),    
Or(And(x<19,(t2-t1)==0,S1,Not(off),Not(on),Not(S2),(x-x_next)==0),
And(x>21,(t2-t1)==0,Not(on),Not(off),S2,Not(S1),(x-x_next)==0))))

问题是需要采用跳转条件（例如，如果 x<19 则 ....），这似乎在这里不起作用。有人可以帮助我使用 z3 python API 将跳转条件编码为一阶公式的结合吗？

Answer 1

寻找或构建一个可以从更高级别的描述中对 HA 公式进行编码的工具可能会很有用。他们可以帮助调试一些细节。比如你说有“开”和“关”两种模式。这些似乎被编码为命题变量。通常使用程序计数器来编码自动机的状态，因此例如会有一个程序计数器“状态”，其值可以是“开”或“关”。您可以使用 Z3 中的标量来编码状态变量的可能值，或者您可以使用整数或位向量，或者在这种情况下使用布尔标志。然后是编码转换关系的问题。您通常需要在不被转换改变的变量上编码帧条件。