3 ms·

I also did some time with Alloy. It soon became clear to me, that it seems to prove validity of logic through brute forcing and trying to search for counter exa

• vintermann 5y ago
  Of course. It's very upfront about being a model/counterexample finder, not a theorem prover. The UI (old Swing thing) also leaves a lot to be desired. But the language itself is lovely expressive, not what you expect from these sorts of told.
  • grayswandyr 5y ago
    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.