No state elim with bigstep?

moves-rwth · Jan 10, 2025 · 532e0f6 · 532e0f6
1 parent bd495c7
commit 532e0f6
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 14 deletions.
diff --git a/resources/examples/testfiles/dtmc/non_graph_preserving.pm b/resources/examples/testfiles/dtmc/non_graph_preserving.pm
@@ -1,10 +1,9 @@
 dtmc
 
-const double p0;
+    const double p0;
+
+module nonsimple s: [0..3] init 0;
 
-module nonsimple
-    s : [0..3] init 0;
-    
     [] s=0 ->
         p0 : (s'=0)
         1-p0 : (s'=1);
@@ -13,4 +12,3 @@ module nonsimple
 endmodule
 
 label "target" = s=2;
-
diff --git a/resources/examples/testfiles/pdtmc/only_p.pm b/resources/examples/testfiles/pdtmc/only_p.pm
@@ -1,14 +1,14 @@
 dtmc
 
-const double p;
+    const double p;
 
 module test
 
-	// local state
-	s : [0..1] init 0;
-	
-	[] s=0 -> p : (s'=0) + (1-p) : (s'=1);
-	[] s=1 -> 1 : (s'=1);
+    // local state
+    s: [0..1] init 0;
+
+[] s = 0->p : (s '=0) + (1-p) : (s' = 1);
+    [] s=1 -> 1 : (s'=1);
 		
 endmodule
 

diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -93,10 +93,9 @@ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType, Robus
 
     reset();
 
-    std::cout << "Eliminating: " << allowModelSimplifications << graphPreserving << std::endl;
     if (allowModelSimplifications && graphPreserving) {
         auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*dtmc);
-        if (!graphPreserving) {
+        if (!graphPreserving || !transformer::TimeTravelling::lastSavedAnnotations.empty()) {
             simplifier.setSkipConstantDeterministicStateElimination(true);
         }
         if (!simplifier.simplify(checkTask.getFormula())) {

diff --git a/src/storm/utility/logging.h b/src/storm/utility/logging.h
@@ -13,7 +13,8 @@ using carl::operator<<;
 
 #include <l3pp.h>
 
-#if !defined(STORM_LOG_DISABLE_DEBUG) && !defined(STORM_LOG_DISABLE_TRACE)
+// #if !defined(STORM_LOG_DISABLE_DEBUG) && !defined(STORM_LOG_DISABLE_TRACE)
+#if 1
 #define STORM_LOG_TRACE(message) L3PP_LOG_TRACE(l3pp::Logger::getRootLogger(), message)
 #else
 #define STORM_LOG_TRACE(message) (void)(0)