Added a run command

[pkriens]

Added a run command to the evaluator. Without parameters it shows the existing commands.

Also printout the skolems with the -s option

Need some feedback how to navigate the new configuration etc. space. Never really understood what we were doing there exactly. If you design the commands and tell me what to call then I can add them

[grayswandyr]

Thanks.

• I don't really get how this works. IIUC, I should add -e to the commandline? But wouldn't it be more user-friendly if launching this shell could be disconnected from exec? I.e add a shell directive. And then allow to run an /exec command from the shell.
• /state is a a goto state?
• what does /continue correspond to? New config, New trace...?

What we call a configuration is one full valuation of static sigs and fields., up to symmetry. Other New ... commands do not change the configuration, just the valuation of var sigs and fields (in a given configuration). So if you click New ... repeatedly, you may exhaust all traces for the current configuration, but there may be others in other configurations (until you also exhaust all traces in all other configurations).

What would be really useful isn't necessarily linked to the shell: on the command line, even, I'd love to be able to issue a --all option to exec to get back all possible instances for a command (in a directory or in a file up to your convenience).

[pkriens]

It is in a state that makes it very easy to add significant functionality. (The shell is really awesome to add functions, like the native code commands, that take way less them than a GUI function. Even with ChatGPT.)

If you could spare an hour or so we could play with it over zoom. My usage of Alloy is pretty limited and it is not always clear to me what would work well for hard core users. In this session we could add the commands & help texts interactively.

The multiple outputs of the exec command have me struggling. In principle, we have file -> solver -> command. Currently, when multiple commands are specified I am aggregating the output in one file. However, the idea to store each output in a directory is probably better but then I need a naming scheme for the output files. (And I lose the advantage of having a single output file.) The JSON solution allows for any combination, it is now a list of instances.

The easy solution is just to add all options but I am not fond of that. It gets very messy and you tend to have lots of options that are incompatible.

I will add the shell command again.

Anyway, need some detailed help here.

[grayswandyr]

To me, the biggest added value of the shell is for people who can't use the GUI for some reason.

OTOH I think getting all instances for a command, non-interactively, is really useful because this is not something for which you have an alternative, even in the GUI as -there- you must click and click again until exhaustion. This adds to Alloy something that you must usually do at the programmatic level, in Kodkod/Pardinus. As to whether it's better to use a single file or a directory, I think the decision can be made based on what's the simplest for you, once again we don't need too much sophistication (a directory nicely separates instances, but a single file would make it easier to add metadata relative to the whole generation operation, as full time, etc.). What you did here is already great and helpful, so if you think you can allocate a bit more time to development, perhaps it'd be better to address other issues (e.g. we desperately lack a Replace command in the editor #198)

[pkriens]

As I said, the shell is in a phase that it is 2 mins to add some functionality. Mucking around in the GUI, especially in Alloy, is always costing 10x the time I estimate :-( But I can take a look.

[grayswandyr]

Forget it then. My point was that we already have a great feature with the new CLI and if we can gather all instances for a command with a single command-line option. The rest is icing on the cake.

[grayswandyr]

I'm not sure the change comes from this work exactly, but nuXmv isn't listed as a possibility in my build:

~/REPOS/org.alloytools.alloy (feature/cli2 ✘)✹✭ ᐅ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar solvers -l
MiniSat
Lingeling
Glucose
Glucose41
CryptoMiniSat
ZChaffMincost
SAT4J
Electrod/NuSMV
Output CNF to file
Output Kodkod to file

[pkriens]

can you show the output of natives?

[grayswandyr]

~/REPOS/org.alloytools.alloy (feature/cli2 ✘)✹✭ ᐅ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar natives   
┌───────────────────────┬───────────────────┬───────────────────┬──────────────────────┬─────────────────┬───────────┐
│                       │Linux/amd64        │Linux/x86          │MacOS Intel           │Windows/x86      │MacOS Apple│
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│MiniSat                │libminisat.so      │libminisat.so      │libminisat.dylib      │minisat.dll      │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│MiniSatX1              │                   │libminisatx1.so    │                      │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│MiniSat with Unsat Core│libminisatprover.so│libminisatprover.so│libminisatprover.dylib│minisatprover.dll│           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Lingeling              │liblingeling.so    │liblingeling.so    │liblingeling.dylib    │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Glucose                │libglucose.so      │libglucose.so      │libglucose.dylib      │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Glucose41              │libglucose41.so    │                   │libglucose41.dylib    │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│CryptoMiniSat          │libcryptominisat.so│libcryptominisat.so│                      │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│ZChaffMincost          │libzchaffmincost.so│                   │                      │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│SAT4J                  │                   │                   │                      │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Electrod/NuSMV         │electrod           │                   │electrod              │electrod.exe     │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Electrod/nuXmv         │electrod           │                   │electrod              │electrod.exe     │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Output CNF to file     │                   │                   │                      │                 │           │
├───────────────────────┼───────────────────┼───────────────────┼──────────────────────┼─────────────────┼───────────┤
│Output Kodkod to file  │                   │                   │                      │                 │           │
└───────────────────────┴───────────────────┴───────────────────┴──────────────────────┴─────────────────┴───────────┘

[pkriens]

See the last commit, misspelled the nuXmv exe

[grayswandyr]

That was it, thanks.

[pkriens]

@grayswandyr could you approve the request? I want to close this and it is pretty small and I am getting confused with the different PRs outstanding ...

[grayswandyr]

What is the preferred policy? Squash and merge or rebase and merge?

[pkriens]

Just do a review ok and then I can merge.

[grayswandyr]

One last question: it's not clear to me whether you have implemented an option for exec to yield all instances (incl. Skolems) for a command? Without going through the evaluator (-e).

[pkriens]

Do not specify -c will iterate over all commands. The skolems should be in there.

But before we continue, I really need to get a single branch again. It is getting too messy for me so I need it all on master.

[grayswandyr]

Not all commands, all instances for one command (e.g. all instances for a run, or all counter-examples for a check).