I like Alloy, especially after they added the new temporal features in version 6.
Last time I played with it, it had to be used from inside some awful IDE though. I know this is a common complaint, my point is not to repeat it. What I wanted to say is that while I was browsing the download page for Alloy just now, I noticed that it links to Sterling: A Web-based Visualizer for Relational Modeling Languages. I was hoping it would allow me to use my own editor and do custom visualisations in a browser, this doesn’t seem to be the case, rather it’s a new web-based IDE.
However, as I was skimming through the Sterling paper, I noticed that it said that Sterling also “is the visualizer for an Alloy-like model finder called Forge, which is being developed at Brown University and is used to teach a Logic for Systems class of over 60 students”. So I looked up Forge, it appears to be a Racket “language”/eDSL which looks like Alloy. I’m still not sure what the exact difference is, their readme says “Forge is heavily adapted from the excellent Alloy, a more widely used and somewhat more scalable tool. Forge and Alloy even use the same engines!”, but also “For broader historical context on Forge, the Alloy documentation or an Alloy demo may be useful. We don’t suggest using these as reference for Forge itself, however.”. In either case, it seems Forge might be a way to get a taste of Alloy without the sour taste of their IDE!
Hi, I’m one of the authors of Alloy 6 and of this new book.
I think the image of the Alloy Analyzer your depicting is a bit too dark. The IDE is quite sophisticated since it features an interconnection of a solving engine, a rich visualizer as well as a very useful evaluator (to navigate instances and counterexamples). Compared with other formal methods, I think Alloy is quite good in terms of user-friendliness and usefulness of results it provides. The legacy integrated editor is on the other hand quite basic but, considering models in Alloy are rather small, the -real- annoyances remain limited in my view (the editor has syntax highlighting, error reporting, find&replace…). An interesting aspect for non-power users is that this is all delivered in a single, ready-to-run JAR file. This is in particular invaluable with students (Alloy is taught in several universities, at least in Europe and in America).
A future version will allow users to rely on LSP and use an editor of their choice (there were already some experiments with LSP and there actually is an unofficial VSCode plugin but it’s not up to date). As an “epxert” user myself, what I would not want, however, would be to lose the the above-mentioned sophisticated interactions present in the tool, for the sake of getting a slicker editing experience.
Alloy 6.2 now has a command line but it’s not that great for solving, more for automated build chains. Many serious Alloy users I know use the Vscode extension.
The new A6.2 command line indeed allows to execute the same kinds commands than in the GUI, with roughly the same options, so it’s mainly aimed at facilitating batch verification and benchmarks, I’d say.
For people who do not know the Alloy Analyzer completely, this is different from the Evaluator feature mentioned above, which allows to query, in Alloy itself, an instance or counter-example currently being shown by the Visualizer. This feature, which isn’t new by the way, is very useful in practice when models become complex.
Finally, the VSCode extension does not use Alloy analyzer 6.1 nor 6.2 but it ships a tailored version, AFAIK. It’s indeed already great but, hopefully, in the future, we will be able to get a plugin that can connect to the “real”, official Alloy.
I like Alloy, especially after they added the new temporal features in version 6.
Last time I played with it, it had to be used from inside some awful IDE though. I know this is a common complaint, my point is not to repeat it. What I wanted to say is that while I was browsing the download page for Alloy just now, I noticed that it links to Sterling: A Web-based Visualizer for Relational Modeling Languages. I was hoping it would allow me to use my own editor and do custom visualisations in a browser, this doesn’t seem to be the case, rather it’s a new web-based IDE.
However, as I was skimming through the Sterling paper, I noticed that it said that Sterling also “is the visualizer for an Alloy-like model finder called Forge, which is being developed at Brown University and is used to teach a Logic for Systems class of over 60 students”. So I looked up Forge, it appears to be a Racket “language”/eDSL which looks like Alloy. I’m still not sure what the exact difference is, their readme says “Forge is heavily adapted from the excellent Alloy, a more widely used and somewhat more scalable tool. Forge and Alloy even use the same engines!”, but also “For broader historical context on Forge, the Alloy documentation or an Alloy demo may be useful. We don’t suggest using these as reference for Forge itself, however.”. In either case, it seems Forge might be a way to get a taste of Alloy without the sour taste of their IDE!
Hi, I’m one of the authors of Alloy 6 and of this new book.
I think the image of the Alloy Analyzer your depicting is a bit too dark. The IDE is quite sophisticated since it features an interconnection of a solving engine, a rich visualizer as well as a very useful evaluator (to navigate instances and counterexamples). Compared with other formal methods, I think Alloy is quite good in terms of user-friendliness and usefulness of results it provides. The legacy integrated editor is on the other hand quite basic but, considering models in Alloy are rather small, the -real- annoyances remain limited in my view (the editor has syntax highlighting, error reporting, find&replace…). An interesting aspect for non-power users is that this is all delivered in a single, ready-to-run JAR file. This is in particular invaluable with students (Alloy is taught in several universities, at least in Europe and in America).
A future version will allow users to rely on LSP and use an editor of their choice (there were already some experiments with LSP and there actually is an unofficial VSCode plugin but it’s not up to date). As an “epxert” user myself, what I would not want, however, would be to lose the the above-mentioned sophisticated interactions present in the tool, for the sake of getting a slicker editing experience.
Alloy 6.2 now has a command line but it’s not that great for solving, more for automated build chains. Many serious Alloy users I know use the Vscode extension.
The new A6.2 command line indeed allows to execute the same kinds commands than in the GUI, with roughly the same options, so it’s mainly aimed at facilitating batch verification and benchmarks, I’d say.
For people who do not know the Alloy Analyzer completely, this is different from the Evaluator feature mentioned above, which allows to query, in Alloy itself, an instance or counter-example currently being shown by the Visualizer. This feature, which isn’t new by the way, is very useful in practice when models become complex.
Finally, the VSCode extension does not use Alloy analyzer 6.1 nor 6.2 but it ships a tailored version, AFAIK. It’s indeed already great but, hopefully, in the future, we will be able to get a plugin that can connect to the “real”, official Alloy.