2

この質問はこれとほとんど同じですが、解決策がうまくいきません。申し訳ありませんが、新しい質問をするのではなく、その回答にコメントしたいのですが、十分な評判がありません...

エレベータの単純なステート マシンをモデル化しています。2 つのフロアと 2 つのボタンUpとDownがあります。遷移を述語Action x Elevator x Elevator (Elevator = State)としてモデル化したので、アクションaがsからs'への遷移を引き起こす可能性がある場合に T(a,s,s')が成立します。ここで、アクションは上ボタンまたは下ボタンのいずれかを押します。問題の充足可能性はボタンを押す人に依存するものではありませんが、関数subject : Action -> Personに何らかの解釈を Z3 に割り当ててもらいたいと思います。

目標は、エレベータの動作を理解するのに役立つステート マシンのkトレースを見つけることです。

auto-config=falseとを含むオプションのさまざまな組み合わせを試しましたがmodel-completion=true、成功しませんでした。また、 (subject Action0)の値を求めるモデル補完を強制しようとしましたが、Z3 はまだsubjectに解釈を割り当てません。

私の Z3 バージョンは Linux amd64 で動作する 4.3.1 です。

4

2 に答える 2

3

パラメータの問題:model-completionが修正されました。この修正は、 http://z3.codeplex.com/SourceControl/changeset/a895506dac75で既に入手できます。

修正は、次の公式リリースで利用可能になります。必要に応じて、(進行中の) ブランチをダウンロードしてunstableコンパイルできます。ダウンロードするにはDownload、上のリンクのボタンをクリックするだけです。

ところで、新しい Z3 には、内部モジュール パラメータを設定できる新しいパラメータ設定フレームワークがあります。次のリリース (およびunstableブランチ) で。使用する必要があります

(set-option :model_evaluator.completion true)

それ以外の

(set-option :model_completion true)

モジュールのパラメータを設定しているためですmodel_evaluator。さらに、使用する必要があります

(eval <term> :completion true)

それ以外の

(eval <term> :model_completion true)

completionモデル評価器のパラメータを設定しているためです。

于 2013-01-25T17:41:18.793 に答える
2

良い例え。抽象ソート Person はアサーションに現れず、Person を返す関数もアサーションで使用されません。

パラメータを関数に直接渡すことで、eval にモデルを完成させることができます。

http://rise4fun.com/Z3/Pslt4

つまり、

   (eval <term> :model-completion true)

それ以外の

   (eval <term>)

別のハックな方法は、評価したい項が元のモデルに含まれていることを確認することです: http://rise4fun.com/Z3/Yukv

于 2013-01-25T16:01:23.907 に答える