我目前正在制作一个程序,该程序在 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);
}
}
我更新的合金代码如下所示:
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 将为所有扩展信号设置范围?
编辑*
我用建议更新了我的合金模型,但仍然收到相同的错误:“您必须为 sig “this/Controller”指定一个范围以上合金代码在合金分析器中工作并给出以下结果:
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.