Kodkod provides different result from Alloy Analyzer

API Issues
1

Hi,

I have a model checking confidentiality on the documents by level.
I want the model starts with no documents, no accesses as below. In Alloy Analyzer the property takes hours to terminate (in fact it has not terminated yet). So, I decided to check it with a more powerful machine using the Java API Kodkod since I can’t run the Alloy Analyzer in that machine (no user interface). However, when I run the same model with the Kodkod, looks like it doesn’t take the ‘fact init’ into account. It produces a single state output that has documents and roles that have accesses to these documents and terminates very quickly. I used the SAT4J solver in both.

A part of the model looks like this:

pred Confidentiality {

    all d : Domain | all m : Module | all res : find_resources[d] |
        some (res & m.accesses) implies (find_role[m] = level[res.~content])

}

fact init {
  #(Operation + NoOperation) = 1
  #documents = 0
  #accesses = 0
  always some Operation + NoOperation
}

assert CheckConfidentiality {
  always ( Confidentiality )
} 
check CheckConfidentiality for 4 but 5 Author, 5 Role, 5 Document

My Java code with Kodkod is as the following:

public static A4Solution executeAlloyModel(String fileName, String property) throws Err  {
		
		CompModule world = null;
		A4Reporter rep = new A4Reporter();
		try {
			world = CompUtil.parseEverything_fromFile(rep, null, fileName);
		}catch(Err e) {
			System.err.println("Load failed at " + e.pos);
            System.exit(1);
		}
		
		A4Options options = new A4Options();
		
		options.solver = A4Options.SatSolver.SAT4J;
		
		for (Command command : world.getAllCommands()) {
			
			if (command.label.equals(property)) {
				
				A4Solution ans = TranslateAlloyToKodkod.execute_command(null, world.getAllReachableSigs(), command, options);
				
				return ans;

			}
			
		}
		return null;
	}

}
public static void main(String[] args) throws IOException {
		
		String modelName = "models/analysis.als";
		
		String predicate = "CheckConfidentiality";
		
		A4Solution modelExecuterResult = executeAlloyModel(modelName, predicate);
		
		if (modelExecuterResult == null) {
			System.out.println("Property not found");
		}else {
			if (modelExecuterResult.satisfiable()) {
				System.out.println("Counterexample found");
				Path fileName = Path.of("timeStamp.txt");
				
				Files.writeString(fileName, modelExecuterResult.toString());
			}else {
				System.out.println("Property is proved");
			}
		}

	}

I have used the Electrum 2.1.4 jar file here Release Electrum v2.1.4 · haslab/Electrum2 · GitHub
What could I be doing wrong?

2

For future reference if somebody else has the same problem. Looks like I should have declared the fields in the init constraints with their father signature. Then, the Kodkod behaves the same with the Alloy Analyzer.