From 92932fced10eecd82b93c5fedcfea557b2e49b2f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 Sep 2016 17:12:30 +0200 Subject: [PATCH 1/4] support for initial constructs in PRISM programs Former-commit-id: 0c8132aa432a46bff8de64792bd9a9204efd2ce3 --- src/parser/PrismParser.cpp | 18 +-- src/parser/PrismParser.h | 6 +- src/storage/prism/BooleanVariable.cpp | 16 ++- src/storage/prism/BooleanVariable.h | 2 + src/storage/prism/IntegerVariable.cpp | 14 ++- src/storage/prism/IntegerVariable.h | 2 + src/storage/prism/Module.cpp | 11 +- src/storage/prism/Module.h | 5 + src/storage/prism/Program.cpp | 171 ++++++++++++++++---------- src/storage/prism/Program.h | 7 +- src/storage/prism/Variable.cpp | 12 +- src/storage/prism/Variable.h | 27 ++-- 12 files changed, 199 insertions(+), 92 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index f9f4350b9..d3e5191e2 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -105,10 +105,10 @@ namespace storm { formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition.name("formula definition"); - booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)]; + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > -((qi::lit("init") > expressionParser[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; booleanVariableDefinition.name("boolean variable definition"); - integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; integerVariableDefinition.name("integer variable definition"); variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]); @@ -210,7 +210,7 @@ namespace storm { moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)]; moduleDefinitionList.name("module list"); - start = (qi::eps + start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)] > modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1] > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] @@ -278,7 +278,7 @@ namespace storm { return true; } - bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { + bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); if (globalProgramInformation.hasInitialConstruct) { return false; @@ -587,7 +587,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed."); - booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1))); } // Rename the integer variables. @@ -596,7 +596,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed."); - integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), this->getFilename(), get_line(qi::_1))); } // Rename commands. @@ -642,7 +642,11 @@ namespace storm { } storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { - return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::optional(storm::prism::InitialConstruct(manager->boolean(false))), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + } + + void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { + globalProgramInformation.hasInitialConstruct = false; } } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 84a5b601e..2a83e3193 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -188,7 +188,7 @@ namespace storm { // Rules for variable definitions. qi::rule&, std::vector&), Skipper> variableDefinition; - qi::rule booleanVariableDefinition; + qi::rule, Skipper> booleanVariableDefinition; qi::rule, Skipper> integerVariableDefinition; // Rules for command definitions. @@ -241,7 +241,7 @@ namespace storm { // Helper methods used in the grammar. bool isValidIdentifier(std::string const& identifier); - bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); + bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addSystemCompositionConstruct(std::shared_ptr const& composition, GlobalProgramInformation& globalProgramInformation); @@ -274,6 +274,8 @@ namespace storm { storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; + void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const; + // An error handler function. phoenix::function handler; }; diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index c38812ec6..422b2266f 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -1,5 +1,7 @@ #include "src/storage/prism/BooleanVariable.h" +#include "src/storage/expressions/ExpressionManager.h" + namespace storm { namespace prism { BooleanVariable::BooleanVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, initialValueExpression, false, filename, lineNumber) { @@ -7,11 +9,21 @@ namespace storm { } BooleanVariable BooleanVariable::substitute(std::map const& substitution) const { - return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber()); + } + + void BooleanVariable::createMissingInitialValue() { + if (!this->hasInitialValue()) { + this->setInitialValueExpression(this->getExpressionVariable().getManager().boolean(false)); + } } std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { - stream << variable.getName() << ": bool init " << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": bool"; + if (variable.hasInitialValue()) { + stream << " init " << variable.getInitialValueExpression(); + } + stream << ";"; return stream; } diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h index 5b43e191c..c5c3ba8e4 100644 --- a/src/storage/prism/BooleanVariable.h +++ b/src/storage/prism/BooleanVariable.h @@ -37,6 +37,8 @@ namespace storm { */ BooleanVariable substitute(std::map const& substitution) const; + virtual void createMissingInitialValue() override; + friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable); }; diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index b2306ece0..8b60b0e56 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -19,11 +19,21 @@ namespace storm { } IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { - return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->getFilename(), this->getLineNumber()); + } + + void IntegerVariable::createMissingInitialValue() { + if (!this->hasInitialValue()) { + this->setInitialValueExpression(this->getLowerBoundExpression()); + } } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { - stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << " init " << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]"; + if (variable.hasInitialValue()) { + stream << " init " << variable.getInitialValueExpression(); + } + stream << ";"; return stream; } } // namespace prism diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h index fc1c6ecf5..335c2ce05 100644 --- a/src/storage/prism/IntegerVariable.h +++ b/src/storage/prism/IntegerVariable.h @@ -60,6 +60,8 @@ namespace storm { */ IntegerVariable substitute(std::map const& substitution) const; + virtual void createMissingInitialValue() override; + friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable); private: diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 755c4c78a..095ac3e11 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -42,7 +42,7 @@ namespace storm { std::vector const& Module::getIntegerVariables() const { return this->integerVariables; } - + std::set Module::getAllExpressionVariables() const { std::set result; for (auto const& var : this->getBooleanVariables()) { @@ -221,6 +221,15 @@ namespace storm { return true; } + void Module::createMissingInitialValues() { + for (auto& variable : booleanVariables) { + variable.createMissingInitialValue(); + } + for (auto& variable : integerVariables) { + variable.createMissingInitialValue(); + } + } + std::ostream& operator<<(std::ostream& stream, Module const& module) { stream << "module " << module.getName() << std::endl; for (auto const& booleanVariable : module.getBooleanVariables()) { diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index df8a61c21..c3179b407 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -225,6 +225,11 @@ namespace storm { */ bool containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const; + /*! + * Equips all of the modules' variables without initial values with initial values based on their type. + */ + void createMissingInitialValues(); + friend std::ostream& operator<<(std::ostream& stream, Module const& module); private: diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index cdc3d323a..3cf9df8ae 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -152,20 +152,26 @@ namespace storm { if (initialConstruct) { this->initialConstruct = initialConstruct.get(); } else { + // First, add all missing initial values. + this->createMissingInitialValues(); + for (auto& modules : this->modules) { + modules.createMissingInitialValues(); + } + // Create a new initial construct if none was given. storm::expressions::Expression newInitialExpression = manager->boolean(true); - for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { + for (auto& booleanVariable : this->getGlobalBooleanVariables()) { newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); } - for (auto const& integerVariable : this->getGlobalIntegerVariables()) { + for (auto& integerVariable : this->getGlobalIntegerVariables()) { newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); } - for (auto const& module : this->getModules()) { - for (auto const& booleanVariable : module.getBooleanVariables()) { + for (auto& module : this->getModules()) { + for (auto& booleanVariable : module.getBooleanVariables()) { newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); } - for (auto const& integerVariable : module.getIntegerVariables()) { + for (auto& integerVariable : module.getIntegerVariables()) { newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); } } @@ -241,13 +247,17 @@ namespace storm { // Now check initial value expressions of global variables. for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { - if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { - return false; + if (booleanVariable.hasInitialValue()) { + if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + return false; + } } } for (auto const& integerVariable : this->getGlobalIntegerVariables()) { - if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { - return false; + if (integerVariable.hasInitialValue()) { + if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + return false; + } } if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { return false; @@ -809,18 +819,20 @@ namespace storm { // Now we check the variable declarations. We start with the global variables. std::set variables; for (auto const& variable : this->getGlobalBooleanVariables()) { - // Check the initial value of the variable. - std::set containedVariables = variable.getInitialValueExpression().getVariables(); - std::set illegalVariables; - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - bool isValid = illegalVariables.empty(); - - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasInitialValue()) { + // Check the initial value of the variable. + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } // Record the new identifier for future checks. @@ -855,16 +867,18 @@ namespace storm { STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - // Check the initial value of the variable. - containedVariables = variable.getInitialValueExpression().getVariables(); - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasInitialValue()) { + // Check the initial value of the variable. + containedVariables = variable.getInitialValueExpression().getVariables(); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } // Record the new identifier for future checks. @@ -877,17 +891,19 @@ namespace storm { // Now go through the variables of the modules. for (auto const& module : this->getModules()) { for (auto const& variable : module.getBooleanVariables()) { - // Check the initial value of the variable. - std::set containedVariables = variable.getInitialValueExpression().getVariables(); - std::set illegalVariables; - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - bool isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasInitialValue()) { + // Check the initial value of the variable. + std::set containedVariables = variable.getInitialValueExpression().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + bool isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } // Record the new identifier for future checks. @@ -920,17 +936,19 @@ namespace storm { STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - // Check the initial value of the variable. - containedVariables = variable.getInitialValueExpression().getVariables(); - illegalVariables.clear(); - std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); - isValid = illegalVariables.empty(); - if (!isValid) { - std::vector illegalVariableNames; - for (auto const& var : illegalVariables) { - illegalVariableNames.push_back(var.getName()); + if (variable.hasInitialValue()) { + // Check the initial value of the variable. + containedVariables = variable.getInitialValueExpression().getVariables(); + illegalVariables.clear(); + std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin())); + isValid = illegalVariables.empty(); + if (!isValid) { + std::vector illegalVariableNames; + for (auto const& var : illegalVariables) { + illegalVariableNames.push_back(var.getName()); + } + STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } - STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << "."); } // Record the new identifier for future checks. @@ -1571,7 +1589,7 @@ namespace storm { } storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager); storm::expressions::Expression globalInitialStatesExpression; - + // Add all constants of the PRISM program to the JANI model. for (auto const& constant : constants) { janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional(constant.getExpression()) : boost::none)); @@ -1580,13 +1598,17 @@ namespace storm { // Add all global variables of the PRISM program to the JANI model. for (auto const& variable : globalIntegerVariables) { janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); - storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); - globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + if (variable.hasInitialValue()) { + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + } } for (auto const& variable : globalBooleanVariables) { janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable())); - storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); - globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + if (variable.hasInitialValue()) { + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + } } // Add all actions of the PRISM program to the JANI model. @@ -1598,7 +1620,7 @@ namespace storm { } // Because of the rules of JANI, we have to make all variables of modules global that are read by other modules. - + // Create a mapping from variables to the indices of module indices that write/read the variable. std::map> variablesToAccessingModuleIndices; for (uint_fast64_t index = 0; index < modules.size(); ++index) { @@ -1627,20 +1649,24 @@ namespace storm { for (auto const& module : modules) { storm::jani::Automaton automaton(module.getName()); storm::expressions::Expression initialStatesExpression; - + for (auto const& variable : module.getIntegerVariables()) { storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; // If there is exactly one module reading and writing the variable, we can make the variable local to this module. if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { automaton.addBoundedIntegerVariable(newIntegerVariable); - storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); - initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; + if (variable.hasInitialValue()) { + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; + } } else if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. janiModel.addBoundedIntegerVariable(newIntegerVariable); - storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); - globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + if (variable.hasInitialValue()) { + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + } } } for (auto const& variable : module.getBooleanVariables()) { @@ -1649,13 +1675,17 @@ namespace storm { // If there is exactly one module reading and writing the variable, we can make the variable local to this module. if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { automaton.addBooleanVariable(newBooleanVariable); - storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); - initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; + if (variable.hasInitialValue()) { + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; + } } else if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. janiModel.addBooleanVariable(newBooleanVariable); - storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); - globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + if (variable.hasInitialValue()) { + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; + } } } @@ -1713,6 +1743,19 @@ namespace storm { return janiModel; } + void Program::createMissingInitialValues() { + for (auto& variable : globalBooleanVariables) { + if (!variable.hasInitialValue()) { + variable.setInitialValueExpression(manager->boolean(false)); + } + } + for (auto& variable : globalIntegerVariables) { + if (!variable.hasInitialValue()) { + variable.setInitialValueExpression(variable.getLowerBoundExpression()); + } + } + } + std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) { switch (type) { case Program::ModelType::UNDEFINED: out << "undefined"; break; diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 8c30079e0..50bd84603 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -175,7 +175,7 @@ namespace storm { * @return The global boolean variables of the program. */ std::vector const& getGlobalBooleanVariables() const; - + /*! * Retrieves a the global boolean variable with the given name. * @@ -587,6 +587,11 @@ namespace storm { */ Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector> const& commands) const; + /*! + * Equips all global variables without initial values with initial values based on their type. + */ + void createMissingInitialValues(); + // The manager responsible for the variables/expressions of the program. std::shared_ptr manager; diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp index 7d347bcec..cda8317a5 100644 --- a/src/storage/prism/Variable.cpp +++ b/src/storage/prism/Variable.cpp @@ -5,11 +5,11 @@ namespace storm { namespace prism { - Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) { + Variable::Variable(storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), initialValueExpression(initialValueExpression) { // Nothing to do here. } - Variable::Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(manager.declareVariable(newName, oldVariable.variable.getType())), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) { + Variable::Variable(storm::expressions::ExpressionManager& manager, Variable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(manager.declareVariable(newName, oldVariable.variable.getType())), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)) { // Intentionally left empty. } @@ -17,14 +17,18 @@ namespace storm { return this->variable.getName(); } - bool Variable::hasDefaultInitialValue() const { - return this->defaultInitialValue; + bool Variable::hasInitialValue() const { + return this->initialValueExpression.isInitialized(); } storm::expressions::Expression const& Variable::getInitialValueExpression() const { return this->initialValueExpression; } + void Variable::setInitialValueExpression(storm::expressions::Expression const& initialValueExpression) { + this->initialValueExpression = initialValueExpression; + } + storm::expressions::Variable const& Variable::getExpressionVariable() const { return this->variable; } diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h index 3a19c2b75..40f47eb27 100644 --- a/src/storage/prism/Variable.h +++ b/src/storage/prism/Variable.h @@ -28,19 +28,27 @@ namespace storm { std::string const& getName() const; /*! - * Retrieves the expression defining the initial value of the variable. + * Retrieves whether the variable has an initial value. + * + * @return True iff the variable has an initial value. + */ + bool hasInitialValue() const; + + /*! + * Retrieves the expression defining the initial value of the variable. This can only be called if there is + * an initial value (expression). * * @return The expression defining the initial value of the variable. */ storm::expressions::Expression const& getInitialValueExpression() const; - + /*! - * Retrieves whether the variable has the default initial value with respect to its type. + * Sets the expression defining the initial value of the variable. * - * @return True iff the variable has the default initial value. + * @param initialValueExpression The expression defining the initial value of the variable. */ - bool hasDefaultInitialValue() const; - + void setInitialValueExpression(storm::expressions::Expression const& initialValueExpression); + /*! * Retrieves the expression variable associated with this variable. * @@ -55,6 +63,10 @@ namespace storm { */ storm::expressions::Expression getExpression() const; + /*! + * Equips the variable with an initial value based on its type if not initial value is present. + */ + virtual void createMissingInitialValue() = 0; // Make the constructors protected to forbid instantiation of this class. protected: @@ -90,9 +102,6 @@ namespace storm { // The constant expression defining the initial value of the variable. storm::expressions::Expression initialValueExpression; - - // A flag that stores whether the variable has its default initial expression. - bool defaultInitialValue; }; } // namespace prism From af8d9b0ad8a6977f9f538556719a75ce4c3ae8ef Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Sep 2016 10:54:47 +0200 Subject: [PATCH 2/4] added underflow check in PRISM next-state generator Former-commit-id: dc7f0ea3c7f88936c0d02bb44379b12e5c7f667e --- src/generator/PrismNextStateGenerator.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 7eb2291c5..ab1311076 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -305,6 +305,7 @@ namespace storm { } int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } From 8e565a2930a27f40ba19ba3982893050646129da Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 26 Sep 2016 20:09:06 +0200 Subject: [PATCH 3/4] forcing boost to use old optional implementation to prevent bug in spirit in boost 1.61; everyone can finally update and we take out the option as soon as this is resolved on the boost side of things Former-commit-id: 92bc4796a04733e8959e84797cb459e64e437059 --- CMakeLists.txt | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 6e749e419..645f0649d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -125,7 +125,12 @@ if(CMAKE_COMPILER_IS_GNUCC) # Set standard flags for GCC set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops") - add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) + + # TODO: remove forcing the old version of optional as soon as the related Spirit bug is fixed: + # https://svn.boost.org/trac/boost/ticket/12349 + # Fix thanks to: https://github.com/freeorion/freeorion/issues/777 + add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE -DBOOST_OPTIONAL_CONFIG_USE_OLD_IMPLEMENTATION_OF_OPTIONAL) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas") set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations") if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0) @@ -187,7 +192,10 @@ else(CLANG) set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++") endif() - add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) + # TODO: remove forcing the old version of optional as soon as the related Spirit bug is fixed: + # https://svn.boost.org/trac/boost/ticket/12349 + # Fix thanks to: https://github.com/freeorion/freeorion/issues/777 + add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE -DBOOST_OPTIONAL_CONFIG_USE_OLD_IMPLEMENTATION_OF_OPTIONAL) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -Wno-unused-local-typedefs -ftemplate-depth=1024 -Wno-parentheses-equality") if(FORCE_COLOR) From cb97da887c1539c13c65d1c2654d6742fa75a8c3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Oct 2016 15:20:15 +0200 Subject: [PATCH 4/4] went from deque to vector-based representation of splitter queue in bisimulation Former-commit-id: 70471926416ab789126995475aa6cfab4c17e7e4 --- .../BisimulationDecomposition.cpp | 8 +++--- .../bisimulation/BisimulationDecomposition.h | 4 +-- ...ministicModelBisimulationDecomposition.cpp | 8 +++--- ...erministicModelBisimulationDecomposition.h | 10 +++---- ...ministicModelBisimulationDecomposition.cpp | 26 +++---------------- ...erministicModelBisimulationDecomposition.h | 8 +++--- 6 files changed, 22 insertions(+), 42 deletions(-) diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index dbad8c633..bce19fd51 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -231,7 +231,7 @@ namespace storm { template void BisimulationDecomposition::performPartitionRefinement() { // Insert all blocks into the splitter queue as a (potential) splitter. - std::deque*> splitterQueue; + std::vector*> splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } ); // Then perform the actual splitting until there are no more splitters. @@ -242,9 +242,9 @@ namespace storm { // Get and prepare the next splitter. // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but // tends to work well. - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - Block* splitter = splitterQueue.front(); - splitterQueue.pop_front(); + std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } ); + Block* splitter = splitterQueue.back(); + splitterQueue.pop_back(); splitter->data().setSplitter(false); // Now refine the partition using the current splitter. diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 6507e3b07..e3322444c 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -1,8 +1,6 @@ #ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ -#include - #include "src/settings/SettingsManager.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/storage/sparse/StateType.h" @@ -224,7 +222,7 @@ namespace storm { * @param splitter The splitter to use. * @param splitterQueue The queue into which to insert the newly discovered potential splitters. */ - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) = 0; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterQueue) = 0; /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 3f70fd379..66b1a9ec5 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -157,7 +157,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterQueue) { for (auto block : predecessorBlocks) { STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); @@ -378,7 +378,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterQueue) { // First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities // for all non-silent states. computeConditionalProbabilitiesForNonSilentStates(block); @@ -416,7 +416,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterQueue) { for (auto block : predecessorBlocks) { if (*block != splitter) { refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); @@ -439,7 +439,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterQueue) { STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId()); // The outline of the refinement is as follows. diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index b9f2a2a5a..b4db574cb 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -39,11 +39,11 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterQueue) override; private: // Refines the predecessor blocks wrt. strong bisimulation. - void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterQueue); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -99,10 +99,10 @@ namespace storm { void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block& block); // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. - void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterQueue); // Refines the given block wrt to weak bisimulation in DTMCs. - void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue); + void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterQueue); // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // for weak bisimulation (on DTMCs). @@ -127,4 +127,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 64a7efe45..6fc317d3f 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -198,7 +198,7 @@ namespace storm { } template - void NondeterministicModelBisimulationDecomposition::updateQuotientDistributionsOfPredecessors(Block const& newBlock, Block const& oldBlock, std::deque*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition::updateQuotientDistributionsOfPredecessors(Block const& newBlock, Block const& oldBlock, std::vector*>& splitterQueue) { uint_fast64_t lastState = 0; bool lastStateInitialized = false; @@ -332,36 +332,23 @@ namespace storm { } template - bool NondeterministicModelBisimulationDecomposition::splitBlockAccordingToCurrentQuotientDistributions(Block& block, std::deque*>& splitterQueue) { + bool NondeterministicModelBisimulationDecomposition::splitBlockAccordingToCurrentQuotientDistributions(Block& block, std::vector*>& splitterQueue) { std::list*> newBlocks; bool split = this->partition.splitBlock(block, [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { bool result = quotientDistributionsLess(state1, state2); -// std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl; return result; }, [this, &block, &splitterQueue, &newBlocks] (Block& newBlock) { newBlocks.push_back(&newBlock); - -// this->checkBlockStable(newBlock); -// this->checkDistributionsDifferent(block, block.getEndIndex()); -// this->checkQuotientDistributions(); }); - // The quotient distributions of the predecessors of block do not need to be updated, since the probability - // will go to the block with the same id as before. - -// std::cout << "partition after split: " << std::endl; -// this->partition.print(); - - // defer updating the quotient distributions until *after* all splits, because + // Defer updating the quotient distributions until *after* all splits, because // it otherwise influences the subsequent splits! for (auto el : newBlocks) { this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue); } -// this->checkQuotientDistributions(); - return split; } @@ -369,11 +356,6 @@ namespace storm { bool NondeterministicModelBisimulationDecomposition::quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const { STORM_LOG_TRACE("Comparing the quotient distributions of state " << state1 << " and " << state2 << "."); std::vector nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); - -// std::cout << "distributions of state " << state1 << std::endl; -// this->printDistributions(state1); -// std::cout << "distributions of state " << state2 << std::endl; -// this->printDistributions(state2); auto firstIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1]; auto firstIte = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1 + 1]; @@ -405,7 +387,7 @@ namespace storm { } template - void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterQueue) { if (!possiblyNeedsRefinement(splitter)) { return; } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index 18a6e8e58..6c25d6cf9 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -37,7 +37,7 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterQueue) override; virtual void initialize() override; @@ -52,7 +52,7 @@ namespace storm { bool possiblyNeedsRefinement(bisimulation::Block const& block) const; // Splits the given block according to the current quotient distributions. - bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block& block, std::deque*>& splitterQueue); + bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block& block, std::vector*>& splitterQueue); // Retrieves whether the quotient distributions of state 1 are considered to be less than the ones of state 2. bool quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const; @@ -62,7 +62,7 @@ namespace storm { // Updates the quotient distributions of the predecessors of the new block by taking the probability mass // away from the old block. - void updateQuotientDistributionsOfPredecessors(bisimulation::Block const& newBlock, bisimulation::Block const& oldBlock, std::deque*>& splitterQueue); + void updateQuotientDistributionsOfPredecessors(bisimulation::Block const& newBlock, bisimulation::Block const& oldBlock, std::vector*>& splitterQueue); bool checkQuotientDistributions() const; bool checkBlockStable(bisimulation::Block const& newBlock) const; @@ -81,4 +81,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */