alloy - Alloy Analyzer 4.2 (mac) と Alloy API

Question

私は現在、Java でいくつかの注釈を処理して合金モデルを構築し、合金 API を使用して解析し、いくつかの合金コマンドを実行するプログラムを作成しています。生成された合金モデルを合金アプリでテストすると、正常に動作し、期待どおりの結果が得られます。しかし、生成された合金モデルを API で実行すると、「sig this/ObjectName のスコープを指定する必要があります」と表示されます。こんな感じで文字列から合金コードを読み取ります。

world = CompUtil.parseOneModule(String model);

私が使用する唯一のオプションは、SAT4J ソルバーと 1 の skolemdepth です。

次に、world からのコマンドを繰り返し処理し、それらを 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 のスコープを設定すると思っていたので、これを修正する方法を知っている人はいますか?

編集*

提案を使用して合金モデルを更新しましたが、同じエラーが表示されます。

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.