1

我使用 Z3 的 PDR 引擎来证明转换系统中的不变量。当转换系统包含一个计数器循环时，必须通过该循环才能达到特定状态，则性能很慢。

在下面的源代码中，您会看到一个包含 3 个状态和 3 个转换的转换系统示例，该转换系统使用Z3 Fixedpoint Homepage上的转换系统 Python 类实现。在最后一行中，查询从状态 L0 开始到达状态 L2。因此转换 t2 必须经过 y 次。

如果我初始化 y==10，则答案计算得很快。但是初始化 y==1000 时性能很慢。

L0 = L.L0 
L1 = L.L1
L2 = L.L2
y=Int('y')
i = Int('i')
state  = Const('state', L)

t1 = { "guard" : state == L0,
   "effect" : [ L1, i ] }
t2 = { "guard" : And(state == L1),
   "effect" : [ L1, i+1 ] }
t3 = { "guard" : And(state == L1,i>y),
   "effect" : [ L2, i]}

ptr = TransitionSystem( And(state == L0, i == 0, y==10),[t1, t2, t3],[state, i])
ptr.query(state==L2)

是否有可能以 Z3 获得更好性能的其他方式计算从 L0 到 L2 的路径？

4

1 回答 1

2

对于您的示例，Z3 目前没有更快的方法。Z3 的实现在反例循环的深度上花费了大致二次开销，因为它试图将（相同的）属性推送到展开的深度。

一般来说，Z3 的 PDR 引擎不太适合规划问题。确定不存在痕迹时会好一些。

于 2013-04-12T04:13:00.510 回答