我似乎无法理解解决完成后显示的 vars.
和 primary vars.
数字的含义 . 第5.2.1节中的Alloy书解释了Alloy关系变量被映射到与每个关系的元组相关联的布尔变量 . 但我不明白这个变量定义与gui中显示的变量计数之间的对应关系 . 例如,当运行此代码时(我使用Alloy Analyzer 4.2构建日期:2012-09-25 15:54 EDT . ):
sig A {}
pred show {}
run show for 2
它显示
0 vars. 0 primary vars. 0 clauses.
虽然存在一种关系 . 当这段代码运行时:
sig A {}
fact {no A }
pred show {}
run show for 2
变量count是这样的:
6 vars. 2 primary vars. 5 clauses.
我可以理解,2个主变量可能对应于集合A的最多2个元素,但我不明白枚举的另外4个变量是什么 .
1 回答
本质上,主变量是与声明的签名实例对应的变量 . 它们的数字代表整个Alloy宇宙中创建的所有实例 . 另一方面,变量的总数通常更大,因为它还反映了在编码到SAT公式中时表示给定事实所需的变量 . (关于KodKod底层求解器的统计数据的一些细节可以在here找到 . )
因此,在第二个示例中,由于签名实例的限制为2,主要变量的数量为3.(例如,如果添加另一个签名,则主要变量的数量将为4.)总变量的数量反映公式的(CNF)编码中的变量总数,而后者又取决于您声明的具体事实 . 请注意,在第一个示例中,由于没有要检查的内容(并且求解器不需要发出任何内容),因此不需要变量 .