boolean¶
Emulates boolean variables by creating True
and False
atoms.
-- module definition
module util/boolean
abstract sig Bool {}
one sig True, False extends Bool {}
pred isTrue[b: Bool] { b in True }
pred isFalse[b: Bool] { b in False }
In our code:
-- our code
open util/boolean
sig Account {
premium: Bool
}
Booleans created in this matter are not “true” booleans and cannot be used as part of regular Constraints, IE you cannot do bool1 && bool2
. Instead you must use the dedicated boolean predicates, below. As such, boolean
should be considered a proof-of-concept and is generally not recommended for use in production specs. You should instead represent booleans using subtyping.
Functions¶
All of the following have expected logic, but return Bool
atoms:
Not
And
Or
Xor
Nand
Nor
So to emulate bool1 && bool2
, write bool1.And[bool2].isTrue
.