The best practice to use boolean in Alloy model

Question

I'm building a simple Alloy to generate simple Java Pojo objects and some fields of that pojo are Boolean values. I'm now using the following mechanism to achieve this function

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

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

This will work but everytime I introduced a new boolean field I have to modify the boolean fact to make sure the value to be either "true" or "false". Is there any best practice to do this? Like what we Alloy does for Integers?

Garmon

Answer 1

It would be much better to introduce a Bool sig, and then use it for all your boolean fields, e.g.,

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

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

No additional fact is needed in this case.

If you like this approach, there is a built-in "util/boolean" library which defines Bool, True, and False sigs exactly like I did above, and additionally provides some helper functions (like isTrue, And, Or, etc.) so you can simply say

open util/boolean 

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

Hydrolyze

Even easier is enum Boolean { True, False } – Zea