Pkriens/api

[pkriens]

This is a big PR. However, there is only one commit in it that affects the current code base (e68e7f7). The rest is new code and things that have been rearranged.

The primary change is an abstract API that allows code to be written against Alloy without having to go to different places in static variables and methods. The abstract API allows one to access the environment, the solvers available on the device, the visualizers, and the compiler. An implementation of the API is provided that uses the existing code base. A fully abstract API is also provided for Solutions, Instance, Relation,Tuple,Atom, Sig, Field. etc. In the current implementation there was no clear distinction between their interface (and thus supported long term) and their implementation, which we need to be able to vary over time. This API will make it easier to remain backward compatible over time.

Since it is very important that Alloy becomes easy to extend the Java Service Loader is used to find the implementations of solvers and visualizers. Especially the solvers were tricky since so far they are tightly coupled to Kodkod. The solution was to provide a Solver API above Kodkod and then use the Kodkod code inside the 'plugin' solvers. Solvers have become self describing so we can now adjust the UI to query the Alloy object instead of hard coding things.

This is all available from the API but the existing application has not been adjusted yet. It is better to get some experience. To get some experience, I've rearranged the test cases to use the new API. They have been moved in a separate test project. Since the new API makes it easy to iterate over all the available solvers I've added tests to run all solvers on all models that we're testing.

The follow up plan is to start using the API instead of the implementation. First thing I want to do when this one is in is to provide a good command line and distribute it on brew. Then I think we should try to port the GUI part to the API.

Last but not least. I've documented the API also in an Alloy markdown document. I asked Daniel and David Chemouil to take a look but it seems a bit outside their comfort zone.

I realize that this a big job to review but I think this work is paramount to make progress.

[pkriens]

Is there a reason you removed the Eclipse autoformatting? We discussed this earlier and decided that consistent formatting was important? See 8dcfa151e4

[pkriens]

I've done a forced update of the branch so I could include the current master.

[aleksandarmilicevic]

Is there a reason you removed the Eclipse autoformatting? We discussed this earlier and decided that consistent formatting was important? See 8dcfa151e4

I removed it because it is terribly annoying to have a machine overwrite everything I type.

Consistent common sense formatting is important. I couldn't configure Eclipse to use common sense when it comes to alignment_for_selector_in_method_invocation. For example, when using stream, I like the following formatting:

something.stream()
    .map(...)
    .filter(...)
    .collect(...);

There is a value for the aforementioned setting that allows this. But, when using that value, Eclipse automatically breaks every expression that uses more than 1 method invocation:

something.stream()
    .map(x -> x.property
        .equals(y))
    .filter(...)
    .collect(...);

This is terribly ugly.

There is also that other spot in this PR regarding weirdly formatted string constants that you blamed on the auto-formatter, which is another reason to disable it.

[aleksandarmilicevic]

I've done a forced update of the branch so I could include the current master.

Does that mean that this force push overwrote some of my changes? At first glance, most of them seem to still be there, though.

[pkriens]

Well, we had the formatting discussion. I prefer automated formatting over manual formatting even though it might not always be perfect. It sounds like a perfect example of better being the enemy of good? So how do we then decide the standardized format? Maintaining a manual style guide to prevent some odd cases looks like too much cost for too little value?

[pkriens]

Thanks, for taking this attitude. I am aware I am an outlier that coding style issues are low on my list (and often disagree with the perceived value) while architecture and modularity are extremely high on my list (and often disagree with the perceived value :-). Maybe together we and make the right combination :-)

I really appreciate you engage with this. I will take another look and then commit it. Thanks.

[pkriens]

This is so outdated that I do not even know where to start. That said, it is a great idea :-(