Not understanding the visualization for mutable sets

1

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

sig Bookmark {}

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

fact Init {
	all s : LocalStore | no s.bookmarksStored
	all s : LocalStore | no s.bookmarksStoring

	always (
		some b : Bookmark, s : LocalStore | LocalSaveInitiate[b, s]
	)
}

pred LocalSaveInitiate[b : Bookmark, s : LocalStore] {
	b not in s.bookmarksStoring
	b not in s.bookmarksStored

	s'.bookmarksStored = s.bookmarksStored
	after (s'.bookmarksStoring = s.bookmarksStoring + b)
}

assert NoStored {
	all s : LocalStore | no s.bookmarksStored
}

check NoStored

run { }

This seems pretty straightforward. There are mutable local stores, and they should (according to Init) start out empty.

There’s one possible transition, currently, LocalSaveInitiate that places a bookmark into the bookmarksStoring set, and leaves the bookmarksStored set untouched.

The NoStored assertion shows that there are no local stores that ever have a non-empty bookmarksStored set, but the visualization shows:

stored
stored1150×520 29 KB

Why does the visualization seem to show a non-empty bookmarksStored set?

2

Hi,

The effect of the LocalSaveInitiate event is not correctly specified. You are using the prime on the LocalStore but that is not what you want to change in the next state. You should use the prime on the relations bookmarksStored and bookmarksStoring. Something like:

pred LocalSaveInitiate[b : Bookmark, s : LocalStore] {
	b not in s.bookmarksStoring
	b not in s.bookmarksStored

	s.bookmarksStored' = s.bookmarksStored
	s.bookmarksStoring' = s.bookmarksStoring + b
}

However, after this change you should also add a stuttering event, where nothing changes, to allow for infinite behaviours, since its not possible to keep adding bookmarks to the store.

A couple more comments about your model:

  • If there is always exactly one LocalStore do you really want to make it mutable? Or do you intend to allow multiple local stores later? If that is the case in the specification of LocalSaveInitiate you will also need to add frame conditions that keep the bookmarks of other stores unchanged.
  • In the assertion NoStore I believe you are missing an always temporal operator. Without that operator you are only checking that in the initial state all local stores have no bookmarks stored.

Best,
Alcino

1 Like
3

Thanks for the reply.

Adding the stutter appears to do nothing, but I’ve abandoned this formulation and am trying other things instead. I’ll start a separate thread on the new issues I’m running into as they’re not related to this.

If there is always exactly one LocalStore do you really want to make it mutable?

There is always exactly one LocalStore, but I don’t know if I want to make it mutable. I thought I had to make it mutable as there’s essentially no documentation
for Alloy 6, the older documentation is incompatible, and I’m following the Haslab Formal Software Design guide. The very first bit of Alloy code in that guide uses the var keyword.

In the assertion NoStore I believe you are missing an always temporal operator.

Makes sense. Thanks!