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

join lemma is broken #17

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

the lemma

"(forall ((a0 Atom)(a1 Atom)(a2 Atom)(r Rel3)) (=> (in_3 a0 a1 a2 r) (in_1 a2 (join_1x3 (a2r_1 a0) r))))"

has a type mismatch.

join_1x3 is of Rel2, but the in-function used is in_1.

same for "(forall ((a0 Atom)(a1 Atom)(a2 Atom)(r Rel3)) (=> (in_1 a2 (join_1x3 (a2r_1 a0) r)) (in_3 a0 a1 a2 r)))"

jonnybest commented 12 years ago

also crashes with Exception if left hand side is of greater arity than the right hand side

edu.kit.asa.alloy2key.key.ModelException: Something went wrong creating a call. Parameters cannot be null. at edu.kit.asa.alloy2key.key.Term.call(Term.java:230) at edu.kit.asa.alloy2key.key.KeYFile.assertLemmasJoin(KeYFile.java:427) at edu.kit.asa.alloy2key.key.KeYFile.declareJoin(KeYFile.java:419) at edu.kit.asa.alloy2key.Translator$ThisJoin.alter(Translator.java:1608) at edu.kit.asa.alloy2key.Translator.translateDecl(Translator.java:721) at edu.kit.asa.alloy2key.Translator.translateDecl(Translator.java:755) at edu.kit.asa.alloy2key.Translator.translateSigDecls(Translator.java:546) at edu.kit.asa.alloy2key.Translator.translate(Translator.java:119) at edu.kit.asa.alloy2key.Main.translate(Main.java:123) at edu.kit.asa.alloy2key.Main.doIt(Main.java:96) at edu.kit.asa.alloy2key.Main.main(Main.java:33)

jonnybest commented 12 years ago

fixing original problem with a136278f6cc7210586abea1ac9a9bfae5d37adfd moving rest to new