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。つまり、イテレーション 8 でt1is40/3とxis です。上記の 3 つのアサーションは満足できません。56/3最初の 2 つはそれを意味しt2 <= 40/3、最後のt2 > 40/3.

ところで、次のステートメントは正しくないようです。つまり、それがあなたの意図を反映しているとは思えません。これは直交問題であることに注意してください。

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

式はorx_next<19に評価されません。Z3 (シンボリック) 式を作成します。この式がモデルで真かどうかを評価したいと思います。その場合は、次のように書く必要があります。TrueFalsex_next < 19m

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

このコマンドは、モデル内m.evaluate(t)の式を評価します。結果は Z3 式です。関数は、Z3 式が true の場合に戻ります。tmis_true(t)Truet

于 2012-08-06T15:08:47.623 に答える