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

Further work on PrismParser and the related PRISM classes... 

Former-commit-id: be4ae055dd
tempestpy_adaptions
dehnert 11 years ago
parent
e67eb05309
commit
f6587b424d
23 changed files with 925 additions and 385 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. 98
      src/parser/PrismParser.cpp
  2. 35
      src/parser/PrismParser.h
  3. 415
      src/parser/prismparser/PrismGrammar.cpp
  4. 230
      src/parser/prismparser/PrismGrammar.h
  5. 70
      src/parser/prismparser/PrismParser.cpp
  6. 36
      src/parser/prismparser/PrismParser.h
  7. 4
      src/storage/expressions/BinaryBooleanFunctionExpression.cpp
  8. 4
      src/storage/expressions/Expression.cpp
  9. 1
      src/storage/expressions/Expression.h
  10. 4
      src/storage/prism/BooleanVariable.h
  11. 8
      src/storage/prism/Command.cpp
  12. 3
      src/storage/prism/Command.h
  13. 3
      src/storage/prism/Constant.cpp
  14. 2
      src/storage/prism/IntegerVariable.cpp
  15. 8
      src/storage/prism/LocatedInformation.cpp
  16. 14
      src/storage/prism/LocatedInformation.h
  17. 37
      src/storage/prism/Module.cpp
  18. 6
      src/storage/prism/Module.h
  19. 106
      src/storage/prism/Program.cpp
  20. 49
      src/storage/prism/Program.h
  21. 15
      src/storage/prism/Update.cpp
  22. 5
      src/storage/prism/Update.h
  23. 157
      test/functional/parser/PrismParserTest.cpp

98
src/parser/PrismParser.cpp
View File

@ -1,98 +0,0 @@
#include "src/parser/PrismParser.h"
#include "src/parser/prismparser/PrismGrammar.h"
// If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/WrongFormatException.h"
// Needed for file IO.
#include <fstream>
#include <iomanip>
#include <limits>
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
#include "log4cplus/consoleappender.h"
#include "log4cplus/fileappender.h"
log4cplus::Logger logger;
namespace storm {
namespace parser {
storm::prism::Program PrismParserFromFile(std::string const& filename) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
storm::prism::Program result;
// Now try to parse the contents of the file.
try {
result = PrismParser(inputFileStream, filename);
} catch(std::exception& e) {
// In case of an exception properly close the file before passing exception.
inputFileStream.close();
throw e;
}
// Close the stream in case everything went smoothly and return result.
inputFileStream.close();
return result;
}
storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename) {
// Prepare iterators to input.
// TODO: Right now, this parses the whole contents of the file into a string first.
// While this is usually not necessary, because there exist adapters that make an input stream
// iterable in both directions without storing it into a string, using the corresponding
// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
std::string fileContent((std::istreambuf_iterator<char>(inputStream)), (std::istreambuf_iterator<char>()));
BaseIteratorType stringIteratorBegin = fileContent.begin();
BaseIteratorType stringIteratorEnd = fileContent.end();
PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename);
PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename);
PositionIteratorType positionIteratorEnd;
// Prepare resulting intermediate representation of input.
storm::prism::Program result;
// In order to instantiate the grammar, we have to pass the type of the skipping parser.
// As this is more complex, we let Boost figure out the actual type for us.
storm::parser::prism::PrismGrammar grammar;
try {
// Now parse the content using phrase_parse in order to be able to supply a skipping parser.
// First run.
LOG4CPLUS_INFO(logger, "Start parsing...");
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
LOG4CPLUS_INFO(logger, "Finished parsing, here is the parsed program:" << std::endl << result);
} catch(const qi::expectation_failure<PositionIteratorType>& e) {
// If the parser expected content different than the one provided, display information
// about the location of the error.
const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
// Construct the error message including a caret display of the position in the
// erroneous line.
std::stringstream msg;
std::string line = e.first.get_currentline();
while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," ");
msg << pos.file << ", line " << pos.line << ", column " << pos.column
<< ": parse error: expected " << e.what_ << std::endl << "\t"
<< line << std::endl << "\t";
int i = 0;
for (i = 1; i < pos.column; ++i) {
msg << "-";
}
msg << "^";
for (; i < 80; ++i) {
msg << "-";
}
msg << std::endl;
std::cerr << msg.str();
// Now propagate exception.
throw storm::exceptions::WrongFormatException() << msg.str();
}
return result;
}
} // namespace parser
} // namespace storm

35
src/parser/PrismParser.h
View File

@ -1,35 +0,0 @@
#ifndef STORM_PARSER_PRISMPARSER_H_
#define STORM_PARSER_PRISMPARSER_H_
// All classes of the intermediate representation are used.
#include "src/storage/prism/Program.h"
// Used for file input.
#include <istream>
namespace storm {
namespace parser {
using namespace storm::prism;
using namespace storm::expressions;
/*!
* Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
*
* @param filename the name of the file to parse.
* @return The resulting PRISM program.
*/
storm::prism::Program PrismParserFromFile(std::string const& filename);
/*!
* Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax.
*
* @param inputStream The input stream to parse.
* @param filename The name of the file the input stream belongs to.
* @return The resulting PRISM program.
*/
storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename);
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_PRISMPARSER_H_ */

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

@ -1,153 +1,372 @@
// #define BOOST_SPIRIT_DEBUG
#include "src/parser/prismparser/PrismGrammar.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
namespace parser {
namespace prism {
PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start) {
PrismGrammar::PrismGrammar(std::string const& filename, Iterator first) : PrismGrammar::base_type(start), doExpressionGeneration(false), filename(filename), annotate(first) {
// Parse simple identifier.
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]] - keywords_;
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismGrammar::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
// Parse a composed expression.
expression %= (booleanExpression | numericalExpression);
expression.name("expression");
setExpressionGeneration(doExpressionGeneration);
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");
modelTypeDefinition = modelType_;
modelTypeDefinition %= modelType_;
modelTypeDefinition.name("model type");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r1) | undefinedDoubleConstantDefinition(qi::_r1));
undefinedConstantDefinition.name("undefined constant definition");
undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, phoenix::bind(&GlobalProgramInformation::undefinedBooleanConstants, qi::_r1), qi::_1)];
undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, phoenix::bind(&GlobalProgramInformation::undefinedIntegerConstants, qi::_r1), qi::_1)];
undefinedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, phoenix::bind(&GlobalProgramInformation::undefinedDoubleConstants, qi::_r1), qi::_1)];
undefinedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)];
undefinedDoubleConstantDefinition.name("undefined double constant definition");
definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r1) | definedDoubleConstantDefinition(qi::_r1));
definedConstantDefinition.name("defined constant definition");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
undefinedConstantDefinition.name("undefined constant definition");
definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedBooleanConstant, phoenix::bind(&GlobalProgramInformation::definedBooleanConstants, qi::_r1), qi::_1, qi::_2)];
definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedIntegerConstant, phoenix::bind(&GlobalProgramInformation::definedIntegerConstants, qi::_r1), qi::_1, qi::_2)];
definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedDoubleConstant, phoenix::bind(&GlobalProgramInformation::definedDoubleConstants, qi::_r1), qi::_1, qi::_2)];
definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedDoubleConstantDefinition.name("defined double constant declaration");
formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addFormula, phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1, qi::_2)];
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant definition");
formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition.name("formula definition");
globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1)) | integerVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1))));
booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
booleanVariableDefinition.name("boolean variable definition");
integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismGrammar::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression[qi::_a = qi::_1] > qi::lit("..") > expression > qi::lit("]")[phoenix::bind(&PrismGrammar::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
integerVariableDefinition.name("integer variable definition");
variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
variableDefinition.name("variable declaration");
globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
globalVariableDefinition.name("global variable declaration list");
programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1]
> *( undefinedConstantDefinition(qi::_r1)
| definedConstantDefinition(qi::_r1)
| formulaDefinition(qi::_r1)
| globalVariableDefinition(qi::_r1)
);
programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1]
> *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)])
> *(formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1)])
> *(globalVariableDefinition(qi::_r1));
programHeader.name("program header");
rewardModelDefinition = (qi::lit("rewards") > qi::lit("\"") > identifier > qi::lit("\"")
> +( stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)]
| transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]
)
>> qi::lit("endrewards"))[phoenix::bind(&PrismGrammar::addRewardModel, phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_r1), qi::_1, qi::_a, qi::_b)];
rewardModelDefinition.name("reward model definition");
stateRewardDefinition = (booleanExpression > qi::lit(":") > numericalExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createStateReward, qi::_1, qi::_2)];
stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createTransitionReward, qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit(":") > plusExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition.name("transition reward definition");
labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > booleanExpression >> qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addLabel, phoenix::bind(&GlobalProgramInformation::labels, qi::_r1), qi::_1, qi::_2)];
rewardModelDefinition = (qi::lit("rewards") > qi::lit("\"") > identifier > qi::lit("\"")
> +( stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)]
| transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]
)
>> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismGrammar::createRewardModel, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)];
rewardModelDefinition.name("reward model definition");
initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismGrammar::addInitialStatesExpression, phoenix::ref(*this), qi::_1, qi::_r1)];
initialStatesConstruct.name("initial construct");
labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
labelDefinition.name("label definition");
assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_pass = phoenix::bind(&PrismGrammar::addAssignment, qi::_r1, qi::_1, qi::_2)];
assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&PrismGrammar::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
assignmentDefinition.name("assignment");
assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&";
assignmentDefinitionList.name("assignment list");
moduleDefinitionList %= +(moduleDefinition(qi::_r1) | moduleRenaming(qi::_r1));
moduleDefinitionList.name("module list");
assignmentDefinitionList %= +assignmentDefinition % "&";
assignmentDefinitionList.name("assignment list");
updateDefinition = (((numericalExpression >> qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList(qi::_a))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, qi::_1, qi::_a)];
updateDefinition = (((plusExpression > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
updateDefinition.name("update");
updateListDefinition %= +updateDefinition % "+";
updateListDefinition %= +updateDefinition(qi::_r1) % "+";
updateListDefinition.name("update list");
commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createCommand, qi::_a, qi::_2, qi::_3)];
commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
commandDefinition.name("command definition");
booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > booleanExpression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addBooleanVariable, qi::_r1, qi::_1, qi::_2)];
booleanVariableDefinition.name("boolean variable definition");
integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")) > numericalExpression[qi::_a = qi::_1] > qi::lit("..") > numericalExpression > qi::lit("]") > -(qi::lit("init") > numericalExpression[qi::_a = qi::_1]) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addIntegerVariable, qi::_r1, qi::_1, qi::_2, qi::_3, qi::_a)];
integerVariableDefinition.name("integer variable definition");
variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2));
variableDefinition.name("variable declaration");
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createModule, qi::_1, qi::_a, qi::_b, qi::_2)];
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
moduleDefinition.name("module definition");
moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")
moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")
> ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] % ",") > qi::lit("]")
> qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createRenamedModule, qi::_1, qi::_2, qi::_a, qi::_r1)];
> qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_2, qi::_a, qi::_r1)];
moduleRenaming.name("module definition via renaming");
start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(rewardModelDefinition(qi::_a) | labelDefinition(qi::_a)))[qi::_val = phoenix::bind(&PrismGrammar::createProgram, qi::_a, qi::_1)];
moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)];
moduleDefinitionList.name("module list");
start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(initialStatesConstruct(qi::_a) | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismGrammar::createProgram, phoenix::ref(*this), qi::_a)];
start.name("probabilistic program");
// Enable location tracking for important entities.
auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction);
qi::on_success(undefinedIntegerConstantDefinition, setLocationInfoFunction);
qi::on_success(undefinedDoubleConstantDefinition, setLocationInfoFunction);
qi::on_success(definedBooleanConstantDefinition, setLocationInfoFunction);
qi::on_success(definedIntegerConstantDefinition, setLocationInfoFunction);
qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction);
qi::on_success(booleanVariableDefinition, setLocationInfoFunction);
qi::on_success(integerVariableDefinition, setLocationInfoFunction);
qi::on_success(moduleDefinition, setLocationInfoFunction);
qi::on_success(moduleRenaming, setLocationInfoFunction);
qi::on_success(formulaDefinition, setLocationInfoFunction);
qi::on_success(rewardModelDefinition, setLocationInfoFunction);
qi::on_success(labelDefinition, setLocationInfoFunction);
qi::on_success(commandDefinition, setLocationInfoFunction);
qi::on_success(updateDefinition, setLocationInfoFunction);
qi::on_success(assignmentDefinition, setLocationInfoFunction);
}
void PrismGrammar::setExpressionGeneration(bool doExpressionGeneration) {
if (doExpressionGeneration) {
floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> 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("floor/ceil expression");
minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> 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");
identifierExpression = identifier[qi::_val = phoenix::bind(&PrismGrammar::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
identifierExpression.name("identifier expression");
literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&storm::expressions::Expression::createTrue)] | qi::lit("false")[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)] | strict_double[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleLiteral, qi::_1)] | qi::int_[qi::_val = phoenix::bind(&storm::expressions::Expression::createIntegerLiteral, qi::_1)];
literalExpression.name("literal expression");
atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression;
atomicExpression.name("atomic expression");
unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = !qi::_1] | (qi::lit("-") >> atomicExpression)[qi::_val = -qi::_1];
unaryExpression.name("unary expression");
multiplicationExpression = unaryExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> unaryExpression[phoenix::if_(qi::_a) [qi::_val = qi::_val * qi::_1] .else_ [qi::_val = qi::_val / qi::_1]]);
multiplicationExpression.name("multiplication 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("plus expression");
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = qi::_1 >= qi::_1] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = qi::_1 > qi::_2] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = qi::_1 <= qi::_2] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = qi::_1 < qi::_2] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = qi::_1 == qi::_2] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = qi::_1 != qi::_2] | plusExpression[qi::_val = qi::_1];
relativeExpression.name("relative expression");
andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = qi::_val && qi::_1];
andExpression.name("and expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = qi::_val || qi::_1];
orExpression.name("or expression");
expression %= orExpression;
expression.name("expression");
} else {
floorCeilExpression = ((qi::lit("floor") | qi::lit("ceil")) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
floorCeilExpression.name("floor/ceil expression");
minMaxExpression = ((qi::lit("min") | qi::lit("max")) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
minMaxExpression.name("min/max expression");
identifierExpression = identifier[qi::_val = phoenix::construct<storm::expressions::Expression>(), qi::_pass = phoenix::bind(&PrismGrammar::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifierExpression.name("identifier expression");
literalExpression = (qi::lit("true") | qi::lit("false") | strict_double | qi::int_)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
literalExpression.name("literal expression");
atomicExpression = (minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
atomicExpression.name("atomic expression");
unaryExpression = (atomicExpression | (qi::lit("!") >> atomicExpression) | (qi::lit("-") >> atomicExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
unaryExpression.name("unary expression");
multiplicationExpression = (unaryExpression >> *((qi::lit("*") | qi::lit("/")) >> unaryExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
multiplicationExpression.name("multiplication expression");
plusExpression = (multiplicationExpression >> *((qi::lit("+") | qi::lit("-")) >> multiplicationExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
plusExpression.name("plus expression");
relativeExpression = ((plusExpression >> qi::lit(">=") >> plusExpression) | (plusExpression >> qi::lit(">") >> plusExpression) | (plusExpression >> qi::lit("<=") >> plusExpression) | (plusExpression >> qi::lit("<") >> plusExpression) | (plusExpression >> qi::lit("=") >> plusExpression) | (plusExpression >> qi::lit("!=") >> plusExpression) | plusExpression)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
relativeExpression.name("relative expression");
andExpression = (relativeExpression >> *(qi::lit("&") >> relativeExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
andExpression.name("and expression");
orExpression = (andExpression >> *(qi::lit("|") >> andExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
orExpression.name("or expression");
expression %= orExpression;
expression.name("expression");
}
// Enable error reporting.
qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
// Finally toggle the internal flag.
this->doExpressionGeneration = doExpressionGeneration;
}
void PrismGrammar::toggleExpressionGeneration() {
setExpressionGeneration(!doExpressionGeneration);
}
void PrismGrammar::allowDoubleLiterals(bool flag) {
if (flag) {
if (this->doExpressionGeneration) {
literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&storm::expressions::Expression::createTrue)] | qi::lit("false")[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)] | strict_double[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleLiteral, qi::_1)] | qi::int_[qi::_val = phoenix::bind(&storm::expressions::Expression::createIntegerLiteral, qi::_1)];
literalExpression.name("literal expression");
} else {
literalExpression = (qi::lit("true") | qi::lit("false") | strict_double | qi::int_)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
literalExpression.name("literal expression");
}
} else {
if (this->doExpressionGeneration) {
literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&storm::expressions::Expression::createTrue)] | qi::lit("false")[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)] | qi::int_[qi::_val = phoenix::bind(&storm::expressions::Expression::createIntegerLiteral, qi::_1)];
literalExpression.name("literal expression");
} else {
literalExpression = (qi::lit("true") | qi::lit("false") | qi::int_)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)];
literalExpression.name("literal expression");
}
}
}
std::string const& PrismGrammar::getFilename() const {
return this->filename;
}
bool PrismGrammar::isValidIdentifier(std::string const& identifier) {
if (this->keywords_.find(identifier) != nullptr) {
return false;
}
return true;
}
bool PrismGrammar::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::InvalidArgumentException, "Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialStatesExpression) {
return false;
}
globalProgramInformation.hasInitialStatesExpression = true;
globalProgramInformation.initialStatesExpression = initialStatesExpression;
return true;
}
storm::expressions::Expression PrismGrammar::getIdentifierExpression(std::string const& identifier) const {
storm::expressions::Expression const* expression = this->identifiers_.find(identifier);
LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Undeclared identifier '" << identifier << "'.");
return *expression;
}
storm::prism::Constant PrismGrammar::createUndefinedBooleanConstant(std::string const& newConstant) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
return storm::prism::Constant(storm::prism::Constant::ConstantType::Bool, newConstant, this->getFilename());
}
storm::prism::Constant PrismGrammar::createUndefinedIntegerConstant(std::string const& newConstant) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
return storm::prism::Constant(storm::prism::Constant::ConstantType::Integer, newConstant, this->getFilename());
}
storm::prism::Constant PrismGrammar::createUndefinedDoubleConstant(std::string const& newConstant) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
return storm::prism::Constant(storm::prism::Constant::ConstantType::Double, newConstant, this->getFilename());
}
storm::prism::Constant PrismGrammar::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
return storm::prism::Constant(storm::prism::Constant::ConstantType::Bool, newConstant, expression, this->getFilename());
}
storm::prism::Constant PrismGrammar::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
return storm::prism::Constant(storm::prism::Constant::ConstantType::Integer, newConstant, expression, this->getFilename());
}
storm::prism::Constant PrismGrammar::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
return storm::prism::Constant(storm::prism::Constant::ConstantType::Double, newConstant, expression, this->getFilename());
}
storm::prism::Formula PrismGrammar::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
this->identifiers_.add(formulaName, expression);
return storm::prism::Formula(formulaName, expression, this->getFilename());
}
storm::prism::Label PrismGrammar::createLabel(std::string const& labelName, storm::expressions::Expression expression) const {
return storm::prism::Label(labelName, expression, this->getFilename());
}
storm::prism::RewardModel PrismGrammar::createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const {
return storm::prism::RewardModel(rewardModelName, stateRewards, transitionRewards, this->getFilename());
}
storm::prism::StateReward PrismGrammar::createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const {
return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename());
}
storm::prism::TransitionReward PrismGrammar::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const {
return storm::prism::TransitionReward(actionName, statePredicateExpression, rewardValueExpression, this->getFilename());
}
storm::prism::Assignment PrismGrammar::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {
return storm::prism::Assignment(variableName, assignedExpression, this->getFilename());
}
storm::prism::Update PrismGrammar::createUpdate(storm::expressions::Expression likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, GlobalProgramInformation& globalProgramInformation) const {
++globalProgramInformation.currentUpdateIndex;
return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpression, assignments, this->getFilename());
}
storm::prism::Command PrismGrammar::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const {
++globalProgramInformation.currentCommandIndex;
return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName, guardExpression, updates, this->getFilename());
}
storm::prism::BooleanVariable PrismGrammar::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
}
storm::prism::IntegerVariable PrismGrammar::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
}
storm::prism::Module PrismGrammar::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 {
globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
return storm::prism::Module(moduleName, booleanVariables, integerVariables, commands, this->getFilename());
}
storm::prism::Module PrismGrammar::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "No module named '" << oldModuleName << "' to rename.");
globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
uint_fast64_t commandBaseIndex = globalProgramInformation.currentCommandIndex;
uint_fast64_t updateBaseIndex = globalProgramInformation.currentUpdateIndex;
storm::prism::Module const& moduleToClone = globalProgramInformation.modules[moduleIndexPair->second];
globalProgramInformation.currentCommandIndex += moduleToClone.getNumberOfCommands();
globalProgramInformation.currentUpdateIndex += moduleToClone.getNumberOfUpdates();
return storm::prism::Module(moduleToClone, newModuleName, commandBaseIndex, updateBaseIndex, renaming, this->getFilename());
}
storm::prism::Program PrismGrammar::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, globalProgramInformation.hasInitialStatesExpression, globalProgramInformation.initialStatesExpression, globalProgramInformation.labels, this->getFilename());
}
} // namespace prism
} // namespace parser

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

@ -4,33 +4,32 @@
// Include files for file input.
#include <istream>
#include <memory>
#include <iomanip>
// Include boost spirit.
#define BOOST_SPIRIT_USE_PHOENIX_V3
#include <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
#include <boost/spirit/include/classic_position_iterator.hpp>
#include <boost/spirit/include/support_multi_pass.hpp>
#include <boost/spirit/include/support_line_pos_iterator.hpp>
#include <boost/spirit/home/classic/iterator/position_iterator.hpp>
namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
typedef boost::spirit::line_pos_iterator<BaseIteratorType> PositionIteratorType;
typedef PositionIteratorType Iterator;
typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
typedef boost::spirit::unused_type Unused;
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h"
#include "src/exceptions/ExceptionMacros.h"
namespace storm {
namespace parser {
namespace prism {
struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
modelTypeStruct() {
add
@ -42,7 +41,7 @@ namespace storm {
}
};
struct keywordsStruct : qi::symbols<char, unsigned> {
struct keywordsStruct : qi::symbols<char, bool> {
keywordsStruct() {
add
("dtmc", 1)
@ -58,7 +57,12 @@ namespace storm {
("rewards", 11)
("endrewards", 12)
("true", 13)
("false", 14);
("min", 14)
("max", 15)
("floor", 16)
("ceil", 17)
("init", 18)
("endinit", 19);
}
};
@ -69,32 +73,104 @@ namespace storm {
// Members for all essential information that needs to be collected.
storm::prism::Program::ModelType modelType;
std::set<std::string> undefinedBooleanConstants;
std::set<std::string> undefinedIntegerConstants;
std::set<std::string> undefinedDoubleConstants;
std::map<std::string, storm::expressions::Expression> definedBooleanConstants;
std::map<std::string, storm::expressions::Expression> definedIntegerConstants;
std::map<std::string, storm::expressions::Expression> definedDoubleConstants;
std::map<std::string, storm::expressions::Expression> formulas;
std::map<std::string, storm::prism::BooleanVariable> globalBooleanVariables;
std::map<std::string, storm::prism::IntegerVariable> globalIntegerVariables;
std::map<std::string, storm::prism::Module> modules;
std::map<std::string, storm::prism::RewardModel> rewardModels;
std::map<std::string, storm::expressions::Expression> labels;
std::vector<storm::prism::Constant> constants;
std::vector<storm::prism::Formula> formulas;
std::vector<storm::prism::BooleanVariable> globalBooleanVariables;
std::vector<storm::prism::IntegerVariable> globalIntegerVariables;
std::map<std::string, uint_fast64_t> moduleToIndexMap;
std::vector<storm::prism::Module> modules;
std::vector<storm::prism::RewardModel> rewardModels;
std::vector<storm::prism::Label> labels;
storm::expressions::Expression initialStatesExpression;
bool hasInitialStatesExpression;
// Counters to provide unique indexing for commands and updates.
uint_fast64_t currentCommandIndex;
uint_fast64_t currentUpdateIndex;
};
// Functor used for displaying error information.
struct ErrorHandler {
typedef qi::error_handler_result result_type;
template<typename T1, typename T2, typename T3, typename T4>
qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
// LOG4CPLUS_ERROR(logger, "Error: expecting " << what << " in line " << get_line(where) << " at column " << get_column(b, where, 4) << ".");
std::cerr << "Error: expecting " << what << " in line " << get_line(where) << "." << std::endl;
T3 end(where);
while (end != e && *end != '\r' && *end != '\n') {
++end;
}
std::cerr << "Error: expecting " << what << " in line " << get_line(where) << ": \n" << std::string(get_line_start(b, where), end) << " ... \n" << std::setw(std::distance(b, where)) << '^' << "---- here\n";
return qi::fail;
}
};
// Functor used for annotating entities with line number information.
class PositionAnnotation {
public:
typedef void result_type;
PositionAnnotation(Iterator first) : first(first) {
// Intentionally left empty.
}
template<typename Entity, typename First, typename Last>
result_type operator()(Entity& entity, First f, Last l) const {
entity.setLineNumber(get_line(f));
}
private:
std::string filename;
Iterator const first;
};
class PrismGrammar : public qi::grammar<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> {
public:
/*!
* Default constructor that creates an empty and functional grammar.
* Creates a grammar for the given filename and the iterator to the first input to parse.
*
* @param filename The filename that is to be read. This is used for proper error reporting.
* @param first The iterator to the beginning of the input.
*/
PrismGrammar(std::string const& filename, Iterator first);
/*!
* Toggles whether or not expressions are generated.
*/
PrismGrammar();
void toggleExpressionGeneration();
private:
// A flag that stores whether the grammar currently generates expressions or not.
bool doExpressionGeneration;
/*!
* Sets the expression generation to the desired value.
*
* @param doExpressionGeneration A flag that sets whether or not expressions are generated.
*/
void setExpressionGeneration(bool doExpressionGeneration);
/*!
* Sets whether doubles literals are allowed in the parsed expression.
*
* @param flag Indicates whether to allow or forbid double literals in the parsed expression.
*/
void allowDoubleLiterals(bool flag);
// The name of the file being parsed.
std::string filename;
/*!
* Retrieves the name of the file currently being parsed.
*
* @return The name of the file currently being parsed.
*/
std::string const& getFilename() const;
// A function used for annotating the entities with their position.
phoenix::function<ErrorHandler> handler;
phoenix::function<PositionAnnotation> annotate;
// The starting point of the grammar.
qi::rule<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> start;
@ -103,14 +179,14 @@ namespace storm {
// Rules for parsing the program header.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> programHeader;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> definedDoubleConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> definedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> definedDoubleConstantDefinition;
// Rules for global variable definitions.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalVariableDefinition;
@ -119,81 +195,83 @@ namespace storm {
// Rules for modules definition.
qi::rule<Iterator, std::vector<storm::prism::Module>(GlobalProgramInformation&), Skipper> moduleDefinitionList;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, storm::prism::BooleanVariable>, std::map<std::string, storm::prism::IntegerVariable>>, Skipper> moduleDefinition;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>>, Skipper> moduleDefinition;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::BooleanVariable>&, std::map<std::string, storm::prism::IntegerVariable>&), Skipper> variableDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::BooleanVariable>&), Skipper> booleanVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::IntegerVariable>&), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&), Skipper> variableDefinition;
qi::rule<Iterator, storm::prism::BooleanVariable(), Skipper> booleanVariableDefinition;
qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, storm::prism::Command(), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<storm::prism::Update>(), Skipper> updateListDefinition;
qi::rule<Iterator, storm::prism::Update(), qi::locals<std::map<std::string, storm::prism::Assignment>>, Skipper> updateDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::prism::Assignment>&), Skipper> assignmentDefinitionList;
qi::rule<Iterator, storm::prism::Assignment(std::map<std::string, storm::prism::Assignment>&), Skipper> assignmentDefinition;
qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<storm::prism::Update>(GlobalProgramInformation&), Skipper> updateListDefinition;
qi::rule<Iterator, storm::prism::Update(GlobalProgramInformation&), Skipper> updateDefinition;
qi::rule<Iterator, std::vector<storm::prism::Assignment>(), Skipper> assignmentDefinitionList;
qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
// Rules for reward definitions.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
qi::rule<Iterator, storm::prism::RewardModel(), qi::locals<std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, storm::prism::TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
// Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
// Rules for label definitions.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> labelDefinition;
qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition;
// Rules for formula definitions.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> formulaDefinition;
qi::rule<Iterator, storm::prism::Formula(), 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> multiplicationExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
// Parsers that recognize special keywords and model types.
storm::parser::prism::keywordsStruct keywords_;
storm::parser::prism::modelTypeStruct modelType_;
qi::symbols<char, storm::expressions::Expression> identifiers_;
// Helper methods that add data to data structures.
static bool addUndefinedBooleanConstant(std::set<std::string>& undefinedBooleanConstants, std::string const& newUndefinedBooleanConstant);
static bool addUndefinedIntegerConstant(std::set<std::string>& undefinedIntegerConstants, std::string const& newUndefinedIntegerConstant);
static bool addUndefinedDoubleConstant(std::set<std::string>& undefinedDoubleConstants, std::string const& newUndefinedDoubleConstant);
static bool addDefinedBooleanConstant(std::map<std::string, storm::expressions::Expression>& definedBooleanConstants, std::string const& newDefinedBooleanConstant, storm::expressions::Expression expression);
static bool addDefinedIntegerConstant(std::map<std::string, storm::expressions::Expression>& definedIntegerConstants, std::string const& newDefinedIntegerConstant, storm::expressions::Expression expression);
static bool addDefinedDoubleConstant(std::map<std::string, storm::expressions::Expression>& definedDoubleConstants, std::string const& newDefinedDoubleConstant, storm::expressions::Expression expression);
static bool addFormula(std::map<std::string, storm::expressions::Expression>& formulas, std::string const& formulaName, storm::expressions::Expression expression);
static storm::prism::RewardModel addRewardModel(std::map<std::string, storm::prism::RewardModel>& rewardModels, std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards);
static storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression);
static storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression);
static bool addLabel(std::map<std::string, storm::expressions::Expression>& labels, std::string const& labelName, storm::expressions::Expression expression);
static bool addAssignment(std::map<std::string, storm::prism::Assignment>& assignments, std::string const& variableName, storm::expressions::Expression assignedExpression);
static storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::map<std::string, storm::prism::Assignment>& assignments);
static storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates);
static bool addBooleanVariable(std::map<std::string, storm::prism::BooleanVariable>& booleanVariables, std::string const& variableName, storm::expressions::Expression initialValueExpression);
static bool addIntegerVariable(std::map<std::string, storm::prism::IntegerVariable>& integerVariables, std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression);
static storm::prism::Module createModule(std::string const& moduleName, std::map<std::string, storm::prism::BooleanVariable> const& booleanVariables, std::map<std::string, storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands);
static storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation const& globalProgramInformation);
static storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation, std::vector<storm::prism::Module> const& modules);
// Helper methods used in the grammar.
bool isValidIdentifier(std::string const& identifier);
bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const;
storm::prism::Constant createUndefinedBooleanConstant(std::string const& newConstant) const;
storm::prism::Constant createUndefinedIntegerConstant(std::string const& newConstant) const;
storm::prism::Constant createUndefinedDoubleConstant(std::string const& newConstant) const;
storm::prism::Constant createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Constant createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Constant createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression) const;
storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const;
storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const;
storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;
storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;
storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const;
storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const;
storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const;
storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
};
} // namespace prism
} // namespace parser

70
src/parser/prismparser/PrismParser.cpp
View File

@ -0,0 +1,70 @@
#include "src/parser/prismparser/PrismParser.h"
#include "src/parser/prismparser/PrismGrammar.h"
// If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/WrongFormatException.h"
// Needed for file IO.
#include <fstream>
#include <iomanip>
#include <limits>
namespace storm {
namespace parser {
storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file " << filename << ".");
storm::prism::Program result;
// Now try to parse the contents of the file.
try {
std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
result = parseFromString(fileContent, filename, typeCheck);
} catch(std::exception& e) {
// In case of an exception properly close the file before passing exception.
inputFileStream.close();
throw e;
}
// Close the stream in case everything went smoothly and return result.
inputFileStream.close();
return result;
}
storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool typeCheck) {
PositionIteratorType first(input.begin());
PositionIteratorType iter = first;
PositionIteratorType last(input.end());
// Create empty result;
storm::prism::Program result;
// Create grammar.
storm::parser::prism::PrismGrammar grammar(filename, first);
try {
// Now parse the content using phrase_parse in order to be able to supply a skipping parser.
bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
if (typeCheck) {
first = PositionIteratorType(input.begin());
iter = first;
last = PositionIteratorType(input.end());
grammar.toggleExpressionGeneration();
succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass.");
}
} catch (qi::expectation_failure<PositionIteratorType> const& e) {
// If the parser expected content different than the one provided, display information about the location of the error.
std::size_t lineNumber = boost::spirit::get_line(e.first);
// Now propagate exception.
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
}
return result;
}
} // namespace parser
} // namespace storm

36
src/parser/prismparser/PrismParser.h
View File

@ -0,0 +1,36 @@
#ifndef STORM_PARSER_PRISMPARSER_H_
#define STORM_PARSER_PRISMPARSER_H_
// All classes of the intermediate representation are used.
#include "src/storage/prism/Program.h"
// Used for file input.
#include <istream>
namespace storm {
namespace parser {
class PrismParser {
public:
/*!
* Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
*
* @param filename the name of the file to parse.
* @param typeCheck Sets whether the expressions are generated and therefore typechecked.
* @return The resulting PRISM program.
*/
static storm::prism::Program parse(std::string const& filename, bool typeCheck = true);
/*!
* Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax.
*
* @param input The input string to parse.
* @param filename The name of the file from which the input was read.
* @param typeCheck Sets whether the expressions are generated and therefore typechecked.
* @return The resulting PRISM program.
*/
static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool typeCheck = true);
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_PRISMPARSER_H_ */

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

@ -86,8 +86,8 @@ namespace storm {
void BinaryBooleanFunctionExpression::printToStream(std::ostream& stream) const {
stream << "(" << *this->getFirstOperand();
switch (this->getOperatorType()) {
case OperatorType::And: stream << " && "; break;
case OperatorType::Or: stream << " || "; break;
case OperatorType::And: stream << " & "; break;
case OperatorType::Or: stream << " | "; break;
case OperatorType::Implies: stream << " => "; break;
case OperatorType::Iff: stream << " <=> "; break;
}

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

@ -124,6 +124,10 @@ namespace storm {
return Expression(std::shared_ptr<BaseExpression>(new VariableExpression(ExpressionReturnType::Double, variableName)));
}
Expression Expression::createUndefinedVariable(std::string const& variableName) {
return Expression(std::shared_ptr<BaseExpression>(new VariableExpression(ExpressionReturnType::Undefined, variableName)));
}
Expression Expression::createBooleanConstant(std::string const& constantName) {
return Expression(std::shared_ptr<BaseExpression>(new BooleanConstantExpression(constantName)));
}

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

@ -33,6 +33,7 @@ namespace storm {
static Expression createBooleanVariable(std::string const& variableName);
static Expression createIntegerVariable(std::string const& variableName);
static Expression createDoubleVariable(std::string const& variableName);
static Expression createUndefinedVariable(std::string const& variableName);
static Expression createBooleanConstant(std::string const& constantName);
static Expression createIntegerConstant(std::string const& constantName);
static Expression createDoubleConstant(std::string const& constantName);

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

@ -23,7 +23,7 @@ namespace storm {
* @param filename The filename in which the variable is defined.
* @param lineNumber The line number in which the variable is defined.
*/
BooleanVariable(std::string const& variableName, std::string const& filename, uint_fast64_t lineNumber);
BooleanVariable(std::string const& variableName, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a boolean variable with the given name and the given constant initial value expression.
@ -33,7 +33,7 @@ namespace storm {
* @param filename The filename in which the variable is defined.
* @param lineNumber The line number in which the variable is defined.
*/
BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber);
BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given boolean variable and performs the provided renaming.

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

@ -6,14 +6,18 @@ namespace storm {
// Nothing to do here.
}
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute<std::map>(renaming)), globalIndex(newGlobalIndex) {
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, uint_fast64_t newGlobalUpdateIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute<std::map>(renaming)), globalIndex(newGlobalIndex) {
// Rename the action name of the command.
auto const& namePair = renaming.find(this->actionName);
if (namePair != renaming.end()) {
this->actionName = namePair->second;
}
// Rename the updates of the command.
this->updates.reserve(oldCommand.getNumberOfUpdates());
for (Update const& update : oldCommand.getUpdates()) {
this->updates.emplace_back(update, update.getGlobalIndex(), renaming, filename, lineNumber);
this->updates.emplace_back(update, newGlobalUpdateIndex, renaming, filename, lineNumber);
++newGlobalUpdateIndex;
}
}

3
src/storage/prism/Command.h
View File

@ -29,11 +29,12 @@ namespace storm {
*
* @param oldCommand The command to copy.
* @param newGlobalIndex The global index of the copy of the command.
* @param newGlobalUpdateIndex The global starting index for the updates of the renamed command.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
* @param filename The filename in which the command is defined.
* @param lineNumber The line number in which the command is defined.
*/
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, uint_fast64_t newGlobalUpdateIndex, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Command() = default;

3
src/storage/prism/Constant.cpp
View File

@ -35,8 +35,9 @@ namespace storm {
}
stream << constant.getConstantName();
if (constant.isDefined()) {
stream << " = " << constant.getExpression() << ";";
stream << " = " << constant.getExpression();
}
stream << ";";
return stream;
}
}

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

@ -23,7 +23,7 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) {
stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << variable.getInitialValueExpression() << ";";
stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << " init " << variable.getInitialValueExpression() << ";";
return stream;
}
} // namespace prism

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

@ -10,8 +10,16 @@ namespace storm {
return this->filename;
}
void LocatedInformation::setFilename(std::string const& filename) {
this->filename = filename;
}
uint_fast64_t LocatedInformation::getLineNumber() const {
return this->lineNumber;
}
void LocatedInformation::setLineNumber(uint_fast64_t lineNumber) {
this->lineNumber = lineNumber;
}
}
}

14
src/storage/prism/LocatedInformation.h
View File

@ -29,12 +29,26 @@ namespace storm {
*/
std::string const& getFilename() const;
/*!
* Sets the filename of this information.
*
* @param filename The new filename of this information.
*/
void setFilename(std::string const& filename);
/*!
* Retrieves the line number in which the information was found.
*
* @return The line number in which the information was found.
*/
uint_fast64_t getLineNumber() const;
/*!
* Sets the line number of this information.
*
* @param lineNumber The new line number for this information.
*/
void setLineNumber(uint_fast64_t lineNumber);
private:
// The file in which the piece of information was found.

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

@ -6,19 +6,18 @@
namespace storm {
namespace prism {
Module::Module(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, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap() {
// FIXME: construct mappings from variable names to their indices.
// Initialize the internal mappings for fast information retrieval.
this->collectActions();
this->createMappings();
}
Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() {
Module::Module(Module const& oldModule, std::string const& newModuleName, uint_fast64_t newGlobalCommandIndex, uint_fast64_t newGlobalUpdateIndex, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() {
// Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown.
for (auto const& booleanVariable : oldModule.getBooleanVariables()) {
auto const& renamingPair = renaming.find(booleanVariable.getName());
LOG_THROW(renamingPair != renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable '" << booleanVariable.getName() << " was not renamed.");
this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, renaming, filename, lineNumber);
}
// Now do the same for the integer variables.
for (auto const& integerVariable : oldModule.getIntegerVariables()) {
auto const& renamingPair = renaming.find(integerVariable.getName());
@ -26,16 +25,16 @@ namespace storm {
this->integerVariables.emplace_back(integerVariable, renamingPair->second, renaming, filename, lineNumber);
}
// FIXME: construct mappings from variable names to their indices.
// Now we are ready to clone all commands and rename them if requested.
this->commands.reserve(oldModule.getNumberOfCommands());
for (Command const& command : oldModule.getCommands()) {
this->commands.emplace_back(command, command.getGlobalIndex(), renaming);
this->commands.emplace_back(command, newGlobalCommandIndex, newGlobalUpdateIndex, renaming, filename, lineNumber);
++newGlobalCommandIndex;
newGlobalUpdateIndex += this->commands.back().getNumberOfUpdates();
}
// Finally, update internal mapping.
this->collectActions();
// Finally, update internal mappings.
this->createMappings();
}
std::size_t Module::getNumberOfBooleanVariables() const {
@ -108,18 +107,28 @@ namespace storm {
LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module.");
}
void Module::collectActions() {
// Clear the current mapping.
void Module::createMappings() {
// Clear the current mappings.
this->actionsToCommandIndexMap.clear();
this->booleanVariableToIndexMap.clear();
this->integerVariableToIndexMap.clear();
// Create the mappings for the variables.
for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) {
this->booleanVariableToIndexMap[this->getBooleanVariables()[i].getName()] = i;
}
for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) {
this->integerVariableToIndexMap[this->getIntegerVariables()[i].getName()] = i;
}
// Add the mapping for all commands.
for (unsigned int id = 0; id < this->commands.size(); id++) {
std::string const& action = this->commands[id].getActionName();
for (uint_fast64_t i = 0; i < this->commands.size(); i++) {
std::string const& action = this->commands[i].getActionName();
if (action != "") {
if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) {
this->actionsToCommandIndexMap.emplace(action, std::set<uint_fast64_t>());
}
this->actionsToCommandIndexMap[action].insert(id);
this->actionsToCommandIndexMap[action].insert(i);
this->actions.insert(action);
}
}

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

@ -34,11 +34,13 @@ namespace storm {
*
* @param oldModule The module to be copied.
* @param newModuleName The name of the new module.
* @param newGlobalCommandIndex The global starting index for commands of the renamed module.
* @param newGlobalUpdateIndex The global starting index for the updates of the renamed module.
* @param renaming A mapping of identifiers to the new identifiers they are to be replaced with.
* @param filename The filename in which the module is defined.
* @param lineNumber The line number in which the module is defined.
*/
Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Module(Module const& oldModule, std::string const& newModuleName, uint_fast64_t newGlobalCommandIndex, uint_fast64_t newGlobalUpdateIndex, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Module() = default;
@ -164,7 +166,7 @@ namespace storm {
/*!
* Computes the locally maintained mappings for fast data retrieval.
*/
void collectActions();
void createMappings();
// The name of the module.
std::string moduleName;

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

@ -5,29 +5,8 @@
namespace storm {
namespace prism {
Program::Program(ModelType modelType, std::vector<Constant> const& undefinedConstants, std::vector<Constant> const& definedConstants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedConstants(undefinedConstants), definedConstants(definedConstants), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), labelToIndexMap(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
// FIXME: build the mappings for constants, formulas, modules, global variables, reward models and labels.
// 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);
for (auto const& action : module.getActions()) {
auto const& actionModuleIndicesPair = this->actionsToModuleIndexMap.find(action);
if (actionModuleIndicesPair == this->actionsToModuleIndexMap.end()) {
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>();
}
this->actionsToModuleIndexMap[action].insert(moduleIndex);
this->actions.insert(action);
}
// Put in the appropriate entries for the mapping from variable names to module index.
for (auto const& booleanVariable : module.getBooleanVariables()) {
this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
}
for (auto const& integerVariable : module.getBooleanVariables()) {
this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
}
}
Program::Program(ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), constants(constants), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), labelToIndexMap(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() {
this->createMappings();
}
Program::ModelType Program::getModelType() const {
@ -35,15 +14,16 @@ namespace storm {
}
bool Program::hasUndefinedConstants() const {
return this->undefinedConstants.size() > 0;
}
std::vector<Constant> const& Program::getUndefinedConstants() const {
return this->undefinedConstants;
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {
return true;
}
}
return true;
}
std::vector<Constant> const& Program::getDefinedConstants() const {
return this->definedConstants;
std::vector<Constant> const& Program::getConstants() const {
return this->constants;
}
std::vector<BooleanVariable> const& Program::getGlobalBooleanVariables() const {
@ -78,6 +58,10 @@ namespace storm {
return this->formulas;
}
std::size_t Program::getNumberOfFormulas() const {
return this->formulas.size();
}
std::size_t Program::getNumberOfModules() const {
return this->getModules().size();
}
@ -140,6 +124,10 @@ namespace storm {
return this->rewardModels;
}
std::size_t Program::getNumberOfRewardModels() const {
return this->rewardModels.size();
}
storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist.");
@ -150,6 +138,10 @@ namespace storm {
return this->labels;
}
std::size_t Program::getNumberOfLabels() const {
return this->labels.size();
}
Program Program::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) {
std::vector<storm::prism::Module> newModules;
newModules.reserve(this->getNumberOfModules());
@ -158,7 +150,52 @@ namespace storm {
newModules.push_back(module.restrictCommands(indexSet));
}
return Program(this->getModelType(), this->getUndefinedConstants(), this->getDefinedConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
return Program(this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
}
void Program::createMappings() {
// Build the mappings for global variables, formulas, modules, reward models and labels.
for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalBooleanVariables(); ++globalVariableIndex) {
this->globalBooleanVariableToIndexMap[this->getGlobalBooleanVariables()[globalVariableIndex].getName()] = globalVariableIndex;
}
for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalIntegerVariables(); ++globalVariableIndex) {
this->globalIntegerVariableToIndexMap[this->getGlobalIntegerVariables()[globalVariableIndex].getName()] = globalVariableIndex;
}
for (uint_fast64_t formulaIndex = 0; formulaIndex < this->getNumberOfFormulas(); ++formulaIndex) {
this->formulaToIndexMap[this->getFormulas()[formulaIndex].getFormulaName()] = formulaIndex;
}
for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
}
for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
}
for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) {
this->labelToIndexMap[this->getLabels()[labelIndex].getLabelName()] = labelIndex;
}
// 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);
for (auto const& action : module.getActions()) {
auto const& actionModuleIndicesPair = this->actionsToModuleIndexMap.find(action);
if (actionModuleIndicesPair == this->actionsToModuleIndexMap.end()) {
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>();
}
this->actionsToModuleIndexMap[action].insert(moduleIndex);
this->actions.insert(action);
}
// Put in the appropriate entries for the mapping from variable names to module index.
for (auto const& booleanVariable : module.getBooleanVariables()) {
this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
}
for (auto const& integerVariable : module.getBooleanVariables()) {
this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
}
}
}
std::ostream& operator<<(std::ostream& stream, Program const& program) {
@ -172,7 +209,7 @@ namespace storm {
}
stream << std::endl;
for (auto const& constant : program.getUndefinedConstants()) {
for (auto const& constant : program.getConstants()) {
stream << constant << std::endl;
}
stream << std::endl;
@ -185,6 +222,11 @@ namespace storm {
}
stream << std::endl;
for (auto const& formula : program.getFormulas()) {
stream << formula << std::endl;
}
stream << std::endl;
for (auto const& module : program.getModules()) {
stream << module << std::endl;
}

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

@ -27,8 +27,7 @@ namespace storm {
* models, labels and initial states.
*
* @param modelType The type of the program.
* @param undefinedConstants The undefined constants of the program.
* @param definedConstants The defined integer constants of the program.
* @param constants The 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.
@ -43,7 +42,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::vector<Constant> const& undefinedConstants, std::vector<Constant> const& definedConstants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Program(ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::vector<RewardModel> const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector<Label> const& labels, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Provide default implementations for constructors and assignments.
Program() = default;
@ -65,21 +64,14 @@ namespace storm {
* @return True iff there are undefined constants of any type in the program.
*/
bool hasUndefinedConstants() const;
/*!
* Retrieves the undefined constants of the program.
*
* @return The undefined constants of the program.
*/
std::vector<Constant> const& getUndefinedConstants() const;
/*!
* Retrieves the defined constants of the program.
* Retrieves all constants defined in the program.
*
* @return The defined constants of the program.
* @return The constants defined in the program.
*/
std::vector<Constant> const& getDefinedConstants() const;
std::vector<Constant> const& getConstants() const;
/*!
* Retrieves the global boolean variables of the program.
*
@ -131,6 +123,13 @@ namespace storm {
*/
std::vector<Formula> const& getFormulas() const;
/*!
* Retrieves the number of formulas in the program.
*
* @return The number of formulas in the program.
*/
std::size_t getNumberOfFormulas() const;
/*!
* Retrieves the number of modules in the program.
*
@ -206,6 +205,13 @@ namespace storm {
*/
std::vector<RewardModel> const& getRewardModels() const;
/*!
* Retrieves the number of reward models in the program.
*
* @return The number of reward models in the program.
*/
std::size_t getNumberOfRewardModels() const;
/*!
* Retrieves the reward model with the given name.
*
@ -221,6 +227,13 @@ namespace storm {
*/
std::vector<Label> const& getLabels() const;
/*!
* Retrieves the number of labels in the program.
*
* @return The number of labels in the program.
*/
std::size_t getNumberOfLabels() const;
/*!
* Creates a new program that drops all commands whose indices are not in the given set.
*
@ -231,14 +244,14 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, Program const& program);
private:
// Creates the internal mappings.
void createMappings();
// The type of the model.
ModelType modelType;
// The undefined constants of the program.
std::vector<Constant> undefinedConstants;
// The defined constants of the program.
std::vector<Constant> definedConstants;
std::vector<Constant> constants;
// The global boolean variables.
std::vector<BooleanVariable> globalBooleanVariables;

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

@ -5,10 +5,11 @@
namespace storm {
namespace prism {
Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector<storm::prism::Assignment> const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) {
// FIXME: construct the mapping from variable names to assignments and check for uniqueness.
this->createAssignmentMapping();
}
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(), variableToAssignmentIndexMap(), globalIndex(newGlobalIndex) {
// Rename all assignments.
for (auto const& assignment : update.getAssignments()) {
auto const& namePair = renaming.find(assignment.getVariableName());
if (namePair != renaming.end()) {
@ -17,8 +18,9 @@ namespace storm {
this->assignments.emplace_back(Assignment(assignment));
}
}
// FIXME: construct the mapping from variable names to assignments and check for uniqueness.
this->likelihoodExpression = update.getLikelihoodExpression().substitute<std::map>(renaming);
// Create the assignment mapping.
this->createAssignmentMapping();
}
storm::expressions::Expression const& Update::getLikelihoodExpression() const {
@ -43,6 +45,13 @@ namespace storm {
return this->globalIndex;
}
void Update::createAssignmentMapping() {
this->variableToAssignmentIndexMap.clear();
for (uint_fast64_t assignmentIndex = 0; assignmentIndex < this->getAssignments().size(); ++assignmentIndex) {
this->variableToAssignmentIndexMap[this->getAssignments()[assignmentIndex].getVariableName()] = assignmentIndex;
}
}
std::ostream& operator<<(std::ostream& stream, Update const& update) {
stream << update.getLikelihoodExpression() << " : ";
uint_fast64_t i = 0;

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

@ -77,6 +77,11 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, Update const& assignment);
private:
/*!
* Creates the internal mapping of variables to their assignments.
*/
void createAssignmentMapping();
// An expression specifying the likelihood of taking this update.
storm::expressions::Expression likelihoodExpression;

157
test/functional/parser/PrismParserTest.cpp
View File

@ -0,0 +1,157 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/prismparser/PrismParser.h"
TEST(PrismParser, SimpleParsingOnlyTest) {
std::string testInput =
R"(dtmc
module mod1
b : bool;
[a] true -> 1: (b'=true);
endmodule)";
storm::prism::Program result;
EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false));
EXPECT_EQ(1, result.getNumberOfModules());
EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
}
TEST(PrismParser, StandardModelParsingTest) {
storm::prism::Program result;
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3_5.pm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm", false));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm", false));
}
TEST(PrismParser, SimpleFullTest) {
std::string testInput =
R"(dtmc
module mod1
b : bool;
[a] true -> 1: (b'=true);
endmodule)";
storm::prism::Program result;
EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true));
EXPECT_EQ(1, result.getNumberOfModules());
EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType());
}
TEST(PrismParser, ComplexFullTest) {
std::string testInput =
R"(ma
const int a;
const int b = 10;
const bool c;
const bool d = true | false;
const double e;
const double f = 9;
formula test = a >= 10 & (max(a,b) > floor(e));
formula test2 = a+b;
global g : bool init false;
global h : [0 .. b];
module mod1
i : bool;
j : bool init c;
k : [125..a] init a;
[a] test2&false -> (i'=true)&(h'=1+1) + 1 : (j'=floor(a) <= max(k, b) - 1 + k);
endmodule
module mod2
[b] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (j'=(1-a) * 2 + floor(f));
endmodule
module mod3 = mod2 [ x = y ] endmodule
label "mal" = max(a, 10) > 0;
init
true
endinit
rewards "testrewards"
[stateRew] true : a + 7;
max(f, a) <= 8 : 2*b;
endrewards
rewards "testrewards2"
[stateRew] true : a + 7;
max(f, a) <= 8 : 2*b;
endrewards)";
storm::prism::Program result;
result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true);
std::cout << result << std::endl;
EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType());
EXPECT_EQ(3, result.getNumberOfModules());
EXPECT_EQ(2, result.getNumberOfRewardModels());
EXPECT_EQ(1, result.getNumberOfLabels());
EXPECT_TRUE(result.definesInitialStatesExpression());
}
TEST(PrismParser, ComplexParsingTest) {
std::string testInput =
R"(ma
const int a;
const int b = 10;
const bool c;
const bool d = true | false;
const double e;
const double f = 9;
formula test = (a >= 10 & (max(a, b) > floor(e)));
global g : bool init false;
global h : [0 .. b];
module mod1
i : bool;
j : bool init c;
k : [125..a] init a;
[a] true -> (i'=true)&(h'=1+1) + 1 : (j'=floor(a) <= max(k, b) - 1 + k);
endmodule
module mod2
[b] (x > 3) & false & (min(a, b0) < max(as8, b)) -> y: (x'=(1-g) * 2 + a);
[] s=1 -> (a'=a);
[read] c<N-1 -> 1 : (c'=floor(c) + 1);
endmodule
module mod3 = mod2 [ x = y ] endmodule
label "mal" = max(x, i) > 0;
init
true
endinit
rewards "testrewards"
[stateRew] true : a + 7;
max(z, f) <= 8 : 2*b;
endrewards
rewards "testrewards2"
[stateRew] true : a + 7;
max(z, f) <= 8 : 2*b;
endrewards)";
storm::prism::Program result;
result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false);
EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType());
EXPECT_EQ(3, result.getNumberOfModules());
EXPECT_EQ(2, result.getNumberOfRewardModels());
EXPECT_EQ(1, result.getNumberOfLabels());
EXPECT_TRUE(result.definesInitialStatesExpression());
}
Write Preview
Loading…
Cancel
Save