Added more precise domainsize control

ftsrg · Feb 21, 2024 · 8548ad0 · 8548ad0
1 parent 996e9fd
commit 8548ad0
Showing 1 changed file with 7 additions and 5 deletions.
diff --git a/...s/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java b/...s/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java
@@ -68,14 +68,16 @@ public SafetyResult<MddWitness, MddCex> check(Void input) {
         final var initToExprResult = StmtUtils.toExpr(xsts.getInit(), VarIndexingFactory.indexing(0));
 
         for(var v : xsts.getVars()){
-            stateOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), 0));
+            final var domainSize = /*v.getType() instanceof BoolType ? 2 :*/ 0;
 
-            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(envTranToExprResult.getIndexing().get(v) == 0 ? 1 : envTranToExprResult.getIndexing().get(v)), 0));
-            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), 0));
+            stateOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize));
+
+            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(envTranToExprResult.getIndexing().get(v) == 0 ? 1 : envTranToExprResult.getIndexing().get(v)), domainSize));
+            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize));
 
             // TODO if indexes are identical, inject v'=v
-            initOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(initToExprResult.getIndexing().get(v) == 0 ? 1 : initToExprResult.getIndexing().get(v)), 0));
-            initOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), 0));
+            initOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(initToExprResult.getIndexing().get(v) == 0 ? 1 : initToExprResult.getIndexing().get(v)), domainSize));
+            initOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize));
         }
 
         final var stateSig = stateOrder.getDefaultSetSignature();