Use bounded domain when possible

ftsrg · Feb 20, 2024 · f141ec4 · f141ec4
1 parent f9ae8d8
commit f141ec4
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/checker/MddChecker.java b/...alysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/checker/MddChecker.java
@@ -76,10 +76,12 @@ public SafetyResult<MddWitness, MddCex> check(Void input) {
 
         final Set<VarDecl<?>> vars = ExprUtils.getVars(List.of(initRel, transRel.toExpr(), safetyProperty));
         for(var v : vars){
-            stateOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(initIndexing.get(v)), 0));
+            final var domainSize = v.getType() instanceof BoolType ? 2 : 0;
 
-            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(transRel.nextIndexing().get(v)), 0));
-            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), 0));
+            stateOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(initIndexing.get(v)), domainSize));
+
+            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(transRel.nextIndexing().get(v)), domainSize));
+            transOrder.createOnTop(MddVariableDescriptor.create(v.getConstDecl(0), domainSize));
         }
 
         final var stateSig = stateOrder.getDefaultSetSignature();