Your Alloy model contains syntax errors, so you couldn't run it using the Alloy Analyzer either.
First of all, the correct way to specify scope for your testcontroller check is this
check testcontroller for 8 but 1 Configuration
This means "for 8 atoms of everything, but 1 atom of Configuration", whereas what you wrote doesn't event parse.
Next, the mvc_controller_style
predicate is undefined, which will also cause you problems.
As for your API usage, just change parseOneModule
to parseEverything_fromFile
and it should work. I would also expect parseOneModule
to work in this case (because there is only one module in your model), but it just doesn't, because, for some reason, some names don't get properly resolved. I'm not sure whether that's a bug or maybe that method is not supposed to be part of the public API. Anyway, here is my code that worked properly for your example:
public static void main(String[] args) throws Exception {
A4Reporter rep = new A4Reporter();
Module world = CompUtil.parseEverything_fromFile(rep, null, "mvc.als");
A4Options options = new A4Options();
options.solver = A4Options.SatSolver.SAT4J;
options.skolemDepth = 1;
for (Command command : world.getAllCommands()) {
A4Solution ans = null;
try {
ans = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), command, options);
System.out.println(ans);
} catch (Err ex) {
Logger.getLogger(AlloyTest.class.getName()).log(Level.SEVERE, null, ex);
}
}
}