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

Started reducing the complexity in the PRISM grammar. 

Former-commit-id: c17dc6d27b
tempestpy_adaptions
dehnert 11 years ago
parent
eb2b2fed30
commit
7610bc8e76
10 changed files with 269 additions and 485 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. 285
      src/parser/prismparser/PrismGrammar.cpp
  2. 207
      src/parser/prismparser/PrismGrammar.h
  3. 79
      src/parser/prismparser/Tokens.h
  4. 2
      src/storage/expressions/Expression.h
  5. 13
      src/storage/expressions/Expressions.h
  6. 8
      src/storage/prism/Program.cpp
  7. 17
      src/storage/prism/Program.h
  8. 63
      src/storage/prism/Update.cpp
  9. 48
      src/storage/prism/Update.h
  10. 32
      test/functional/parser/ParsePrismTest.cpp

285
src/parser/prismparser/PrismGrammar.cpp
View File

@ -1,152 +1,96 @@
/*
* PrismGrammar.cpp
*
* Created on: 11.01.2013
* Author: chris
*/
// Needed for file IO.
#include <fstream>
#include <iomanip>
#include <limits>
#include "PrismGrammar.h"
#include "src/utility/OsDetection.h"
#include "src/parser/prismparser/Includes.h"
#include "src/parser/prismparser/BooleanExpressionGrammar.h"
#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h"
#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h"
#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h"
#include "src/parser/prismparser/IntegerExpressionGrammar.h"
#include "src/parser/prismparser/IdentifierGrammars.h"
#include "src/parser/prismparser/VariableState.h"
#include "src/parser/prismparser/PrismGrammar.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
// Some typedefs and namespace definitions to reduce code size.
typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
namespace storm {
namespace parser {
namespace prism {
void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap) {
this->state->labelNames_.add(name, name);
nameToExpressionMap[name] = value->clone();
}
void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
this->state->assignedIntegerVariables_.add(variable, variable);
variableToAssignmentMap[variable] = Assignment(variable, value->clone());
}
void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
this->state->assignedBooleanVariables_.add(variable, variable);
variableToAssigmentMap[variable] = Assignment(variable, value->clone());
}
void PrismGrammar::addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap) {
this->state->booleanConstants_.add(name, std::shared_ptr<BaseExpression>(new BooleanConstantExpression(name)));
this->state->allConstantNames_.add(name, name);
nameToExpressionMap.emplace(name, std::unique_ptr<BooleanConstantExpression>(new BooleanConstantExpression(dynamic_cast<BooleanConstantExpression&>(*this->state->booleanConstants_.at(name)))));
}
void PrismGrammar::addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap) {
this->state->integerConstants_.add(name, std::shared_ptr<BaseExpression>(new IntegerConstantExpression(name)));
this->state->allConstantNames_.add(name, name);
nameToExpressionMap.emplace(name, std::unique_ptr<IntegerConstantExpression>(new IntegerConstantExpression(dynamic_cast<IntegerConstantExpression&>(*this->state->integerConstants_.at(name)))));
}
void PrismGrammar::addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap) {
this->state->doubleConstants_.add(name, std::shared_ptr<BaseExpression>(new DoubleConstantExpression(name)));
this->state->allConstantNames_.add(name, name);
nameToExpressionMap.emplace(name, std::unique_ptr<DoubleConstantExpression>(new DoubleConstantExpression(dynamic_cast<DoubleConstantExpression&>(*this->state->doubleConstants_.at(name)))));
}
Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string> const& renaming) {
this->state->moduleNames_.add(newName, newName);
Module* old = this->moduleMap_.find(oldName);
if (old == nullptr) {
LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist.");
throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist.";
}
Module res(*old, newName, renaming, *this->state);
this->moduleMap_.at(newName) = res;
return res;
}
Module PrismGrammar::createModule(std::string const& name, std::vector<BooleanVariable> const& bools, std::vector<IntegerVariable> const& ints, std::map<std::string, uint_fast64_t> const& boolids, std::map<std::string, uint_fast64_t> const& intids, std::vector<storm::ir::Command> const& commands) {
this->state->moduleNames_.add(name, name);
Module res(name, bools, ints, boolids, intids, commands);
this->moduleMap_.at(name) = res;
return res;
}
void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
uint_fast64_t id = this->state->addIntegerVariable(name);
uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
vars.emplace_back(newLocalIndex, id, name, lower != nullptr ? lower->clone() : nullptr, upper != nullptr ? upper->clone() : nullptr, init != nullptr ? init->clone() : nullptr);
varids[name] = newLocalIndex;
++this->state->nextLocalIntegerVariableIndex;
this->state->localIntegerVariables_.add(name, name);
if (isGlobalVariable) {
this->state->globalIntegerVariables_.add(name, name);
}
}
void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
uint_fast64_t id = this->state->addBooleanVariable(name);
uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
vars.emplace_back(newLocalIndex, id, name, init != nullptr ? init->clone() : nullptr);
varids[name] = newLocalIndex;
++this->state->nextLocalBooleanVariableIndex;
this->state->localBooleanVariables_.add(name, name);
if (isGlobalVariable) {
this->state->globalBooleanVariables_.add(name, name);
}
}
StateReward createStateReward(std::shared_ptr<BaseExpression> const& guard, std::shared_ptr<BaseExpression> const& reward) {
return StateReward(guard->clone(), reward->clone());
}
TransitionReward createTransitionReward(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::shared_ptr<BaseExpression> const& reward) {
return TransitionReward(label, guard->clone(), reward->clone());
}
void createRewardModel(std::string const& name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
mapping[name] = RewardModel(name, stateRewards, transitionRewards);
}
Update PrismGrammar::createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
this->state->nextGlobalUpdateIndex++;
return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood != nullptr ? likelihood->clone() : nullptr, bools, ints);
}
Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates) {
this->state->nextGlobalCommandIndex++;
return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard->clone(), updates);
}
Program createProgram(
Program::ModelType modelType,
std::map<std::string, std::unique_ptr<BooleanConstantExpression>> const& undefBoolConst,
std::map<std::string, std::unique_ptr<IntegerConstantExpression>> const& undefIntConst,
std::map<std::string, std::unique_ptr<DoubleConstantExpression>> const& undefDoubleConst,
GlobalVariableInformation const& globalVariableInformation,
std::vector<Module> const& modules,
std::map<std::string, RewardModel> const& rewards,
std::map<std::string, std::unique_ptr<BaseExpression>> const& labels) {
return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst,
globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables,
globalVariableInformation.booleanVariableToIndexMap,
globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels);
}
PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) {
PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start) {
// Parse simple identifier.
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]] - keywords_;
identifier.name("identifier");
// Parse a composed expression.
expression %= (booleanExpression | numericalExpression);
expression.name("expression");
booleanExpression %= orExpression;
expression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = qi::_val * qi::_1];
orExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = qi::_val * qi::_1];
andExpression.name("boolean expression");
notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = !qi::_1];
notExpression.name("boolean expression");
atomicBooleanExpression %= relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")");
atomicBooleanExpression.name("boolean expression");
relativeExpression = ((numericalExpression >> ">") > numericalExpression)[qi::_val = qi::_1 > qi::_2] | ((numericalExpression >> ">=") > numericalExpression)[qi::_val = qi::_1 >= qi::_2] | ((numericalExpression >> "<") > numericalExpression)[qi::_val = qi::_1 < qi::_2] | ((numericalExpression >> "<=") > numericalExpression)[qi::_val = qi::_1 <= qi::_2];
relativeExpression.name("relative expression");
booleanVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createBooleanVariable, qi::_1)];
booleanVariableExpression.name("boolean variable");
numericalExpression %= plusExpression;
numericalExpression.name("numerical expression");
plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = qi::_val + qi::_1] .else_ [qi::_val = qi::_val - qi::_1]];
plusExpression.name("numerical expression");
multiplicationExpression = atomicNumericalExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicNumericalExpression[qi::_val = qi::_val * qi::_1]);
multiplicationExpression.name("numerical expression");
atomicNumericalExpression %= minMaxExpression | floorCeilExpression | numericalVariableExpression | qi::lit("(") >> numericalExpression >> qi::lit(")");
atomicNumericalExpression.name("numerical expression");
minMaxExpression %= ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(",") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::minimum, qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::maximum, qi::_1, qi::_2)]];
minMaxExpression.name("min/max expression");
floorCeilExpression %= ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::floor, qi::_1)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::ceil, qi::_1)]];
floorCeilExpression.name("integer floor/ceil expression");
numericalVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleVariable, qi::_1)];
numericalVariableExpression.name("numerical variable");
// Parse a model type.
modelTypeDefinition = modelType_;
modelTypeDefinition.name("model type");
// This block defines all entities that are needed for parsing constant definitions.
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=") > expression > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedDoubleConstantDefinition.name("defined double constant declaration");
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)];
undefinedDoubleConstantDefinition.name("undefined double constant definition");
definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r2) | definedDoubleConstantDefinition(qi::_r3));
definedConstantDefinition.name("defined constant definition");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
undefinedConstantDefinition.name("undefined constant definition");
constantDefinitionList = *(undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3) | definedConstantDefinition(qi::_r4, qi::_r5, qi::_r6));
constantDefinitionList.name("constant definition list");
// Parse the ingredients of a probabilistic program.
start = (qi::eps >
modelTypeDefinition >
constantDefinitionList(qi::_a, qi::_b, qi::_c, qi::_d, qi::_e, qi::_f) >
formulaDefinitionList >
globalVariableDefinitionList(qi::_d) >
moduleDefinitionList >
rewardDefinitionList(qi::_e) >
labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
start.name("probabilistic program declaration");
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))
[phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)];
@ -222,26 +166,6 @@ namespace storm {
globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
globalVariableDefinitionList.name("global variable declaration list");
// This block defines all entities that are needed for parsing constant definitions.
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
definedDoubleConstantDefinition.name("defined double constant declaration");
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)];
undefinedDoubleConstantDefinition.name("undefined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant declaration");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
undefinedConstantDefinition.name("undefined constant declaration");
constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
constantDefinitionList.name("constant declaration list");
constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)];
constantBooleanFormulaDefinition.name("constant boolean formula definition");
booleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->booleanFormulas_.add, qi::_1, qi::_2)];
@ -256,40 +180,7 @@ namespace storm {
formulaDefinition.name("formula definition");
formulaDefinitionList = *formulaDefinition;
formulaDefinitionList.name("formula definition list");
// This block defines all entities that are needed for parsing a program.
modelTypeDefinition = modelType_;
modelTypeDefinition.name("model type");
start = (qi::eps >
modelTypeDefinition >
constantDefinitionList(qi::_a, qi::_b, qi::_c) >
formulaDefinitionList >
globalVariableDefinitionList(qi::_d) >
moduleDefinitionList >
rewardDefinitionList(qi::_e) >
labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
start.name("probabilistic program declaration");
}
void PrismGrammar::prepareForSecondRun() {
LOG4CPLUS_INFO(logger, "Preparing parser for second run.");
this->state->prepareForSecondRun();
BooleanExpressionGrammar::secondRun();
ConstBooleanExpressionGrammar::secondRun();
ConstDoubleExpressionGrammar::secondRun();
ConstIntegerExpressionGrammar::secondRun();
IntegerExpressionGrammar::secondRun();
}
void PrismGrammar::resetGrammars() {
LOG4CPLUS_INFO(logger, "Resetting grammars.");
BooleanExpressionGrammar::resetInstance();
ConstBooleanExpressionGrammar::resetInstance();
ConstDoubleExpressionGrammar::resetInstance();
ConstIntegerExpressionGrammar::resetInstance();
IntegerExpressionGrammar::resetInstance();
}
} // namespace prism
} // namespace parser
} // namespace storm

207
src/parser/prismparser/PrismGrammar.h
View File

@ -34,7 +34,7 @@ using namespace storm::expressions;
namespace storm {
namespace parser {
namespace prism {
class PrismGrammar : public qi::grammar<Iterator, Program(), Skipper> {
class PrismGrammar : public qi::grammar<Iterator, Program(), qi::locals<std::set<std::string>, std::set<std::string>, std::set<std::string>, std::map<std::string, storm::expressions::Expression>, std::map<std::string, storm::expressions::Expression>, std::map<std::string, storm::expressions::Expression>, std::map<std::string, Module>>, Skipper> {
public:
/*!
* Default constructor that creates an empty and functional grammar.
@ -43,182 +43,89 @@ namespace storm {
private:
// The starting point of the grammar.
qi::rule<Iterator, Program(), Skipper> start;
// The locals are used for: (a) undefined boolean constants, (b) undefined integer constants, (c) undefined double constants, (d) defined boolean constants, (e) defined integer constants, (f) defined double constants, (g) module name to module map
qi::rule<Iterator, Program(), qi::locals<std::set<std::string>, std::set<std::string>, std::set<std::string>, std::map<std::string, storm::expressions::Expression>, std::map<std::string, storm::expressions::Expression>, std::map<std::string, storm::expressions::Expression>, std::map<std::string, Module>>, Skipper> start;
// Rules for model type.
qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
// Rules for global constant definitions.
qi::rule<Iterator, qi::unused_type(std::set<std::string>&, std::set<std::string>&, std::set<std::string>&, std::map<std::string, storm::expression::Expression>&, std::map<std::string, storm::expression::Expression>&, std::map<std::string, storm::expression::Expression>&), Skipper> constantDefinitionList;
// Rules for global variable definitions
// Rules for constant definitions.
qi::rule<Iterator, qi::unused_type(std::set<std::string>&, std::set<std::string>&, std::set<std::string>&, std::map<std::string, storm::expressions::Expression>&, std::map<std::string, storm::expressions::Expression>&, std::map<std::string, storm::expressions::Expression>&), Skipper> constantDefinitionList;
qi::rule<Iterator, qi::unused_type(std::set<std::string>&, std::set<std::string>&, std::set<std::string>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::expressions::Expression>&, std::map<std::string, storm::expressions::Expression>&, std::map<std::string, storm::expressions::Expression>&), Skipper> definedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::set<std::string>&), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::set<std::string>&), Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::set<std::string>&), Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::expressions::Expression>&), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::expressions::Expression>&), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::expressions::Expression>&), Skipper> definedDoubleConstantDefinition;
// Rules for global variable definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&, std::map<std::string, IntegerVariable>), Skipper> globalVariableDefinitionList;
// Rules for modules definition.
qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
qi::rule<Iterator, Module(), qi::locals<std::map<std::string, BooleanVariable>, std::map<std::string, IntegerVariable>>, Skipper> moduleDefinition;
qi::rule<Iterator, Module(std::map<std::string, Module>&), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&, bool), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, bool), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&, std::map<std::string, IntegerVariable>&), Skipper> variableDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&), Skipper> booleanVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, IntegerVariable>&), Skipper> integerVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition;
// Rules for variable/command names.
qi::rule<Iterator, std::string(), Skipper> commandName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>>, Skipper> updateDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
qi::rule<Iterator, Assignment(), Skipper> assignmentDefinition;
// Rules for reward definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList;
qi::rule<Iterator, std::map<std::string, RewardModel>(), Skipper> rewardDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition;
qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
qi::rule<Iterator, TransitionReward(), Skipper> transitionRewardDefinition;
// Rules for label definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinition;
// Rules for constant definitions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&), Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
qi::rule<Iterator, std::map<std::string, storm::expressions::Expression>(), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::expressions::Expression>&), Skipper> labelDefinition;
// Rules for formula definitions.
qi::rule<Iterator, qi::unused_type(), Skipper> formulaDefinitionList;
qi::rule<Iterator, qi::unused_type(), Skipper> formulaDefinition;
qi::rule<Iterator, qi::unused_type(), Skipper> constantIntegerFormulaDefinition;
qi::rule<Iterator, qi::unused_type(), Skipper> integerFormulaDefinition;
qi::rule<Iterator, qi::unused_type(), Skipper> constantDoubleFormulaDefinition;
qi::rule<Iterator, qi::unused_type(), Skipper> constantBooleanFormulaDefinition;
qi::rule<Iterator, qi::unused_type(), Skipper> booleanFormulaDefinition;
// Rules for variable recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
qi::rule<Iterator, std::map<std::string, storm::expressions::Expression>(), Skipper> formulaDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::expressions::Expression>&), Skipper> formulaDefinition;
// Rules for identifier parsing.
qi::rule<Iterator, std::string(), Skipper> identifier;
// Rules for parsing a composed expression.
qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> booleanExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> orExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> notExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicBooleanExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> booleanVariableExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> numericalExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> multiplicationExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicNumericalExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> numericalVariableExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
// Parsers that recognize special keywords and operations.
storm::parser::prism::keywordsStruct keywords_;
storm::parser::prism::modelTypeStruct modelType_;
storm::parser::prism::relationalOperatorStruct relations_;
// A mapping from module names to the modules themselves so they can be looked up for renaming later.
struct qi::symbols<char, Module> moduleMap_;
storm::parser::prism::BinaryRelationOperatorStruct relationOperator_;
storm::parser::prism::BinaryBooleanOperatorStruct binaryBooleanOperator_;
storm::parser::prism::UnaryBooleanOperatorStruct unaryBooleanOperator_;
storm::parser::prism::BinaryNumericalOperatorStruct binaryNumericalOperator_;
storm::parser::prism::UnaryNumericalOperatorStruct unaryNumericalOperator_;
/*!
* Adds a label with the given name and expression to the given label-to-expression map.
*
* @param name The name of the label.
* @param expression The expression associated with the label.
* @param nameToExpressionMap The map to which the label is added.
*/
void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap);
/*!
* Adds a boolean assignment for the given variable with the given expression and adds it to the
* provided variable-to-assignment map.
*
* @param variable The name of the variable that the assignment targets.
* @param expression The expression that is assigned to the variable.
* @param variableToAssignmentMap The map to which the assignment is added.
*/
void addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
/*!
* Adds a boolean assignment for the given variable with the given expression and adds it to the
* provided variable-to-assignment map.
*
* @param variable The name of the variable that the assignment targets.
* @param expression The expression that is assigned to the variable.
* @param variableToAssignmentMap The map to which the assignment is added.
*/
void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
void addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap);
void addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap);
void addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap);
/*!
* Creates a module by renaming, i.e. takes the module given by the old name, creates a new module
* with the given name which renames all identifiers according to the given mapping.
*
* @param name The name of the new module.
* @param oldName The name of the module that is to be copied (modulo renaming).
* @param renaming A mapping from identifiers to their new names.
*/
Module renameModule(std::string const& name, std::string const& oldName, std::map<std::string, std::string> const& renaming);
/*!
* Creates a new module with the given name, boolean and integer variables and commands.
*
* @param name The name of the module to create.
* @param booleanVariables The boolean variables of the module.
* @param integerVariables The integer variables of the module.
* @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
* @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
* @param commands The commands associated with this module.
*/
Module createModule(std::string const& name, std::vector<BooleanVariable> const& booleanVariables, std::vector<IntegerVariable> const& integerVariables, std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap, std::vector<storm::ir::Command> const& commands);
/*!
* Creates an integer variable with the given name, domain and initial value and adds it to the
* provided list of integer variables and the given mappings.
*
* @param name The name of the integer variable.
* @param lower The expression that defines the lower bound of the domain.
* @param upper The expression that defines the upper bound of the domain.
* @param init The expression that defines the initial value of the variable.
* @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices.
* @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not.
*/
void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap, bool isGlobalVariable);
/*!
* Creates an boolean variable with the given name and initial value and adds it to the
* provided list of boolean variables and the given mappings.
*
* @param name The name of the boolean variable.
* @param init The expression that defines the initial value of the variable.
* @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices.
* @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not.
*/
void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap, bool isGlobalVariable);
/*!
* Creates a command with the given label, guard and updates.
*
* @param label The label of the command.
* @param guard The guard of the command.
* @param updates The updates associated with the command.
*/
Command createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates);
/*!
* Creates an update with the given likelihood and the given assignments to boolean and integer variables, respectively.
*
* @param likelihood The likelihood of this update being executed.
* @param booleanAssignments The assignments to boolean variables this update involves.
* @param integerAssignments The assignments to integer variables this update involves.
*/
Update createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& booleanAssignments, std::map<std::string, Assignment> const& integerAssignments);
// Helper methods that add data to data structures.
};
} // namespace prism
} // namespace parser
} // namespace storm

79
src/parser/prismparser/Tokens.h
View File

@ -1,7 +1,8 @@
#ifndef STORM_PARSER_PRISMPARSER_TOKENS_H_
#define STORM_PARSER_PRISMPARSER_TOKENS_H_
#include "src/storage/expressions/Expression.h"
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expressions.h"
namespace storm {
namespace parser {
@ -10,14 +11,14 @@ namespace storm {
* A structure mapping the textual representation of a model type to the model type
* representation of the intermediate representation.
*/
struct modelTypeStruct : qi::symbols<char, Program::ModelType> {
struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
modelTypeStruct() {
add
("dtmc", Program::ModelType::DTMC)
("ctmc", Program::ModelType::CTMC)
("mdp", Program::ModelType::MDP)
("ctmdp", Program::ModelType::CTMDP)
("ma", Program::ModelType::MA);
("dtmc", storm::prism::Program::ModelType::DTMC)
("ctmc", storm::prism::Program::ModelType::CTMC)
("mdp", storm::prism::Program::ModelType::MDP)
("ctmdp", storm::prism::Program::ModelType::CTMDP)
("ma", storm::prism::Program::ModelType::MA);
}
};
@ -45,17 +46,63 @@ namespace storm {
};
/*!
* A structure mapping the textual representation of a binary relation.
* A structure mapping the textual representation of binary relations to the corresponding enum values.
*/
struct relationalOperatorStruct : qi::symbols<char, BinaryRelationExpression::RelationType> {
relationalOperatorStruct() {
struct BinaryRelationOperatorStruct : qi::symbols<char, storm::expressions::BinaryRelationExpression::RelationType> {
BinaryRelationOperatorStruct() {
add
("=", BinaryRelationExpression::RelationType::EQUAL)
("!=", BinaryRelationExpression::RelationType::NOT_EQUAL)
("<", BinaryRelationExpression::RelationType::LESS)
("<=", BinaryRelationExpression::RelationType::LESS_OR_EQUAL)
(">", BinaryRelationExpression::RelationType::GREATER)
(">=", BinaryRelationExpression::RelationType::GREATER_OR_EQUAL);
("=", storm::expressions::BinaryRelationExpression::RelationType::Equal)
("!=", storm::expressions::BinaryRelationExpression::RelationType::NotEqual)
("<", storm::expressions::BinaryRelationExpression::RelationType::Less)
("<=", storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual)
(">", storm::expressions::BinaryRelationExpression::RelationType::Greater)
(">=", storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual);
}
};
/*!
* A structure mapping the textual representation of binary operators to the corresponding enum values.
*/
struct BinaryBooleanOperatorStruct : qi::symbols<char, storm::expressions::BinaryBooleanFunctionExpression::OperatorType> {
BinaryBooleanOperatorStruct() {
add
("&", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And)
("|", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or)
("=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies)
("<=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff);
}
};
/*!
* A structure mapping the textual representation of binary operators to the corresponding enum values.
*/
struct UnaryBooleanOperatorStruct : qi::symbols<char, storm::expressions::UnaryBooleanFunctionExpression::OperatorType> {
UnaryBooleanOperatorStruct() {
add
("!", storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not);
}
};
/*!
* A structure mapping the textual representation of binary boolean operators to the corresponding enum values.
*/
struct BinaryNumericalOperatorStruct : qi::symbols<char, storm::expressions::BinaryNumericalFunctionExpression::OperatorType> {
BinaryNumericalOperatorStruct() {
add
("+", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus)
("-", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus)
("*", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times)
("/", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide);
}
};
/*!
* A structure mapping the textual representation of binary operators to the corresponding enum values.
*/
struct UnaryNumericalOperatorStruct : qi::symbols<char, storm::expressions::UnaryNumericalFunctionExpression::OperatorType> {
UnaryNumericalOperatorStruct() {
add
("!", storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus);
}
};
}

2
src/storage/expressions/Expression.h
View File

@ -1,7 +1,7 @@
#ifndef STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
#define STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_
#include <functional>
#include <memory>
#include "src/storage/expressions/BaseExpression.h"

13
src/storage/expressions/Expressions.h
View File

@ -0,0 +1,13 @@
#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
#include "src/storage/expressions/BinaryRelationExpression.h"
#include "src/storage/expressions/BooleanConstantExpression.h"
#include "src/storage/expressions/BooleanLiteralExpression.h"
#include "src/storage/expressions/DoubleConstantExpression.h"
#include "src/storage/expressions/DoubleLiteralExpression.h"
#include "src/storage/expressions/IntegerConstantExpression.h"
#include "src/storage/expressions/IntegerLiteralExpression.h"
#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
#include "src/storage/expressions/VariableExpression.h"
#include "src/storage/expressions/Expression.h"

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

@ -5,7 +5,7 @@
namespace storm {
namespace prism {
Program::Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), definedBooleanConstants(definedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), definedIntegerConstants(definedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), definedDoubleConstants(definedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
Program::Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> const& definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> const& definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> const& definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::map<std::string, storm::expressions::Expression>const& formulas, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), definedBooleanConstants(definedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), definedIntegerConstants(definedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), definedDoubleConstants(definedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), formulas(formulas), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
// Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
Module const& module = this->getModule(moduleIndex);
@ -101,6 +101,10 @@ namespace storm {
return this->getGlobalIntegerVariables().size();
}
std::map<std::string, storm::expressions::Expression> const& Program::getFormulas() const {
return this->formulas;
}
std::size_t Program::getNumberOfModules() const {
return this->getModules().size();
}
@ -175,7 +179,7 @@ namespace storm {
newModules.push_back(module.restrictCommands(indexSet));
}
return Program(this->getModelType(), this->getUndefinedBooleanConstants(), this->getUndefinedIntegerConstants(), this->getUndefinedDoubleConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
return Program(this->getModelType(), this->getUndefinedBooleanConstants(), this->getDefinedBooleanConstants(), this->getUndefinedIntegerConstants(), this->getDefinedIntegerConstants(), this->getUndefinedDoubleConstants(), this->getDefinedDoubleConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
}
std::ostream& operator<<(std::ostream& stream, Program const& program) {

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

@ -32,6 +32,7 @@ namespace storm {
* @param definedDoubleConstants The defined double constants of the program.
* @param globalBooleanVariables The global boolean variables of the program.
* @param globalIntegerVariables The global integer variables of the program.
* @param formulas The formulas defined in the program.
* @param modules The modules of the program.
* @param hasInitialStatesExpression A flag indicating whether the program specifies its initial states via
* an explicit initial construct.
@ -43,7 +44,7 @@ namespace storm {
* @param filename The filename in which the program is defined.
* @param lineNumber The line number in which the program is defined.
*/
Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Program(ModelType modelType, std::set<std::string> const& undefinedBooleanConstants, std::map<std::string, storm::expressions::Expression> const& definedBooleanConstants, std::set<std::string> const& undefinedIntegerConstants, std::map<std::string, storm::expressions::Expression> const& definedIntegerConstants, std::set<std::string> const& undefinedDoubleConstants, std::map<std::string, storm::expressions::Expression> const& definedDoubleConstants, std::map<std::string, BooleanVariable> const& globalBooleanVariables, std::map<std::string, IntegerVariable> const& globalIntegerVariables, std::map<std::string, storm::expressions::Expression> const& formulas, std::vector<storm::prism::Module> const& modules, std::map<std::string, storm::prism::RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map<std::string, storm::expressions::Expression> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Provide default implementations for constructors and assignments.
Program() = default;
@ -173,6 +174,13 @@ namespace storm {
*/
std::size_t getNumberOfGlobalIntegerVariables() const;
/*!
* Retrieves the formulas defined in the program.
*
* @return The formulas defined in the program.
*/
std::map<std::string, storm::expressions::Expression> const& getFormulas() const;
/*!
* Retrieves the number of modules in the program.
*
@ -286,12 +294,15 @@ namespace storm {
// A mapping of (defined) double constants to their values (given as expressions).
std::map<std::string, storm::expressions::Expression> definedDoubleConstants;
// A list of global boolean variables.
// The global boolean variables.
std::map<std::string, BooleanVariable> globalBooleanVariables;
// A list of global integer variables.
// The global integer variables.
std::map<std::string, IntegerVariable> globalIntegerVariables;
// A mapping of formula names to the corresponding expressions.
std::map<std::string, storm::expressions::Expression> formulas;
// The modules associated with the program.
std::vector<storm::prism::Module> modules;

63
src/storage/prism/Update.cpp
View File

@ -3,25 +3,17 @@
namespace storm {
namespace prism {
Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), globalIndex(globalIndex) {
// Nothing to do here.
}
Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), booleanAssignments(), integerAssignments(), globalIndex(newGlobalIndex) {
for (auto const& variableAssignmentPair : update.getBooleanAssignments()) {
Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute<std::map>(renaming)), assignments(), globalIndex(newGlobalIndex) {
for (auto const& variableAssignmentPair : update.getAssignments()) {
auto const& namePair = renaming.find(variableAssignmentPair.first);
if (namePair != renaming.end()) {
this->booleanAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
this->assignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
} else {
this->booleanAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
}
}
for (auto const& variableAssignmentPair : update.getIntegerAssignments()) {
auto const& namePair = renaming.find(variableAssignmentPair.first);
if (renaming.count(variableAssignmentPair.first) > 0) {
this->integerAssignments.emplace(namePair->second, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
} else {
this->integerAssignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
this->assignments.emplace(variableAssignmentPair.first, Assignment(variableAssignmentPair.second, renaming, filename, lineNumber));
}
}
this->likelihoodExpression = update.getLikelihoodExpression().substitute<std::map>(renaming);
@ -31,35 +23,18 @@ namespace storm {
return likelihoodExpression;
}
std::size_t Update::getNumberOfBooleanAssignments() const {
return booleanAssignments.size();
}
std::size_t Update::getNumberOfIntegerAssignments() const {
return integerAssignments.size();
}
std::map<std::string, storm::prism::Assignment> const& Update::getBooleanAssignments() const {
return booleanAssignments;
}
std::map<std::string, storm::prism::Assignment> const& Update::getIntegerAssignments() const {
return integerAssignments;
std::size_t Update::getNumberOfAssignments() const {
return this->assignments.size();
}
storm::prism::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const {
auto variableAssignmentPair = booleanAssignments.find(variableName);
if (variableAssignmentPair == booleanAssignments.end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '" << variableName << "' in update " << *this << ".";
}
return variableAssignmentPair->second;
std::map<std::string, storm::prism::Assignment> const& Update::getAssignments() const {
return this->assignments;
}
storm::prism::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const {
auto variableAssignmentPair = integerAssignments.find(variableName);
if (variableAssignmentPair == integerAssignments.end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '" << variableName << "' in update " << *this << ".";
storm::prism::Assignment const& Update::getAssignment(std::string const& variableName) const {
auto variableAssignmentPair = this->getAssignments().find(variableName);
if (variableAssignmentPair == this->getAssignments().end()) {
throw storm::exceptions::OutOfRangeException() << "Cannot find assignment for variable '" << variableName << "' in update " << *this << ".";
}
return variableAssignmentPair->second;
@ -72,17 +47,9 @@ namespace storm {
std::ostream& operator<<(std::ostream& stream, Update const& update) {
stream << update.getLikelihoodExpression() << " : ";
uint_fast64_t i = 0;
for (auto const& assignment : update.getBooleanAssignments()) {
stream << assignment.second;
if (i < update.getBooleanAssignments().size() - 1 || update.getIntegerAssignments().size() > 0) {
stream << " & ";
}
++i;
}
i = 0;
for (auto const& assignment : update.getIntegerAssignments()) {
for (auto const& assignment : update.getAssignments()) {
stream << assignment.second;
if (i < update.getIntegerAssignments().size() - 1) {
if (i < update.getAssignments().size() - 1) {
stream << " & ";
}
++i;

48
src/storage/prism/Update.h
View File

@ -20,7 +20,7 @@ namespace storm {
* @param filename The filename in which the variable is defined.
* @param lineNumber The line number in which the variable is defined.
*/
Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& booleanAssignments, std::map<std::string, storm::prism::Assignment> const& integerAssignments, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Update(uint_fast64_t index, storm::expressions::Expression const& likelihoodExpression, std::map<std::string, storm::prism::Assignment> const& assignments, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given update and performs the provided renaming.
@ -48,46 +48,25 @@ namespace storm {
storm::expressions::Expression const& getLikelihoodExpression() const;
/*!
* Retrieves the number of boolean assignments associated with this update.
* Retrieves the number of assignments associated with this update.
*
* @return The number of boolean assignments associated with this update.
* @return The number of assignments associated with this update.
*/
std::size_t getNumberOfBooleanAssignments() const;
std::size_t getNumberOfAssignments() const;
/*!
* Retrieves the number of integer assignments associated with this update.
* Retrieves a reference to the map of variable names to their respective assignments.
*
* @return The number of integer assignments associated with this update.
* @return A reference to the map of variable names to their respective assignments.
*/
std::size_t getNumberOfIntegerAssignments() const;
std::map<std::string, storm::prism::Assignment> const& getAssignments() const;
/*!
* Retrieves a reference to the map of boolean variable names to their respective assignments.
* Retrieves a reference to the assignment for the variable with the given name.
*
* @return A reference to the map of boolean variable names to their respective assignments.
* @return A reference to the assignment for the variable with the given name.
*/
std::map<std::string, storm::prism::Assignment> const& getBooleanAssignments() const;
/*!
* Retrieves a reference to the map of integer variable names to their respective assignments.
*
* @return A reference to the map of integer variable names to their respective assignments.
*/
std::map<std::string, storm::prism::Assignment> const& getIntegerAssignments() const;
/*!
* Retrieves a reference to the assignment for the boolean variable with the given name.
*
* @return A reference to the assignment for the boolean variable with the given name.
*/
storm::prism::Assignment const& getBooleanAssignment(std::string const& variableName) const;
/*!
* Retrieves a reference to the assignment for the integer variable with the given name.
*
* @return A reference to the assignment for the integer variable with the given name.
*/
storm::prism::Assignment const& getIntegerAssignment(std::string const& variableName) const;
storm::prism::Assignment const& getAssignment(std::string const& variableName) const;
/*!
* Retrieves the global index of the update, that is, a unique index over all modules.
@ -102,11 +81,8 @@ namespace storm {
// An expression specifying the likelihood of taking this update.
storm::expressions::Expression likelihoodExpression;
// A mapping of boolean variable names to their assignments in this update.
std::map<std::string, storm::prism::Assignment> booleanAssignments;
// A mapping of integer variable names to their assignments in this update.
std::map<std::string, storm::prism::Assignment> integerAssignments;
// A mapping of variable names to their assignments in this update.
std::map<std::string, storm::prism::Assignment> assignments;
// The global index of the update.
uint_fast64_t globalIndex;

32
test/functional/parser/ParsePrismTest.cpp
View File

@ -1,32 +0,0 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/PrismParser.h"
//#include "src/utility/IoUtility.h"
#include "src/ir/Program.h"
#include "src/adapters/ExplicitModelAdapter.h"
#include "src/models/Dtmc.h"
#include "src/models/Mdp.h"
#include "src/settings/Settings.h"
#include "src/settings/InternalOptionMemento.h"
TEST(ParsePrismTest, parseCrowds5_5) {
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(storm::settings::Settings::getInstance()->isSet("fixDeadlocks"));
storm::ir::Program program;
ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.pm"));
std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program);
ASSERT_EQ(model->getNumberOfStates(), 8607ull);
ASSERT_EQ(model->getNumberOfTransitions(), 15113ull);
}
TEST(ParsePrismTest, parseTwoDice) {
storm::ir::Program program;
ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.nm"));
std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, "", "coinflips");
ASSERT_EQ(model->getNumberOfStates(), 169ull);
ASSERT_EQ(model->as<storm::models::AbstractNondeterministicModel<double>>()->getNumberOfChoices(), 254ull);
ASSERT_EQ(model->getNumberOfTransitions(), 436ull);
}
Write Preview
Loading…
Cancel
Save