CODEWITHSUNDEEP
alloy
Simon
Simon

Reputation: 85

Default Run Command in Alloy5: what's the equivalent in Alloy4?

I'm working on a project exam and having trouble to understand what is the equivalent of the default Run command in Alloy5 when I switch to Alloy4.

As you all can see, if I write a model in Alloy5, but not a command (no check no run), if I click 'Execute', it executes the following command: "Run Default for 4 but 4 int, 4 seq expect 1" Which satisfies the mission of my project: check if a described model has instances. No need to check properties or something else. Just if there are instances.

In Alloy4, if I click 'Execute', it tells me "No commands defined", so there is not a predefined run command.

My question is: what is the equivalent of that Allloy5-Default-Run-Command in Alloy4?

I'm going crazy since I have to work on Alloy4 API (on Java) and can't figure out how to solve this problem (because isSolvable() doesn't work if I don't put a command in the model).

Upvotes: 0

Views: 115

Answers (1)

Peter Kriens
Peter Kriens

Reputation: 15372

The following should work:

 run {} for 4

Upvotes: 1

Related Questions