0

次のように、線形ハイブリッドオートマトンを一次式の結合としてエンコードしようとしています。

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を使用して、ジャンプ条件を一次式の結合としてエンコードするのを手伝ってくれる人はいますか?

4

1 に答える 1

1

より高いレベルの記述から HA 式をエンコードできるツールを探したり、作成したりすることが役立つ場合があります。いくつかの詳細をデバッグするのに役立ちます。たとえば、「オン」と「オフ」の 2 つのモードがあるとします。これらは命題変数としてエンコードされているようです。通常、プログラム カウンターを使用してオートマトンの状態をエンコードします。たとえば、値が「オン」または「オフ」のいずれかになるプログラム カウンター「状態」があります。Z3 でスカラーを使用して状態変数の可能な値をエンコードするか、整数、ビットベクトル、またはこの場合はブール フラグを使用できます。次に、遷移関係のエンコードの問題があります。通常、遷移によって変更されない変数のフレーム条件をエンコードする必要があります。

于 2012-08-05T23:00:51.613 に答える