首页 文章

合金分析仪4.2(mac)与合金api

提问于
浏览
2

我目前正在制作一个程序来处理java中的一些注释,然后构建一个合金模型,使用合金api解析它,然后运行一些合金命令 . 当我在合金应用程序中测试生成的合金模型时,它工作正常并给出了预期的结果 . 但是,当我通过API运行生成的合金模型时,它告诉我:“你必须为sig this / ObjectName指定一个范围” . 我从这样的字符串中读取合金代码 .

world = CompUtil.parseOneModule(String model);

我使用的唯一选项是SAT4J解算器和1的skolemdepth .

然后我迭代来自世界的命令,将它们转换为kodkod,然后执行它们 .

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

我的UPDATED合金代码如下所示:

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

那么有没有人知道如何解决这个问题,因为我认为for 1 Configuration,8 Elements会为所有扩展sigs设置范围?

编辑*

我用我的建议更新了我的合金模型,我得到了同样的错误:“你必须为sig指定一个范围”这个/控制器“上面的合金代码在合金分析仪中工作并给出了这个结果:

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.

1 回答

  • 0

    您的Alloy模型包含语法错误,因此您无法使用Alloy Analyzer运行它 .

    首先,为testcontroller检查指定范围的正确方法是这样的

    check testcontroller for 8 but 1 Configuration
    

    这意味着“对于所有的8个原子,但是1个原子的配置”,而你所写的不是事件解析 .

    接下来, mvc_controller_style 谓词未定义,这也会导致问题 .

    至于您的API用法,只需将 parseOneModule 更改为 parseEverything_fromFile 即可 . 我也希望 parseOneModule 在这种情况下工作(因为你的模型中只有一个模块),但它没有得到正确的解决 . 我'm not sure whether that'是一个错误,或者该方法不应该是公共API的一部分 . 无论如何,这是我的代码适用于您的示例:

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

相关问题