# PlusCal in Alloy **URL:** \ **Category:** Experimental\ **Created:** [August 27, 2020, 7:29am UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59 "2020-08-27T07:29:33Z")\ **Posts on this page:** 13\ **Page:** 2
**Author:** ![tinelli](https://avatars.discourse-cdn.com/v4/letter/t/f4b2a3/32.png) [@tinelli](https://alloytools.discourse.group/u/tinelli)\ **Post date:** [September 7, 2020, 9:39pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/21 "2020-09-07T21:39:16Z")
I have used Huth & Ryan in our Logic in Computer Science course at Iowa and I think it is an excellent introductory text. A more specialized one that I found pretty good and would recommend for an introduction to LTL is Software Reliability Methods by Doron Peled [https://link.springer.com/book/10.1007/978-1-4757-3540-6](https://link.springer.com/book/10.1007/978-1-4757-3540-6) 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. Cesare ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [September 8, 2020, 7:14am UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/22 "2020-09-08T07:14:03Z")
Hmm. It is a bit scary to realize all these books are long out of print. Then again, maybe it is time for the formal methods renaissance with Alloy! 🙂 ---
**Author:** ![tinelli](https://avatars.discourse-cdn.com/v4/letter/t/f4b2a3/32.png) [@tinelli](https://alloytools.discourse.group/u/tinelli)\ **Post date:** [September 8, 2020, 6:25pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/23 "2020-09-08T18:25:29Z")
> 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 🙂 Cesare ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [September 9, 2020, 9:55am UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/24 "2020-09-09T09:55:37Z")
My concern is more that this area seems to not moving into interesting commercial waters. Ah, well, story of my life 🙂 ---
**Author:** ![awwaiid](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/awwaiid/32/222_2.png) [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\ **Post date:** [February 25, 2024, 3:00am UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/25 "2024-02-25T03:00:15Z")
This sounds like an interesting experiment – did anything come of it? ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [March 1, 2024, 2:51pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/26 "2024-03-01T14:51:34Z")
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 … ---
**Author:** ![rix0rrr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/rix0rrr/32/102_2.png) [@rix0rrr](https://alloytools.discourse.group/u/rix0rrr)\ **Post date:** [November 9, 2024, 4:06pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/27 "2024-11-09T16:06:46Z")
Hey Peter, Don’t be down by a lack of interest in a group of specialists. I’d be interested in your work, to make Alloy easier to apply to certain problems. Any chance your compiler is up on GitHub somewhere? ---
**Author:** ![mica](https://avatars.discourse-cdn.com/v4/letter/m/85e7bf/32.png) [@mica](https://alloytools.discourse.group/u/mica)\ **Post date:** [November 10, 2024, 3:19pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/28 "2024-11-10T15:19:02Z")
Having hand translated the wire transfer example from PlusCal TLA+ to Alloy I am interested now too. ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [November 11, 2024, 2:57pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/29 "2024-11-11T14:57:16Z")
The code is here [GitHub - pkriens/org.alloytools.alloy at feature/pluscal](https://github.com/pkriens/org.alloytools.alloy/tree/feature/pluscal) 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 🙂 ) ---
**Author:** ![rix0rrr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/rix0rrr/32/102_2.png) [@rix0rrr](https://alloytools.discourse.group/u/rix0rrr)\ **Post date:** [November 11, 2024, 6:16pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/30 "2024-11-11T18:16:28Z")
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 :). ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [November 12, 2024, 11:00am UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/31 "2024-11-12T11:00:25Z")
Is that true? 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. ---
**Author:** ![rix0rrr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/rix0rrr/32/102_2.png) [@rix0rrr](https://alloytools.discourse.group/u/rix0rrr)\ **Post date:** [November 12, 2024, 12:04pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/32 "2024-11-12T12:04:28Z")
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. ---
**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Post date:** [November 12, 2024, 1:52pm UTC](https://alloytools.discourse.group/t/pluscal-in-alloy/59/33 "2024-11-12T13:52:03Z")
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. But lets agree to disagree … 🙂 [Previous page](https://alloytools.discourse.group/t/pluscal-in-alloy/59.md?page=1)