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

preserving action knowledge from first to second PRISM parser pass

tempestpy_adaptions
dehnert 7 years ago
parent
6e548627ee
commit
2d99ff3126
2 changed files with 37 additions and 14 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. 25
      src/storm/parser/PrismParser.cpp
  2. 26
      src/storm/parser/PrismParser.h

25
src/storm/parser/PrismParser.cpp
View File

@ -216,19 +216,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[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)]
> *(modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), 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(qi::_a)[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)]
start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]
> *(modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)]
| definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
| undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
| globalVariableDefinition(phoenix::ref(globalProgramInformation))
| (moduleRenaming(phoenix::ref(globalProgramInformation)) | moduleDefinition(phoenix::ref(globalProgramInformation)))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, phoenix::ref(globalProgramInformation)), qi::_1)]
| initialStatesConstruct(phoenix::ref(globalProgramInformation))
| rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)]
| labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
)
> -(systemCompositionConstruct(qi::_a)) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
> -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))];
start.name("probabilistic program");
// Enable location tracking for important entities.
@ -267,6 +267,7 @@ namespace storm {
this->secondRun = true;
this->expressionParser->setIdentifierMapping(&this->identifiers_);
this->globalProgramInformation.moveToSecondRun();
}
void PrismParser::allowDoubleLiterals(bool flag) {

26
src/storm/parser/PrismParser.h
View File

@ -30,6 +30,25 @@ namespace storm {
actionIndices.emplace("", 0);
}
void moveToSecondRun() {
// Clear all data except the action to indices mapping.
modelType = storm::prism::Program::ModelType::UNDEFINED;
constants.clear();
formulas.clear();
globalBooleanVariables.clear();
globalIntegerVariables.clear();
moduleToIndexMap.clear();
modules.clear();
rewardModels.clear();
labels.clear();
hasInitialConstruct = false;
initialConstruct = storm::prism::InitialConstruct();
systemCompositionConstruct = boost::none;
currentCommandIndex = 0;
currentUpdateIndex = 0;
}
// Members for all essential information that needs to be collected.
storm::prism::Program::ModelType modelType;
std::vector<storm::prism::Constant> constants;
@ -50,7 +69,7 @@ namespace storm {
uint_fast64_t currentUpdateIndex;
};
class PrismParser : public qi::grammar<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> {
class PrismParser : public qi::grammar<Iterator, storm::prism::Program(), Skipper> {
public:
/*!
* Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
@ -161,8 +180,11 @@ namespace storm {
// A function used for annotating the entities with their position.
phoenix::function<PositionAnnotation> annotate;
// An object gathering information about the program while parsing.
GlobalProgramInformation globalProgramInformation;
// The starting point of the grammar.
qi::rule<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> start;
qi::rule<Iterator, storm::prism::Program(), Skipper> start;
// Rules for model type.
qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;

Write Preview
Loading…
Cancel
Save