more efficient instantiation of matrices.

Former-commit-id: 0f4c36f2f2

src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp

@@ -4,7 +4,6 @@
 
 #include "src/adapters/CarlAdapter.h"
 
-//#include "src/storage/StronglyConnectedComponentDecomposition.h"
 
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -15,7 +14,9 @@
 
 #include "modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-//#include "modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
+
+#include "src/modelchecker/region/ApproximationModel.h"
+#include "src/modelchecker/region/SamplingModel.h"
 
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/exceptions/InvalidStateException.h"
@@ -183,9 +184,10 @@ namespace storm {
                 eliminationModelChecker(model),
                 smtSolver(nullptr),
                 probabilityOperatorFormula(nullptr),
-                sampleDtmc(nullptr),
-                approxMdp(nullptr),
-                isReachProbFunctionComputed(false) {
+                samplingModel(nullptr),
+                approximationModel(nullptr),
+                isReachProbFunctionComputed(false),
+                isResultConstant(false) {
             //intentionally left empty
         }
         
@@ -221,66 +223,19 @@ namespace storm {
             std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now();
             STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::IllegalArgumentException, "Tried to specify a formula that can not be handled.");
             
-            //Get subformula, initial state, target states
+            //Get subformula, target states
             //Note: canHandle already ensures that the formula has the right shape and that the model has a single initial state.
             this->probabilityOperatorFormula= std::unique_ptr<storm::logic::ProbabilityOperatorFormula>(new storm::logic::ProbabilityOperatorFormula(formula.asStateFormula().asProbabilityOperatorFormula()));
             storm::logic::EventuallyFormula const& eventuallyFormula = this->probabilityOperatorFormula->getSubformula().asPathFormula().asEventuallyFormula();
             std::unique_ptr<CheckResult> targetStatesResultPtr = this->eliminationModelChecker.check(eventuallyFormula.getSubformula());
             storm::storage::BitVector const& targetStates = targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector();
             
-            // Then, compute the subset of states that has a probability of 0 or 1, respectively.
-            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, storm::storage::BitVector(model.getNumberOfStates(),true), targetStates);
-            storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
-            storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
-            storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-            
-            // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction.
-            if (model.getInitialStates().isDisjointFrom(maybeStates)) {
-                STORM_LOG_WARN("The probability of the initial state is constant (0 or 1)");
-                this->reachProbFunction = statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero<ParametricType>() : storm::utility::one<ParametricType>();
-                this->isReachProbFunctionComputed=true;
-            }
-            
-            // Determine the set of states that is reachable from the initial state without jumping over a target state.
-            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1);
-            // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
-            maybeStates &= reachableStates;
-            // Create a vector for the probabilities to go to a state with probability 1 in one step.
-            this->oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
-            // Determine the initial state of the sub-model.
-            //storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
-            this->initialState = *(model.getInitialStates() % maybeStates).begin();
-            // We then build the submatrix that only has the transitions of the maybe states.
-            storm::storage::SparseMatrix<ParametricType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
-            storm::storage::SparseMatrix<ParametricType> submatrixTransposed = submatrix.transpose();
-            
-            // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
-            this->flexibleTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix);
-            this->flexibleBackwardTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrixTransposed, true);
-            
-            // Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated.
-            this->subsystem = storm::storage::BitVector(submatrix.getRowCount(), true);
-            
-            std::chrono::high_resolution_clock::time_point timeInitialStateEliminationStart = std::chrono::high_resolution_clock::now();
-            // eliminate all states with only constant outgoing transitions
-            //TODO: maybe also states with constant incoming tranistions. THEN the ordering of the eliminated states does matter.
-            eliminateStatesConstSucc(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->oneStepProbabilities, this->hasOnlyLinearFunctions, this->initialState);
-            STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl);
-            std::cout << "Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl;
-            
-            
-            //eliminate the remaining states to get the reachability probability function
-            this->sparseTransitions = this->flexibleTransitions.getSparseMatrix();
-            this->sparseBackwardTransitions = this->sparseTransitions.transpose();
-
-            std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now();
-            
-            initializeSampleDtmcAndApproxMdp(this->sampleDtmc,this->sampleDtmcMapping,this->approxMdp,this->approxMdpMapping,this->approxMdpSubstitutions,this->subsystem, this->sparseTransitions,this->oneStepProbabilities, this->initialState);
+            computeSimplifiedModel(targetStates);
+            initializeSampleAndApproxModel();
            
             //some information for statistics...
             std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
             this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart;
-            this->timeInitialStateElimination = timeInitialStateEliminationEnd-timeInitialStateEliminationStart;
             this->numOfCheckedRegions=0;
             this->numOfRegionsSolvedThroughSampling=0;
             this->numOfRegionsSolvedThroughApproximation=0;