Alloy: a compact Java program to perform different run command scopes

Question

Let say I am wanting to create a Java program to perform several Alloy runs, changing their scope values (integers from 0 to 9) for each loop, to check which is going to find a less time spent solution.

Have a note that the command is practically the same, I mean, only the values of the scope (and the presence/absence of the reserved word “exactly”) will vary.

Here is an numeric example:

1st run → command: run MyPred for 3 but 5 Int, exactly 1 Sig_Scope1, 1 Sig_Scope2, exactly 1 Sig_Scope3
2nd run → command: run MyPred for 4 but 5 Int, 2 Sig_Scope1, exactly 2 Sig_Scope2, exactly 2 Sig_Scope3
3rd run → command: run MyPred for 4 but 5 Int, 2 Sig_Scope1, exactly 1 Sig_Scope2, 1 Sig_Scope3

And so on, until a max number of iterations (suppose 10) has reached.

10th run → command: run MyPred for 4 but 5 Int, 0 Sig_Scope1, exactly 2 Sig_Scope2, 0 Sig_Scope3

A program output would be something like this:

1st run. Found solution: Yes. Spent time: 17 seconds
2nd run. Found solution: No. Spent time: [it may take a time until the Alloy analyzer is going to return no solution]
3nd run. Found solution: No. Spent time: [it may take a time until the Alloy analyzer is going to return no solution]
...
9th run. Found solution: Yes. Spent time: 21 seconds
10th run. Found solution: Yes. Spent time: 10 seconds

Here a pseudo code I am trying to go through, but there are a lot of pieces (text questions) I have no idea how to implement it or how can I find more study material:

...
A4Reporter rep = new A4Reporter() {...}
...
Module world = CompUtil.parseEverything_fromFile(rep, null, filename); //reading Alloy filename.
...
A4Options options = new A4Options(); //Analyzer’s options.
...
Command command: world.getAllCommands(); //I’am looking for Alloy’s ‘run’ commands, for instance, the first run command would be: run MyPred for 3 but 3 Int, exactly 1 Sig_Scope1, 1 Sig_Scope2, exactly 1 Sig_Scope3
...
Int max_number_of_runs = 10;
for(i = 0; i < max_number_of_runs; i++) {
    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options); //get all Signatures, fine :)
    System.out.println(ans); //printing the whole command.
    if (ans.satisfiable()) {
        //How can I get the amount of time (in seconds) to found a solution as an integer or String?
        //Getting the label of the Sigs. I have got this way, however I do not know if it is the right one.
        SafeList<Sig> sigs = ans.getAllReachableSigs();
            for (Sig sig : sigs) {
                System.out.println(sig.shortLabel());
            }
        //For each Sig how can I get their values?
        //How can I build a new command (Command new_built_command) for the next run? The values of scope Sig will come from a list or they will be generated through Java Random class (I mean a know how to generate random integers).
        command = new_built_command;
    } else {
        //A message that the current command did not find a solution as a String!
    }
}

Could you help me out on that, please?

Answer 1

How can I build a new command

You can see ExampleUsingTheAPI for an example of using the Alloy API for constructing Alloy models. Using that API you can programmatically construct a Command to run. Alternatively, you can start with an Alloy model in a text form, parse it using CompUtil.parseEverything_fromString, then do a string find-replace on the original Alloy model to update the command, and start all over again.

For each Sig how can I get their values?

See ExampleCompilingFromSource, line 44. Basically, once you get an A4Solution object, you can call the eval method on it to evaluate any expression against the found solution (if you pass a Sig object, you'll get its value in the solution).

How can I get the amount of time (in seconds) to found a solution as an integer or String?

I'm not sure A4Solution contains any information about solving time, so in that case you'd have to measure time yourself.