Alloy建模疑问：状态异常变化与状态语句差异

问题1：状态1的raised告警集合比状态0少，仅定义添加逻辑为何出现减少？ #

Alloy的状态转换是非确定性的，除非你通过约束明确限制状态变化的范围。如果只定义了“允许添加告警”的逻辑，但没有添加State.raised in State'.raised这类约束，Alloy会生成所有满足转换谓词的可能状态——包括那些随机丢失告警的情况。

解决办法是在转换规则中明确约束告警集合的变化：要么指定State'.raised = State.raised + newAlerts（精确控制新增的告警），要么至少保证原告警集合是新集合的子集，避免丢失。

问题2：State' = State与State.raised' = State.raised的差异，替换后提示“No instance found”的原因？ #

两者差异 #

• State' = State：表示整个状态完全不变，所有状态属性（比如禁用规则集合、其他可能的字段）都必须和原状态完全一致。
• State.raised' = State.raised：仅约束raised属性保持不变，其他状态字段（比如disabledRules）可以自由变化。

无实例的原因 #

如果你的模型中存在其他强制的状态变化约束（比如fact要求每次转换必须禁用一个规则），仅固定raised不变的话，其他字段的变化可能和模型中的其他约束冲突，导致没有能满足所有条件的实例。比如若有fact要求“每次转换必须新增一个禁用规则”，但结合其他规则（比如禁用的规则不能重复），可能不存在合法的状态转换路径，最终导致无实例。

后续修改相关问题：移除always才能生成有效实例，以及Alloy无限轨迹规则的资料 #

移除always才能生成实例的原因 #

Alloy的模型检查器处理always这类时序约束时，默认会搜索无限状态轨迹（遵循线性时序逻辑LTL的标准语义）。如果你的liveness谓词用always约束了某个必须永久成立的条件，但模型中不存在能无限满足该条件的轨迹，就会找不到实例。比如若liveness要求“永远有新告警触发”，但当所有规则都被禁用后就无法生成新告警，无限轨迹中必然会出现无法满足该条件的状态，因此无实例。

Alloy无限轨迹规则的资料来源 #

Alloy官方文档的时序逻辑章节明确说明，Alloy的时序分析基于无限状态轨迹，这是因为它采用了LTL的标准语义。另外，Alloy的核心参考书籍《Software Abstractions: Logic, Language, and Analysis》中，时序逻辑部分也详细解释了这一点——Alloy的模型检查器会通过循环某个状态来模拟无限序列，以此验证时序约束。

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