Unable to get simple example to produce a trace

I’m currently two days into Alloy, and am unable to get what appear to be trivial examples to do what they apparently should. I’m starting to be concerned that the 6.1.0 version is actually broken on my system as I occasionally see exceptions on the console.

I have, once again, a mindlessly trivial model of a bookmark store. Given a single bookmark store and a set of bookmarks, it’s possible to try to attempt to store a bookmark. This can either succeed or fail, but currently it can only succeed, in a desperate attempt to get the analyzer to show a sensible trace:

sig Bookmark {}

one sig LocalStore {
	bookmarksStored  : set Bookmark,
	bookmarksStoring : set Bookmark

fact {
	// Initially, no bookmarks are in the process of being stored,
    // but there can be any number of bookmarks that are already stored.
	no LocalStore.bookmarksStoring

	always (
		(some b : Bookmark | LocalSaveInitiate[b]) or
		(some b : Bookmark | LocalSaveSuccess[b]) or

pred LocalSaveInitiate[b : Bookmark] {
	after LocalStore.bookmarksStoring' = LocalStore.bookmarksStoring + b and
		  LocalStore.bookmarksStored' = LocalStore.bookmarksStored

pred LocalSaveSuccess[b : Bookmark] {
	b in LocalStore.bookmarksStoring

	after LocalStore.bookmarksStoring' = LocalStore.bookmarksStoring - b and
		LocalStore.bookmarksStored' = LocalStore.bookmarksStored + b

pred Stutter {
	LocalStore' = LocalStore

run { } for 3 but 1 LocalStore

My reasoning about this is:

  • The anonymous fact states that at any given step, one of LocalSaveInitiate, LocalSaveSuccess or Stutter must be true. Stutter is evidently required, because without it, the other predicates will lead to a finite execution trace and so the analyzer will reject the model.
  • Assuming the existence of a LocalStore and Bookmark, LocalSaveInitiate will always be true as there’s no “guard” on the predicate.
  • Assuming that LocalSaveInitiate is true, then LocalSaveSuccess will be true because the only guard condition is that there’s a bookmark in the bookmarksStoring set.
  • Assuming there are no more bookmarks, only Stutter will be true, and so the execution trace is effectively infinite.

What I actually see is this:

That’s OK, that was presumably a case where the only and only initial bookmark was already stored.

Clicking “New config”, however, leads me to (had to replace this image with text due to forum limits):

integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7, Bookmark$0, Bookmark$1, LocalStore$0}
Int={-1, -2, -3, -4, -5, -6, -7, -8, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2}
this/Bookmark={Bookmark$0, Bookmark$1}

All of the “New Trace” “New Init” and “New Fork” buttons state “There are no more satisfying instances.”. Trying to evaluate LocalSaveInitiate[Bookmark$0] in the evaluator returns false.

For every single instance, the visualization window shows 0 -> 0^. There appear to be no traces where a bookmark can be shown to pass through the LocalSaveInitiate or
LocalSaveSuccess transitions. In fact, if I add no LocalStore.bookmarksStoring to the fact to exclude any possibility of initially stored books, there are no states whatsoever where bookmarksStored is non-empty.

Occasionally, on the console, I see:


java.lang.IllegalArgumentException: Cannot iterate boundless after segment iteration, breaks completeness.

An error has occurred!

Or even just:



An error has occurred!

This is the seventh rewrite of this utterly trivial example, and I’ve never been able to get results that look even remotely similar to any book examples.

Am I misunderstanding something fundamental, or is Alloy broken on my system?

For reference:

$ uname -a
Linux workstation01 6.4.8-arch1-1 #1 SMP PREEMPT_DYNAMIC Thu, 03 Aug 2023 16:02:01 +0000 x86_64 GNU/Linux

$ java -version
openjdk version "17.0.8" 2023-07-18
OpenJDK Runtime Environment (build 17.0.8+7)
OpenJDK 64-Bit Server VM (build 17.0.8+7, mixed mode)

$ alloy --version

I did not look at the model (no time) but I noticed you make the mistake to think always has lower priority than and. In almost all cases, the expression after always must be in parenthesis.


after LocalStore.bookmarksStoring' = LocalStore.bookmarksStoring - b and
		LocalStore.bookmarksStored' = LocalStore.bookmarksStored + b

after ( LocalStore.bookmarksStoring' = LocalStore.bookmarksStoring - b and
		LocalStore.bookmarksStored' = LocalStore.bookmarksStored + b )


You forgot to declare fields bookmarksStored and bookmarksStoring as mutable (with the var keyword)!

And a couple more issues: 1) in the specification of the events you don’t need the after temporal operator - the prime applies to a field already evaluates its value in the next state, so a constraint like LocalStore.bookmarksStoring' = LocalStore.bookmarksStoring + b already states that, in the next state, the field LocalStore.bookmarksStoring will have an additional bookmark; 2) in the Stutter event you need to constraint all mutable sets and fields to remain equal - in this case, after you add the var in the declarations, those will be bookmarksStored and bookmarksStoring, so the stuttering event should be

pred Stutter {
  bookmarksStored' = bookmarksStored
  bookmarksStoring' = bookmarksStoring