several *small* fixes and better direct encoding

Former-commit-id: 04265d8fb5

src/modelchecker/reachability/DirectEncoding.h

@@ -28,7 +28,7 @@ namespace storm
 					std::vector<carl::Variable> stateVars;
 					for(carl::Variable p : parameters)
 					{
-						smt2 << carl::io::smt2flag::ASSERT;
+						smt2 << ("parameter_bound_" + vpool.getName(p));
 						smt2 << carl::io::smt2node::AND;
 						smt2 << carl::Constraint<Polynomial>(Polynomial(p), carl::CompareRelation::GT);
 						smt2 << carl::Constraint<Polynomial>(Polynomial(p) - Polynomial(1), carl::CompareRelation::LT);
@@ -41,16 +41,15 @@ namespace storm
 						stateVars.push_back(stateVar);
 						if(!finalStates[state])
 						{
-							smt2 << carl::io::smt2flag::ASSERT;
+							smt2 << ("state_bound_" + std::to_string(state));
 							smt2 << carl::io::smt2node::AND;
-							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar), carl::CompareRelation::GE);
-							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LE);
+							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar), carl::CompareRelation::GT);
+							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LT);
 							smt2 << carl::io::smt2node::CLOSENODE;
 						}
 						
 					}
-					smt2 << carl::io::smt2flag::ASSERT;
-					smt2 << carl::io::smt2node::AND;
+					
 					smt2.setAutomaticLineBreaks(true);
 					Polynomial initStateReachSum;
 					for(uint_fast64_t state = 0; state < nrStates-1; ++state)
@@ -82,16 +81,20 @@ namespace storm
 								}
 								
 							}
+							smt2 << ("transition_" + std::to_string(state));
 							smt2 << carl::Constraint<T>(reachpropPol - stateVars[state], carl::CompareRelation::EQ);
 						}
 					}
 					//smt2 << carl::Constraint<Polynomial>(Polynomial(stateVars[nrStates-1]), carl::CompareRelation::EQ);
-					smt2 << carl::io::smt2node::CLOSENODE;
-					smt2 << carl::io::smt2flag::ASSERT;
+					
+					
+					smt2 << ("reachability");
 					
 					carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LE : carl::CompareRelation::GE;
 					smt2 <<  carl::Constraint<Polynomial>(initStateReachSum - threshold, thresholdRelation);
 					smt2 << carl::io::smt2flag::CHECKSAT;
+					smt2 << carl::io::smt2flag::MODEL;
+					smt2 << carl::io::smt2flag::UNSAT_CORE;
 					std::stringstream strm;
 					strm << smt2;
 					return strm.str();

src/models/AbstractModel.h

@@ -303,6 +303,10 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 		storm::models::AtomicPropositionsLabeling const& getStateLabeling() const {
 			return stateLabeling;
 		}
+		
+		storm::models::AtomicPropositionsLabeling & getStateLabeling() {
+			return stateLabeling;
+		}
 
 		/*!
 		 * Retrieves whether this model has a state reward model.

src/models/Dtmc.h

@@ -272,7 +272,7 @@ public:
 
 			// Get the choice label sets and move the needed values to the front.
 			std::vector<boost::container::flat_set<uint_fast64_t>> newChoice(this->getChoiceLabeling());
-			storm::utility::vector::selectVectorValues(newChoice, subSysStates, newChoice);
+			storm::utility::vector::selectVectorValues(newChoice, subSysStates, this->getChoiceLabeling());
 
 			// Throw away all values after the last state and set the choice label set for s_b as empty.
 			newChoice.resize(newStateCount);

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -1,5 +1,6 @@
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
 #include "src/models/AbstractModel.h"
+#include "src/storage/parameters.h"
 
 namespace storm {
     namespace storage {
@@ -204,5 +205,11 @@ namespace storm {
         
         // Explicitly instantiate the SCC decomposition.
         template class StronglyConnectedComponentDecomposition<double>;
+        #ifdef PARAMETRIC_SYSTEMS
+        template class StronglyConnectedComponentDecomposition<Polynomial>;
+        template class StronglyConnectedComponentDecomposition<RationalFunction>;
+        #endif
+        
+        
     } // namespace storage
 } // namespace storm

src/storage/prism/Constant.cpp

@@ -25,7 +25,8 @@ namespace storm {
         }
         
         storm::expressions::Expression const& Constant::getExpression() const {
-            LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant.");
+            assert(this->isDefined());
+            LOG_THROW(this->isDefined(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve defining expression for undefined constant: " + this->getName());
             return this->expression;
         }
         

src/storage/prism/Program.cpp

@@ -272,7 +272,7 @@ namespace storm {
                     constantSubstitution.emplace(constant.getName(), constant.getExpression());
                 
                 
-                    // If there is at least one more constant to come, we substitute the costants we have so far.
+                    // If there is at least one more constant to come, we substitute the constants we have so far.
                     if (constantIndex + 1 < newConstants.size()) {
                         newConstants[constantIndex + 1] = newConstants[constantIndex + 1].substitute(constantSubstitution);
                     }

src/stormParametric.cpp

@@ -32,31 +32,33 @@ std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& lab
     dtmc->makeAbsorbing(targetStates);
     // 2. throw away anything which does not add to the reachability probability.
     // 2a. remove non productive states
-    storm::storage::BitVector productive = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates);
-    // 2b. throw away non reachable states
-    storm::storage::BitVector reachable = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates);
-    storm::storage::BitVector bv = productive & reachable;
+    storm::storage::BitVector productiveStates = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates);
+    // 2b. calculate set of states wich 
+    storm::storage::BitVector almostSurelyReachingTargetStates = ~utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, ~productiveStates);
+    // 2c. Make such states also target states.
+    dtmc->makeAbsorbing(almostSurelyReachingTargetStates);
+    // 2d. throw away non reachable states 
+    storm::storage::BitVector reachableStates = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates);
+    storm::storage::BitVector bv = productiveStates & reachableStates;
+    dtmc->getStateLabeling().addAtomicProposition("__targets__", targetStates | almostSurelyReachingTargetStates);
     models::Dtmc<RationalFunction> subdtmc = dtmc->getSubDtmc(bv);
     
     phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true);
     initStates = subdtmc.getInitialStates();
-    targetStates = subdtmc.getLabeledStates(label);
+    targetStates = subdtmc.getLabeledStates("__targets__");
     storm::storage::BitVector deadlockStates(phiStates);
     deadlockStates.set(subdtmc.getNumberOfStates()-1,false);
-    // Calculate whether there are states which surely lead into the target.
-    storm::storage::BitVector potentialIntoDeadlock = utility::graph::performProbGreater0(subdtmc, subdtmc.getBackwardTransitions(), phiStates, deadlockStates);
-    storm::storage::BitVector extraTargets = ~potentialIntoDeadlock & ~targetStates;
-    if(extraTargets.empty())
-    {
-        // TODO implement this if necessary.
-        std::cout << "Extra targets exist. Please implement!" << std::endl;
-    }
+    
     // Search for states with only one non-deadlock successor.
     std::map<StateId, storage::DeterministicTransition<RationalFunction>> chainedStates;
     StateId nrStates = subdtmc.getNumberOfStates();
     StateId deadlockState = nrStates - 1;
-    for(StateId source = 0; source < nrStates; ++source)
+    for(StateId source = 0; source < nrStates - 1; ++source)
     {
+        if(targetStates[source])
+        {
+            continue;
+        }
         storage::DeterministicTransition<RationalFunction> productiveTransition(nrStates);
         for(auto const& transition : subdtmc.getRows(source))
         {
@@ -79,16 +81,37 @@ std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& lab
         {
             chainedStates.emplace(source, productiveTransition);
         }
-        for(auto chainedState : chainedStates)
+    }
+    storage::BitVector eliminatedStates(nrStates, false);
+    for(auto & chainedState : chainedStates)
+    {
+        assert(chainedState.first != chainedState.second.targetState());
+        auto it = chainedStates.find(chainedState.second.targetState());
+        if(it != chainedStates.end())
         {
-            auto it = chainedStates.find(chainedState.second.targetState());
-            if(it != chainedStates.end())
-            {
-                chainedState.second.targetState() = it->second.targetState();
-                chainedState.second.probability() *= it->second.probability();
-            }
+            //std::cout << "----------------------------" << std::endl;
+            //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl;
+            //std::cout << it->first << " -- " << it->second.probability() << " --> " << it->second.targetState() << std::endl;
+            chainedState.second.targetState() = it->second.targetState();
+            chainedState.second.probability() *= it->second.probability();
+            //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl;
+            //std::cout << "----------------------------" << std::endl;
+            chainedStates.erase(it);
+            eliminatedStates.set(it->first, true);
+        }
+    }
+    
+    
+    for(auto chainedState : chainedStates)
+    {
+        if(!eliminatedStates[chainedState.first])
+        {
+            std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl;
         }
     }
+    
+    storage::StronglyConnectedComponentDecomposition<RationalFunction> sccs(subdtmc);
+    std::cout << sccs << std::endl;
 
     modelchecker::reachability::DirectEncoding dec;
     std::vector<carl::Variable> parameters;
@@ -102,7 +125,7 @@ std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& lab
             parameters.push_back(p);
         }
     }
-    return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates(label), mpq_class(1,2));
+    return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2));
     
 }