diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsTest.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsTest.java
index 53fa9eb620..0f21639a60 100644
--- a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsTest.java
+++ b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsTest.java
@@ -12,25 +12,18 @@
 import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.ExprLatticeDefinition;
 import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.MddExpressionTemplate;
 import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.MddNodeNextStateDescriptor;
-import hu.bme.mit.theta.analysis.utils.MddNodeCacheVisualizer;
+import hu.bme.mit.theta.analysis.algorithm.symbolic.symbolicnode.expression.MddNodeInitializer;
 import hu.bme.mit.theta.analysis.utils.MddNodeVisualizer;
 import hu.bme.mit.theta.common.visualization.Graph;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
-import hu.bme.mit.theta.core.decl.ConstDecl;
 import hu.bme.mit.theta.core.decl.Decl;
-import hu.bme.mit.theta.core.decl.Decls;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.stmt.NonDetStmt;
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
-import hu.bme.mit.theta.core.type.inttype.IntExprs;
-import hu.bme.mit.theta.core.type.inttype.IntType;
-import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.core.utils.PathUtils;
 import hu.bme.mit.theta.core.utils.StmtUtils;
-import hu.bme.mit.theta.core.utils.indexings.BasicVarIndexing;
-import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
 import hu.bme.mit.theta.frontend.petrinet.analysis.PtNetSystem;
 import hu.bme.mit.theta.frontend.petrinet.analysis.VariableOrderingFactory;
@@ -41,7 +34,6 @@
 import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.xsts.XSTS;
 
-import java.io.ByteArrayInputStream;
 import java.io.File;
 import java.io.FileNotFoundException;
 import java.util.*;
@@ -56,7 +48,7 @@ public static void main(String[] args){
 
         final PetriNet petriNet;
         try {
-            petriNet = PetriNetParser.loadPnml(new File("subprojects\\frontends\\petrinet-frontend\\petrinet-analysis\\src\\test\\resources\\dekker-15.pnml")).parsePTNet().get(0);
+            petriNet = PetriNetParser.loadPnml(new File("subprojects\\frontends\\petrinet-frontend\\petrinet-analysis\\src\\test\\resources\\Philosophers-5.pnml")).parsePTNet().get(0);
         } catch (Exception e) {
             throw new RuntimeException(e);
         }
@@ -67,7 +59,7 @@ public static void main(String[] args){
 //        ));
         final List<Place> ordering;
         try {
-            ordering = VariableOrderingFactory.fromFile("subprojects\\frontends\\petrinet-frontend\\petrinet-analysis\\src\\test\\resources\\dekker-15.pnml.gsat.order", petriNet);
+            ordering = VariableOrderingFactory.fromFile("subprojects\\frontends\\petrinet-frontend\\petrinet-analysis\\src\\test\\resources\\Philosophers-5.pnml.order", petriNet);
         } catch (Exception e) {
             throw new RuntimeException(e);
         }
@@ -98,7 +90,8 @@ public static void main(String[] args){
         var transSig = transOrder.getDefaultSetSignature();
         var stateSig = stateOrder.getDefaultSetSignature();
 
-        MddHandle initNode = stateSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(initExpr, o -> (Decl) o, new SolverPool(Z3SolverFactory.getInstance()::createSolver)));
+        MddHandle initNode = stateSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(initExpr, o -> (Decl) o, new SolverPool(Z3SolverFactory.getInstance())));
+//        MddValuationCollector.collect(initNode.getNode());
 
         final List<AbstractNextStateDescriptor> descriptors = new ArrayList<>();
         final List<MddHandle> transitionHandles = new ArrayList<>();
@@ -115,7 +108,7 @@ public static void main(String[] args){
             }
             if(!identityExprs.isEmpty()) stmtUnfold = And(stmtUnfold, And(identityExprs));
 
-            MddHandle transitionNode = transSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(stmtUnfold, o -> (Decl) o, new SolverPool(Z3SolverFactory.getInstance()::createSolver)));
+            MddHandle transitionNode = transSig.getTopVariableHandle().checkInNode(MddExpressionTemplate.of(stmtUnfold, o -> (Decl) o, new SolverPool(Z3SolverFactory.getInstance())));
             transitionHandles.add(transitionNode);
             descriptors.add(MddNodeNextStateDescriptor.of(transitionNode));
         }
@@ -135,17 +128,16 @@ public static void main(String[] args){
         final MddVariableOrder variableOrder = JavaMddFactory.getDefault().createMddVariableOrder(LatticeDefinition.forSets());
         ordering.forEach(p -> variableOrder.createOnTop(MddVariableDescriptor.create(p)));
 
-        final GeneralizedSaturationProvider gs = new GeneralizedSaturationProvider(variableOrder);
-        final MddHandle satResult = gs.compute(system.getInitializer(),
-                system.getTransitions(),
-                variableOrder.getDefaultSetSignature().getTopVariableHandle()
-        );
+//        final GeneralizedSaturationProvider gs = new GeneralizedSaturationProvider(variableOrder);
+//        final MddHandle satResult = gs.compute(system.getInitializer(),
+//                system.getTransitions(),
+//                variableOrder.getDefaultSetSignature().getTopVariableHandle()
+//        );
 
-//        var gs = new CursorGeneralizedSaturationProvider(stateSig.getVariableOrder());
+        var gs = new GeneralizedSaturationProvider(stateSig.getVariableOrder());
+        var satResult = gs.compute(new MddNodeInitializer(initNode), nextStates, stateSig.getTopVariableHandle());
 //        var satResult = gs.compute(initNode, nextStates, stateSig.getTopVariableHandle());
 
-        System.out.println(Z3SolverFactory.solversCreated);
-
         Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(satResult);
         System.out.println("State space size: "+stateSpaceSize);
 
@@ -160,6 +152,8 @@ public static void main(String[] args){
             e.printStackTrace();
         }
 
+
+
 //        int i = 0;
 //        for(var handle: transitionHandles){
 //            final Graph g = new MddNodeCacheVisualizer(XstsTest::nodeToString).visualize(handle.getNode());