How to run a specific predicate in an Alloy command via the API?

Experimental
1

We add an Alloy predicate defn to a CompModule using the method addFunc() in file CompModule.java. We then use the method CompModule.addCommand() (the version that takes an ExprVar as an argument) to add a command that calls the predicate we created within the same CompModule.

For this command, we create an ExprVar with the same label/name as the predicate and pass it as an argument to the addCommand method.

We do not encounter any errors when we resolve the CompModule that contains this predicate and command.

However, we encounter an error when we try to execute the command using TranslateAlloyToKodkod.execute_command() .

When we use an ExprVar of Type.EMPTY for the predicate name to addCommand, and tried executing the command, we get a type error that this error was caused because the type of the variable is Type.EMPTY (thrown by line 136 of Class Expr).

If we try Type.FORMULA (and Type.INTANDFORMULA) for the ExprVar, we get the following error: Fatal Error: Variable “[pred name]” is not bound to a legal value during translation.

So, our question is: how can we create an Alloy run command to run a specific Alloy predicate using the existing functions in CompModule, Command, Expr, ExprVar or any other relevant classes?

2

The API around the AST and the module is … ehh … complicated.

The CompModule contains an addDefaultCommand() that will add a command when no other command is present. This added command works so you could start with that code and figure it out from there? You don’t have to add a predicate BTW. An expression would do.

Running Alloy in Eclipse with bndtools makes it very easy to single step through the code, modify the objects, and set breakpoints. If you do this, make sure to set -Ddebug=yes. Alloy will then not run the solver in another process.

If you can’t solve the problems, make repository on Github that I can try with your code.