[Aborted] Temporal Specification and Analysis (Electrum)

[nmacedo]

[aborted, created new PR #136]

Enhances Alloy with the ability to write mutable models (var sigs and fields), specify dynamic properties (LTL with past), and verify such properties through alternative backends (SAT and SMV). A presentation of this extended Alloy is available at here.

This is a major pull request, with significant changes in:

• the language: signatures/fields can be marked as variable; expressions can be primed; formulas can use past/future LTL operators; scopes can be assigned to trace lengths (including unbounded scopes for complete model checking)
• the analyses: relies on an extended version of Kodkod which natively supports LTL with past and analysis through SAT or SMV (including complete model checking); new configuration options selected through menu; a decomposed parallel analysis strategy
• the visualiser: instances are now navigable traces rather than single states; new iteration operations available (new init, new config, fork)

This extension is not expected to not break compatibility with previous Alloy models, whose analysis should result in the same experience.

I've annotated changes with an [HASLab] tag to make them more evident during development. I'll also leave local comments in the PR for relevant changes.

[pkriens]

Could you resolve the conflicts? There is not going on at the moment so this is a one time thing and it makes it easier to see what the changes are.

Is it a good idea to schedule some meetings to go through the code together? @aleksandarmilicevic ? @eskang ?

Anyway, nice work! Can't wait until we can release Alloy 6

[nmacedo]

Could you resolve the conflicts? There is not going on at the moment so this is a one time thing and it makes it easier to see what the changes are.

Is it a good idea to schedule some meetings to go through the code together? @aleksandarmilicevic ? @eskang ?

Anyway, nice work! Can't wait until we can release Alloy 6

Of course! This is still a draft of the PR, to be honest I thought it would not visible to anyone else before marking it as "ready for review".

[aleksandarmilicevic]

Yes, it would be a good idea to go through the PR together.

Just let us know when you're ready.

On Mon, Nov 16, 2020 at 7:02 AM Nuno Macedo notifications@github.com wrote:

Could you resolve the conflicts? There is not going on at the moment so this is a one time thing and it makes it easier to see what the changes are.

Is it a good idea to schedule some meetings to go through the code together? @aleksandarmilicevic https://github.com/aleksandarmilicevic ? @eskang https://github.com/eskang ?

Anyway, nice work! Can't wait until we can release Alloy 6

Of course! This is still a draft of the PR, to be honest I thought it would not visible to anyone else before marking it as "ready for review".

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/pull/135#issuecomment-728117922, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA3QGLNTH54JIJVLLKMMBKLSQE5IVANCNFSM4TW57PLA .

[nmacedo]

I had to commit some changes to Electrum which, for archival purposes, could not be pushed to the master branch. Unfortunately, GitHub doesn't support changing the source branch of a PR after creation, so I'll be closing this one and opening a new one, sorry for the trouble.

Also, I'd like again to suggest creating a temporary branch in which to merge this PR until we are sure it is stable enough for merging into the master branch.

[pkriens]

We do not need a stable branch as we discussed. Master is the develpment branch. In the extremely unlikely case that we need to do a fix to Alloy 5, we create an emergency branch of the release tag.

Keep it simple ...