From ce36601f7ccc8eadeada8a334e07d31ff1c15f1a Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 6 Jan 2017 14:28:04 +0100 Subject: [PATCH] fixed gmp dependency (lib), fixed parser to reject formulas that appear later in the PRISM file --- resources/3rdparty/CMakeLists.txt | 5 +++-- src/storm/parser/PrismParser.cpp | 6 +++--- src/storm/storage/prism/Constant.cpp | 6 +++--- src/storm/storage/prism/Constant.h | 3 --- src/storm/storage/prism/Program.cpp | 27 +++++++++++++++++++-------- src/storm/utility/dd.cpp | 4 ++++ 6 files changed, 32 insertions(+), 19 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 8c21ddd75..d3e7f915e 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -319,10 +319,11 @@ if (ENABLE_MSAT) list(APPEND STORM_LINK_LIBRARIES "mathsat") if(GMP_FOUND) include_directories("${GMP_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES "gmp") + list(APPEND STORM_LINK_LIBRARIES ${GMP_LIBRARY}) elseif(MPIR_FOUND) include_directories("${GMP_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx") + list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIR_LIBRARY}) + list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIRXX_LIBRARY}) else(GMP_FOUND) message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") endif(GMP_FOUND) diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 564d83187..73b42fd45 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -420,11 +420,11 @@ namespace storm { } storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) { - if (!this->secondRun) { + // Only register formula in second run. This prevents the parser from accepting formulas that depend on future + // formulas. + if (this->secondRun) { STORM_LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'."); this->identifiers_.add(formulaName, expression); - } else { - this->identifiers_.at(formulaName) = expression; } return storm::prism::Formula(formulaName, expression, this->getFilename()); } diff --git a/src/storm/storage/prism/Constant.cpp b/src/storm/storage/prism/Constant.cpp index cb820cf19..cc7e3fad4 100644 --- a/src/storm/storage/prism/Constant.cpp +++ b/src/storm/storage/prism/Constant.cpp @@ -4,11 +4,11 @@ namespace storm { namespace prism { - Constant::Constant(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), defined(true), expression(expression) { + Constant::Constant(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), expression(expression) { // Intentionally left empty. } - Constant::Constant(storm::expressions::Variable const& variable, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), defined(false), expression() { + Constant::Constant(storm::expressions::Variable const& variable, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), expression() { // Intentionally left empty. } @@ -25,7 +25,7 @@ namespace storm { } bool Constant::isDefined() const { - return this->defined; + return this->expression.isInitialized(); } storm::expressions::Expression const& Constant::getExpression() const { diff --git a/src/storm/storage/prism/Constant.h b/src/storm/storage/prism/Constant.h index 608aac74a..fad235e5c 100644 --- a/src/storm/storage/prism/Constant.h +++ b/src/storm/storage/prism/Constant.h @@ -90,9 +90,6 @@ namespace storm { // The expression variable associated with the constant. storm::expressions::Variable variable; - // A flag that stores whether or not the constant is defined. - bool defined; - // The expression that defines the constant (in case it is defined). storm::expressions::Expression expression; }; diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index bc44cf59b..210077d04 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1292,18 +1292,29 @@ namespace storm { } } + for (auto const& variable : module.getBooleanVariables()) { + if (booleanVars.find(variable.getExpressionVariable()) != booleanVars.end()) { + if (variable.hasInitialValue()) { + newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression()); + } else { + newBooleanVars.push_back(variable); + } + } + } + for (auto const& variable : module.getIntegerVariables()) { + if (integerVars.find(variable.getExpressionVariable()) != integerVars.end()) { + if (variable.hasInitialValue()) { + newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression()); + } else { + newIntegerVars.push_back(variable); + } + } + } + newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands); // Determine the set of action indices that have been deleted entirely. std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin())); - - for (auto const& entry : booleanVars) { - newConstants.emplace_back(entry.first, entry.second); - } - - for (auto const& entry : integerVars) { - newConstants.emplace_back(entry.first, entry.second); - } } // If we have to delete whole actions, do so now. diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 362c731f3..cf7a9add6 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -11,6 +11,9 @@ namespace storm { template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables) { + + STORM_LOG_TRACE("Computing reachable states: transition matrix BDD has " << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount() << " non-zero(s), " << initialStates.getNonZeroCount() << " initial states)."); + auto start = std::chrono::high_resolution_clock::now(); storm::dd::Bdd reachableStates = initialStates; @@ -30,6 +33,7 @@ namespace storm { reachableStates |= newReachableStates; ++iteration; + STORM_LOG_TRACE("Iteration " << iteration << " of reachability computation completed: " << reachableStates.getNonZeroCount() << " reachable states found."); } while (changed); auto end = std::chrono::high_resolution_clock::now();