Alloy 6, Electrum is merged on the master branch

peter.kriens · March 2, 2021, 10:36am

The Electrum team has merged their epic work on the Alloy master branch, which will be used for release 6. This is still early days but you might want to take a peek.

steve.freeman · March 2, 2021, 10:49am

Good news. I’ve been in TLA land for a while because it was more suitable for the problem, but this should make a difference. This would be a good opportunity to get the word out with some associated content.

S

ocharles · March 8, 2021, 5:06pm

This is wonderful news! Is there a .jar available that we can try?

peter.kriens · March 9, 2021, 9:15am

The files are not stored yet. I need to move it to Github Actions and make this work.

You can checkout the repository and build it yourself though.

grayswandyr · March 10, 2021, 6:11pm

Meanwhile, you can use the Electrum jar that @nmacedo built: Release Electrum v2.1.4 · haslab/Electrum2 · GitHub

nday · May 5, 2021, 2:30pm

When I build Alloy 6, I’m getting a lot of failed tests:

Task :org.alloytools.pardinus:test

kodkod.test.pardinus.temporal.InstanceExpansionTests > testTmp1SMV FAILED
kodkod.engine.AbortedException at InstanceExpansionTests.java:91

kodkod.test.pardinus.temporal.InstanceExpansionTests > testTmp2SMV FAILED
kodkod.engine.AbortedException at InstanceExpansionTests.java:148

kodkod.test.pardinus.temporal.InstanceExpansionTests > testTmp3SMV FAILED
kodkod.engine.AbortedException at InstanceExpansionTests.java:200

kodkod.test.pardinus.temporal.ExampleTests > testUNSATFormulaComplete FAILED
kodkod.engine.AbortedException at ExampleTests.java:96

kodkod.test.pardinus.temporal.ExampleTests > testSATComplete FAILED
kodkod.engine.AbortedException at ExampleTests.java:84

kodkod.test.pardinus.temporal.BaseTests > testUnsatSMVLength FAILED
kodkod.engine.AbortedException at BaseTests.java:355

kodkod.test.pardinus.temporal.BaseTests > testUnsatSMV FAILED
kodkod.engine.AbortedException at BaseTests.java:279

kodkod.test.pardinus.temporal.BaseTests > testSatSMV FAILED
kodkod.engine.AbortedException at BaseTests.java:243

kodkod.test.pardinus.temporal.BaseTests > testSatSMVComplete FAILED
kodkod.engine.AbortedException at BaseTests.java:317

kodkod.test.pardinus.temporal.TemporalIdentitiesTests > test[(always(after(some g)) iff after(always(some g))) electrod false] FAILED
kodkod.engine.AbortedException at TemporalIdentitiesTests.java:260

kodkod.test.pardinus.temporal.TemporalIdentitiesTests > test[(always(some g) iff !eventually(!some g)) electrod false] FAILED
kodkod.engine.AbortedException at TemporalIdentitiesTests.java:260

etc.

The GUI runs although I haven’t yet tried the Pardinus functionality. Should I be concerned about the failed tests?

grayswandyr · May 10, 2021, 9:47am

Do you have nuXmv installed and in your PATH?

nday · May 10, 2021, 4:11pm

Thanks for the advice. I’ve installed nuXmv and more tests now pass. (I suggest putting the instructions to install nuXmv in the README.md) However, there are still 11 tests that fail: