alloy

How to set up visualization of event-style models


I'm working through the book and trying examples in Alloy 6. For section 6.2.4 "An Event-Based Variation" I can't really understand the results. Specifically removing NoIntervening fact produces counterexample, but even a reduced scope is hard to follow. While trace style was quite easy to understand with simple time-projected visualization. Here are my version of the example ported to Alloy 6: https://gist.github.com/CheatEx/dc7ee7e8bd0750f350c5a270095c792e

The visualization looks totally different from the book. Neither time nor event projections make sense because diagrams are cluttered with either non-relevant events of non-relevant times.

enter image description here enter image description here

Is there a good way to tune visualizer to show the event-style models? Specifically to show only relevant events in time projection?

EDIT A screen with the accepted answer applied accepted


Solution

  • First you need to project on Time, to get a representation by instants. Then, the issue is that you still see all events. To keep only events happening in a given moment, you can change the theme to say that Events shouldn't be visible but that the set pre should be visible (meaning events whose firing instant is the current instant).

    I should add that this can be made completely clearer using the new features of Alloy 6 (there is no finished, printed book describing it yet but there are lecture notes here).