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

try not to use a2r #13

Closed jonnybest closed 12 years ago

jonnybest commented 12 years ago

Improvement:

in Alloy the "in" operator is an isomorphic operator. It express membership predicate as in "a in R", where a is an atom and R a unary relation, and subset property as in "R1 in R2", where R1 and R2 are two relations. In our logic/representation we have an explicit operator for the membership property, namely "in_x" and an explicit one for subset "subset_x".

In the current translation we translate both meanings of the Alloy "in" to our "subset_x". For "a in R" we use our "a2r" and produce "subset(a2r(a), r)". If we do not do this, and keep simple thinks simple the automatic translation can prove our file system example.

Sure one may think about a lemma like "all r: Rel, a: Atom | subset(a2r(a), r) => in(a, r)". I tried it (in a hurry) but with no success.

jonnybest commented 12 years ago

Right now it seems that a2r_ is used only in join expressions. There are no expressions with subset and a2r in my examples.

jonnybest commented 12 years ago

fixed in 337e5ac3adce0d8d378884b7e0415ce1a9a2f69f