TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Integration with Alloy #4

Closed mhyee closed 11 years ago

mhyee commented 11 years ago

We originally attempted to strip Alloy out completely, but that didn't work because of JVM limitations and the fact that Alloy deduplicates results. (We do want more than one solution per Pareto point, but we don't want different permutations of the same solution. Alloy dedupes these permutations).

Therefore, the new approach is to bring Alloy and Kodkod together.

Alloy expects Kodkod to have "int overflow" support. That way, the constraint x < y + z can be true even if y + z overflows. Unfortunately, the changes to Kodkod were too invasive to pull in, so I just stubbed it out. This shouldn't matter because our models were designed to not overflow.

The corresponding changes to Alloy are committed at 1c66dea52380bffcd58966ae8a750590a704c95a.

Note that this pull request is a superset of https://github.com/TeamAmalgam/kodkod/pull/3

To get an easier diff to view (sorry, I had a macro that strips trailing whitespace), append w=1 to the diff url, eg https://github.com/TeamAmalgam/kodkod/commit/3bc51ed2068c678e723c0f4c11884058a3e48596?w=1

cpkleynhans commented 11 years ago

This code will need a lot of cleanup. In particular I don't like how specific these changes are to Alloy (e.g. AlloySolver class). As with #3 we can wait until the refactor to fix these issues. LGTM.

joseph39 commented 11 years ago

looks good!

AtulanZaman commented 11 years ago

good to go