Alloy 6, Electrum is merged on the master branch

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.

1 Like

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

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

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.

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

1 Like

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?

Do you have nuXmv installed and in your PATH?

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:

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.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.decomp.UbdSymmetryTests > test[V2 V2 V1] FAILED
kodkod.engine.AbortedException at UbdSymmetryTests.java:273

kodkod.test.pardinus.decomp.UbdSymmetryTests > test[V5 V2 V1] FAILED
kodkod.engine.AbortedException at UbdSymmetryTests.java:273

kodkod.test.pardinus.decomp.UbdSymmetryTests > test[V6 V2 V1] FAILED
kodkod.engine.AbortedException at UbdSymmetryTests.java:273

1376 tests completed, 11 failed

Any ideas? Thanks!

Do you also have NuSMV installed?
(I will transmit your suggestion, thanks)

That worked! Now all tests are passing when I build Alloy. Thanks very much for your help :slight_smile: