alloy - 在合金模型中使用 bool 值的最佳实践

Question

我正在构建一个简单的 Alloy 来生成简单的 Java Pojo 对象，该 pojo 的某些字段是 bool 值。我现在使用下面的机制来实现这个功能

one sig item {
    autoPay: String,
    Price: Int
}

fact boolean {
    all n: item {
        item.autoPay = "true" or
        item.autoPay = "false"
    } 
}

这会起作用，但每次我引入一个新的 bool 字段时，我都必须修改 bool 事实以确保该值为“真”或“假”。有没有最好的做法来做到这一点？就像我们合金对整数所做的那样？

Answer 1

最好引入一个 Bool sig，然后将它用于所有 bool 字段，例如，

abstract sig Bool{}
one sig True extends Bool
one sig False extends Bool

one sig item {
  autoPay: Bool,
  Price: Int
}

在这种情况下不需要额外的事实。

如果你喜欢这种方法，有一个内置的“util/boolean”库定义了 Bool , True , 和 False sigs 和我上面做的完全一样，另外还提供了一些辅助函数(比如 isTrue 、 And 、 Or 等)所以你可以简单地说

open util/boolean 

one sig item {
  autoPay: Bool,
  Price: Int
}