Following the online book, and running into issues

Questions
1

Hey All,

I’m finally picking up Alloy again, and trying to work through the online book: Formal Software Design with Alloy 6 — Formal Software Design with Alloy 6

I tried run the following assertion, and was getting an interesting error:

check restore_after_delete for 3 but 1… steps

and the error:

Bounded engines do not support open bounds on steps.

I was honestly a bit surprised with this, when the expected behavior is that there should be no issues. I’m guessing something is wrong with my setup (windows + default settings) but it’s not obvious what’s wrong. Any recommendations?

2

To check an assertion with 1.. steps scope you need to select in the options menu a solver with support for unbounded model checking. Currently, only two solvers support unbounded model checking, namely Electod/NuSMV and Electrod/nuXmv, but they rely on the external model checkers NuSMV and nuXmv that do not come packaged with the Alloy Analyzer. You need to install them directly and then the Analyzer will hopefully detect them and show you those options for solvers.

1 Like