我学习Alloy很开心，很高兴能把它应用到我正在进行的一些软件项目中。
在过去，我曾非正式地使用轻量级形式化方法（如果有的话），以一阶逻辑编写我期望系统具有的一些不变量。我从来没有用它来发现缺陷，只是把我的设计和测试重点放在关键的特性上。
我现在想超越这一点，实际使用Alloy来查找架构中的错误。我该怎么做？我一直采用的方法是：
- 将体系结构剥离到一些内核（例如，删除使用集而不是更复杂的数据结构，使用sig而不是更详细的枚举）
- 将不变量编码为
assert check和run
然而，尽管我学习了很多关于Alloy的知识，但这并没有帮助我改进我的体系结构。在简化我的模型的过程中，我编码的不变量似乎得到了相应的简化，并且自然成立。
例如，体系结构中有一个错误，我们只是在原型设计和测试中遇到的。这个错误与假设如果我们在一个序列中有n项有关，我们可以将它们分解为m的组，并按顺序处理每个m组。（n恰好比m大得多。）当然，问题是m不一定划分n，因此最后一组可能太小。这是一个设计级别的缺陷，完全可以用逻辑表达，正是Alloy为设计的缺陷类型。然而，我的Alloy模型没有找到它。它只是抽象掉了整数大小（请参阅《为什么Alloy告诉我3>=10？》中给出的建议，以避免使用数字），将n划分为不相交的组，并且运行得很好。
换句话说，似乎要确保您的模型包含足够的细节来捕捉缺陷，您几乎需要提前了解缺陷。
然后，您如何使用Alloy来审查软件架构？
附言：我知道在很多情况下你都没有这个问题。例如，当查看分布式系统的规范，并希望显示不变量时。我在这里的挑战是应用Alloy来帮助实现，而不是审查协议、规范、状态机或其他逻辑结构。
Alloy不太适合对数字或字符串进行推理。因此，您的模型通常无法检测到与给定字符串的格式或给定整数字段的值有关的错误。
现在，Alloy的伟大之处在于对关系进行推理，以及对这些关系的约束。检查断言是确保给定属性成立的一种方法，因此您是对的，仅使用此技术，您可能会觉得需要提前了解缺陷。
因此，我更喜欢这种方法，即使用run命令，只需为您提供一组满足模型约束的实例。在这里，您将自己检查生成的一系列实例在建模的上下文中是否"有意义"。您可能会看到您的一些约束过于严格或不够严格，从而允许您增强模型。