Staged Evaluation of Partial Instances in a Relational Model Finder
Staged Evaluation of Partial Instances in a Relational Model Finder
复制标题
关系模型查找器中部分实例的分阶段评估
DOI：
10.1007/978-3-662-43652-3_32
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Derek Rayside
中科院分区：
文献类型：
--
作者：
Vajih Montaghami;Derek Rayside
为了使用关系模型查找器评估“对于所有 x 都存在一些 y”形式的属性，需要一个生成器公理来强制 y 的所有实例都存在于论域中。如果没有生成器公理，模型查找器将通过简单地不包含 y 的重要实例来产生虚假的反例。生成器公理通常被认为评估成本高昂，极大地限制了分析范围。我们证明，在与属性不同的阶段评估生成器公理可以显着提高分析速度和可扩展性
To evaluate a property of the form 'for all x there exists some y' with a relational model finder requires a generator axiom to force all instances of y to exist in the universe of discourse. Without the generator axiom the model finder will produce a spurious counter-example by simply not including an important instance of y. Generator axioms are generally considered to be expensive to evaluate, significantly limiting the scope of the analysis. We demonstrate that evaluating the generator axiom in a separate stage from the property results in substantial improvements in analysis speed and scalability