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.


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.