From 2b909755259df6106d6c966fdc09015458184088 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 8 Oct 2018 16:24:42 +0200 Subject: [PATCH] parsing prism PTAs --- src/storm-parsers/parser/PrismParser.cpp | 69 ++++++++++++++++++++--- src/storm-parsers/parser/PrismParser.h | 47 ++++++++------- src/storm/storage/prism/ClockVariable.cpp | 24 ++++++++ src/storm/storage/prism/ClockVariable.h | 37 ++++++++++++ src/storm/storage/prism/Module.cpp | 44 +++++++++++++-- src/storm/storage/prism/Module.h | 52 ++++++++++++++++- src/storm/storage/prism/Program.cpp | 46 +++++++++++++-- src/storm/storage/prism/Program.h | 2 +- 8 files changed, 280 insertions(+), 41 deletions(-) create mode 100644 src/storm/storage/prism/ClockVariable.cpp create mode 100644 src/storm/storage/prism/ClockVariable.h diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 4c0edbb34..f0ce8d71c 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -85,8 +85,6 @@ namespace storm { modelTypeDefinition %= modelType_; modelTypeDefinition.name("model type"); - - undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); @@ -121,7 +119,10 @@ namespace storm { integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")) > expression_ > qi::lit("..") > expression_ > qi::lit("]") > -(qi::lit("init") > expression_[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)]); + clockVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)]; + clockVariableDefinition.name("clock variable definition"); + + variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]); variableDefinition.name("variable declaration"); globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)])); @@ -150,6 +151,9 @@ namespace storm { observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)]; observablesConstruct.name("observables construct"); + invariantConstruct = (qi::lit("invariant") > expression_ > qi::lit("endinvariant"))[qi::_val = qi::_1]; + invariantConstruct.name("invariant construct"); + systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; systemCompositionConstruct.name("system composition construct"); @@ -211,8 +215,8 @@ namespace storm { > +(qi::char_ - qi::lit(";")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)]; commandDefinition.name("command definition"); - - moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > *commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)]; + + moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)]; moduleDefinition.name("module definition"); moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[") @@ -249,6 +253,7 @@ namespace storm { qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction); qi::on_success(booleanVariableDefinition, setLocationInfoFunction); qi::on_success(integerVariableDefinition, setLocationInfoFunction); + qi::on_success(clockVariableDefinition, setLocationInfoFunction); qi::on_success(moduleDefinition, setLocationInfoFunction); qi::on_success(moduleRenaming, setLocationInfoFunction); qi::on_success(formulaDefinition, setLocationInfoFunction); @@ -585,15 +590,36 @@ namespace storm { return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename()); } + + storm::prism::ClockVariable PrismParser::createClockVariable(std::string const& variableName) const { + if (!this->secondRun) { + try { + storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName); + this->identifiers_.add(variableName, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(variableName)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'."); + } + } + } + bool observable = this->observables.count(variableName) > 0; + if(observable) { + this->observables.erase(variableName); + } + + return storm::prism::ClockVariable(manager->getVariable(variableName), observable, this->getFilename()); + } void PrismParser::createObservablesList(std::vector const& observables) { this->observables.insert(observables.begin(), observables.end()); // We need this list to be filled in both runs. } - storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { + storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size(); - return storm::prism::Module(moduleName, booleanVariables, integerVariables, commands, this->getFilename()); + return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename()); } storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const { @@ -622,6 +648,15 @@ namespace storm { this->observables.erase(renamingPair->second); } } + for (auto const& variable : moduleToRename.getClockVariables()) { + 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) << ": Clock variable '" << variable.getName() << " was not renamed."); + storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second); + this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); + if(this->observables.count(renamingPair->second) > 0) { + this->observables.erase(renamingPair->second); + } + } for (auto const& command : moduleToRename.getCommands()) { std::string newActionName = command.getActionName(); @@ -677,6 +712,24 @@ namespace storm { } 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(), observable, this->getFilename(), get_line(qi::_1))); } + + // Rename the clock variables. + std::vector clockVariables; + for (auto const& variable : moduleToRename.getClockVariables()) { + 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) << ": Clock variable '" << variable.getName() << " was not renamed."); + bool observable = this->observables.count(renamingPair->second) > 0; + if (observable) { + this->observables.erase(renamingPair->second); + } + clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), get_line(qi::_1))); + } + + // Rename invariant (if present) + storm::expressions::Expression invariant; + if (moduleToRename.hasInvariant()) { + invariant = moduleToRename.getInvariant().substitute(expressionRenaming); + } // Rename commands. std::vector commands; @@ -716,7 +769,7 @@ namespace storm { ++globalProgramInformation.currentCommandIndex; } - return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming); + return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming); } } diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index a5367d2c6..7a53bd359 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -98,7 +98,8 @@ namespace storm { ("mdp", storm::prism::Program::ModelType::MDP) ("ctmdp", storm::prism::Program::ModelType::CTMDP) ("ma", storm::prism::Program::ModelType::MA) - ("pomdp", storm::prism::Program::ModelType::POMDP); + ("pomdp", storm::prism::Program::ModelType::POMDP) + ("pta", storm::prism::Program::ModelType::PTA); } }; @@ -111,21 +112,24 @@ namespace storm { ("ctmdp", 4) ("ma", 5) ("pomdp", 6) - ("const", 7) - ("int", 8) - ("bool", 9) - ("module", 10) - ("endmodule", 11) - ("rewards", 12) - ("endrewards", 13) - ("true", 14) - ("false", 15) - ("min", 16) - ("max", 17) - ("floor", 18) - ("ceil", 19) - ("init", 20) - ("endinit", 21); + ("pta", 7) + ("const", 8) + ("int", 9) + ("bool", 10) + ("module", 11) + ("endmodule", 12) + ("rewards", 13) + ("endrewards", 14) + ("true", 15) + ("false", 16) + ("min", 17) + ("max", 18) + ("floor", 19) + ("ceil", 20) + ("init", 21) + ("endinit", 22) + ("invariant", 23) + ("endinvariant", 24); } }; @@ -213,13 +217,14 @@ namespace storm { // Rules for modules definition. qi::rule(GlobalProgramInformation&), Skipper> moduleDefinitionList; - qi::rule, std::vector>, Skipper> moduleDefinition; + qi::rule, std::vector, std::vector>, Skipper> moduleDefinition; qi::rule>, Skipper> moduleRenaming; // Rules for variable definitions. - qi::rule&, std::vector&), Skipper> variableDefinition; + qi::rule&, std::vector&, std::vector&), Skipper> variableDefinition; qi::rule, Skipper> booleanVariableDefinition; qi::rule, Skipper> integerVariableDefinition; + qi::rule, Skipper> clockVariableDefinition; // Rules for command definitions. qi::rule, Skipper> commandDefinition; @@ -238,6 +243,9 @@ namespace storm { qi::rule initialStatesConstruct; qi::rule observablesConstruct; + + // Rules for invariant constructs + qi::rule invariantConstruct; // Rules for the system composition. qi::rule systemCompositionConstruct; @@ -303,7 +311,8 @@ namespace storm { storm::prism::Command createDummyCommand(boost::optional const& actionName, GlobalProgramInformation& globalProgramInformation) const; storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const; storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const; - storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::ClockVariable createClockVariable(std::string const& variableName) const; + storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; 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 createObservablesList(std::vector const& observables); diff --git a/src/storm/storage/prism/ClockVariable.cpp b/src/storm/storage/prism/ClockVariable.cpp new file mode 100644 index 000000000..96984babc --- /dev/null +++ b/src/storm/storage/prism/ClockVariable.cpp @@ -0,0 +1,24 @@ +#include "storm/storage/prism/ClockVariable.h" + +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/constants.h" + +namespace storm { + namespace prism { + ClockVariable::ClockVariable(storm::expressions::Variable const& variable, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, variable.getManager().rational(storm::utility::zero()), observable, filename, lineNumber) { + // Nothing to do here. + } + + void ClockVariable::createMissingInitialValue() { + if (!this->hasInitialValue()) { + this->setInitialValueExpression(this->getExpressionVariable().getManager().rational(storm::utility::zero())); + } + } + + std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable) { + stream << variable.getName() << ": clock" << ";"; + return stream; + } + + } // namespace prism +} // namespace storm diff --git a/src/storm/storage/prism/ClockVariable.h b/src/storm/storage/prism/ClockVariable.h new file mode 100644 index 000000000..8cba64f58 --- /dev/null +++ b/src/storm/storage/prism/ClockVariable.h @@ -0,0 +1,37 @@ +#pragma once + +#include + +#include "storm/storage/prism/Variable.h" + +namespace storm { + namespace prism { + class ClockVariable : public Variable { + public: + // Create default implementations of constructors/assignment. + ClockVariable() = default; + ClockVariable(ClockVariable const& other) = default; + ClockVariable& operator=(ClockVariable const& other)= default; + ClockVariable(ClockVariable&& other) = default; + ClockVariable& operator=(ClockVariable&& other) = default; + + /*! + * Creates a clock variable + * + * @param variable The expression variable associated with this variable. + * @param filename The filename in which the variable is defined. + * @param lineNumber The line number in which the variable is defined. + */ + ClockVariable(storm::expressions::Variable const& variable, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + /*! + * Sets a missing initial value (note that for clock variables, this is always zero) + */ + virtual void createMissingInitialValue() override; + + friend std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable); + }; + + } // namespace prism +} // namespace storm + diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index 33d8258f7..a47021959 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -6,11 +6,11 @@ namespace storm { namespace prism { - Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, commands, "", std::map(), filename, lineNumber) { + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant, commands, "", std::map(), filename, lineNumber) { // Intentionally left empty. } - Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) { + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), clockVariables(clockVariables), clockVariableToIndexMap(), invariant(invariant), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) { // Initialize the internal mappings for fast information retrieval. this->createMappings(); } @@ -42,6 +42,20 @@ namespace storm { std::vector const& Module::getIntegerVariables() const { return this->integerVariables; } + + std::size_t Module::getNumberOfClockVariables() const { + return this->clockVariables.size(); + } + + storm::prism::ClockVariable const& Module::getClockVariable(std::string const& variableName) const { + auto const& nameIndexPair = this->clockVariableToIndexMap.find(variableName); + STORM_LOG_THROW(nameIndexPair != this->clockVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown clock variable '" << variableName << "'."); + return this->getClockVariables()[nameIndexPair->second]; + } + + std::vector const& Module::getClockVariables() const { + return this->clockVariables; + } std::set Module::getAllExpressionVariables() const { std::set result; @@ -51,6 +65,9 @@ namespace storm { for (auto const& var : this->getIntegerVariables()) { result.insert(var.getExpressionVariable()); } + for (auto const& var : this->getClockVariables()) { + result.insert(var.getExpressionVariable()); + } return result; } @@ -134,6 +151,9 @@ namespace storm { for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { this->integerVariableToIndexMap[this->getIntegerVariables()[i].getName()] = i; } + for (uint_fast64_t i = 0; i < this->clockVariables.size(); ++i) { + this->booleanVariableToIndexMap[this->getClockVariables()[i].getName()] = i; + } // Add the mapping for all commands. for (uint_fast64_t i = 0; i < this->commands.size(); i++) { @@ -169,7 +189,7 @@ namespace storm { } } - return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands); + return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands); } Module Module::restrictActionIndices(boost::container::flat_set const& actionIndices) const { @@ -181,7 +201,7 @@ namespace storm { } } - return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands); + return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands); } Module Module::substitute(std::map const& substitution) const { @@ -203,7 +223,7 @@ namespace storm { newCommands.emplace_back(command.substitute(substitution)); } - return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber()); + return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(), this->getLineNumber()); } bool Module::containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const { @@ -240,8 +260,19 @@ namespace storm { for (auto& variable : integerVariables) { variable.createMissingInitialValue(); } + for (auto& variable : clockVariables) { + variable.createMissingInitialValue(); + } } + bool Module::hasInvariant() const { + return this->invariant.isInitialized(); + } + + storm::expressions::Expression const& Module::getInvariant() const { + return this->invariant; + } + std::ostream& operator<<(std::ostream& stream, Module const& module) { stream << "module " << module.getName() << std::endl; for (auto const& booleanVariable : module.getBooleanVariables()) { @@ -250,6 +281,9 @@ namespace storm { for (auto const& integerVariable : module.getIntegerVariables()) { stream << "\t" << integerVariable << std::endl; } + for (auto const& clockVariable : module.getClockVariables()) { + stream << "\t" << clockVariable << std::endl; + } for (auto const& command : module.getCommands()) { stream << "\t" << command << std::endl; } diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 9c1286805..970304ab5 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -10,6 +10,7 @@ #include "storm/storage/prism/BooleanVariable.h" #include "storm/storage/prism/IntegerVariable.h" +#include "storm/storage/prism/ClockVariable.h" #include "storm/storage/prism/Command.h" #include "storm/utility/OsDetection.h" @@ -23,11 +24,13 @@ namespace storm { * @param moduleName The name of the module. * @param booleanVariables The boolean variables defined by the module. * @param integerVariables The integer variables defined by the module. + * @param clockVariables The clock variables defined by the module (only for PTA models). + * @param invariant An invariant that is used to restrict the values of the clock variables (only for PTA models). * @param commands The commands of the module. * @param filename The filename in which the module is defined. * @param lineNumber The line number in which the module is defined. */ - Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a module with the given name, variables and commands that is marked as being renamed from the @@ -36,13 +39,15 @@ namespace storm { * @param moduleName The name of the module. * @param booleanVariables The boolean variables defined by the module. * @param integerVariables The integer variables defined by the module. + * @param clockVariables The clock variables defined by the module (only for PTA models). + * @param invariant An invariant that is used to restrict the values of the clock variables (only for PTA models). * @param commands The commands of the module. * @param renamedFromModule The name of the module from which this module was renamed. * @param renaming The renaming of identifiers used to create this module. * @param filename The filename in which the module is defined. * @param lineNumber The line number in which the module is defined. */ - Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Module() = default; @@ -94,7 +99,29 @@ namespace storm { * @return The integer variables of the module. */ std::vector const& getIntegerVariables() const; - + + /*! + * Retrieves the number of clock variables in the module. + * + * @return the number of clock variables in the module. + */ + std::size_t getNumberOfClockVariables() const; + + /*! + * Retrieves a reference to the clock variable with the given name. + * + * @param variableName The name of the clock variable to retrieve. + * @return A reference to the clock variable with the given name. + */ + storm::prism::ClockVariable const& getClockVariable(std::string const& variableName) const; + + /*! + * Retrieves the clock variables of the module. + * + * @return The clock variables of the module. + */ + std::vector const& getClockVariables() const; + /*! * Retrieves all expression variables used by this module. * @@ -236,6 +263,16 @@ namespace storm { */ void createMissingInitialValues(); + /*! + * Returns true, if an invariant was specified (only relevant for PTA models) + */ + bool hasInvariant() const; + + /*! + * Returns the specified invariant (only relevant for PTA models) + */ + storm::expressions::Expression const& getInvariant() const; + friend std::ostream& operator<<(std::ostream& stream, Module const& module); private: @@ -258,6 +295,15 @@ namespace storm { // A mapping from integer variables to the corresponding indices in the vector. std::map integerVariableToIndexMap; + + // A list of clock variables. + std::vector clockVariables; + + // A mapping from clock variables to the corresponding indices in the vector. + std::map clockVariableToIndexMap; + + // An invariant (only for PTA models) + storm::expressions::Expression invariant; // The commands associated with the module. std::vector commands; diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index e9f6f8ecb..a0b32175a 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -810,9 +810,12 @@ namespace storm { for (auto const& booleanVariable : module.getBooleanVariables()) { this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex; } - for (auto const& integerVariable : module.getBooleanVariables()) { + for (auto const& integerVariable : module.getIntegerVariables()) { this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex; } + for (auto const& clockVariable : module.getClockVariables()) { + this->variableToModuleIndexMap[clockVariable.getName()] = moduleIndex; + } } } @@ -1104,6 +1107,12 @@ namespace storm { variables.insert(variable.getExpressionVariable()); all.insert(variable.getExpressionVariable()); } + + for (auto const& variable : module.getClockVariables()) { + // Record the new identifier for future checks. + variables.insert(variable.getExpressionVariable()); + all.insert(variable.getExpressionVariable()); + } } // Create the set of valid identifiers for future checks. @@ -1121,7 +1130,7 @@ namespace storm { } } - // Check the commands of the modules. + // Check the commands and invariants of the modules. bool hasProbabilisticCommand = false; bool hasMarkovianCommand = false; bool hasLabeledMarkovianCommand = false; @@ -1133,6 +1142,24 @@ namespace storm { for (auto const& variable : module.getIntegerVariables()) { legalVariables.insert(variable.getExpressionVariable()); } + for (auto const& variable : module.getClockVariables()) { + legalVariables.insert(variable.getExpressionVariable()); + } + + if (module.hasInvariant()) { + std::set containedVariables = module.getInvariant().getVariables(); + std::set illegalVariables; + std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.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 " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant() << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << "."); + } + STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant() << " must evaluate to type 'bool'."); + } for (auto& command : module.getCommands()) { // Check the guard. @@ -1189,7 +1216,7 @@ namespace storm { } } STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'."); - STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'."); + STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() || (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'."); containedVariables = assignment.getExpression().getVariables(); illegalVariables.clear(); @@ -1409,7 +1436,8 @@ namespace storm { } } - newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands); + // we currently do not simplify clock variables or invariants + newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, module.getClockVariables(), module.getInvariant(), newCommands); // Determine the set of action indices that have been deleted entirely. std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin())); @@ -1464,6 +1492,7 @@ namespace storm { std::stringstream newModuleName; std::vector allBooleanVariables; std::vector allIntegerVariables; + std::vector allClockVariables; std::vector newCommands; uint_fast64_t nextCommandIndex = 0; uint_fast64_t nextUpdateIndex = 0; @@ -1489,6 +1518,7 @@ namespace storm { // this is just for simplicity and is not needed. allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end()); allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end()); + storm::expressions::Expression newInvariant; // Now go through the modules, gather the variables, construct the name of the new module and assert the // bounds of the discovered variables. @@ -1496,12 +1526,17 @@ namespace storm { newModuleName << module.getName() << "_"; allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end()); allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end()); + allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end()); for (auto const& variable : module.getIntegerVariables()) { solver->add(variable.getExpression() >= variable.getLowerBoundExpression()); solver->add(variable.getExpression() <= variable.getUpperBoundExpression()); } + if (module.hasInvariant()) { + newInvariant = newInvariant.isInitialized() ? (newInvariant && module.getInvariant()) : module.getInvariant(); + } + // The commands without a synchronizing action name, can simply be copied (plus adjusting the global // indices of the command and its updates). for (auto const& command : module.getCommands()) { @@ -1643,7 +1678,7 @@ namespace storm { } // Finally, we can create the module and the program and return it. - storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0); + storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands, this->getFilename(), 0); return Program(manager, this->getModelType(), this->getConstants(), std::vector(), std::vector(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true); } @@ -1852,6 +1887,7 @@ namespace storm { case Program::ModelType::CTMDP: out << "ctmdp"; break; case Program::ModelType::MA: out << "ma"; break; case Program::ModelType::POMDP: out << "pomdp"; break; + case Program::ModelType::PTA: out << "pta"; break; } return out; } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 3958c5155..8b6cb1eb1 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -31,7 +31,7 @@ namespace storm { /*! * An enum for the different model types. */ - enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP}; + enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA}; enum class ValidityCheckLevel : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};