Translate Alloy File to CNF using CLI

[zakiournani]

Hi all, Being an adept on alloy, i have an issue using alloy jar to translate an alloy description to a cnf file. the code bellow can be used with sat4J and gives the output. but when using CNF i get no output. Any tips on how to optain the output within a file "resultfile.cnf for example" thank you.

import edu.mit.csail.sdg.alloy4.A4Reporter; import edu.mit.csail.sdg.alloy4.Err; import edu.mit.csail.sdg.alloy4.ErrorWarning; import edu.mit.csail.sdg.alloy4compiler.ast.Command; import edu.mit.csail.sdg.alloy4compiler.ast.Module; import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil; import edu.mit.csail.sdg.alloy4compiler.translator.A4Options; import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution; import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;

public final class Cli {

public static void main(String[] args)  {

    A4Reporter rep = new A4Reporter() {};
    String filename = args[0];
        Module world = CompUtil.parseEverything_fromFile(rep, null, filename);
        A4Options options = new A4Options();
        options.solver = A4Options.SatSolver.CNF;
        for (Command command : world.getAllCommands()) {
        A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);

        }

}

}

[sorawee]

Change your reporter to something like this:

        A4Reporter rep = new A4Reporter() {
            @Override public void resultCNF(String filename) {
                System.out.println(filename);
            }
        };

Instead of printing filename out, you could also move the file to a desired location.

[zakiournani]

thank you a lot for your quick answer. Changing the reporter generates a cnf file as needed. and changing the tempDirectory through options allows to change the directory when the file will be generated. however i still cant specify the result cnf filename. am i missing something?

[sorawee]

You can simply rename/move it.

[zakiournani]

You mean manually ? i need to rename this through code to build something automatic. in the worst case i ll use a bash script that renames the tmp file. so it's not possible to juste specify the name of the result cnf using some options filed? thanks in advance

[sorawee]

As you can see from https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java#L1401, the code creates a temporary file which you have no control over its filename. Then, it calls the callback rep.resultCNF with the temporary filename.

So, if you would like to use SatSolver.CNF, you won't be able to specify the filename directly. You will instead get a temporary file. But given that, you can move, rename, read it to do whatever you want.

For how to rename/move in Java, I found this as the first result in Google:

https://stackoverflow.com/questions/4645242/how-do-i-move-a-file-from-one-location-to-another-in-java

[zakiournani]

thank you for your answer.