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();