From 4eea90646a2ec784fee9686dcd68ffeac3b366ef Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 6 Oct 2014 17:07:53 +0200 Subject: [PATCH] Fixed attributes of some example files. Added option to eliminate entry states in the very end (added option module for model checking of parametric models). Added feature to specify the formulas to check on the command line. Former-commit-id: 4ce8932fc4ed96be9c3ac997998f83c19194eae0 --- examples/pdtmc/brp/brp_32-4.pm | 0 examples/pdtmc/brp/brp_64-4.pm | 0 examples/pdtmc/brp/brp_64-5.pm | 0 src/adapters/extendedCarl.h | 2 +- .../reachability/SparseSccModelChecker.cpp | 149 +++++++++++++----- .../reachability/SparseSccModelChecker.h | 18 ++- src/settings/SettingsManager.cpp | 5 + src/settings/SettingsManager.h | 8 + src/settings/modules/GeneralSettings.cpp | 2 +- src/settings/modules/ParametricSettings.cpp | 22 +++ src/settings/modules/ParametricSettings.h | 39 +++++ .../expressions/ExpressionEvaluation.h | 5 +- src/storage/parameters.h | 2 +- src/stormParametric.cpp | 14 +- src/utility/cli.h | 11 +- 15 files changed, 214 insertions(+), 63 deletions(-) mode change 100755 => 100644 examples/pdtmc/brp/brp_32-4.pm mode change 100755 => 100644 examples/pdtmc/brp/brp_64-4.pm mode change 100755 => 100644 examples/pdtmc/brp/brp_64-5.pm create mode 100644 src/settings/modules/ParametricSettings.cpp create mode 100644 src/settings/modules/ParametricSettings.h diff --git a/examples/pdtmc/brp/brp_32-4.pm b/examples/pdtmc/brp/brp_32-4.pm old mode 100755 new mode 100644 diff --git a/examples/pdtmc/brp/brp_64-4.pm b/examples/pdtmc/brp/brp_64-4.pm old mode 100755 new mode 100644 diff --git a/examples/pdtmc/brp/brp_64-5.pm b/examples/pdtmc/brp/brp_64-5.pm old mode 100755 new mode 100644 diff --git a/src/adapters/extendedCarl.h b/src/adapters/extendedCarl.h index d611e14bc..5534fb7ab 100644 --- a/src/adapters/extendedCarl.h +++ b/src/adapters/extendedCarl.h @@ -8,7 +8,7 @@ #ifndef STORM_ADAPTERS_EXTENDEDCARL_H_ #define STORM_ADAPTERS_EXTENDEDCARL_H_ - +#include #include #include #include diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 76a331d22..1c06a4ee7 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -4,9 +4,11 @@ #include "src/storage/parameters.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" +#include "src/properties/Prctl.h" + +#include "src/exceptions/InvalidStateException.h" #include "src/utility/graph.h" #include "src/utility/vector.h" -#include "src/exceptions/InvalidStateException.h" #include "src/utility/macros.h" namespace storm { @@ -23,7 +25,9 @@ namespace storm { static RationalFunction&& simplify(RationalFunction&& value) { // In the general case, we don't to anything here, but merely return the value. If something else is // supposed to happen here, the templated function can be specialized for this particular type. + STORM_LOG_DEBUG("Simplifying " << value << " ... "); value.simplify(); + STORM_LOG_DEBUG("done."); return std::forward(value); } @@ -40,12 +44,41 @@ namespace storm { } template - ValueType SparseSccModelChecker::computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - // First, do some sanity checks to establish some required properties. + ValueType SparseSccModelChecker::computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula) { + + // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract + // the bitvector representation of the atomic propositions. + std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); + std::shared_ptr> phiStateFormula; + std::shared_ptr> psiStateFormula; + if (untilFormula.get() != nullptr) { + phiStateFormula = untilFormula->getLeft(); + psiStateFormula = untilFormula->getRight(); + } else { + std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); + STORM_LOG_THROW(eventuallyFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *untilFormula << " for parametric model checking. Note that only unbounded reachability properties are admitted."); + + phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); + psiStateFormula = eventuallyFormula->getChild(); + } + + // Now we need to make sure the formulas defining the phi and psi states are just labels. + std::shared_ptr> phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); + std::shared_ptr> psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); + STORM_LOG_THROW(phiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); + STORM_LOG_THROW(psiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); + + // Now retrieve the appropriate bitvectors from the atomic propositions. + storm::storage::BitVector phiStates = phiStateFormulaApFormula->getAp() != "true" ? dtmc.getLabeledStates(phiStateFormulaApFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); + storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiStateFormulaApFormula->getAp()); + + // Do some sanity checks to establish some required properties. STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - typename FlexibleSparseMatrix::index_type initialStateIndex = *dtmc.getInitialStates().begin(); + storm::storage::sparse::state_type initialStateIndex = *dtmc.getInitialStates().begin(); // Then, compute the subset of states that has a probability of 0 or 1, respectively. + auto totalTimeStart = std::chrono::high_resolution_clock::now(); + auto preprocessingStart = std::chrono::high_resolution_clock::now(); std::pair statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; @@ -61,10 +94,10 @@ namespace storm { // 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; - - std::cout << "Solving parametric system with " << maybeStates.getNumberOfSetBits() << " states." << std::endl; + auto preprocessingEnd = std::chrono::high_resolution_clock::now(); // Create a vector for the probabilities to go to a state with probability 1 in one step. + auto conversionStart = std::chrono::high_resolution_clock::now(); std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1); // Determine the set of initial states of the sub-DTMC. @@ -79,29 +112,65 @@ namespace storm { // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix); FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrix.transpose(), true); + auto conversionEnd = std::chrono::high_resolution_clock::now(); // Then, we recursively treat all SCCs. - treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0); + auto modelCheckingStart = std::chrono::high_resolution_clock::now(); + std::vector entryStateQueue; + uint_fast64_t maximalDepth = treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0,entryStateQueue); + + // If the entry states were to be eliminated last, we need to do so now. + STORM_LOG_DEBUG("Eliminating entry states as a last step."); + if (storm::settings::parametricSettings().isEliminateEntryStatesLastSet()) { + for (auto const& state : entryStateQueue) { + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); + } + } + + auto modelCheckingEnd = std::chrono::high_resolution_clock::now(); + auto totalTimeEnd = std::chrono::high_resolution_clock::now(); + + if (storm::settings::generalSettings().isShowStatisticsSet()) { + auto preprocessingTime = preprocessingEnd - preprocessingStart; + auto conversionTime = conversionEnd - conversionStart; + auto modelCheckingTime = modelCheckingEnd - modelCheckingStart; + auto totalTime = totalTimeEnd - totalTimeStart; + + STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); + STORM_PRINT_AND_LOG(" * time for preprocessing: " << std::chrono::duration_cast(preprocessingTime).count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for conversion: " << std::chrono::duration_cast(conversionTime).count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for checking: " << std::chrono::duration_cast(modelCheckingTime).count() << "ms" << std::endl); + STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" * total time: " << std::chrono::duration_cast(totalTime).count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Other:" << std::endl); + STORM_PRINT_AND_LOG(" * number of states eliminated: " << maybeStates.getNumberOfSetBits() << std::endl); + STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); + } // Now, we return the value for the only initial state. return oneStepProbabilities[initialStateIndex]; } template - void SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) { + uint_fast64_t SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, std::vector& entryStateQueue) { + uint_fast64_t maximalDepth = level; + // If the SCCs are large enough, we try to split them further. if (scc.getNumberOfSetBits() > SparseSccModelChecker::maximalSccSize) { + STORM_LOG_DEBUG("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further."); + // Here, we further decompose the SCC into sub-SCCs. storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, false, false); - - // To eliminate the remaining one-state SCCs, we need to keep track of them. - // storm::storage::BitVector remainingStates(scc); + STORM_LOG_DEBUG("Decomposed SCC into " << decomposition.size() << " sub-SCCs."); // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which // we eliminate the SCCs. storm::storage::BitVector remainingSccs(decomposition.size(), true); // First, get rid of the trivial SCCs. + STORM_LOG_DEBUG("Eliminating trivial SCCs."); for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) { storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex); if (scc.isTrivial()) { @@ -112,17 +181,12 @@ namespace storm { } // And then recursively treat the remaining sub-SCCs. + STORM_LOG_DEBUG("Eliminating remaining SCCs on level " << level << "."); for (auto sccIndex : remainingSccs) { storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex); - // If the SCC consists of just one state, we do not explore it recursively, but rather eliminate - // it directly. - if (newScc.size() == 1) { - continue; - } - + // Rewrite SCC into bit vector and subtract it from the remaining states. storm::storage::BitVector newSccAsBitVector(forwardTransitions.getRowCount(), newScc.begin(), newScc.end()); - // remainingStates &= ~newSccAsBitVector; // Determine the set of entry states of the SCC. storm::storage::BitVector entryStates(dtmc.getNumberOfStates()); @@ -135,40 +199,33 @@ namespace storm { } // Recursively descend in SCC-hierarchy. - treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, true, level + 1); + uint_fast64_t depth = treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, entryStateQueue); + maximalDepth = std::max(maximalDepth, depth); } - // If we are not supposed to eliminate the entry states, we need to take them out of the set of - // remaining states. - // if (!eliminateEntryStates) { - // remainingStates &= ~entryStates; - // } - // - // Now that we eliminated all non-trivial sub-SCCs, we need to take care of trivial sub-SCCs. - // Therefore, we need to eliminate all states. - // for (auto const& state : remainingStates) { - // eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); - // } } else { // In this case, we perform simple state elimination in the current SCC. - storm::storage::BitVector remainingStates = scc; - -// if (eliminateEntryStates) { - remainingStates &= ~entryStates; -// } + storm::storage::BitVector remainingStates = scc & ~entryStates; // Eliminate the remaining states. for (auto const& state : remainingStates) { eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); } - - // Finally, eliminate the entry states (if we are allowed to do so). - if (eliminateEntryStates) { - for (auto state : entryStates) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); - } + } + + // Finally, eliminate the entry states (if we are required to do so). + STORM_LOG_DEBUG("Finally, eliminating/adding entry states."); + if (eliminateEntryStates) { + for (auto state : entryStates) { + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); + } + } else { + for (auto state : entryStates) { + entryStateQueue.push_back(state); } } + + return maximalDepth; } static int chunkCounter = 0; @@ -178,9 +235,10 @@ namespace storm { void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions) { ++counter; + STORM_LOG_DEBUG("Eliminating state " << counter << "."); if (counter > matrix.getNumberOfRows() / 10) { ++chunkCounter; - std::cout << "Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl; + STORM_PRINT_AND_LOG("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl); counter = 0; } @@ -209,6 +267,8 @@ namespace storm { oneStepProbabilities[state] = simplify(oneStepProbabilities[state] * loopProbability); } + STORM_LOG_DEBUG((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop.")); + // Now connect the predecessors of the state being eliminated with its successors. typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); for (auto const& predecessorEntry : currentStatePredecessors) { @@ -279,6 +339,8 @@ namespace storm { // Add the probabilities to go to a target state in just one step. oneStepProbabilities[predecessor] = simplify(oneStepProbabilities[predecessor] + simplify(multiplyFactor * oneStepProbabilities[state])); + + STORM_LOG_DEBUG("Fixed new next-state probabilities of predecessor states."); } // Finally, we need to add the predecessor to the set of predecessors of every successor. @@ -325,8 +387,9 @@ namespace storm { // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); + } - + STORM_LOG_DEBUG("Fixed predecessor lists of successor states."); // Clear the eliminated row to reduce memory consumption. currentStateSuccessors.clear(); diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index b1e19c295..f2ca965b0 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -1,4 +1,9 @@ +#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSESCCMODELCHECKER_H_ +#define STORM_MODELCHECKER_REACHABILITY_SPARSESCCMODELCHECKER_H_ + +#include "src/storage/sparse/StateType.h" #include "src/models/Dtmc.h" +#include "src/properties/prctl/PrctlFilter.h" namespace storm { namespace modelchecker { @@ -29,10 +34,10 @@ namespace storm { template class SparseSccModelChecker { public: - static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula); private: - static void treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level); + static uint_fast64_t treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, std::vector& entryStateQueue); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions); static bool eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions); @@ -40,6 +45,9 @@ namespace storm { static const uint_fast64_t maximalSccSize = 1000; }; - } - } -} \ No newline at end of file + + } // namespace reachability + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSESCCMODELCHECKER_H_ */ diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 26fb6070d..a2e5c2a43 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -25,6 +25,7 @@ namespace storm { this->addModule(std::unique_ptr(new modules::NativeEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::GlpkSettings(*this))); this->addModule(std::unique_ptr(new modules::GurobiSettings(*this))); + this->addModule(std::unique_ptr(new modules::ParametricSettings(*this))); } SettingsManager::~SettingsManager() { @@ -496,5 +497,9 @@ namespace storm { storm::settings::modules::GurobiSettings const& gurobiSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::GurobiSettings::moduleName)); } + + storm::settings::modules::ParametricSettings const& parametricSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::ParametricSettings::moduleName)); + } } } \ No newline at end of file diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 41383f336..660d334f8 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -27,6 +27,7 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GlpkSettings.h" #include "src/settings/modules/GurobiSettings.h" +#include "src/settings/modules/ParametricSettings.h" #include "src/utility/macros.h" #include "src/exceptions/OptionParserException.h" @@ -296,6 +297,13 @@ namespace storm { */ storm::settings::modules::GurobiSettings const& gurobiSettings(); + /*! + * Retrieves the settings for parametric model checking. + * + * @return An object that allows accessing the settings for parameteric model checking. + */ + storm::settings::modules::ParametricSettings const& parametricSettings(); + } // namespace settings } // namespace storm diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 585bcfdfb..44170063b 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -90,7 +90,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); } diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp new file mode 100644 index 000000000..0a5c8b9af --- /dev/null +++ b/src/settings/modules/ParametricSettings.cpp @@ -0,0 +1,22 @@ +#include "src/settings/modules/ParametricSettings.h" + +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string ParametricSettings::moduleName = "parametric"; + const std::string ParametricSettings::entryStatesLastOptionName = "entrylast"; + + ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); + } + + bool ParametricSettings::isEliminateEntryStatesLastSet() const { + return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet(); + } + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/ParametricSettings.h b/src/settings/modules/ParametricSettings.h new file mode 100644 index 000000000..eaf0a6e9c --- /dev/null +++ b/src/settings/modules/ParametricSettings.h @@ -0,0 +1,39 @@ +#ifndef STORM_SETTINGS_MODULES_PARAMETRICSETTINGS_H_ +#define STORM_SETTINGS_MODULES_PARAMETRICSETTINGS_H_ + +#include "src/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for parametric model checking. + */ + class ParametricSettings : public ModuleSettings { + public: + /*! + * Creates a new set of parametric model checking settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ + ParametricSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether the option to eliminate entry states in the very end is set. + * + * @return True iff the option is set. + */ + bool isEliminateEntryStatesLastSet() const; + + const static std::string moduleName; + + private: + const static std::string entryStatesLastOptionName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_PARAMETRICSETTINGS_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index 25fd5a2bf..1b0056988 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/src/storage/expressions/ExpressionEvaluation.h @@ -82,7 +82,6 @@ namespace expressions { mValue *= visitor->value(); break; case BinaryNumericalFunctionExpression::OperatorType::Divide: - assert(false); mValue /= visitor->value(); break; default: @@ -125,7 +124,9 @@ namespace expressions { } virtual void visit(IntegerLiteralExpression const* expression) { - mValue = T(typename T::CoeffType(std::to_string(expression->getValue()), 10)); + // mValue = T(typename T::CoeffType(std::to_string(expression->getValue()), 10)); + + mValue = T(expression->getValue()); } virtual void visit(DoubleLiteralExpression const* expression) { diff --git a/src/storage/parameters.h b/src/storage/parameters.h index 852215b83..d718d9c64 100644 --- a/src/storage/parameters.h +++ b/src/storage/parameters.h @@ -10,7 +10,7 @@ namespace storm { - typedef carl::MultivariatePolynomial Polynomial; + typedef carl::MultivariatePolynomial Polynomial; //typedef Parameter carl::Variable ; typedef carl::RationalFunction RationalFunction; } diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 7803501f1..092378256 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -35,15 +35,15 @@ int main(const int argc, const char** argv) { // Program Translation Time Measurement, End std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); - std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl; + std::cout << "Parsing and translating the model took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; storm::modelchecker::reachability::SparseSccModelChecker modelChecker; - storm::storage::BitVector trueStates(model->getNumberOfStates(), true); - storm::storage::BitVector targetStates = model->getLabeledStates("target"); -// storm::storage::BitVector targetStates = model->getLabeledStates("one"); -// storm::storage::BitVector targetStates = model->getLabeledStates("elected"); - storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as>(), trueStates, targetStates); - std::cout << "computed value " << value << std::endl; + + STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); + std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); + + storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as>(), filterFormula); + STORM_PRINT_AND_LOG(std::endl << "computed value " << value << std::endl); // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp(); diff --git a/src/utility/cli.h b/src/utility/cli.h index 2be0bd112..354dba208 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -60,10 +60,11 @@ namespace storm { */ void initializeLogger() { logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; + logger.setLogLevel(loglevel); log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); consoleLogAppender->setName("mainConsoleAppender"); - consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); + consoleLogAppender->setThreshold(loglevel); consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); logger.addAppender(consoleLogAppender); } @@ -285,7 +286,11 @@ namespace storm { } void processOptions() { - storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); + if (storm::settings::debugSettings().isLogfileSet()) { + initializeFileLogging(); + } + + storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); // Start by parsing/building the model. std::shared_ptr> model = buildModel();