I should note that both books are out of date with respect to the state of the art in automated reasoning/verification. They are perhaps more useful as references on the foundations.
Hmm. It is a bit scary to realize all these books are long out of print.
There are several other books on FMs which are in print but they are more technical.
I suggested Huth&Ryan and Peled because the temporal logic chapters there are pretty accessible, as they are meant to be undergraduate textbooks. And while they may be out of print, they are still available in electronic format
Well, it did work. But I did not find anybody remotely interested to further it. So I figured it was one of those things my kids told me the world wasn’t like me …
Please remember it was an experiment and because nobody seemed interested I’ve not done any industrialization.Use it at your own risk. (But let me know how it goes )
Ahh, I see you built it into the Alloy toolset itself. I think I had expected it to be a separate compiler which would translate PlusCalloy → Alloy.
That would perhaps also be a viable way to get it started; if it can be independent of Alloy itself, there is no need for Alloy maintainers to be bought into the idea, and anyone seeing use in it can pick it up and add it to their toolbox.
I’m halfway tempted to get that started but I also don’t want to kid myself into thinking I have more spare time than I do :).
The advantage of the ‘pluscal’ syntax is fully integrated with the Alloy. It is quite natural to use normal Alloy together with the proposed syntax. Over the last years we added the temporal logic and I do not see why adding syntax to handle sequential algorithms more easily would be out of place?People now do this now manually and are really bad in it. Especially the automatic frame conditions (ensuring a non-used variable does not change) is a godsend.
But my problem has always been that I am very open to change, if it seems better why not go for it. However, I find more and more that the far far majority is very conservative and the formal specifications area seems extremely conservative.
I think my argument is mainly one from practicality, as I am wont to do: this is a way to achieve X with the least amount of friction, so let’s do it! Admittedly, that usually gets me to local optima but not necessarily global ones.
The argument of automatic frame conditions is a perfect example of why this tool would be extremely useful; I don’t think it necessarily requires it to be integrated into the Alloy Analyzer itself.
If we look at the origins of PlusCal itself, if I recall correctly translating PlusCal → TLA requires an explicit translation step as well which you need to run by hand and is separate from model checking.
Not saying the user experience is ideal, just that there’s precedent, and it seems to work out “Fine”, for certain values of fine.
This also saved a lot of work, I could manipulate the AST that setup a new parser. Also did not need to create a UI or infrastructure. Which saved a lot of work.
)