diff --git a/.gitignore b/.gitignore index 03286848f..69866a060 100644 --- a/.gitignore +++ b/.gitignore @@ -45,3 +45,4 @@ build//CMakeLists.txt *.*~ # CMake generated/configured files src/utility/storm-version.cpp +nbproject/ diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp index eb55943b9..084f0c987 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp @@ -1,8 +1,5 @@ #include "src/modelchecker/reachability/SparseDtmcRegionModelChecker.h" -//TODO remove useless includes - -//#include #include #include "src/adapters/CarlAdapter.h" @@ -122,7 +119,7 @@ namespace storm { template - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : model(model), eliminationModelChecker(model) { + SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc const& model) : model(model), eliminationModelChecker(model), probabilityOperatorFormula(nullptr) { // Intentionally left empty. } @@ -155,14 +152,13 @@ namespace storm { template void SparseDtmcRegionModelChecker::specifyFormula(storm::logic::Formula const& formula) { - std::chrono::high_resolution_clock::time_point timeStart = std::chrono::high_resolution_clock::now(); + 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 //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(new storm::logic::ProbabilityOperatorFormula(formula.asStateFormula().asProbabilityOperatorFormula())); storm::logic::EventuallyFormula const& eventuallyFormula = this->probabilityOperatorFormula->getSubformula().asPathFormula().asEventuallyFormula(); - storm::storage::sparse::state_type initialState = *model.getInitialStates().begin(); std::unique_ptr targetStatesResultPtr = this->eliminationModelChecker.check(eventuallyFormula.getSubformula()); storm::storage::BitVector const& targetStates = targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -184,31 +180,129 @@ namespace storm { 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 set of initial states of the sub-model. - storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates; + // 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 submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - //TODO do we need this? - std::vector statePriorities = this->eliminationModelChecker.getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); - // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. - FlexibleMatrix flexibleMatrix = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrix); - FlexibleMatrix flexibleBackwardTransitions = this->eliminationModelChecker.getFlexibleSparseMatrix(submatrixTransposed, true); - - // Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated. - storm::storage::BitVector subsystem = storm::storage::BitVector(submatrix.getRowCount(), true); - eliminateStates(subsystem, flexibleMatrix, oneStepProbabilities, flexibleBackwardTransitions, newInitialStates, submatrix, statePriorities); - - - // std::chrono::high_resolution_clock::time_point timeStateElemEnd = std::chrono::high_resolution_clock::now(); - - + 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->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 = flexibleTransitions.getSparseMatrix(); + this->sparseBackwardTransitions = this->sparseTransitions.transpose(); + this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState); + std::cout << std::endl <<"the resulting reach prob function is " << std::endl << this->reachProbFunction << std::endl << std::endl; + std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now(); + + //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; + } + + template + void SparseDtmcRegionModelChecker::eliminateStatesConstSucc( + storm::storage::BitVector& subsys, + FlexibleMatrix& flexTransitions, + FlexibleMatrix& flexBackwardTransitions, + std::vector& oneStepProbs, + storm::storage::sparse::state_type const& initialState) { + + //temporarily unselect the initial state to skip it. + subsys.set(initialState, false); + + boost::optional> missingStateRewards; + for (auto const& state : subsys) { + bool onlyConstantOutgoingTransitions=true; + for(auto const& entry : flexTransitions.getRow(state)){ + if(!this->parametricTypeComparator.isConstant(entry.getValue())){ + onlyConstantOutgoingTransitions=false; + break; + } + } + if(onlyConstantOutgoingTransitions){ + this->eliminationModelChecker.eliminateState(flexTransitions, oneStepProbs, state, flexBackwardTransitions, missingStateRewards); + subsys.set(state,false); + } + } + subsys.set(initialState, true); + } + + + template + ParametricType SparseDtmcRegionModelChecker::computeReachProbFunction( + storm::storage::BitVector const& subsys, + FlexibleMatrix const& flexTransitions, + FlexibleMatrix const& flexBackwardTransitions, + storm::storage::SparseMatrix const& spTransitions, + storm::storage::SparseMatrix const& spBackwardTransitions, + std::vector const& oneStepProbs, + storm::storage::sparse::state_type const& initState){ + + //Note: this function is very similar to eliminationModelChecker.computeReachabilityValue + + //get working copies of the flexible transitions and oneStepProbabilities with which we will actually work (eliminate states etc). + FlexibleMatrix workingCopyFlexTrans(flexTransitions); + FlexibleMatrix workingCopyFlexBackwTrans(flexBackwardTransitions); + std::vector workingCopyOneStepProbs(oneStepProbs); + + storm::storage::BitVector initialStates(subsys.size(),false); + initialStates.set(initState, true); + std::vector statePriorities = this->eliminationModelChecker.getStatePriorities(spTransitions, spBackwardTransitions, initialStates, workingCopyOneStepProbs); + boost::optional> missingStateRewards; + + // Remove the initial state from the states which we need to eliminate. + storm::storage::BitVector statesToEliminate(subsys); + statesToEliminate.set(initState, false); + + //pure state elimination or hybrid method? + if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { + std::vector states(statesToEliminate.begin(), statesToEliminate.end()); + std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities[a] < statePriorities[b]; }); + + STORM_LOG_DEBUG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); + for (auto const& state : states) { + this->eliminationModelChecker.eliminateState(workingCopyFlexTrans, workingCopyOneStepProbs, state, workingCopyFlexBackwTrans, missingStateRewards); + } + } + else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { + uint_fast64_t maximalDepth = 0; + std::vector entryStateQueue; + STORM_LOG_DEBUG("Eliminating " << statesToEliminate.size() << " states using the hybrid elimination technique." << std::endl); + maximalDepth = eliminationModelChecker.treatScc(workingCopyFlexTrans, workingCopyOneStepProbs, initialStates, statesToEliminate, spTransitions, workingCopyFlexBackwTrans, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, missingStateRewards, statePriorities); + + // If the entry states were to be eliminated last, we need to do so now. + STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); + if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) { + for (auto const& state : entryStateQueue) { + eliminationModelChecker.eliminateState(workingCopyFlexTrans, workingCopyOneStepProbs, state, workingCopyFlexBackwTrans, missingStateRewards); + } + } + } + else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The selected state elimination Method has not been implemented."); + } + //finally, eliminate the initial state + this->eliminationModelChecker.eliminateState(workingCopyFlexTrans, workingCopyOneStepProbs, initState, workingCopyFlexBackwTrans, missingStateRewards); + + return workingCopyOneStepProbs[initState]; } - + template<> @@ -681,6 +775,31 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); } } + + template + void SparseDtmcRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { + + std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast(this->timePreprocessing); + std::chrono::milliseconds timeInitialStateEliminationInMilliseconds = std::chrono::duration_cast(this->timeInitialStateElimination); + + std::chrono::high_resolution_clock::duration timeOverall = timePreprocessing; // + ... + std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(timeOverall); + + outstream << std::endl << "Statistics Region Model Checker:" << std::endl; + outstream << "-----------------------------------------------" << std::endl; + outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl; + outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << this->sparseTransitions.getEntryCount() << "transitions" << std::endl; + outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl; + outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl; + outstream << "Running times:" << std::endl; + outstream << " " << timeOverallInMilliseconds.count() << "ms overall" << std::endl; + outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl; + outstream << " " << timeInitialStateEliminationInMilliseconds.count() << "ms Initial state elimination" << std::endl; + //outstream << " " << timeInMilliseconds.count() << "ms " << std::endl; + outstream << "-----------------------------------------------" << std::endl; + + } + #endif diff --git a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h index 7851883f2..29b2700ed 100644 --- a/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcRegionModelChecker.h @@ -92,6 +92,11 @@ namespace storm { * ParameterRegions should contain all parameters. */ bool checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions); + + /*! + * Prints statistical information (mostly running times) to the given stream. + */ + void printStatisticsToStream(std::ostream& outstream); private: typedef typename storm::modelchecker::SparseDtmcEliminationModelChecker::FlexibleSparseMatrix FlexibleMatrix; @@ -137,29 +142,68 @@ namespace storm { template bool valueIsInBoundOfFormula(ValueType value); + //eliminates all states for which the outgoing transitions are constant. + void eliminateStatesConstSucc( + storm::storage::BitVector& subsys, + FlexibleMatrix& flexTransitions, + FlexibleMatrix& flexBackwardTransitions, + std::vector& oneStepProbs, + storm::storage::sparse::state_type const& initState + ); + + //Computes the reachability probability function by performing state elimination + ParametricType computeReachProbFunction( + storm::storage::BitVector const& subsys, + FlexibleMatrix const& flexTransitions, + FlexibleMatrix const& flexBackwardTransitions, + storm::storage::SparseMatrix const& spTransitions, + storm::storage::SparseMatrix const& spBackwardTransitions, + std::vector const& oneStepProbs, + storm::storage::sparse::state_type const& initState + ); + + + + // The model this model checker is supposed to analyze. storm::models::sparse::Dtmc const& model; - + + //classes that provide auxilliary functions // Instance of an elimination model checker to access its functions storm::modelchecker::SparseDtmcEliminationModelChecker eliminationModelChecker; + // comparators that can be used to compare constants. + storm::utility::ConstantsComparator parametricTypeComparator; + storm::utility::ConstantsComparator constantTypeComparator; - // - - // A comparator that can be used to compare constants. - //storm::utility::ConstantsComparator comparator; + + //the following members depend on the currently specified formula: - //the following members depend on the currently specified formula //the currently specified formula std::unique_ptr probabilityOperatorFormula; - // the propabilities to go to a state with probability 1 in one step + + // The ingredients of the model where constant transitions have been eliminated as much as possible + // the probability matrix + FlexibleMatrix flexibleTransitions; + storm::storage::SparseMatrix sparseTransitions; + //the corresponding backward transitions + FlexibleMatrix flexibleBackwardTransitions; + storm::storage::SparseMatrix sparseBackwardTransitions; + // the propabilities to go to a state with probability 1 in one step (belongs to flexibleTransitions) std::vector oneStepProbabilities; + // the initial state + storm::storage::sparse::state_type initialState; + // the set of states that have not been eliminated + storm::storage::BitVector subsystem; // The function for the reachability probability in the initial state ParametricType reachProbFunction; - // running times + // runtimes and other information for statistics. + uint_fast64_t numOfCheckedRegions; + std::chrono::high_resolution_clock::duration timePreprocessing; + std::chrono::high_resolution_clock::duration timeInitialStateElimination; }; } // namespace modelchecker diff --git a/src/utility/cli.h b/src/utility/cli.h index 32defa498..1b730de51 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -478,6 +478,13 @@ namespace storm { auto regions=storm::utility::regions::RegionParser::getRegionsFromSettings(); storm::modelchecker::SparseDtmcRegionModelChecker modelchecker(*dtmc); + if (modelchecker.canHandle(*formula.get())) { + modelchecker.specifyFormula(*formula.get()); + } + else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric region check engine currently does not support this property."); + } + auto result = modelchecker.checkRegion(*formula.get(), regions); std::cout << "... done." << std::endl; if (!result){ @@ -486,6 +493,7 @@ namespace storm { for(auto const& reg : regions){ std::cout << reg.getRegionAsString() << " Result: " << reg.getCheckResultAsString() << std::endl; } + modelchecker.printStatisticsToStream(std::cout); } else{ diff --git a/src/utility/constants.h b/src/utility/constants.h index e8573130c..94b4dbbb7 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -58,6 +58,8 @@ namespace storm { bool isZero(ValueType const& value) const; bool isEqual(ValueType const& value1, ValueType const& value2) const; + + bool isConstant(ValueType const& value) const; }; // For floats we specialize this class and consider the comparison modulo some predefined precision. diff --git a/src/utility/regions.cpp b/src/utility/regions.cpp index c99cb7919..84ada2e41 100644 --- a/src/utility/regions.cpp +++ b/src/utility/regions.cpp @@ -52,7 +52,7 @@ namespace storm { STORM_LOG_WARN_COND((upperBound==convertNumber(ub, true, actualPrecision)), "The upper bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?"); lowerBounds.emplace(std::make_pair(var, lb)); upperBounds.emplace(std::make_pair(var, ub)); - std::cout << "parsed bounds " << parameterBoundsString << ": lb=" << lowerBound << " ub=" << upperBound << " param='" << parameter << "' precision=" << actualPrecision << std::endl; + // std::cout << "parsed bounds " << parameterBoundsString << ": lb=" << lowerBound << " ub=" << upperBound << " param='" << parameter << "' precision=" << actualPrecision << std::endl; } template