1

以下代码在 8 次迭代后终止（虽然它应该迭代 14 次）为什么？

该代码编码了一个线性混合自动机，它应该运行指定的迭代次数，但没有。

from z3 import *
x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')

location=[None]
location='off'
x=20
t1=0

s=Solver()
#set_option(precision=10)
k=14
for   i in range(k):

  print location 
  if location=='off':
      s.add((10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0)
  elif location=='on':
      s.add(10*x_next>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0)


  if  [location=='off' and x_next<19] :
      location='on'
  elif [location=='on' and x_next>21]:
       location='off'

  if s.check()==unsat:
      break

  m=s.model()
  #print s.check()
  print i
  print location
  print s.model()

  print "value of x_next"
  print m[x_next].as_decimal(10)

  x=m[x_next]
  t1=m[t2]
4

1 回答 1

1

程序停止，因为在迭代 8 后断言集不可满足，并且在您的循环中，您有以下语句：

if s.check()==unsat:
    break

在第一次迭代中添加断言：

10*x_next <= 200 - t2 - 0

在最后一次迭代中，您添加：

10*x_next >= t2 - Q(40,3) + 10*Q(56,3),
t2 - Q(40,3) > 0

其中，该命令Q(a, b)用于创建有理数a/b。也就是说，t1is40/3和xis56/3在第 8 次迭代。上面的三个断言是不可满足的。前两个暗示，t2 <= 40/3最后一个t2 > 40/3。

顺便说一句，以下陈述似乎是不正确的。也就是说，我不相信它反映了你的意图。请注意，这是正交问题。

if  [location=='off' and x_next<19] :

表达式x_next<19不计算为Trueor False。它创建 Z3（符号）表达式x_next < 19。我相信，您想评估此表达式在模型中是否为真m。如果是这种情况，你应该写：

if  location=='off' and is_true(m.evaluate(x_next<19)) :

该命令计算模型中m.evaluate(t)的表达式。结果是一个 Z3 表达式。如果Z3 表达式为真，则该函数返回。tmis_true(t)Truet

于 2012-08-06T15:08:47.623 回答