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

Further fixes for new variable handling. libstorm now compiles again, yay. 

Former-commit-id: a9ac5c0356
tempestpy_adaptions
dehnert 10 years ago
parent
f76d0f93eb
commit
7ec3e8b214
13 changed files with 159 additions and 102 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. 34
      src/parser/ExpressionParser.cpp
  2. 14
      src/parser/ExpressionParser.h
  3. 134
      src/parser/PrismParser.cpp
  4. 6
      src/parser/PrismParser.h
  5. 6
      src/solver/Z3SmtSolver.cpp
  6. 8
      src/storage/dd/CuddDd.cpp
  7. 4
      src/storage/expressions/Variable.cpp
  8. 16
      src/storage/expressions/Variable.h
  9. 2
      src/storage/prism/Module.cpp
  10. 4
      src/storage/prism/Module.h
  11. 27
      src/storage/prism/Program.cpp
  12. 2
      src/storage/prism/RewardModel.cpp
  13. 4
      src/storage/prism/RewardModel.h

34
src/parser/ExpressionParser.cpp
View File

@ -5,7 +5,7 @@
namespace storm {
namespace parser {
ExpressionParser::ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
@ -98,7 +98,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -113,7 +113,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -127,7 +127,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -144,7 +144,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -159,7 +159,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -174,7 +174,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -189,7 +189,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@ -203,7 +203,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1) const {
@ -222,7 +222,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const {
@ -232,17 +232,17 @@ namespace storm {
}
if (this->createExpressions) {
return storm::expressions::Expression::createDoubleLiteral(value);
return manager.rational(value);
} else {
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
}
storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const {
if (this->createExpressions) {
return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value));
return manager.integer(value);
} else {
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
}
@ -258,7 +258,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const {
@ -273,7 +273,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const {
@ -283,7 +283,7 @@ namespace storm {
STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
return *expression;
} else {
return storm::expressions::Expression::createFalse();
return manager.boolean(false);
}
}

14
src/parser/ExpressionParser.h
View File

@ -19,16 +19,17 @@ namespace storm {
* generate the actual expressions, a mapping of valid identifiers to their expressions need to be provided
* later.
*
* @param manager The manager responsible for the expressions.
* @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected.
*/
ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
/*!
* Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to
* expressions will be substituted wherever the key value appears in the parsed expression. After setting
* this, the parser will generate expressions.
*
* @param identifiers A pointer to a mapping from identifiers to expressions.
* @param identifiers_ A pointer to a mapping from identifiers to expressions.
*/
void setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_);
@ -157,16 +158,19 @@ namespace storm {
minMaxOperatorStruct minMaxOperator_;
struct trueFalseOperatorStruct : qi::symbols<char, storm::expressions::Expression> {
trueFalseOperatorStruct() {
trueFalseOperatorStruct(storm::expressions::ExpressionManager& manager) {
add
("true", storm::expressions::Expression::createTrue())
("false", storm::expressions::Expression::createFalse());
("true", manager.boolean(true))
("false", manager.boolean(false));
}
};
// A parser used for recognizing the literals true and false.
trueFalseOperatorStruct trueFalse_;
// The manager responsible for the expressions.
storm::expressions::ExpressionManager& manager;
// A flag that indicates whether expressions should actually be generated or just a syntax check shall be
// performed.
bool createExpressions;

134
src/parser/PrismParser.cpp
View File

@ -61,7 +61,7 @@ namespace storm {
return result;
}
PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), expressionParser(keywords_) {
PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(*manager, keywords_) {
// Parse simple identifier.
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
@ -96,7 +96,7 @@ 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(storm::expressions::Expression::createFalse())) > 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::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
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)];
@ -133,7 +133,7 @@ namespace storm {
assignmentDefinitionList %= +assignmentDefinition % "&";
assignmentDefinitionList.name("assignment list");
updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
updateDefinition.name("update");
updateListDefinition %= +updateDefinition(qi::_r1) % "+";
@ -224,50 +224,98 @@ namespace storm {
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
try {
storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType());
this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
}
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
}
storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
try {
storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
}
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
}
storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
try {
storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getRationalType());
this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
}
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
try {
storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType());
this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
}
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
try {
storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
}
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
try {
storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
}
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
}
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
@ -312,18 +360,34 @@ namespace storm {
storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
try {
storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getBooleanType());
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 << "'.");
}
}
}
return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, this->getFilename());
}
storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
try {
storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getIntegerType());
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 << "'.");
}
}
}
return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
}
storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
@ -342,12 +406,14 @@ namespace storm {
for (auto const& variable : moduleToRename.getBooleanVariables()) {
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.");
this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second));
storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType());
this->identifiers_.add(renamingPair->first, renamedVariable.getExpression());
}
for (auto const& variable : moduleToRename.getIntegerVariables()) {
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.");
this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second));
storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType());
this->identifiers_.add(renamingPair->first, renamedVariable.getExpression());
}
// Return a dummy module in the first pass.
@ -357,12 +423,12 @@ namespace storm {
globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
// Create a mapping from identifiers to the expressions they need to be replaced with.
std::map<std::string, storm::expressions::Expression> expressionRenaming;
std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
for (auto const& namePair : renaming) {
storm::expressions::Expression const* substitutedExpression = this->identifiers_.find(namePair.second);
// If the mapped-to-value is an expression, we need to replace it.
if (substitutedExpression != nullptr) {
expressionRenaming.emplace(namePair.first, *substitutedExpression);
expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression);
}
}
@ -372,7 +438,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(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
// Rename the integer variables.
@ -381,7 +447,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(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.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
// Rename commands.
@ -417,7 +483,7 @@ namespace storm {
}
storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
}
} // namespace parser
} // namespace storm

6
src/parser/PrismParser.h
View File

@ -9,6 +9,7 @@
#include "src/parser/SpiritParserDefinitions.h"
#include "src/parser/ExpressionParser.h"
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/Expressions.h"
#include "src/utility/macros.h"
@ -20,7 +21,7 @@ namespace storm {
class GlobalProgramInformation {
public:
// Default construct the header information.
GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(),hasInitialConstruct(false), initialConstruct(storm::expressions::Expression::createFalse()), currentCommandIndex(0), currentUpdateIndex(0) {
GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) {
// Intentionally left empty.
}
@ -212,7 +213,8 @@ namespace storm {
storm::parser::PrismParser::modelTypeStruct modelType_;
qi::symbols<char, storm::expressions::Expression> identifiers_;
// Parser used for recognizing expressions.
// Parser and manager used for recognizing expressions.
std::shared_ptr<storm::expressions::ExpressionManager> manager;
storm::parser::ExpressionParser expressionParser;
// Helper methods used in the grammar.

6
src/solver/Z3SmtSolver.cpp
View File

@ -201,7 +201,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) {
storm::expressions::SimpleValuation stormModel(this->getManager());
storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer());
for (unsigned i = 0; i < model.num_consts(); ++i) {
z3::func_decl variableI = model.get_const_decl(i);
@ -252,7 +252,7 @@ namespace storm {
z3::model model = this->solver->get_model();
z3::expr modelExpr = this->context->bool_val(true);
storm::expressions::SimpleValuation valuation(this->getManager());
storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
for (storm::expressions::Variable const& importantAtom : important) {
z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
@ -294,7 +294,7 @@ namespace storm {
z3::model model = this->solver->get_model();
z3::expr modelExpr = this->context->bool_val(true);
storm::expressions::SimpleValuation valuation(this->getManager());
storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
for (storm::expressions::Variable const& importantAtom : important) {
z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());

8
src/storage/dd/CuddDd.cpp
View File

@ -303,10 +303,10 @@ namespace storm {
}
}
std::set<std::string> unionOfMetaVariableNames;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin()));
std::set<std::string> containedMetaVariableNames;
std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin()));
std::set<storm::expressions::Variable> unionOfMetaVariables;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
std::set<storm::expressions::Variable> containedMetaVariables;
std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables);
}

4
src/storage/expressions/Variable.cpp
View File

@ -11,6 +11,10 @@ namespace storm {
return manager == other.manager && index == other.index;
}
bool Variable::operator<(Variable const& other) const {
return this->getIndex() < other.getIndex();
}
storm::expressions::Expression Variable::getExpression() const {
return storm::expressions::Expression(*this);
}

16
src/storage/expressions/Variable.h
View File

@ -40,6 +40,14 @@ namespace storm {
* @return True iff the two variables are the same.
*/
bool operator==(Variable const& other) const;
/*!
* Checks whether the variable appears earlier in the total ordering of variables.
*
* @param other The variable to compare with.
* @return True iff the first variable appears earlier than the given one.
*/
bool operator<(Variable const& other) const;
/*!
* Retrieves the name of the variable.
@ -129,14 +137,6 @@ namespace std {
return std::hash<uint_fast64_t>()(variable.getIndex());
}
};
// Provide a less operator, so we can put variables in ordered collections.
template <>
struct less<storm::expressions::Variable> {
std::size_t operator()(storm::expressions::Variable const& variable1, storm::expressions::Variable const& variable2) const {
return variable1.getIndex() < variable2.getIndex();
}
};
}
#endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */

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

@ -146,7 +146,7 @@ namespace storm {
return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
}
Module Module::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
Module Module::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
std::vector<BooleanVariable> newBooleanVariables;
newBooleanVariables.reserve(this->getNumberOfBooleanVariables());
for (auto const& booleanVariable : this->getBooleanVariables()) {

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

@ -189,12 +189,12 @@ namespace storm {
Module restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const;
/*!
* Substitutes all identifiers in the module according to the given map.
* Substitutes all variables in the module according to the given map.
*
* @param substitution The substitution to perform.
* @return The resulting module.
*/
Module substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
friend std::ostream& operator<<(std::ostream& stream, Module const& module);

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

@ -255,7 +255,7 @@ namespace storm {
STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
// Now replace the occurrences of undefined constants in its defining expression.
newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
newConstants.emplace_back(constant.getExpressionVariable(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
} else {
auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
@ -344,9 +344,6 @@ namespace storm {
}
void Program::checkValidity() const {
// We need to construct a mapping from identifiers to their types, so we can type-check the expressions later.
std::map<std::string, storm::expressions::ExpressionReturnType> identifierToTypeMap;
// Start by checking the constant declarations.
std::set<std::string> allIdentifiers;
std::set<std::string> globalIdentifiers;
@ -362,9 +359,6 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers.");
}
// Finally, register the type of the constant for later type checks.
identifierToTypeMap.emplace(constant.getName(), constant.getType());
// Record the new identifier for future checks.
constantNames.insert(constant.getName());
allIdentifiers.insert(constant.getName());
@ -382,9 +376,6 @@ namespace storm {
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
// Register the type of the constant for later type checks.
identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
// Record the new identifier for future checks.
variableNames.insert(variable.getName());
allIdentifiers.insert(variable.getName());
@ -408,9 +399,6 @@ namespace storm {
isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
// Register the type of the constant for later type checks.
identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
// Record the new identifier for future checks.
variableNames.insert(variable.getName());
allIdentifiers.insert(variable.getName());
@ -428,9 +416,6 @@ namespace storm {
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
// Register the type of the constant for later type checks.
identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
// Record the new identifier for future checks.
variableNames.insert(variable.getName());
allIdentifiers.insert(variable.getName());
@ -439,9 +424,6 @@ namespace storm {
// Check for duplicate identifiers.
STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
// Register the type of the constant for later type checks.
identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
// Check that bound expressions of the range.
std::set<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
@ -500,8 +482,7 @@ namespace storm {
}
}
STORM_LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName());
STORM_LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'.");
STORM_LOG_THROW(manager->getVariable(assignment.getVariableName()).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 '" << manager->getVariable(assignment.getVariableName()).getType() << "'.");
containedIdentifiers = assignment.getExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
@ -572,11 +553,11 @@ namespace storm {
}
storm::expressions::ExpressionManager const& Program::getManager() const {
return this->manager;
return *this->manager;
}
storm::expressions::ExpressionManager& Program::getManager() {
return this->manager;
return *this->manager;
}
std::ostream& operator<<(std::ostream& stream, Program const& program) {

2
src/storage/prism/RewardModel.cpp
View File

@ -30,7 +30,7 @@ namespace storm {
return this->transitionRewards;
}
RewardModel RewardModel::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
RewardModel RewardModel::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
std::vector<StateReward> newStateRewards;
newStateRewards.reserve(this->getStateRewards().size());
for (auto const& stateReward : this->getStateRewards()) {

4
src/storage/prism/RewardModel.h
View File

@ -76,12 +76,12 @@ namespace storm {
std::vector<storm::prism::TransitionReward> const& getTransitionRewards() const;
/*!
* Substitutes all identifiers in the reward model according to the given map.
* Substitutes all variables in the reward model according to the given map.
*
* @param substitution The substitution to perform.
* @return The resulting reward model.
*/
RewardModel substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
RewardModel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);

Write Preview
Loading…
Cancel
Save