合金模型中变量特征的不明确行为

Question

我目前正在学习 Alloy，并且正在努力理解变量签名的行为。我正在尝试建立一个简单的租赁系统模型，其中所有物品最初都是可用的，并且可以出租给客户。

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

首先，我不确定这种方法是否是实现此规范的正确方法，因为我很难使用静态签名对其进行建模 其次，在执行过程中，我注意到项目似乎在状态之间意外出现或消失的情况。我的理解是，可变签名原子可以通过谓词进行更改，根据需要添加或删除它们，但它们不应该简单地凭空出现。除了在事实中设置值之外，是否有其他方法可以为

Item

签名强制执行固定数量的原子？

我预计

Item

的原子在整个执行过程中保持一致，但物品会从可用变为租用。

Answer 1

Alloy 的语义基于逻辑：签名或关系的值仅受您编写的约束影响，因此不禁止发生的事情也可能会发生。这与旨在“执行”的语言（状态机、程序...）形成鲜明对比，其中唯一可能的更改是明确声明的更改。

可变

(= var) 签名或关系

不

被迫沿轨迹保持不变，因此在某些情况下它们会发生变化，而有些情况则不会。 静态（=非var）签名和关系具有在每次执行过程中保持恒定的附加约束。如果您想允许跟踪中的突变，但仅当某些事件（建模为

pred

）发生时，那么您不仅必须描述事件发生（您所做的）时发生的变化，还必须描述

不改变的内容

。这称为框架条件。