From 92932fced10eecd82b93c5fedcfea557b2e49b2f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 Sep 2016 17:12:30 +0200 Subject: [PATCH] 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