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

Added some checks for validity of identifiers in PRISM programs. Added some illegal tests to test suite. 

Former-commit-id: fc44db75a7
tempestpy_adaptions
dehnert 11 years ago
parent
d0d80cf5e1
commit
82836f1ad1
3 changed files with 129 additions and 19 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. 67
      src/parser/PrismParser.cpp
  2. 2
      src/parser/PrismParser.h
  3. 79
      test/functional/parser/PrismParserTest.cpp

67
src/parser/PrismParser.cpp
View File

@ -147,13 +147,7 @@ namespace storm {
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]
> *(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");
stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
@ -199,7 +193,19 @@ namespace storm {
moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)];
moduleDefinitionList.name("module list");
start = (qi::eps > 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)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
start = (qi::eps
> modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1]
> *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
| undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
| globalVariableDefinition(qi::_a)
| (moduleRenaming(qi::_a) | moduleDefinition(qi::_a))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_a), qi::_1)]
| 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)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]
)
> qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
start.name("probabilistic program");
// Enable error reporting.
@ -258,7 +264,7 @@ namespace storm {
}
bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::InvalidArgumentException, "Program must not define two initial constructs.");
LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialStatesExpression) {
return false;
}
@ -483,37 +489,56 @@ namespace storm {
}
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
}
storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
}
storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
}
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
if (this->secondRun) {
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << formulaName << "'.");
this->identifiers_.add(formulaName, expression);
}
return storm::prism::Formula(formulaName, expression, this->getFilename());
@ -550,12 +575,18 @@ namespace storm {
}
storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
}
return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
}
storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
}
return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
}

2
src/parser/PrismParser.h
View File

@ -189,7 +189,7 @@ namespace storm {
qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;
// Rules for parsing the program header.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> programHeader;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedIntegerConstantDefinition;

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

@ -54,6 +54,21 @@ TEST(PrismParser, SimpleFullTest) {
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());
testInput =
R"(mdp
module main
x : [1..5] init 1;
[] x=1 -> 1:(x'=2);
[] x=2 -> 1:(x'=3);
[] x=3 -> 1:(x'=1);
[] x=3 -> 1:(x'=4);
[] x=4 -> 1:(x'=5);
endmodule)";
EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true));
EXPECT_EQ(1, result.getNumberOfModules());
EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType());
}
TEST(PrismParser, ComplexFullTest) {
@ -167,4 +182,68 @@ TEST(PrismParser, ComplexParsingTest) {
EXPECT_EQ(2, result.getNumberOfRewardModels());
EXPECT_EQ(1, result.getNumberOfLabels());
EXPECT_TRUE(result.definesInitialStatesExpression());
}
TEST(PrismParser, IllegalInputTest) {
std::string testInput =
R"(ctmc
const int a;
const bool a = true;
module mod1
c : [0 .. 8] init 1;
[] c < 3 -> 2: (c' = c+1);
endmodule
)";
storm::prism::Program result;
EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException);
testInput =
R"(dtmc
const int a;
module mod1
a : [0 .. 8] init 1;
[] a < 3 -> 1: (a' = a+1);
endmodule)";
EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException);
testInput =
R"(dtmc
const int a = 2;
formula a = 41;
module mod1
c : [0 .. 8] init 1;
[] c < 3 -> 1: (c' = c+1);
endmodule)";
EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException);
testInput =
R"(dtmc
const int a = 2;
init
c > 3
endinit
module mod1
c : [0 .. 8] init 1;
[] c < 3 -> 1: (c' = c+1);
endmodule
init
c > 3
endinit
)";
EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException);
}
Write Preview
Loading…
Cancel
Save