# Uncategorized **URL:** https://alloytools.discourse.group/c/uncategorized/1.md [Latest](https://alloytools.discourse.group/latest.md) · [Categories](https://alloytools.discourse.group/categories.md) --- ## [Welcome to Alloytools](https://alloytools.discourse.group/t/welcome-to-alloytools/7)
**Author:** [@system](https://alloytools.discourse.group/u/system)\ **Replies:** 4\ **Last updated:** [August 11, 2020, 4:59pm UTC](https://alloytools.discourse.group/t/welcome-to-alloytools/7 "2020-08-11T16:59:14Z")
This is the Alloytools discussion site. Discuss any issue you feel like as long as it is related to formal modeling and/or Alloy. --- ## [ABZ'27 Call for Papers](https://alloytools.discourse.group/t/abz27-call-for-papers/574)
**Author:** [@alcino](https://alloytools.discourse.group/u/alcino)\ **Replies:** 0\ **Last updated:** [October 5, 2026, 2:13pm UTC](https://alloytools.discourse.group/t/abz27-call-for-papers/574 "2026-10-05T14:13:41Z")
Hi, ABZ is a conference dedicated to state-based methods such as Alloy. The Call for Papers for next year edition can be found in the conference web page at: I’ve read several posts in this forum about the usage of A… --- ## [Relational Algebra versus Algebra of Relations](https://alloytools.discourse.group/t/relational-algebra-versus-algebra-of-relations/573)
**Author:** [@mica](https://alloytools.discourse.group/u/mica)\ **Replies:** 0\ **Last updated:** [September 22, 2026, 4:07am UTC](https://alloytools.discourse.group/t/relational-algebra-versus-algebra-of-relations/573 "2026-09-22T04:07:00Z")
Relation algebra ≠ relational algebra One major piece of software built on it is the Alloy analyzer which calls it “relational logic” (which was incorrectly redirected to the page for relational algebra until I fixed i… --- ## [A human-subject study on how people create visualizations for Alloy](https://alloytools.discourse.group/t/a-human-subject-study-on-how-people-create-visualizations-for-alloy/571)
**Author:** [@yiliangl](https://alloytools.discourse.group/u/yiliangl)\ **Replies:** 0\ **Last updated:** [September 8, 2026, 3:32pm UTC](https://alloytools.discourse.group/t/a-human-subject-study-on-how-people-create-visualizations-for-alloy/571 "2026-09-08T15:32:59Z")
Hi everyone, I am Yiliang Liang, a PhD student at Carnegie Mellon University advised by Prof. Eunsuk Kang and Prof. Joshua Sunshine. My research is on the roles that visualizations play in making formal modeling more ac… --- ## [A field report of using Alloy with agent-based development](https://alloytools.discourse.group/t/a-field-report-of-using-alloy-with-agent-based-development/555)
**Author:** [@ohpauleez](https://alloytools.discourse.group/u/ohpauleez)\ **Replies:** 12\ **Last updated:** [June 29, 2026, 1:58pm UTC](https://alloytools.discourse.group/t/a-field-report-of-using-alloy-with-agent-based-development/555 "2026-06-29T13:58:48Z")
Hi all! I wanted to share some results and high-level techniques of using Alloy as part of AI-based development, specifically using agents and harnesses. I’ll leave my own conclusions until the end of the post. And pleas… --- ## [Do not forget to play your wordle today!](https://alloytools.discourse.group/t/do-not-forget-to-play-your-wordle-today/554)
**Author:** [@alcino](https://alloytools.discourse.group/u/alcino)\ **Replies:** 0\ **Last updated:** [June 4, 2026, 5:32pm UTC](https://alloytools.discourse.group/t/do-not-forget-to-play-your-wordle-today/554 "2026-06-04T17:32:12Z")
:slightly\_smiling\_face: And sorry for ruining your game… Alcino --- ## [What are the possibilities of using alloy?](https://alloytools.discourse.group/t/what-are-the-possibilities-of-using-alloy/549)
**Author:** [@joel6603](https://alloytools.discourse.group/u/joel6603)\ **Replies:** 0\ **Last updated:** [March 5, 2026, 2:32pm UTC](https://alloytools.discourse.group/t/what-are-the-possibilities-of-using-alloy/549 "2026-03-05T14:32:30Z")
Hi, I am a post graduate student and pretty new to model checking. I got interest in alloy . I hope to do a good work in it. Can anyone suggest some problems or potential area for research which make use of alloy? --- ## [Current use of Alloy in the age of AI](https://alloytools.discourse.group/t/current-use-of-alloy-in-the-age-of-ai/544)
**Author:** [@roehst](https://alloytools.discourse.group/u/roehst)\ **Replies:** 1\ **Last updated:** [January 27, 2026, 3:39pm UTC](https://alloytools.discourse.group/t/current-use-of-alloy-in-the-age-of-ai/544 "2026-01-27T15:39:37Z")
I have been using Alloy as my daily driver now. I can spec from whole system do algorithm or protocol designs and hand it over to an LLM to code it. This was step one. Step two was tweaking Alloy to extract code from th… --- ## [Integer bitwidth, again](https://alloytools.discourse.group/t/integer-bitwidth-again/532)
**Author:** [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\ **Replies:** 3\ **Last updated:** [April 9, 2025, 9:20am UTC](https://alloytools.discourse.group/t/integer-bitwidth-again/532 "2025-04-09T09:20:57Z")
Looking at this Stack Overflow question, in response to which @peter.kriens explains that the int bitwidth needs to be set. This is really horrible, isn’t it? Any way we could mitigate it? For example, set the integer b… --- ## [Alloy, Dependability Cases, and \`evidence\`](https://alloytools.discourse.group/t/alloy-dependability-cases-and-evidence/472)
**Author:** [@ohpauleez](https://alloytools.discourse.group/u/ohpauleez)\ **Replies:** 3\ **Last updated:** [July 22, 2024, 1:17pm UTC](https://alloytools.discourse.group/t/alloy-dependability-cases-and-evidence/472 "2024-07-22T13:17:19Z")
I’ve been using Alloy for well over a decade now, but I’m looking to get more out of it (inspired by a research arc spanning from Jackson’s “A direct path to dependable software” to Torlak’s “How We Built Cedar: A Verifi… --- ## [Got Tripped at Alloy4Fun Photo Sharing Social Network](https://alloytools.discourse.group/t/got-tripped-at-alloy4fun-photo-sharing-social-network/427)
**Author:** [@mica](https://alloytools.discourse.group/u/mica)\ **Replies:** 4\ **Last updated:** [May 20, 2024, 2:53pm UTC](https://alloytools.discourse.group/t/got-tripped-at-alloy4fun-photo-sharing-social-network/427 "2024-05-20T14:53:43Z")
Hello, I have been looking at Alloy thanks to hwayne and glad to come back see Alloy 6 extended with temporal logic! I am trying to get back to learning Alloy and going through the Alloy 6 book. And I am a bit embarrasse… --- ## [Inline theme hints?](https://alloytools.discourse.group/t/inline-theme-hints/461)
**Author:** [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\ **Replies:** 3\ **Last updated:** [April 17, 2024, 3:48pm UTC](https://alloytools.discourse.group/t/inline-theme-hints/461 "2024-04-17T15:48:18Z")
Has any thought been given to some sort of inline theme configuration, right inside of the .als file? Here’s the sort of thing I have in mind. I’m modeling a simple (existing) inventory control system, which keeps track… --- ## [Alloy Facts - Blog Post from Hillel Wayne](https://alloytools.discourse.group/t/alloy-facts-blog-post-from-hillel-wayne/460)
**Author:** [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\ **Replies:** 0\ **Last updated:** [April 11, 2024, 7:46pm UTC](https://alloytools.discourse.group/t/alloy-facts-blog-post-from-hillel-wayne/460 "2024-04-11T19:46:17Z")
I’ve enjoyed this blog post from @hwayne yesterday! Good exposition on facts vs predicates, as discussed previously here. --- ## [What is electrod?](https://alloytools.discourse.group/t/what-is-electrod/458)
**Author:** [@awwaiid](https://alloytools.discourse.group/u/awwaiid)\ **Replies:** 7\ **Last updated:** [April 11, 2024, 8:17am UTC](https://alloytools.discourse.group/t/what-is-electrod/458 "2024-04-11T08:17:01Z")
Greetings! What is electrod and how does it related to Alloy’s main repo? I am under the rough understanding that Electrum work was merged in for Alloy6 and that all-is-alloy now, but I see recent activity in the electro… --- ## [How to build Alloy6 'master' branch? (org.alloytools.alloy.lsp is not linked with a Java project)](https://alloytools.discourse.group/t/how-to-build-alloy6-master-branch-org-alloytools-alloy-lsp-is-not-linked-with-a-java-project/441)
**Author:** [@alexn](https://alloytools.discourse.group/u/alexn)\ **Replies:** 12\ **Last updated:** [February 9, 2024, 2:56pm UTC](https://alloytools.discourse.group/t/how-to-build-alloy6-master-branch-org-alloytools-alloy-lsp-is-not-linked-with-a-java-project/441 "2024-02-09T14:56:01Z")
Using latest Eclipse Java (2023-12) on Ubuntu Linux 22.04, I get errors that include: Bndtools: The project in …/org.alloytools.alloy/org.alloytools.alloy.lsp is not linked with a Java project. Imported as instructed i… --- ## [nuSMV and nuXmv on Apple M2](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327)
**Author:** [@esb-dev](https://alloytools.discourse.group/u/esb-dev)\ **Replies:** 23\ **Last updated:** [January 30, 2024, 9:15am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327 "2024-01-30T09:15:09Z")
I tried to install und use nuSMV and nuXmv on the new Apple MacBook with M2. But apparently both model checkers only run on x86. Any suggestions what to do? Kind regards --- ## [Concept Design, Code Reading and Collaboration](https://alloytools.discourse.group/t/concept-design-code-reading-and-collaboration/434)
**Author:** [@mdashx](https://alloytools.discourse.group/u/mdashx)\ **Replies:** 0\ **Last updated:** [January 23, 2024, 1:18pm UTC](https://alloytools.discourse.group/t/concept-design-code-reading-and-collaboration/434 "2024-01-23T13:18:43Z")
I’m interested in reading through existing code to produce concept designs as described by Daniel Jackson in The Essence of Software. I’m also interested in producing Alloy models of existing code bases. Is anyone inter… --- ## [Predicate inv13 in Alloy4Fun Courses seems wrong](https://alloytools.discourse.group/t/predicate-inv13-in-alloy4fun-courses-seems-wrong/428)
**Author:** [@mica](https://alloytools.discourse.group/u/mica)\ **Replies:** 0\ **Last updated:** [January 11, 2024, 5:02pm UTC](https://alloytools.discourse.group/t/predicate-inv13-in-alloy4fun-courses-seems-wrong/428 "2024-01-11T17:02:00Z")
Alloy4Fun Courses is Exercise 1.e in Structural design with Alloy in the book Formal Software Design with Alloy 6. I am working through it and have been quite confused by its predicate inv13, and now that I have figured … --- ## [Merging two sets of relations by some rule](https://alloytools.discourse.group/t/merging-two-sets-of-relations-by-some-rule/407)
**Author:** [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\ **Replies:** 2\ **Last updated:** [October 10, 2023, 10:24am UTC](https://alloytools.discourse.group/t/merging-two-sets-of-relations-by-some-rule/407 "2023-10-10T10:24:23Z")
Say I have a Document with a counts field, like this: open util/natural sig ID {} sig Document { counts: ID -\> lone Natural } I’d like to merge any two documents by combining the counts and taking the max Natural f… --- ## [Trival condition violated in a model of 2Psets?](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404)
**Author:** [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\ **Replies:** 6\ **Last updated:** [October 4, 2023, 11:54am UTC](https://alloytools.discourse.group/t/trival-condition-violated-in-a-model-of-2psets/404 "2023-10-04T11:54:52Z")
I’m trying to model a 2Pset CRDT in Alloy and I’m having some trouble. Basically, I think I’m telling Alloy that syncing two documents should result in them having the same items, but in reality I think there’s some triv… --- ## [Beginner stuck on traces](https://alloytools.discourse.group/t/beginner-stuck-on-traces/399)
**Author:** [@PhoenixRising2023](https://alloytools.discourse.group/u/PhoenixRising2023)\ **Replies:** 1\ **Last updated:** [September 1, 2023, 7:32am UTC](https://alloytools.discourse.group/t/beginner-stuck-on-traces/399 "2023-09-01T07:32:38Z")
I am totally new to this side of the programming world but very interested. I am trying to get my hands dirty so to speak by modeling system that associates papers by the search strategy used to originally retrieve the p… --- ## [Apparently irregular type inference for +/- operators](https://alloytools.discourse.group/t/apparently-irregular-type-inference-for-operators/391)
**Author:** [@Eutectic](https://alloytools.discourse.group/u/Eutectic)\ **Replies:** 2\ **Last updated:** [August 19, 2023, 4:03pm UTC](https://alloytools.discourse.group/t/apparently-irregular-type-inference-for-operators/391 "2023-08-19T16:03:30Z")
Hello everyone, I’m trying to understand the behavior of the + and - operators in the context of the Int/int types. I’ve pored through the documentation, the book, and the source code for parsing, but I can’t figure thi… --- ## [What documentation / learning material would you like to see?](https://alloytools.discourse.group/t/what-documentation-learning-material-would-you-like-to-see/341)
**Author:** [@hwayne](https://alloytools.discourse.group/u/hwayne)\ **Replies:** 9\ **Last updated:** [August 19, 2023, 6:34am UTC](https://alloytools.discourse.group/t/what-documentation-learning-material-would-you-like-to-see/341 "2023-08-19T06:34:11Z")
Planning on getting back to working on alloydocs this summer and updating it with Alloy 6 (finally!) Are there any other topics you’d like to see covered as either reference material or as tutorials/topics/examples/etc? --- ## [Not understanding the visualization for mutable sets](https://alloytools.discourse.group/t/not-understanding-the-visualization-for-mutable-sets/385)
**Author:** [@io7m](https://alloytools.discourse.group/u/io7m)\ **Replies:** 2\ **Last updated:** [August 16, 2023, 3:13pm UTC](https://alloytools.discourse.group/t/not-understanding-the-visualization-for-mutable-sets/385 "2023-08-16T15:13:29Z")
Hello! I’ve just started working with Alloy, and I feel like I’m misunderstanding what the visualization is telling me. I have the following trivial (and very much incomplete) spec that models a mutable store of bookmar… --- ## [TLA+-like unchanged](https://alloytools.discourse.group/t/tla-like-unchanged/358)
**Author:** [@alexshirley](https://alloytools.discourse.group/u/alexshirley)\ **Replies:** 4\ **Last updated:** [June 15, 2023, 1:47pm UTC](https://alloytools.discourse.group/t/tla-like-unchanged/358 "2023-06-15T13:47:52Z")
Hey All, I’m trying to create a TLA±like unchanged function, but there are two problems that I seem to be having. module unchanged\[x\] pred unchanged\[s:x\]{ s' = s } The first, is that I can’t seem to pass relationshi… --- ## [questions about Alloy coding and instances](https://alloytools.discourse.group/t/questions-about-alloy-coding-and-instances/352)
**Author:** [@Najihah](https://alloytools.discourse.group/u/Najihah)\ **Replies:** 1\ **Last updated:** [June 6, 2023, 8:23am UTC](https://alloytools.discourse.group/t/questions-about-alloy-coding-and-instances/352 "2023-06-06T08:23:47Z")
questions about Alloy coding and instances module ORparticipant abstract sig participant {} lone sig participant1 extends participant {verb1: lone event1, verb2: lone event2} {(#verb1=1 or #verb2=1)} lone sig particip… --- ## [Alloy @ ABZ'23 conference](https://alloytools.discourse.group/t/alloy-abz23-conference/335)
**Author:** [@alcino](https://alloytools.discourse.group/u/alcino)\ **Replies:** 0\ **Last updated:** [April 15, 2023, 6:46am UTC](https://alloytools.discourse.group/t/alloy-abz23-conference/335 "2023-04-15T06:46:01Z")
Dear all, At the upcoming ABZ’23 conference Nuno Macedo and myself will give a short tutorial about “Teaching Alloy with Alloy4Fun”. If you are currently teaching (or planning to teach) Alloy please consider attending! … --- ## [Getting Alloy to run on Fedora Linux](https://alloytools.discourse.group/t/getting-alloy-to-run-on-fedora-linux/330)
**Author:** [@Seanny123](https://alloytools.discourse.group/u/Seanny123)\ **Replies:** 0\ **Last updated:** [April 3, 2023, 7:11pm UTC](https://alloytools.discourse.group/t/getting-alloy-to-run-on-fedora-linux/330 "2023-04-03T19:11:32Z")
Sharing the steps I took to get Alloy running on Fedora Linux in case anyone else has problems. Problem I am running Fedora 37 and have Java 8 installed, which I verified with java -version after activating that version… --- ## [Alloy 6 Examples/Tutorials?](https://alloytools.discourse.group/t/alloy-6-examples-tutorials/199)
**Author:** [@mattdf](https://alloytools.discourse.group/u/mattdf)\ **Replies:** 5\ **Last updated:** [April 3, 2023, 4:21pm UTC](https://alloytools.discourse.group/t/alloy-6-examples-tutorials/199 "2023-04-03T16:21:12Z")
Now that Alloy 6 is finally released, will we get an update to the book to cover the new grammar and features, or some tutorials specific to it? Would really help to get my head around the new features properly. I’d be … --- ## [Modeling a presentation with ordered slides](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326)
**Author:** [@marko](https://alloytools.discourse.group/u/marko)\ **Replies:** 8\ **Last updated:** [March 22, 2023, 2:49pm UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326 "2023-03-22T14:49:23Z")
Hi! I’m trying to model a presentation with ordered slides, with no slide appearing in two presentations, and every slide appearing in a presentation. sig Presentation { // At most #Int arrows, exactly #Slide arrows, … [Next page](https://alloytools.discourse.group/c/uncategorized/1.md?page=1)