How to get split view in Visualizer like in the book?

Tooling
1

Versions: macOS Sonoma 14.6.1, VSCode 1.93.1, Alloy 0.7.1, Zulu Java 22
CPU: Apple M1 (ARM64)

The Visualizer does not show a split view of two consecutive states like shown in the book here:

image
image2238Ă—1198 211 KB

Instead I can only see one state at a time. I cannot find any configuration related to this feature either.

2

You must have at least one varsignature or field in your model and use Alloy 6+. Is it the case?

3

I do have var signatures, and I do see the top bar showing the states, as well as buttons “New Config”, “New Trace”, “New Init”, “New Fork”. I can explore the states just fine. I just only have a single panel showing the current state, without side-by-side panels showing previous and current state.

4

Please share the exact model, as well as the Alloy version number shown on the right when you launch the tool.

5

There is no Alloy version number shown “on the right” since I am using the VSCode extension.

OK I have found how to launch the Alloy Analyzer from the extension, I need to run the command Alloy: Open Alloy Editor. On the right it is shown:

Alloy Analyzer [what is new] [spec] built 2021-11-19T05:45:51.188Z

From the “About Alloy…” pop up:

About Alloy Analyzer 6.1.0.202111190545

Build Date: 2021-11-19T05:45:51.188Z
Git Commit: d597bc141c2b7347097f500844baf9d37bd5a0d9

Any model with var shows the issue for me, so here is a minimal one:

open util/ordering[Id]

sig Node {
  succ : one Node,
  id : one Id,
  var inbox : set Id,
  var outbox : set Id
}

sig Id {}

var sig Elected in Node {}

run {}

Thanks to you prompting me to discover the Java UI of the Alloy Analyzer (open from VSCode by command Alloy: Open Alloy Editor), I have found that executing and opening an instance from the Java UI does show a split view, but opening an instance from VSCode only shows a single state without split view.

6

Sorry I hadn’t seen the first post where there was a reference to VS Code. The VS Code plugin is a (nice) contribution external to the official Alloy release and, as far as I know, it ships a modified version of Alloy. In case of unexpected behavior, I would suggest to rely on the official release of Alloy, which you can get at https://alloytools.org .

7

Thanks for your reply. The VSCode extension page lists its repo, which indeed is a fork of Alloy.

In fact someone has written a PR for this problem: Show both state panes in the VizGUI by jemc · Pull Request #2 · s-arash/org.alloytools.alloy · GitHub

Unfortunately the PR has not been merged for 2 years. I wonder what can be done here…

8

An LSP server should be present in the forthcoming of Alloy but I don’t know whether it solves the issue. In any case, a second step will be to update the VS Code extension so that it reaches the official version of Alloy rather than a fork shipped with the extension.

Meanwhile, you can still rely on VS Code to edit models. Open your model both in VS Code and Alloy Analyzer. Edit only in VS Code. When you’re done editing, save your model in VS Code. Then switch to the official Alloy Analyzer and hit Ctrl-R (“reload”), which reloads the edited file in Alloy Analyzer. Then run commands from AA. Granted, this isn’t frictionless but still manageable in my opinion.

1 Like
9

Silly me, I have only now noticed that the snapshot builds are published not to Github but to Index of /repositories/snapshots/org/alloytools

Since the double pane change is in the jar, I just replaced the jar from the extension with a recent mainline snapshot, and voila I can open the double pane viz from VSCode!

I am going to turn off Auto-update for this extension for now just in case.

To find “the jar from the extension”:

  1. Execute “Extensions: Open Extensions Folder” command in VSCode, it should open the extensions folder in Finder/Explorer/what-have-you
  2. Find the folder “arashsahebolamri.alloy-0.7.1” in the extensions folder (0.7.1 is the version of Alloy extension installed at time of writing)
  3. Replace “org.alloytools.alloy.dist.jar” with a snapshot from the sonatype repository
1 Like
10

It seems to me the current VSCode hasn’t been extended in a while and I’m not sure its author is stilla active. In that case, would you be able to help in devising an updated extension, perhaps under the auspices of alloytools.org? The extension would not ship the Analyzer but rather have a setting for the user to point to the Analyzer JAR installed on the system.

11

I can start working towards that, sure.

1 Like