# Questions **URL:** https://alloytools.discourse.group/c/questions/9.md [Latest](https://alloytools.discourse.group/latest.md) · [Categories](https://alloytools.discourse.group/categories.md) --- ## [About the Questions category](https://alloytools.discourse.group/t/about-the-questions-category/33)
**Author:** [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Replies:** 0
Questions about using Alloy. If you got a stuck model, try to minimize it to the essence and post your question here. --- ## [Adversarial review request: soundness of a TLA+ state projection after resource exhaustion](https://alloytools.discourse.group/t/adversarial-review-request-soundness-of-a-tla-state-projection-after-resource-exhaustion/568)
**Author:** [@ausgs](https://alloytools.discourse.group/u/ausgs)\ **Replies:** 1\ **Last updated:** [September 14, 2026, 11:25pm UTC](https://alloytools.discourse.group/t/adversarial-review-request-soundness-of-a-tla-state-projection-after-resource-exhaustion/568 "2026-09-14T23:25:13Z")
Hello, I’m seeking an adversarial formal-methods review of a narrow abstraction question arising from a TLA+ model-checking run. The original model, which I call Step 17, stored four append-only histories directly in t… --- ## [Independent Alloy review request — ChronoRealm Assurance Protocol v1.2 state-transition model](https://alloytools.discourse.group/t/independent-alloy-review-request-chronorealm-assurance-protocol-v1-2-state-transition-model/570)
**Author:** [@ausgs](https://alloytools.discourse.group/u/ausgs)\ **Replies:** 0\ **Last updated:** [August 11, 2026, 3:44pm UTC](https://alloytools.discourse.group/t/independent-alloy-review-request-chronorealm-assurance-protocol-v1-2-state-transition-model/570 "2026-08-11T15:44:40Z")
TITLE: Independent Alloy review request — ChronoRealm Assurance Protocol v1.2 state-transition model BODY: Daniel Jackson recommended that I post this here. I’m seeking adversarial review of this bounded relational/st… --- ## [Am I Creating The Correct Alloy Model To Match My ERD?](https://alloytools.discourse.group/t/am-i-creating-the-correct-alloy-model-to-match-my-erd/559)
**Author:** [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\ **Replies:** 0\ **Last updated:** [July 8, 2026, 3:31pm UTC](https://alloytools.discourse.group/t/am-i-creating-the-correct-alloy-model-to-match-my-erd/559 "2026-07-08T15:31:27Z")
I’m just trying to confirm that the Alloy model I’ve created sort of corresponds to a high-level ERD. I’m trying to model a database to allow me to capture all the various comic book issues I’ve got in anthology books. F… --- ## [Scopes for sigs constrained by the ordering module](https://alloytools.discourse.group/t/scopes-for-sigs-constrained-by-the-ordering-module/557)
**Author:** [@nday](https://alloytools.discourse.group/u/nday)\ **Replies:** 1\ **Last updated:** [July 8, 2026, 2:44pm UTC](https://alloytools.discourse.group/t/scopes-for-sigs-constrained-by-the-ordering-module/557 "2026-07-08T14:44:48Z")
I’ve been looking at the following small Alloy model trying to understand how scopes are chosen for sigs constrained by the ordering module: open util/ordering\[A1\] open util/ordering\[A2\] sig A {} sig A1,A2 extends A {… --- ## [How to tell a story using alloy models?](https://alloytools.discourse.group/t/how-to-tell-a-story-using-alloy-models/556)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 2\ **Last updated:** [June 28, 2026, 6:36pm UTC](https://alloytools.discourse.group/t/how-to-tell-a-story-using-alloy-models/556 "2026-06-28T18:36:21Z")
The books on alloy and blog posts reveal a model step by step, by additions and modifications in files, and we have a list of versions: model\_1.als, …, model\_n.als. I’d like to make this workflow less file-centric and mo… --- ## [What does "expect 1" mean?](https://alloytools.discourse.group/t/what-does-expect-1-mean/308)
**Author:** [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\ **Replies:** 4\ **Last updated:** [May 10, 2026, 6:23am UTC](https://alloytools.discourse.group/t/what-does-expect-1-mean/308 "2026-05-10T06:23:45Z")
When you open up Alloy, the default run in the menu is “Run Default for 4 but 4 int, 4 seq expect 1.” I know what for 4 and but 4 int mean but I don’t know what “expect 1” means! Further, it doesn’t look like the spec me… --- ## [How to initialize a hard-coded sequence?](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553)
**Author:** [@cam](https://alloytools.discourse.group/u/cam)\ **Replies:** 6\ **Last updated:** [April 24, 2026, 11:27am UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553 "2026-04-24T11:27:04Z")
I have a set of ~20 singletons. What’s the best way to create a sequence of those singletons in the order I specify? \`\`\` sig A {} // #A = 20 things that need to be in a particular order sig B { myOrder: seq A // … --- ## ["MiniSat with Unsat Core" missing as option](https://alloytools.discourse.group/t/minisat-with-unsat-core-missing-as-option/479)
**Author:** [@Auri](https://alloytools.discourse.group/u/Auri)\ **Replies:** 2\ **Last updated:** [April 23, 2026, 4:11pm UTC](https://alloytools.discourse.group/t/minisat-with-unsat-core-missing-as-option/479 "2026-04-23T16:11:16Z")
I am currently working on an description of the behavior of Red-Black-Trees in Alloy. This is a greater project than any I have done before in Alloy (I am a beginner). I have run into some problems, which I couldn’t sol… --- ## [Associativity and meaning of multi-arity signature declarations](https://alloytools.discourse.group/t/associativity-and-meaning-of-multi-arity-signature-declarations/550)
**Author:** [@nday](https://alloytools.discourse.group/u/nday)\ **Replies:** 1\ **Last updated:** [April 23, 2026, 12:09pm UTC](https://alloytools.discourse.group/t/associativity-and-meaning-of-multi-arity-signature-declarations/550 "2026-04-23T12:09:12Z")
We have been studying the associativity of the → in multi-arity relations and also the meaning of multiplicities in these declarations. Can an Alloy developer please confirm that the associativity of → is RIGHT?, i.e. … --- ## [How to enforce concurrent operations?](https://alloytools.discourse.group/t/how-to-enforce-concurrent-operations/546)
**Author:** [@krisis](https://alloytools.discourse.group/u/krisis)\ **Replies:** 7\ **Last updated:** [February 27, 2026, 4:47am UTC](https://alloytools.discourse.group/t/how-to-enforce-concurrent-operations/546 "2026-02-27T04:47:23Z")
I’m trying to model a storage system which is composed of multiple shards. Any file uploaded will be placed in one of these shards. This system supports versioning, which means subsequent uploads of a file end up in the … --- ## [Implicit facts with multirelations](https://alloytools.discourse.group/t/implicit-facts-with-multirelations/548)
**Author:** [@MathewKJ2048](https://alloytools.discourse.group/u/MathewKJ2048)\ **Replies:** 0\ **Last updated:** [February 25, 2026, 1:14pm UTC](https://alloytools.discourse.group/t/implicit-facts-with-multirelations/548 "2026-02-25T13:14:52Z")
Hi, I have a question about the associativity of the arrow operator when generating implicit facts associated with multi-relations: sig A {} sig B {} sig C {} sig X { f : one A } sig Y { g : A -\> B -\> C } When creating… --- ## [Date Constrained To Only Month and Year](https://alloytools.discourse.group/t/date-constrained-to-only-month-and-year/545)
**Author:** [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\ **Replies:** 3\ **Last updated:** [February 6, 2026, 3:31pm UTC](https://alloytools.discourse.group/t/date-constrained-to-only-month-and-year/545 "2026-02-06T15:31:06Z")
I’m working on creating a model for a set of anthology books. The anthologies themselves reprint back issues of comic books. I want to be able to record the month and year of the comic book being reprinted. The day is… --- ## [Why did Alloy Analyzer stop supporting the exh and part keywords?](https://alloytools.discourse.group/t/why-did-alloy-analyzer-stop-supporting-the-exh-and-part-keywords/543)
**Author:** [@Rafa10](https://alloytools.discourse.group/u/Rafa10)\ **Replies:** 0\ **Last updated:** [December 29, 2025, 3:17am UTC](https://alloytools.discourse.group/t/why-did-alloy-analyzer-stop-supporting-the-exh-and-part-keywords/543 "2025-12-29T03:17:13Z")
/\*\* \* Generate an error message saying the given keyword is no longer supported. \*/ static ErrorSyntax hint(Pos pos, String name) { String msg = "The name \\"" + name + "\\" cannot be found."; if ("exh".equals(na… --- ## [How to model transactions?](https://alloytools.discourse.group/t/how-to-model-transactions/540)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [October 27, 2025, 1:26pm UTC](https://alloytools.discourse.group/t/how-to-model-transactions/540 "2025-10-27T13:26:35Z")
Hello. I’m reading the Designing Data-Intensive Applications book by Martin Kleppmann, there’s a chapter on transaction isolation levels, and I wonder: are there any examples how transactions could be modeled? Actually,… --- ## [Can Alloy help with normal forms?](https://alloytools.discourse.group/t/can-alloy-help-with-normal-forms/529)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [March 30, 2025, 8:37pm UTC](https://alloytools.discourse.group/t/can-alloy-help-with-normal-forms/529 "2025-03-30T20:37:14Z")
I’ve read a couple of blog posts on designing and changing database schemas: Now, after making a draft of schema, can Alloy help with normal forms? Forgive my ignorance, I took a database course a long time ago. As… --- ## [A couple of questions after reading "Formally specifying UIs"](https://alloytools.discourse.group/t/a-couple-of-questions-after-reading-formally-specifying-uis/520)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 8\ **Last updated:** [March 18, 2025, 4:53pm UTC](https://alloytools.discourse.group/t/a-couple-of-questions-after-reading-formally-specifying-uis/520 "2025-03-18T16:53:40Z")
Here’s a fantastic article: Formally Specifying UIs A couple of questions: There’s a quote: There’s also some properties we can’t easily verify in Alloy, such as finding deadlocks. What are the deadlocks in the co… --- ## [When to use util/ordering instead of temporal logic?](https://alloytools.discourse.group/t/when-to-use-util-ordering-instead-of-temporal-logic/521)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [March 17, 2025, 3:38pm UTC](https://alloytools.discourse.group/t/when-to-use-util-ordering-instead-of-temporal-logic/521 "2025-03-17T15:38:12Z")
Are there problems when util/ordering is a better fit than temporal logic? Asking this question after finding the following topic: And this blog post, where util/ordering is used: --- ## [Alloy for software testing?](https://alloytools.discourse.group/t/alloy-for-software-testing/519)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 6\ **Last updated:** [March 13, 2025, 10:46am UTC](https://alloytools.discourse.group/t/alloy-for-software-testing/519 "2025-03-13T10:46:35Z")
When I search for “small scope hypothesis”, I find something along the lines of “a high proportion of errors can be found by testing a program for all test inputs within some small scope”. So, the question: is Alloy use… --- ## [Is it possible to have multiple inheritance?](https://alloytools.discourse.group/t/is-it-possible-to-have-multiple-inheritance/518)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [March 12, 2025, 9:09pm UTC](https://alloytools.discourse.group/t/is-it-possible-to-have-multiple-inheritance/518 "2025-03-12T21:09:25Z")
This may be a stupid question, but for the sake of completeness: can something like this be expressed? sig C extends A, B {} I’m not sure yet if this even can be useful at all, I’m just exploring alloy. --- ## [Dot join for navigating backwards](https://alloytools.discourse.group/t/dot-join-for-navigating-backwards/512)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 5\ **Last updated:** [March 7, 2025, 9:33am UTC](https://alloytools.discourse.group/t/dot-join-for-navigating-backwards/512 "2025-03-07T09:33:59Z")
Hello. I’m confused about the following from the Practical Alloy book: Relations can be navigated forwards, from the source signature to the target signature, but also backwards from the target signature to the source … --- ## [Larger scope to make sure?](https://alloytools.discourse.group/t/larger-scope-to-make-sure/516)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [February 26, 2025, 3:34pm UTC](https://alloytools.discourse.group/t/larger-scope-to-make-sure/516 "2025-02-26T15:34:37Z")
I’m looking into it too early in learning alloy, probably, but I’m curious, what scope do alloy practitioners usually use. I’ve found the following in an old paper: The dirty work of finding solutions (or looking for c… --- ## [Going back to previous solutions?](https://alloytools.discourse.group/t/going-back-to-previous-solutions/515)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [February 26, 2025, 11:56am UTC](https://alloytools.discourse.group/t/going-back-to-previous-solutions/515 "2025-02-26T11:56:13Z")
When I press the Execute button, I get a solution, and the New button generates next ones one by one. Now, I have a couple of questions. Is it possible to go to the previous solutions using the GUI? It seems currently … --- ## [Is the dot operator only left-associative, not just associative?](https://alloytools.discourse.group/t/is-the-dot-operator-only-left-associative-not-just-associative/513)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 6\ **Last updated:** [February 26, 2025, 6:32am UTC](https://alloytools.discourse.group/t/is-the-dot-operator-only-left-associative-not-just-associative/513 "2025-02-26T06:32:23Z")
From the alloy spec: All binary operators associate to the left, with the exception of implication and sequence, which associate to the right, and of binary temporal connectives which are not associative. Is the dot … --- ## [Why are only top-level, argumentless functions reified in the visualizer?](https://alloytools.discourse.group/t/why-are-only-top-level-argumentless-functions-reified-in-the-visualizer/507)
**Author:** [@dkasak](https://alloytools.discourse.group/u/dkasak)\ **Replies:** 2\ **Last updated:** [January 9, 2025, 4:46pm UTC](https://alloytools.discourse.group/t/why-are-only-top-level-argumentless-functions-reified-in-the-visualizer/507 "2025-01-09T16:46:01Z")
Is there a particular reason why only “top-level” funs without arguments are reified in the visualizer, but not those which either have an argument or are defined on a sig? For example, given the following spec: sig Fo… --- ## [My tree is ill… unless I point at it](https://alloytools.discourse.group/t/my-tree-is-ill-unless-i-point-at-it/502)
**Author:** [@kindaro](https://alloytools.discourse.group/u/kindaro)\ **Replies:** 7\ **Last updated:** [December 5, 2024, 8:09am UTC](https://alloytools.discourse.group/t/my-tree-is-ill-unless-i-point-at-it/502 "2024-12-05T08:09:19Z")
I wanted to solve the exercise A.1.5 from the book Software Abstractions. The task is to define a model which instances are exactly trees. I specifically chose to define directed trees. I also added a relation that lets… --- ## [Why does the name of a signature impact the number of variables?](https://alloytools.discourse.group/t/why-does-the-name-of-a-signature-impact-the-number-of-variables/496)
**Author:** [@mfamelis](https://alloytools.discourse.group/u/mfamelis)\ **Replies:** 2\ **Last updated:** [November 20, 2024, 8:27pm UTC](https://alloytools.discourse.group/t/why-does-the-name-of-a-signature-impact-the-number-of-variables/496 "2024-11-20T20:27:29Z")
I was looking at StackOverflow for unanswered Alloy questions, and stumbled on this one, from 7 years ago. They give this example: sig E {} sig G {} sig D extends G { x: E } sig F1 extends G { x: G } sig F2 extends… --- ## [How to create a new instance of a variable signature](https://alloytools.discourse.group/t/how-to-create-a-new-instance-of-a-variable-signature/297)
**Author:** [@tim.kraeuter](https://alloytools.discourse.group/u/tim.kraeuter)\ **Replies:** 4\ **Last updated:** [October 31, 2024, 10:39am UTC](https://alloytools.discourse.group/t/how-to-create-a-new-instance-of-a-variable-signature/297 "2024-10-31T10:39:33Z")
I want to create a new instance of a variable signature. For example, I want to spawn a subprocess as in the following model: var sig Process { var subprocess : lone Process } pred spawnSubprocessInstance(p:Process) {… --- ## [What models to start learning with?](https://alloytools.discourse.group/t/what-models-to-start-learning-with/494)
**Author:** [@Filipp](https://alloytools.discourse.group/u/Filipp)\ **Replies:** 1\ **Last updated:** [October 24, 2024, 2:00pm UTC](https://alloytools.discourse.group/t/what-models-to-start-learning-with/494 "2024-10-24T14:00:06Z")
Good afternoon! I am learning mostly hands-on, and I would like to create my own models as I learn, not just the ones in the book. Could you please suggest me what can be modeled: simple and understandable, so that I c… --- ## [Alloy gui broken on asahi fedora](https://alloytools.discourse.group/t/alloy-gui-broken-on-asahi-fedora/487)
**Author:** [@nlu](https://alloytools.discourse.group/u/nlu)\ **Replies:** 2\ **Last updated:** [October 9, 2024, 1:58pm UTC](https://alloytools.discourse.group/t/alloy-gui-broken-on-asahi-fedora/487 "2024-10-09T13:58:18Z")
Hi. I wish to use Alloy, but its gui is shucked. Text is blurry, menu bar doesn’t work. This is how it looks like: Macbook M1 Pro Fedora Linux Asahi Remix 40 sway wm (wayland) Runs ok on MacOS, but I do my dev wo… [Next page](https://alloytools.discourse.group/c/questions/9.md?page=1)