sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

support for initial constructs in PRISM programs 

Former-commit-id: 0c8132aa43
tempestpy_adaptions
dehnert 8 years ago
parent
1b19372a14
commit
92932fced1
12 changed files with 199 additions and 92 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 18
      src/parser/PrismParser.cpp
  2. 6
      src/parser/PrismParser.h
  3. 16
      src/storage/prism/BooleanVariable.cpp
  4. 2
      src/storage/prism/BooleanVariable.h
  5. 14
      src/storage/prism/IntegerVariable.cpp
  6. 2
      src/storage/prism/IntegerVariable.h
  7. 11
      src/storage/prism/Module.cpp
  8. 5
      src/storage/prism/Module.h
  9. 171
      src/storage/prism/Program.cpp
  10. 7
      src/storage/prism/Program.h
  11. 12
      src/storage/prism/Variable.cpp
  12. 27
      src/storage/prism/Variable.h

18
src/parser/PrismParser.cpp
View File

@ -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>(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

6
src/parser/PrismParser.h
View File

@ -188,7 +188,7 @@ namespace storm {
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&), Skipper> variableDefinition;
qi::rule<Iterator, storm::prism::BooleanVariable(), Skipper> booleanVariableDefinition;
qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, 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<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation);
@ -274,6 +274,8 @@ namespace storm {
storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const;
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
};

16
src/storage/prism/BooleanVariable.cpp
View File

@ -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<storm::expressions::Variable, storm::expressions::Expression> 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;
}

2
src/storage/prism/BooleanVariable.h
View File

@ -37,6 +37,8 @@ namespace storm {
*/
BooleanVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
virtual void createMissingInitialValue() override;
friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable);
};

14
src/storage/prism/IntegerVariable.cpp
View File

@ -19,11 +19,21 @@ namespace storm {
}
IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> 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

2
src/storage/prism/IntegerVariable.h
View File

@ -60,6 +60,8 @@ namespace storm {
*/
IntegerVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
virtual void createMissingInitialValue() override;
friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable);
private:

11
src/storage/prism/Module.cpp
View File

@ -42,7 +42,7 @@ namespace storm {
std::vector<storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
return this->integerVariables;
}
std::set<storm::expressions::Variable> Module::getAllExpressionVariables() const {
std::set<storm::expressions::Variable> 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()) {

5
src/storage/prism/Module.h
View File

@ -225,6 +225,11 @@ namespace storm {
*/
bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> 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:

171
src/storage/prism/Program.cpp
View File

@ -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<storm::expressions::Variable> variables;
for (auto const& variable : this->getGlobalBooleanVariables()) {
// Check the initial value of the variable.
std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
illegalVariableNames.push_back(var.getName());
if (variable.hasInitialValue()) {
// Check the initial value of the variable.
std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<std::string> 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<std::string> 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<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
illegalVariableNames.push_back(var.getName());
if (variable.hasInitialValue()) {
// Check the initial value of the variable.
std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> 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<std::string> 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<std::string> 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<std::string> 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<storm::expressions::Expression>(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<storm::expressions::Variable, std::set<uint_fast64_t>> 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<uint_fast64_t> 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;

7
src/storage/prism/Program.h
View File

@ -175,7 +175,7 @@ namespace storm {
* @return The global boolean variables of the program.
*/
std::vector<BooleanVariable> 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<std::reference_wrapper<Command const>> 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<storm::expressions::ExpressionManager> manager;

12
src/storage/prism/Variable.cpp
View File

@ -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<storm::expressions::Variable, storm::expressions::Expression> 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<storm::expressions::Variable, storm::expressions::Expression> 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;
}

27
src/storage/prism/Variable.h
View File

@ -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

Write Preview
Loading…
Cancel
Save