Hi, I'm one of the authors of this new version of Alloy (which was code-named Electrum for some years): if you have any question, please do not hesitate to ask.

Hi, I'm one of the authors of this new version of Alloy (which was code-named Electrum for some years): if you have any question, please do not hesitate to ask. Indeed, Alloy is a model finder and you must bound the size of considered signatures. Still, notice you can now rely on complete temporal model-checking (based on NuSMV or nuXmv), meaning the temporal horizon doesn't have to be bounded. In practice, you'll still have small signature bounds, but that's an improvement. The UI is indeed old but the visualization part is really nice and, I think, still quite unique to help you understand a counterexample. We adapted it to display traces and also to allow exploration of alternative traces, which is really useful in practice (e.g. to check whether a certain operation is doable at some point in a trace). We also have a solving option that leverages CPU cores to (usually) accelerate solving quite a bit if the executed command is expected to return an instance.