search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

axiom and lemma for join_2x1 broken #25

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

The axiom for join_2x1 results in:

(assert
(forall ((A Rel2)(B Rel1)(y0 Atom)) (= (in_1 y0 (join_2x1 A B)) (exists ((x0 Atom)(x1 Atom)) (and (in_2 x0 x1 A) (in_2 x1 y0 B)))))
)

This assertion is invalid, because in_2 is not defined for B, which is of Rel1.

jonnybest commented 12 years ago

upon further investigation, the lemmas are also misshaped:

(assert
  ; 1. lemma for join_2x1. direction: join to in
(forall ((a0 Atom)(a1 Atom)(r Rel2)) (=> (in_1 a0 (join_2x1 r (a2r_2 a1))) (in_2 a0 a1 r)))
)
(assert
  ; 2. lemma for join_2x1. direction: in to join
(forall ((a0 Atom)(a1 Atom)(r Rel2)) (=> (in_2 a0 a1 r) (in_1 a0 (join_2x1 r (a2r_2 a1)))))
)

they invoke the wrong a2r function

jonnybest commented 12 years ago

the misshaped lemma and axiom were actually different problems. I fixed the misshaped lemma by properly calling a2r. I fixed the join axiom by changing the way the left hand tuple and the right hand tuple were generated. the previous way worked for all joins with arity = 1 on the left hand argument, but it ignored the actual meaning of the missing atom X and its position within the left hand tuple.