Tip: checking predicates are equivalent

1

This is covered in Software Abstractions but I often see beginners not use it, so I’m sharing it here again.

Say we have a spec like

sig Node {
  , edges: set Node
}

pred dag {
  all n: Node | n not in n.^edges
}

And we decide to simplify our predicate, to make it faster or more obvious or whatnot. Here I’ll put it in relational form:

pred dag2 {
  no iden & ^edges
}

How do you know your simplification is correct? The easiest way is to just make it a property! Write a check that they’re either both true or both false, like this:

assert equivalence {
  dag <=> dag2
}

check equivalence

If you don’t get a counterexample, you know it holds in the scope you checked.

3 Likes