Alloy模型变量签名行为存疑及固定Item原子数需求

问题背景 #

学习Alloy时尝试建模简单租赁系统：所有Item初始可用，可租给Customer。使用变量签名实现了模型，但存在两个疑问：

1. 不确定这种变量签名的实现方式是否正确，此前用静态签名建模遇到困难；
2. 执行时Item原子会莫名出现或消失，希望固定Item原子数，让它们仅在AvailableItem和RentedItems间转换，想了解除了在fact中设置数量外的方法。

原模型代码 #

var one sig Customer {
    var rented: set RentedItems,
}


var abstract sig Item {
}

var sig AvailableItem in Item {}
var sig RentedItems in Item {}

fact init {
    no RentedItems
    all v:Item | v in AvailableItem
    //#Item = 3
}


pred rent [v: AvailableItem, c:Customer] { 
    c.rented' = c.rented + v
    AvailableItem' = AvailableItem - v
}

pred NoMoreItems {
    no AvailableItem
}

fact trans { 
    always (NoMoreItems or (some v:AvailableItem, c:Customer | rent[v, c]))
}

run {} for 3

疑问解答与修正方案 #

1. 变量签名的使用是否正确？

你的核心需求是Item集合固定，仅状态（可用/已租）随时间变化，但原代码中把Item设为var sig是错误的——var sig会让签名的原子集合随时间动态变化，这直接导致了Item原子莫名出现/消失的问题。

正确的做法是：

• 用静态签名定义Item（不添加var），保证原子集合全程固定；
• 用var set来跟踪Item的状态划分（可用/已租），而非var sig in Item。

2. 如何固定Item原子数？

改成静态Item签名后，有两种可靠方式固定原子数：

• 在run命令中直接指定：比如run {} for 3 Item（明确限制Item的数量为3）；
• 在全局fact中声明：fact { #Item = 3 }，但推荐前者，因为更灵活，可快速调整测试数量。

同时必须添加约束，确保AvailableItem和RentedItems始终是Item的完整划分（无重叠、无遗漏），避免Item“丢失”：

fact stateInvariant {
    always (
        AvailableItem + RentedItems = Item  // 所有Item都处于某一状态
        and no AvailableItem & RentedItems  // 两种状态无重叠
    )
}

修正后的完整模型 #

one sig Customer {
    var rented: set Item  // 直接关联到Item，而非状态集合
}

sig Item {}  // 静态签名，原子集合固定

var set AvailableItem: set Item
var set RentedItems: set Item

fact init {
    no Customer.rented
    AvailableItem = Item  // 初始所有Item可用
    no RentedItems
}

pred rent[v: AvailableItem, c: Customer] {
    c.rented' = c.rented + v
    AvailableItem' = AvailableItem - v
    RentedItems' = RentedItems + v  // 同步更新已租集合
}

pred NoMoreItems {
    no AvailableItem
}

fact stateInvariant {
    always (
        AvailableItem + RentedItems = Item
        and no AvailableItem & RentedItems
    )
}

fact trans {
    always (NoMoreItems or (some v: AvailableItem, c: Customer | rent[v, c]))
}

// 明确指定Item数量为3，执行模型
run {} for 3 Item

关键修改说明 #

• 移除了所有不必要的var签名，仅保留状态集合的var修饰；
• Customer.rented直接关联Item，避免依赖状态集合的动态变化；
• 新增stateInvariant事实，强制状态划分的完整性；
• rent谓词中同步更新RentedItems，保证状态一致；
• 在run命令中明确指定Item数量，固定原子集大小。

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