Labs 02

Checking FOL identities and counterexamples.

Formulas from Predicate Logic Informally have no counterexamples.

'Variations' such as:

    (\forall x. (P(x) \land Q(y))) \ \leftrightarrow\ ((\forall x. P(x)) \lor (\forall x. Q(x)))

Relational identities

   (r_1 \cup r_2) \circ s = (r_1 \circ s) \cup (r_2 \circ s)

   (r_1 \cap r_2) \circ s = (r_1 \circ s) \cap (r_2 \circ s)

Sample Alloy Code


sig D { }
sig P in D { }
sig Q in D { }

// this shows no counterexample
//check { (all x:D|  (x in P) and (x in Q)) =>  (all x:D| x in P) and (all x:D| x in Q) }

// this shows counterexample
check { (all x:D|  (x in P) or (x in Q)) =>  (all x:D| x in P) or (all x:D| x in Q) }


// declaring binary relations r1,r2,s on A
sig A {
  r1 : set A,
  r2 : set A,
  s : set A  
// no counterexamples here:
// check { (r1 + r2).s = (r1.s + r2.s) }

// a counterexample here:
// check { (r1 & r2).s = (r1.s & r2.s) }