search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
711 stars 123 forks source link

A command line #214

Closed pkriens closed 1 year ago

pkriens commented 1 year ago
grayswandyr commented 1 year ago

Thanks it looks great! A few comments:

pkriens commented 1 year ago

On 14 Jun 2023, at 11:21, grayswandyr @.***> wrote:Thanks it looks great! A few comments:

the help message could more informative about possible commands When you do help or an unknown command you get natives - Show all the native solvers for all supported platforms prefs - Show the preferences or modify them solvers - Show the list of solvers version - Display the current version

gui - Opens up the Graphic User Interface of Alloy

exec - Execute an Alloy program

lsp - Language Server for Alloy.

Error

  1. no such command pfssf

"executing" a file doesn't print which commands are being run I added a --quiet option and print the command to the console when not quiet while executing, this symbol was displayed, no idea what it means: ☒ Need more info for that

exec -c doesn't seem to accept command numbers, to execute the i-th command, so I don't know how to execute unnamed commands (in the end I found with json output) I've extended it to accept an integer. options do not all say what is the default done

Electrod/nuXmv isn't detected on my machine (NuSMV is) by solvers (but shown by natives) The native code is a mess ... need Nuno to work this out. And I cannot really test anything since I am on an M1 chip and we do not support that yet.

why is -1 the default number of unrolls rather than 0? made it zero

it would be nice to output the full time (in ms) taken by a command, in the json output Done, added to the table output & json

it's a bit a strange that -p must appear before exec Yes, I removed this. I want all the options on the command line for the exec command. Need help which ones are still relevant. It would also nice to be able to define these options in the code since in several cases the model depends on the options. Which means they are not an option. We could easily allow --nooverflow = true etc. in the code.

Problem is that the preferences are hard tied to the Swing UI. Not sure how this will work when you run it in a shell, it seems to want to open a window temporarily.

If you could make a list of options I can add them

SatSolver2 is a strange name for an option Where do you see this?

I seem to remember it was also possible to launch an "interpreter" but I can't find it I removed it. It needed a lot of documentation work and I am spending too much time on this. There was also no feedback on it so I decided to can it. If you really want it I can put it back but it should be marked as experimental.

Kind regards,

Peter Kriens

—

Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/pull/214#issuecomment-1590823407, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABQ6LV4HBZETEB5YAGBCLDXLF677ANCNFSM6AAAAAAZE6VDUA. You are receiving this because you authored the thread.

pkriens commented 1 year ago

Key aspect is the native code but I need @nmacedo to resolve these issues

grayswandyr commented 1 year ago
  1. Very useful: would it be possible to ask to return all instances for a command (as if you typed on Next trace until exhaustion)?
  2. Less important: would it be possible to have an option to list all available commands with their names?