From 0473d1a757b1ea295a8a83ce543365d006408ba4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 19 Aug 2013 14:17:50 +0200 Subject: [PATCH] Fixed a lot of issues with the IR and the explicit state space generator. Former-commit-id: fe80aaaf0f8540118153cf2bc1ef5795d3accfce --- .../gmm-4.2/include/gmm/gmm_solver_gmres.h | 24 +++--- .../3rdparty/ltl2dstar-0.5.1/src/Makefile | 4 +- src/adapters/ExplicitModelAdapter.cpp | 78 +++++++++---------- src/adapters/ExplicitModelAdapter.h | 6 +- src/ir/Module.cpp | 8 ++ src/ir/Module.h | 8 ++ src/ir/expressions/BaseExpression.cpp | 2 +- .../BinaryNumericalFunctionExpression.cpp | 4 +- .../expressions/IntegerConstantExpression.cpp | 4 + .../expressions/IntegerConstantExpression.h | 2 + .../expressions/IntegerLiteralExpression.cpp | 4 + src/ir/expressions/IntegerLiteralExpression.h | 2 + .../UnaryNumericalFunctionExpression.cpp | 2 +- src/ir/expressions/VariableExpression.cpp | 28 ++++--- src/parser/prismparser/VariableState.cpp | 5 ++ src/utility/Settings.cpp | 2 +- 16 files changed, 112 insertions(+), 71 deletions(-) diff --git a/resources/3rdparty/gmm-4.2/include/gmm/gmm_solver_gmres.h b/resources/3rdparty/gmm-4.2/include/gmm/gmm_solver_gmres.h index caaa37e2a..282974f4d 100644 --- a/resources/3rdparty/gmm-4.2/include/gmm/gmm_solver_gmres.h +++ b/resources/3rdparty/gmm-4.2/include/gmm/gmm_solver_gmres.h @@ -126,20 +126,20 @@ t_ref = MPI_Wtime(); size_type i = 0; inner.init(); do { - mult(A, KS[i], u); - mult(M, u, KS[i+1]); - orthogonalize(KS, mat_col(H, i), i); - R a = gmm::vect_norm2(KS[i+1]); - H(i+1, i) = T(a); - gmm::scale(KS[i+1], T(1) / a); - for (size_type k = 0; k < i; ++k) - Apply_Givens_rotation_left(H(k,i), H(k+1,i), c_rot[k], s_rot[k]); + mult(A, KS[i], u); + mult(M, u, KS[i+1]); + orthogonalize(KS, mat_col(H, i), i); + R a = gmm::vect_norm2(KS[i+1]); + H(i+1, i) = T(a); + gmm::scale(KS[i+1], T(1) / a); + for (size_type k = 0; k < i; ++k) + Apply_Givens_rotation_left(H(k,i), H(k+1,i), c_rot[k], s_rot[k]); - Givens_rotation(H(i,i), H(i+1,i), c_rot[i], s_rot[i]); - Apply_Givens_rotation_left(H(i,i), H(i+1,i), c_rot[i], s_rot[i]); - Apply_Givens_rotation_left(s[i], s[i+1], c_rot[i], s_rot[i]); + Givens_rotation(H(i,i), H(i+1,i), c_rot[i], s_rot[i]); + Apply_Givens_rotation_left(H(i,i), H(i+1,i), c_rot[i], s_rot[i]); + Apply_Givens_rotation_left(s[i], s[i+1], c_rot[i], s_rot[i]); - ++inner, ++outer, ++i; + ++inner, ++outer, ++i; } while (! inner.finished(gmm::abs(s[i]))); upper_tri_solve(H, s, i, false); diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/Makefile b/resources/3rdparty/ltl2dstar-0.5.1/src/Makefile index fb906d693..52032e108 100644 --- a/resources/3rdparty/ltl2dstar-0.5.1/src/Makefile +++ b/resources/3rdparty/ltl2dstar-0.5.1/src/Makefile @@ -1,8 +1,8 @@ -GPP = clang++ +GPP = clang++ -std=c++11 -stdlib=libc++ #DEFINES = #DEBUGFLAGS = -g -fno-default-inline -fkeep-inline-functions -OPTFLAGS = -O3 -fkeep-inline-functions +OPTFLAGS = -O4 -fkeep-inline-functions LIBRARY = libltl2dstar.a EXECUTABLE = ltl2dstar diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index aee3208a7..1d22e27cb 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -123,9 +123,9 @@ namespace adapters { } storm::models::AtomicPropositionsLabeling ExplicitModelAdapter::getStateLabeling(std::map> labels) { - storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size()); + storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size() + 1); // Initialize labeling. - for (auto it: labels) { + for (auto it : labels) { results.addAtomicProposition(it.first); } for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { @@ -136,6 +136,15 @@ namespace adapters { } } } + + // Also label the initial state. + results.addAtomicProposition("init"); + StateType* initialState = this->getInitialState(); + uint_fast64_t initialIndex = this->stateToIndexMap[initialState]; + std::cout << initialIndex << std::endl; + results.addAtomicPropositionToState("init", initialIndex); + delete initialState; + return results; } @@ -188,8 +197,12 @@ namespace adapters { for (uint_fast64_t i = 0; i < this->program.getNumberOfModules(); ++i) { storm::ir::Module const& module = this->program.getModule(i); + // If the module has no command labeled with the given action, skip this module. + if (!module.hasAction(action)) { + continue; + } + std::set const& ids = module.getCommandsByAction(action); - if (ids.size() == 0) continue; std::list commands; // Look up commands by their id. Add, if guard holds. @@ -229,32 +242,24 @@ namespace adapters { } /*! - * Generates all initial states and adds them to allStates. + * Generates the initial state. */ - void ExplicitModelAdapter::generateInitialStates() { - // Create a fresh state which can hold as many boolean and integer variables as there are. - this->allStates.clear(); - this->allStates.push_back(new StateType()); - this->allStates[0]->first.resize(this->booleanVariables.size()); - this->allStates[0]->second.resize(this->integerVariables.size()); + StateType* ExplicitModelAdapter::getInitialState() { + StateType* initialState = new StateType(); + initialState->first.resize(this->booleanVariables.size()); + initialState->second.resize(this->integerVariables.size()); // Start with boolean variables. for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) { // Check if an initial value is given if (this->booleanVariables[i].getInitialValue().get() == nullptr) { - // No initial value was given. - uint_fast64_t size = this->allStates.size(); - for (uint_fast64_t pos = 0; pos < size; pos++) { - // Duplicate each state, one with true and one with false. - this->allStates.push_back(new StateType(*this->allStates[pos])); - std::get<0>(*this->allStates[pos])[i] = false; - std::get<0>(*this->allStates[size + pos])[i] = true; - } + // If no initial value was given, we assume that the variable is initially false. + std::get<0>(*initialState)[i] = false; } else { // Initial value was given. - bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(this->allStates[0]); + bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(nullptr); for (auto it : this->allStates) { - std::get<0>(*it)[i] = initialValue; + std::get<0>(*initialState)[i] = initialValue; } } } @@ -262,30 +267,18 @@ namespace adapters { for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { // Check if an initial value was given. if (this->integerVariables[i].getInitialValue().get() == nullptr) { - // No initial value was given. - uint_fast64_t size = this->allStates.size(); - int_fast64_t lower = this->integerVariables[i].getLowerBound()->getValueAsInt(this->allStates[0]); - int_fast64_t upper = this->integerVariables[i].getUpperBound()->getValueAsInt(this->allStates[0]); - - // Duplicate all states for all values in variable interval. - for (int_fast64_t value = lower; value <= upper; value++) { - for (uint_fast64_t pos = 0; pos < size; pos++) { - // If value is lower bound, we reuse the existing state, otherwise we create a new one. - if (value > lower) this->allStates.push_back(new StateType(*this->allStates[pos])); - // Set value to current state. - std::get<1>(*this->allStates[(value - lower) * size + pos])[i] = value; - } - } - } else { + // No initial value was given, so we assume that the variable initially has the least value it can take. + std::get<1>(*initialState)[i] = this->integerVariables[i].getLowerBound()->getValueAsInt(nullptr); + } else { // Initial value was given. - int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(this->allStates[0]); + int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(nullptr); for (auto it : this->allStates) { - std::get<1>(*it)[i] = initialValue; + std::get<1>(*initialState)[i] = initialValue; } } } - stateToIndexMap[this->allStates[0]] = 0; - LOG4CPLUS_DEBUG(logger, "Generated " << this->allStates.size() << " initial states."); + LOG4CPLUS_DEBUG(logger, "Generated initial state."); + return initialState; } /*! @@ -390,7 +383,7 @@ namespace adapters { for (auto it : resultStates) { // Apply the new update and get resulting state. StateType* newState = this->applyUpdate(it.first, this->allStates[stateID], update); - probSum += update.getLikelihoodExpression()->getValueAsDouble(it.first); + probSum += it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); // Insert the new state into newStates array. // Take care of calculation of likelihood, combine identical states. auto s = newStates.find(newState); @@ -542,7 +535,10 @@ namespace adapters { LOG4CPLUS_DEBUG(logger, "Starting to create transition map from program..."); this->clearInternalState(); - this->generateInitialStates(); + this->allStates.clear(); + this->allStates.push_back(this->getInitialState()); + stateToIndexMap[this->allStates[0]] = 0; + for (uint_fast64_t curIndex = 0; curIndex < this->allStates.size(); curIndex++) { this->addUnlabeledTransitions(curIndex, this->transitionMap[curIndex]); diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 87af1048a..18b07b942 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -149,9 +149,11 @@ private: std::unique_ptr>> getActiveCommandsByAction(StateType const * state, std::string& action); /*! - * Generates all initial states and adds them to allStates. + * Generates the initial state. + * + * @return The initial state. */ - void generateInitialStates(); + StateType* getInitialState(); /*! * Retrieves the state id of the given state. diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index 166a6bbda..e9d904dbf 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -155,6 +155,14 @@ namespace storm { return this->actions; } + bool Module::hasAction(std::string const& action) const { + auto const& actionEntry = this->actions.find(action); + if (actionEntry != this->actions.end()) { + return true; + } + return false; + } + std::set const& Module::getCommandsByAction(std::string const& action) const { auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action); if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { diff --git a/src/ir/Module.h b/src/ir/Module.h index 1f7625a4e..f79fa14a0 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -168,6 +168,14 @@ namespace storm { */ std::set const& getActions() const; + /*! + * Retrieves whether or not this module contains a command labeled with the given action. + * + * @param action The action name to look for in this module. + * @return True if the module has at least one command labeled with the given action. + */ + bool hasAction(std::string const& action) const; + /*! * Retrieves the indices of all commands within this module that are labelled by the given action. * diff --git a/src/ir/expressions/BaseExpression.cpp b/src/ir/expressions/BaseExpression.cpp index 18b70d392..a6b90fe56 100644 --- a/src/ir/expressions/BaseExpression.cpp +++ b/src/ir/expressions/BaseExpression.cpp @@ -45,7 +45,7 @@ namespace storm { } double BaseExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { - if (type != bool_) { + if (type != double_ && type != int_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'double'."; } diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp index 920c72126..e3acde6fa 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp @@ -47,9 +47,9 @@ namespace storm { << "Unknown numeric binary operator: '" << functionType << "'."; } } - + double BinaryNumericalFunctionExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { - if (this->getType() != double_) { + if (this->getType() != double_ && this->getType() != int_) { BaseExpression::getValueAsDouble(variableValues); } diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp index 29cc3f1eb..4daa4c244 100644 --- a/src/ir/expressions/IntegerConstantExpression.cpp +++ b/src/ir/expressions/IntegerConstantExpression.cpp @@ -26,6 +26,10 @@ namespace storm { return std::shared_ptr(new IntegerConstantExpression(*this)); } + double IntegerConstantExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { + return getValueAsInt(variableValues); + } + int_fast64_t IntegerConstantExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index dd77cce2a..399c04bca 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -35,6 +35,8 @@ namespace storm { virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; virtual void accept(ExpressionVisitor* visitor) override; diff --git a/src/ir/expressions/IntegerLiteralExpression.cpp b/src/ir/expressions/IntegerLiteralExpression.cpp index 8cb799376..70432c6c5 100644 --- a/src/ir/expressions/IntegerLiteralExpression.cpp +++ b/src/ir/expressions/IntegerLiteralExpression.cpp @@ -26,6 +26,10 @@ namespace storm { return std::shared_ptr(new IntegerLiteralExpression(this->value)); } + double IntegerLiteralExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { + return value; + } + int_fast64_t IntegerLiteralExpression::getValueAsInt(std::pair, std::vector> const* variableValues) const { return value; } diff --git a/src/ir/expressions/IntegerLiteralExpression.h b/src/ir/expressions/IntegerLiteralExpression.h index 488456a3c..eeaa4d78d 100644 --- a/src/ir/expressions/IntegerLiteralExpression.h +++ b/src/ir/expressions/IntegerLiteralExpression.h @@ -35,6 +35,8 @@ namespace storm { virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; virtual void accept(ExpressionVisitor* visitor) override; diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp index 6aa0f380b..787ff4c68 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp @@ -37,7 +37,7 @@ namespace storm { } double UnaryNumericalFunctionExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { - if (this->getType() != double_) { + if (this->getType() != double_ && this->getType() != int_) { BaseExpression::getValueAsDouble(variableValues); } diff --git a/src/ir/expressions/VariableExpression.cpp b/src/ir/expressions/VariableExpression.cpp index 5bf0884fb..a38529c8b 100644 --- a/src/ir/expressions/VariableExpression.cpp +++ b/src/ir/expressions/VariableExpression.cpp @@ -30,9 +30,17 @@ namespace storm { // Perform the proper cloning. auto renamingPair = renaming.find(this->variableName); if (renamingPair != renaming.end()) { - return variableState.getVariableExpression(renamingPair->second); + if (this->getType() == int_) { + return variableState.getIntegerVariableExpression(renamingPair->second); + } else { + return variableState.getBooleanVariableExpression(renamingPair->second); + } } else { - return variableState.getVariableExpression(this->variableName); + if (this->getType() == int_) { + return variableState.getIntegerVariableExpression(this->variableName); + } else { + return variableState.getBooleanVariableExpression(this->variableName); + } } } @@ -52,8 +60,7 @@ namespace storm { if (variableValues != nullptr) { return variableValues->second[globalIndex]; } else { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" - << " involving variables without variable values."; + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression involving variables without variable values."; } } @@ -65,18 +72,21 @@ namespace storm { if (variableValues != nullptr) { return variableValues->first[globalIndex]; } else { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" - << " involving variables without variable values."; + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression involving variables without variable values."; } } double VariableExpression::getValueAsDouble(std::pair, std::vector> const* variableValues) const { - if (this->getType() != double_) { + if (this->getType() != double_ && this->getType() != int_) { BaseExpression::getValueAsDouble(variableValues); } - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression with " - << " variable '" << variableName << "' of type double."; + // Because only int variables can deliver a double value, we only need to check them. + if (variableValues != nullptr) { + return variableValues->second[globalIndex]; + } else { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression with variable '" << variableName << "' of type double."; + } } std::string const& VariableExpression::getVariableName() const { diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index 9ee35dd02..b5f61648e 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -124,6 +124,11 @@ std::shared_ptr VariableState::getVariableExpression(std::st if (variableExpression != nullptr) { return *variableExpression; } + + variableExpression = this->booleanVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; + } LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist."; } diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 97e50e562..ebe98ed93 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -165,7 +165,7 @@ void Settings::initDescriptions() { ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") - ("lemethod", boost::program_options::value()->default_value("bicgstab")->notifier(&storm::settings::validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, qmr, lscg, gmres, jacobi}.") + ("lemethod", boost::program_options::value()->default_value("gmres")->notifier(&storm::settings::validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, qmr, lscg, gmres, jacobi}.") ("maxiter", boost::program_options::value()->default_value(10000), "Sets the maximal number of iterations for iterative equation solving.") ("precision", boost::program_options::value()->default_value(1e-6), "Sets the precision for iterative equation solving.") ("precond", boost::program_options::value()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioning technique for linear equation solving. Must be in {ilu, diagonal, ildlt, none}.")