Alloy Analyzer 4.2 (mac) versus alloy api

Question

I am currently making a program that processes some annotations in java and then builds an alloy model, parses it using the alloy api and then runs some alloy commands. When I test the generated alloy model in the alloy app it works fine and gives me the expected results. However, when I run the generated alloy model through the API, it tells me: "You must specify a scope for sig this/ObjectName". I read the alloy code from a string like this.

world = CompUtil.parseOneModule(String model);

The only options I use are the SAT4J solver and a skolemdepth of 1.

I then iterate over the commands from world, translates them to kodkod, and executes them.

for(Command command: world.getAllCommands()) {
    A4Solution ans = null;
        try {
            ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);
        } catch (Err ex) {
            Logger.getLogger(AlloyTest.class.getName()).log(Level.SEVERE, null, ex);
        }
}

My UPDATED alloy code looks like this:

module mvc
// General model
abstract sig Configuration { elements: set Element }
abstract sig Element { references: set Element }

// MVC Style
abstract sig Model extends Element { }
abstract sig View extends Element { }
abstract sig Controller extends Element { }

pred mvc_model_style [c: Configuration] {
all m: c.elements & Model | all r: m.references | r not in View
}
pred mvc_view_style [c: Configuration] {
all view: c.elements & View | all ref: view.references | ref not in Model
}

pred mvc_controller_style [c: Configuration] {
    all controller: c.elements & Controller | all ref: controller.references | ref in Model or ref in View or ref in Controller
}

pred mvc_style [c: Configuration]{
 mvc_model_style[c] mvc_view_style[c]
}
one sig testMvc extends Configuration { } {
elements = TestController + ViewTest + TestModel + TestController3
}
one sig TestController extends Controller { } {
references = TestController + TestModel
}
one sig ViewTest extends View { } {
references = TestController
}
one sig TestModel extends Model { } {
references = ViewTest + TestController3
}
one sig TestController3 extends Controller { } {
references = TestController + TestModel
}
assert testcontroller {
mvc_controller_style[testMvc]
}
assert viewtest {
mvc_view_style[testMvc]
}
assert testmodel {
mvc_model_style[testMvc]
}
assert testcontroller3 {
mvc_controller_style[testMvc]
}
check testcontroller for 8 but 1 Configuration
check viewtest for 8 but 1 Configuration
check testmodel for 8 but 1 Configuration
check testcontroller3 for 8 but 1 Configuration

So does anybody have any idea for how I can fix this, as I thought that the for 1 Configuration, 8 Elements would set the scope for all the extending sigs?

Edit*

I updated my alloy model with the suggestions and I stil get the same error: "You must specify a scope for sig "this/Controller" The above alloy code works in the Alloy Analyzer and gives this result:

Executing "Check testcontroller for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   83 vars. 26 primary vars. 98 clauses. 5ms.
   No counterexample found. Assertion may be valid. 1ms.

Executing "Check viewtest for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   65 vars. 25 primary vars. 75 clauses. 5ms.
   No counterexample found. Assertion may be valid. 0ms.

Executing "Check testmodel for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   65 vars. 25 primary vars. 75 clauses. 5ms.
   found. Assertion is invalid. 6ms.

Executing "Check testcontroller3 for 8 but 1 Configuration"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   83 vars. 26 primary vars. 98 clauses. 6ms.
   No counterexample found. Assertion may be valid. 0ms.

Aleksandar Milicevic Aleksandar Milicevic · Accepted Answer · 2013-01-26T20:36:47

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);
        }
    }
}

Alloy Analyzer 4.2 (mac) versus alloy api

1 Answers