bug2: lemmas for transitive closure are identical

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

bug2: lemmas for transitive closure are identical #12

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

In addition to me report of yesterday I have found a one additional bug and a one (so fare mandatory) improvement.

Bug:

The two lemmas for the transitive closure are identical. Both talk about the first step of a path in the transitive closure. We also need to talk about the last step. Here the correction:

(assert (forall ((a1 Atom)(a2 Atom)(r Rel2)) (=> (in_2 a1 a2 (transClos r)) (exists ((a3 Atom)) (and (in_2 a1 a3 (transClos r)) (in_2 a3 a2 r))))) )

jonnybest commented 12 years ago

fixed in 47139432c52f1ebeead85fc4e19f60af08d662fe and 32bb7fdea86b2d6270438971ca71d4b7a5bbd9aa