join lemma crashes with right hand join

[jonnybest]

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]

this is probably how it should look:

(assert
    (forall ((a0 Atom)(a1 Atom)(a2 Atom)(r Rel3)) (=> 
    (in_3 a0 a1 a2 r) 
    (in_2 a0 a1 (join_3x1 
        r
        (a2r_1 a2) 
        ))))
)
(assert
    (forall ((a0 Atom)(a1 Atom)(a2 Atom)(r Rel3)) (=> 
    (in_2 a0 a1 (join_3x1
        r 
        (a2r_1 a2))) 
    (in_3 a0 a1 a2 r)))
)

[jonnybest]

There is a simple way around this:

0. create a relation for the larger arity.
1. create a tuple for each unique row. that means all rows not counting the ones being joined
2. create a tuple "relmembers" of the first few. it will be a member of the relation, so create enough atoms to fit the relation.
3. create a tuple "singles" with the last few atoms, starting with the last atom of "relmembers"
4. create a tuple of the resulting expression
5. examine the join expression. if the left hand Relation is of higher arity than the right hand, simply reverse all tuples.
6. create the expressions that make up your lemma. the argument with the higher arity should be filled with the relation, the argument of the lower arity should be filled with tuples. this way, both conditions can be handled with one generation.

I did not examine this generation or the resulting lemmas for their practicality. this is just the way to create similar, valid lemmas for each possible join expression.