Unable to get simple example to produce a trace

Questions
1

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
		Stutter
	)
}

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:

trace0
trace0908×422 18.1 KB

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):

---INSTANCE---
loop=0
end=0
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}
String={}
none={}
this/Bookmark={Bookmark$0, Bookmark$1}
this/LocalStore={LocalStore$0}
this/LocalStore<:bookmarksStored={LocalStore$0->Bookmark$1}
this/LocalStore<:bookmarksStoring={}

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:

Enumerating...

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

An error has occurred!

Or even just:

Enumerating:

java.util.NoSuchElementException

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
6.1.0.202111031525
2

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.

E.g.

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

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

Hi,

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
}

Best,
Alcino

4

Hello good folk,
I am I think on the same kind of path as the original poster here, trying to understand enough to produce simple protocol models (inspired by the “Protocol Design with Alloy” chapter of the online Formal Software Design with Alloy 6). This question was delightful in that regard, an example, and advice about it, and travelling that same path I think I can learn more. The “don’t get traces I expect” is something I’m struggling with.

With built-from-github-this-month Alloy 6.1.0 with SAT4J and no setting changes I’m aware of, and trying to incorporate the advice from the respondents into the original model, and trying to follow the intent of the original mode, I have this now:

sig Bookmark {}

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

fact {
	some Bookmark
	no bookmarksStoring

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

pred LocalSaveInitiate[b : Bookmark] {
	-- no guard here intentionally in the original

	bookmarksStoring' = bookmarksStoring + (LocalStore -> b)
	bookmarksStored' = bookmarksStored
}

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

	bookmarksStoring' = bookmarksStoring - (LocalStore -> b)
	bookmarksStored' = bookmarksStored + (LocalStore -> b)
}

pred Stutter {
	bookmarksStored' = bookmarksStored
	bookmarksStoring' = bookmarksStoring
}

run { } for 4

I am expecting traces that are longer than 1 step, because of the always with the three branches in the anonymous fact. I only get traces with 1 step, even if there are some Bookmark not yet storing or stored.

I am missing something, I’d appreciate any advice, of what small or large basic issue I’m not getting yet here.

cheers,
Nigel

5

Hi,

By default you get the smallest trace possible in empty run commands. Since we have stuttering, the smallest trace can be represented with one single state that loops forever. To see different traces you should use the New buttons: for example, if you keep pressing New Trace you should see some traces with more than one state.
Best,
Alcino

6

Ugh, okay. Thank you. I was using New Config, but now I do see more things. Thank you.
cheers,
Nigel