# Latest **URL:** https://alloytools.discourse.group/latest.md?page=3 [Latest](https://alloytools.discourse.group/latest.md) · [Categories](https://alloytools.discourse.group/categories.md) **Page:** 4 --- ## [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… --- ## [LinkedList module for temporal logic](https://alloytools.discourse.group/t/linkedlist-module-for-temporal-logic/393)
**Author:** [@MATIX](https://alloytools.discourse.group/u/MATIX)\ **Replies:** 1\ **Last updated:** [September 4, 2023, 8:12am UTC](https://alloytools.discourse.group/t/linkedlist-module-for-temporal-logic/393 "2023-09-04T08:12:41Z")
Hi everyone, I would like to share a linked list implementation for temporal logic with you. Maybe someone can use it for himself, develop it further or improve it. It supports basic list functions. The number of chec… --- ## [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… --- ## [Topological Sort: A stepwise implementation](https://alloytools.discourse.group/t/topological-sort-a-stepwise-implementation/395)
**Author:** [@MATIX](https://alloytools.discourse.group/u/MATIX)\ **Replies:** 0\ **Last updated:** [August 21, 2023, 4:13pm UTC](https://alloytools.discourse.group/t/topological-sort-a-stepwise-implementation/395 "2023-08-21T16:13:28Z")
Hi everyone, I would like to share my solution for implementing topological sorting of a graph in Alloy. Any suggestions would be appreciated. I am using my LinkedList implementation that you can check out here. --- ## [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? --- ## [Specify a predicate being true for n steps](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388)
**Author:** [@ale](https://alloytools.discourse.group/u/ale)\ **Replies:** 3\ **Last updated:** [August 18, 2023, 2:21pm UTC](https://alloytools.discourse.group/t/specify-a-predicate-being-true-for-n-steps/388 "2023-08-18T14:21:10Z")
Hi all, I have to model something, and though I have some ideas to do it, maybe someone knows a better way to do it. Lets say I have the predicate P and I want to specify: P is true in the following (the actual include… --- ## [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… --- ## [New to Alloy - discussions and questions](https://alloytools.discourse.group/t/new-to-alloy-discussions-and-questions/382)
**Author:** [@ale](https://alloytools.discourse.group/u/ale)\ **Replies:** 7\ **Last updated:** [August 10, 2023, 1:32pm UTC](https://alloytools.discourse.group/t/new-to-alloy-discussions-and-questions/382 "2023-08-10T13:32:51Z")
Hi everyone! I’m new at Alloy and I am using it and I will going to use it to try to achieve a transpiler from a particular existing specification language to Alloy and use the capabilities of Alloy on the models writte… --- ## [Modeling a key-value-store with snapshot isolation](https://alloytools.discourse.group/t/modeling-a-key-value-store-with-snapshot-isolation/374)
**Author:** [@TurtleTony](https://alloytools.discourse.group/u/TurtleTony)\ **Replies:** 8\ **Last updated:** [July 23, 2023, 4:44pm UTC](https://alloytools.discourse.group/t/modeling-a-key-value-store-with-snapshot-isolation/374 "2023-07-23T16:44:35Z")
Looking at the english wikipedia page of tla+ one may find an example specification of a key-value-store with snapshot isolation for concurrent transactions. I’ve uploaded an alloy model of this mechanism to the models … --- ## [Isn’t frame conditions quite fragile?](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376)
**Author:** [@judofyr](https://alloytools.discourse.group/u/judofyr)\ **Replies:** 5\ **Last updated:** [July 20, 2023, 12:48pm UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376 "2023-07-20T12:48:51Z")
Hey folks. I’ve been learning a bit Alloy with the intention of using the linear temporal logic checking. I’ve had some experience with rewriting systems (most notably, Maude) and I’m really enjoying Alloy so far. Howev… --- ## [Help with book example](https://alloytools.discourse.group/t/help-with-book-example/367)
**Author:** [@Adam](https://alloytools.discourse.group/u/Adam)\ **Replies:** 3\ **Last updated:** [June 23, 2023, 6:11am UTC](https://alloytools.discourse.group/t/help-with-book-example/367 "2023-06-23T06:11:42Z")
I was following along with the Software abstractions book and started to just try things and im wondering if anyone can tell me why its possible with my code to get an example of a name with no address? I thought the fac… --- ## [Checking a function](https://alloytools.discourse.group/t/checking-a-function/357)
**Author:** [@mputic100](https://alloytools.discourse.group/u/mputic100)\ **Replies:** 6\ **Last updated:** [June 20, 2023, 8:21am UTC](https://alloytools.discourse.group/t/checking-a-function/357 "2023-06-20T08:21:46Z")
I have the following simple model: -- SIGNATURES sig Device {} sig Account { var devices: set Device, } -- CONSTRAINTS // Initial conditions fact init { no devices // No devices, they will get added using ad… --- ## [How to check to see if a file has gone through same state](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361)
**Author:** [@Adam](https://alloytools.discourse.group/u/Adam)\ **Replies:** 3\ **Last updated:** [June 16, 2023, 2:53pm UTC](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361 "2023-06-16T14:53:40Z")
Hi, I am new to using Alloy 6 and just was following along with some simple Recycling bin examples on this website I found. Everything in the model is fine I just was wondering how to assert a case I thought of which is… --- ## [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… --- ## [Higher-order quantification could not be skolemized](https://alloytools.discourse.group/t/higher-order-quantification-could-not-be-skolemized/359)
**Author:** [@mputic100](https://alloytools.discourse.group/u/mputic100)\ **Replies:** 1\ **Last updated:** [June 14, 2023, 8:01pm UTC](https://alloytools.discourse.group/t/higher-order-quantification-could-not-be-skolemized/359 "2023-06-14T20:01:47Z")
Suppose we have the following simple model: sig User {} sig Group { users: set User } Is it possible to use Alloy to find a relation over users that isn’t explicitly defined in the model? For example: check { so… --- ## [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… --- ## [Problem in understanding mutable state in Alloy 6](https://alloytools.discourse.group/t/problem-in-understanding-mutable-state-in-alloy-6/268)
**Author:** [@JoshuaSchmidt](https://alloytools.discourse.group/u/JoshuaSchmidt)\ **Replies:** 11\ **Last updated:** [June 1, 2023, 2:13pm UTC](https://alloytools.discourse.group/t/problem-in-understanding-mutable-state-in-alloy-6/268 "2023-06-01T14:13:17Z")
Hi, I tried to model a puzzle in Alloy 6 to get familiar with the new notation of mutable states and temporal logic in Alloy 6. Usually, I use B and Event-B for modeling and ProB for animation and verification. The pu… --- ## [Unbounded Scope](https://alloytools.discourse.group/t/unbounded-scope/344)
**Author:** [@tobias.setnes](https://alloytools.discourse.group/u/tobias.setnes)\ **Replies:** 1\ **Last updated:** [May 28, 2023, 9:00am UTC](https://alloytools.discourse.group/t/unbounded-scope/344 "2023-05-28T09:00:11Z")
I’m working in Alloy 6, trying to implement a workflow language based on tokens moving around and being consumed/created. I’m trying to define a scope for my system, shown below. I was just wondering if it is possib… --- ## [Simple book examples don't work(?)](https://alloytools.discourse.group/t/simple-book-examples-dont-work/340)
**Author:** [@cabman](https://alloytools.discourse.group/u/cabman)\ **Replies:** 1\ **Last updated:** [May 3, 2023, 7:55pm UTC](https://alloytools.discourse.group/t/simple-book-examples-dont-work/340 "2023-05-03T19:55:19Z")
Am I missing something? What I expect for is: two instances of Book to be created (Book1, Book0) Book1 has all of the same Name → Addr mappings as Book0 Book1 additionally must also have a NEW mapping Name → Addr Wha… --- ## [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! … --- ## [Following the online book, and running into issues](https://alloytools.discourse.group/t/following-the-online-book-and-running-into-issues/333)
**Author:** [@alexshirley](https://alloytools.discourse.group/u/alexshirley)\ **Replies:** 1\ **Last updated:** [April 14, 2023, 8:31am UTC](https://alloytools.discourse.group/t/following-the-online-book-and-running-into-issues/333 "2023-04-14T08:31:59Z")
Hey All, I’m finally picking up Alloy again, and trying to work through the online book: Formal Software Design with Alloy 6 — Formal Software Design with Alloy 6 I tried run the following assertion, and was getting an… --- ## [Option to prevent overflows](https://alloytools.discourse.group/t/option-to-prevent-overflows/331)
**Author:** [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Replies:** 1\ **Last updated:** [April 13, 2023, 7:31am UTC](https://alloytools.discourse.group/t/option-to-prevent-overflows/331 "2023-04-13T07:31:28Z")
Since v4.2, Alloy features an option to prevent (arithmetic) overflows. I was wondering whether people use it always/sometimes/never and what is the justification for their choice? --- ## [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, … --- ## [Lack of Activity](https://alloytools.discourse.group/t/lack-of-activity/325)
**Author:** [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Replies:** 0\ **Last updated:** [March 17, 2023, 3:45pm UTC](https://alloytools.discourse.group/t/lack-of-activity/325 "2023-03-17T15:45:51Z")
This is a free site that we use. However, the currency they require is activity … So please if you have discussions about Alloy, do it on this site. Please? --- ## [Having events ordered in event reification](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321)
**Author:** [@ilkane](https://alloytools.discourse.group/u/ilkane)\ **Replies:** 3\ **Last updated:** [January 16, 2023, 3:45pm UTC](https://alloytools.discourse.group/t/having-events-ordered-in-event-reification/321 "2023-01-16T15:45:17Z")
Hi, I converted the Customer-Cards model of peter.kriens in here Can't get a model to change with time \[Electrum\] - #10 by peter.kriens to event reification style as below. enum Status { unissued, issued, cancelled } … --- ## [Kodkod provides different result from Alloy Analyzer](https://alloytools.discourse.group/t/kodkod-provides-different-result-from-alloy-analyzer/320)
**Author:** [@ilkane](https://alloytools.discourse.group/u/ilkane)\ **Replies:** 1\ **Last updated:** [January 13, 2023, 10:49am UTC](https://alloytools.discourse.group/t/kodkod-provides-different-result-from-alloy-analyzer/320 "2023-01-13T10:49:14Z")
Hi, I have a model checking confidentiality on the documents by level. I want the model starts with no documents, no accesses as below. In Alloy Analyzer the property takes hours to terminate (in fact it has not termin… --- ## [Looking for a simpler solution](https://alloytools.discourse.group/t/looking-for-a-simpler-solution/318)
**Author:** [@victor](https://alloytools.discourse.group/u/victor)\ **Replies:** 2\ **Last updated:** [December 31, 2022, 3:52pm UTC](https://alloytools.discourse.group/t/looking-for-a-simpler-solution/318 "2022-12-31T15:52:39Z")
I have this model below, wondering if there is a simpler solution to make sure people are in the company. sig Company {} sig Employee { company : Company } sig Manager { company : Company, team : set Employee } sig D… [Previous page](https://alloytools.discourse.group/latest.md?page=2) [Next page](https://alloytools.discourse.group/latest.md?page=4)