Optimizing version of Alloy

Questions
1

I recall there was a version of Alloy that optimized/maximized the solution. I thought it was called Aluminum but that is just really had to search in combination with Alloy :slight_smile:

Anybody got a pointer to a paper or project?

2

If you are still interested in this, we have a new extension called AlloyMax that you might find relevant:

We are still polishing up the tool, but if you are interested in trying out a “beta” version, here’s the link to the jar file:

3

Wow! Fantastic! The optimization aspect is important I find in many use cases.

First question, how to integrate this in Alloy? I noticed you based this on 5.x. The Electrum integration for 6.0 makes a number of changes. How do you see the integration? Would this be a branch. I.e. a spec would be LTL xor MAX, or can the max facilities be merged with the LTL? I guess that would require changes in Parduinus?

Second issue is about the keywords. softno, softsome are kind of ugly. I guess soft no would already be better? I guess this is syntactic sugar but I wonder if we could use an annotation approach so that language integration would become easier. Where an annotation would be a token that we can pass through the layers but that does not require to be recognized by the parser. In this case for example @soft(1). Anyway, food for thought.

Really interesting work. I guess the biggest missing piece left in Alloy are then support for practical numbers?

Congratulations, nice work.

4

Thank you, Peter!

Regarding integration: It would be nice to merge this into Electrum, but I am not sure how this will interact with LTL. Perhaps there’s a way for MAX to “co-exist” with Electrum if only the SAT-based analysis is used, but I think this requires further deliberation with the Electrum team.

I agree that the names of the keywords can be improved, and we are planning to collect suggestions as we gain more users. I am less sure about the annotation approach though ("@" is already a reserved keyword, and I’m also wary of annotations cluttering up the model), but certainly open to discussion on this as well.

5

Microsoft C# uses [...] for annotations and I think using -- as a delimiter for options & annotations might work nice since they are discarded by older versions.

I think having the option this option would be very valuable … However, just having it only work on classic models would already be worth a lot.