Pass parameter to predicate with Alloy Java API

41 Views Asked by At

How can I create an instance of atom with Alloy API? My goal is create an instance from java and pass it as a parameter to predicate alloy model.

The issue is: Field "field (this/File <: name)" is not bound to a legal value during translation.

Would you let me know how to fix the problem?

My model look like this:

sig Name{}

sig File{
    name: Name
}

pred checkName[f: File]{
    f.name in Name
}

I define signatures:

PrimSig name = new PrimSig("Name");

PrimSig file = new PrimSig("File");
Field fileNameField = file.addField("name", name); 

I create instance:

PrimSig myName = new PrimSig(name, "Name");

PrimSig myFile = new PrimSig(file, "File");
myFile.addField("name", name);
myFile.join(fileNameField).equal(myName);

I run the command:

Expr expr = CompUtil.parseEverything_fromFile(rep, null, improvementModelPath).getAllFunc().get(0).call(myFile);
Command cmd = new Command(false, 3, 3, 3, expr);
A4Solution sol = TranslateAlloyToKodkod.execute_command(NOP, sigs, cmd, opt);
1

There are 1 best solutions below

0
Peter Kriens On

There is no clean API for this, at least as far as I know.

In general I just use source code for this. I.e. if I want a command I add it to the source and then lookup the command from the CompModule.

To see some example, here is the upcoming Evaluator, part of the command line interface in the upcoming release.

I once started to work on a clean API but too many things to do.