2

这个问题与这个问题几乎相同，但解决方案对我不起作用。抱歉，我想对该答案发表评论，而不是提出新问题，但我没有足够的声誉......

我正在为电梯建模一个简单的状态机。有两个楼层和两个按钮Up和Down。我已经将转换建模为谓词Action x Elevator x Elevator (Elevator = State)，这样T(a,s,s')成立，如果动作a可能导致从s到s'的转换，其中一个动作是按向上或向下按钮。问题的可满足性不取决于按下按钮的人，但我希望 Z3 对功能主题分配一些解释： Action -> Person。

目标是找到状态机的k轨迹，这可能有助于理解电梯的行为。

我尝试了不同的选项组合，包括auto-config=falseand model-completion=true，但没有成功。我还尝试强制完成模型，询问(subject Action0)的值，但 Z3 仍然没有为subject分配解释。

我的 Z3 版本是 4.3.1，在 Linux amd64 上运行。

4

2 回答 2

3

参数问题:model-completion已修复。该修复程序已在http://z3.codeplex.com/SourceControl/changeset/a895506dac75提供。

该修复程序将在下一个正式版本中提供。如果你愿意，你可以下载unstable(work-in-progress) 分支，然后编译它。要下载，您只需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 回答