如何查询Alloy Analyzer找到的模型数量及模型调整对实例数的影响

以下两种方案均可实现统计：

• GUI模式下运行分析命令后，结果面板顶部会直接显示共找到X个实例的统计值，该数值不受默认展示20个实例的上限限制。如果需要统计超过默认统计上限的实例数，可以进入Options菜单修改Maximum instances to display参数，设置为目标上限后重新运行分析即可。
• 命令行模式下运行分析时，添加-n -1参数即可返回所有满足约束的实例总数，参考命令：java -jar alloy.jar run 你的模型文件.als -n -1，运行后控制台会直接输出总实例数。

注意：如果实例总数过大超出当前硬件计算能力，Alloy会返回统计上限提示，此时需要缩小scope后再重新统计。

不同调整方向对实例总数的影响可参考以下规则：

• 域（scope）设置调整：sig的全局/局部scope是影响实例数的核心因素，scope每提升一个单位，实例总数通常会呈指数级增长。
• 约束规则调整：新增fact事实、收紧谓词约束会过滤掉不符合要求的实例，总数量会降低；反之删除约束、放宽规则会提升总数量。
• 去重规则调整：开启Prevent isomorphisms（同构实例去重）功能后，结构完全一致的同构实例会被合并计数，总数量会远低于关闭该功能时的统计结果。
• 命令参数调整：run/check命令中指定的局部scope优先级高于全局scope，仅调整局部scope的数值只会影响对应命令返回的实例总数。

内容的提问来源于stack exchange，提问作者Griselle Z