CODEWITHSUNDEEP
alloy
Shevach
Shevach

Reputation: 737

How to check if two predicates are equivalent?

I have two different inplementations for certain predicate and I want to check if both of them return the same instance, how can I achive that?

Thanks.

Upvotes: 0

Views: 681

Answers (1)

C. M. Sperberg-McQueen
C. M. Sperberg-McQueen

Reputation: 25034

I'd assert that the two predicates are always either both true or both false, and check the assertion.

pred P1 { ... }
pred P2 { ... }
assert P1_equiv_P2 { P1 iff P2 }
check P1_equiv_P2

If the predicates take arguments, then of course you need to check them on the same arguments:

pred P1[x : univ] { ... }
pred P2[x : univ] { ... }
assert P1_equiv_P2 { all x : univ | P1[x] iff P2[x] }
check P1_equiv_P2

Upvotes: 3

Related Questions