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

mults must be declared for arity 1 only #16

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

e.g. (forall ((x0 Atom)) (=> (in_1 x0 Node) (lone (join_1x2 (a2r_1 x0)

they get generated in generateMultConstrRight in Translator.java line 1121

edit: changed title from "mults have no associated arity"

jonnybest commented 12 years ago

according to the specs (daniel jackson's book appendix B, page 270), there is no other arity on multiplicity than 1: "if the expression denotes a set (that is, a unary relation), it may be prefixed by a multiplicity keyword"

and if it's not a set, you may not use the mults.