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

removed plenty of empty line whitespaces

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
c12c0352f7
commit
d35e9a6a40
8 changed files with 631 additions and 626 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. 234
      src/storm-parsers/parser/PrismParser.cpp
  2. 66
      src/storm-parsers/parser/PrismParser.h
  3. 16
      src/storm/generator/NextStateGenerator.h
  4. 176
      src/storm/generator/PrismNextStateGenerator.cpp
  5. 40
      src/storm/storage/SymbolicModelDescription.cpp
  6. 10
      src/storm/storage/SymbolicModelDescription.h
  7. 527
      src/storm/storage/prism/Program.cpp
  8. 188
      src/storm/storage/prism/Program.h

234
src/storm-parsers/parser/PrismParser.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
std::ifstream inputFileStream;
storm::utility::openFile(filename, inputFileStream);
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>()));
@ -37,15 +37,15 @@ namespace storm {
storm::utility::closeFile(inputFileStream);
throw e;
}
// Close the stream in case everything went smoothly and return result.
storm::utility::closeFile(inputFileStream);
return result;
}
storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) {
bool hasByteOrderMark = input.size() >= 3 && input[0] == '\xEF' && input[1] == '\xBB' && input[2] == '\xBF';
PositionIteratorType first(hasByteOrderMark ? input.begin() + 3 : input.begin());
PositionIteratorType iter = first;
PositionIteratorType last(input.end());
@ -53,7 +53,7 @@ namespace storm {
// Create empty result;
storm::prism::Program result;
// Create grammar.
storm::parser::PrismParser grammar(filename, first, prismCompatibility);
try {
@ -62,7 +62,7 @@ namespace storm {
bool succeeded = qi::phrase_parse(iter, last, grammar, space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
STORM_LOG_DEBUG("First pass of parsing PRISM input finished.");
// Start second run.
first = PositionIteratorType(input.begin());
iter = first;
@ -73,98 +73,98 @@ namespace storm {
} 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.
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << ".");
}
STORM_LOG_TRACE("Parsed PRISM input: " << result);
return result;
}
PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) {
ExpressionParser& expression_ = *expressionParser;
boolExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfBoolType, phoenix::ref(*this), qi::_val)];
boolExpression.name("boolean expression");
intExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfIntType, phoenix::ref(*this), qi::_val)];
intExpression.name("integer expression");
numericalExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfNumericalType, phoenix::ref(*this), qi::_val)];
numericalExpression.name("numerical expression");
// Parse simple identifier.
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
// Fail if the identifier has been used before
freshIdentifier = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshIdentifier, phoenix::ref(*this), qi::_1)];
freshIdentifier.name("fresh identifier");
modelTypeDefinition %= modelType_;
modelTypeDefinition.name("model type");
// Defined constants. Will be checked before undefined constants.
// ">>" before literal '=' because we can still parse an undefined constant afterwards.
definedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier)
>> (qi::lit("=") > boolExpression > qi::lit(";"))
)[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (((qi::lit("const") >> -qi::lit("int")) >> freshIdentifier)
>> (qi::lit("=") > intExpression > qi::lit(";"))
)[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; // '>>' before freshIdentifier because of the optional 'int'. Otherwise, undefined constant 'const bool b;' would not parse.
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (((qi::lit("const") >> qi::lit("double")) > freshIdentifier)
>> (qi::lit("=") > numericalExpression > qi::lit(";"))
)[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedDoubleConstantDefinition.name("defined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition);
definedConstantDefinition.name("defined constant definition");
// Undefined constants. At this point we already checked for a defined constant, therefore a ";" is required after the identifier;
undefinedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = (((qi::lit("const") >> -qi::lit("int")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = (((qi::lit("const") >> qi::lit("double")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)];
undefinedDoubleConstantDefinition.name("undefined double constant definition");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedDoubleConstantDefinition | undefinedIntegerConstantDefinition); // Due to the 'const N;' syntax, it is important to have integer constants last
undefinedConstantDefinition.name("undefined constant definition");
// formula definitions. This will be changed for the second run.
formulaDefinitionRhs = (qi::lit("=") > qi::as_string[(+(qi::char_ - (qi::lit(";") | qi::lit("endmodule"))))][qi::_val = qi::_1] > qi::lit(";"));
formulaDefinitionRhs.name("formula defining expression");
formulaDefinition = (qi::lit("formula") > freshIdentifier > formulaDefinitionRhs )[qi::_val = phoenix::bind(&PrismParser::createFormulaFirstRun, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition.name("formula definition");
booleanVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)];
booleanVariableDefinition.name("boolean variable definition");
integerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
integerVariableDefinition.name("integer variable definition");
clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)];
clockVariableDefinition.name("clock variable definition");
variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, 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");
stateRewardDefinition = (boolExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
stateActionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > boolExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)];
stateActionRewardDefinition.name("state action reward definition");
@ -181,28 +181,28 @@ namespace storm {
)
> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)];
rewardModelDefinition.name("reward model definition");
initialStatesConstruct = (qi::lit("init") > boolExpression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
initialStatesConstruct.name("initial construct");
observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)];
observablesConstruct.name("observables construct");
invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1];
invariantConstruct.name("invariant construct");
knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1)];
knownModuleName.name("existing module name");
freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshModuleName, phoenix::ref(*this), qi::_1)];
freshModuleName.name("fresh module name");
systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
systemCompositionConstruct.name("system composition construct");
actionNameList %= identifier[phoenix::insert(qi::_val, qi::_1)] >> *("," >> identifier[phoenix::insert(qi::_val, qi::_1)]);
actionNameList.name("action list");
parallelComposition = hidingOrRenamingComposition[qi::_val = qi::_1] >> *((interleavingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createInterleavingParallelComposition, phoenix::ref(*this), qi::_val, qi::_1)] |
(synchronizingParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createSynchronizingParallelComposition, phoenix::ref(*this), qi::_val, qi::_1)] |
(restrictedParallelComposition > hidingOrRenamingComposition)[qi::_val = phoenix::bind(&PrismParser::createRestrictedParallelComposition, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]
@ -211,31 +211,31 @@ namespace storm {
synchronizingParallelComposition = qi::lit("||");
synchronizingParallelComposition.name("synchronizing parallel composition");
interleavingParallelComposition = qi::lit("|||");
interleavingParallelComposition.name("interleaving parallel composition");
restrictedParallelComposition = qi::lit("|[") > actionNameList > qi::lit("]|");
restrictedParallelComposition.name("restricted parallel composition");
hidingOrRenamingComposition = hidingComposition | renamingComposition | atomicComposition;
hidingOrRenamingComposition.name("hiding/renaming composition");
hidingComposition = (atomicComposition >> (qi::lit("/") > (qi::lit("{") > actionNameList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParser::createHidingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
hidingComposition.name("hiding composition");
actionRenamingList = +(identifier >> (qi::lit("<-") >> identifier))[phoenix::insert(qi::_val, phoenix::construct<std::pair<std::string, std::string>>(qi::_1, qi::_2))];
actionRenamingList.name("action renaming list");
renamingComposition = (atomicComposition >> (qi::lit("{") > (actionRenamingList > qi::lit("}"))))[qi::_val = phoenix::bind(&PrismParser::createRenamingComposition, phoenix::ref(*this), qi::_1, qi::_2)];
renamingComposition.name("renaming composition");
atomicComposition = (qi::lit("(") > parallelComposition > qi::lit(")")) | moduleComposition;
atomicComposition.name("atomic composition");
moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)];
moduleComposition.name("module composition");
freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshLabelName, phoenix::ref(*this), qi::_1)];
freshLabelName.name("fresh label name");
@ -247,20 +247,20 @@ namespace storm {
observableDefinition = (qi::lit("observable") > -qi::lit("\"") > freshObservationLabelName > -qi::lit("\"") > qi::lit("=") > (intExpression | boolExpression) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createObservationLabel, phoenix::ref(*this), qi::_1, qi::_2)];
observableDefinition.name("observable definition");
assignmentDefinition = ((qi::lit("(") >> identifier >> qi::lit("'")) > qi::lit("=") > expression_ > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
assignmentDefinition.name("assignment");
assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
assignmentDefinitionList.name("assignment list");
updateDefinition = (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), manager->rational(1), qi::_1, qi::_r1)]
| ((numericalExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]));
updateDefinition.name("update");
updateListDefinition %= +updateDefinition(qi::_r1) % "+";
updateListDefinition.name("update list");
// This is a dummy command-definition (it ignores the actual contents of the command) that is overwritten when the parser is moved to the second run.
commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]"))
|
@ -298,7 +298,7 @@ namespace storm {
)
> -(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.
auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction);
@ -320,16 +320,16 @@ namespace storm {
qi::on_success(commandDefinition, setLocationInfoFunction);
qi::on_success(updateDefinition, setLocationInfoFunction);
qi::on_success(assignmentDefinition, setLocationInfoFunction);
// Enable error reporting.
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
}
void PrismParser::moveToSecondRun() {
// In the second run, we actually need to parse the commands instead of just skipping them,
// so we adapt the rule for parsing commands.
STORM_LOG_THROW(observables.empty(), storm::exceptions::WrongFormatException, "Some variables marked as observable, but never declared, e.g. " << *observables.begin());
commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]"))
|
(qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true]))
@ -350,10 +350,10 @@ namespace storm {
// * in the first run, the type of the formula (int, bool, clock) is not known
// * in the second run, formulas might be used before they are declared
createFormulaIdentifiers(this->globalProgramInformation.formulas);
this->globalProgramInformation.moveToSecondRun();
}
void PrismParser::createFormulaIdentifiers(std::vector<storm::prism::Formula> const& formulas) {
STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException, "Unexpected number of formulas and formula expressions");
this->formulaOrder.clear();
@ -397,22 +397,22 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unable to parse expression for formula '" << formulas[unprocessed.getNextSetIndex(0)].getName() << "'.");
}
}
void PrismParser::allowDoubleLiterals(bool flag) {
this->expressionParser->setAcceptDoubleLiterals(flag);
}
std::string const& PrismParser::getFilename() const {
return this->filename;
}
bool PrismParser::isValidIdentifier(std::string const& identifier) {
if (this->keywords_.find(identifier) != nullptr) {
return false;
}
return true;
}
bool PrismParser::isKnownModuleName(std::string const& moduleName) {
if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'.");
@ -420,7 +420,7 @@ namespace storm {
}
return true;
}
bool PrismParser::isFreshModuleName(std::string const& moduleName) {
if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) != 0) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate module name '" << moduleName << "'.");
@ -428,7 +428,7 @@ namespace storm {
}
return true;
}
bool PrismParser::isFreshIdentifier(std::string const& identifier) {
if (!this->secondRun && this->manager->hasVariable(identifier)) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'.");
@ -436,7 +436,7 @@ namespace storm {
}
return true;
}
bool PrismParser::isFreshLabelName(std::string const& labelName) {
if (!this->secondRun) {
for (auto const& existingLabel : this->globalProgramInformation.labels) {
@ -460,7 +460,7 @@ namespace storm {
}
return true;
}
bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) {
if (!this->secondRun) {
for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) {
@ -472,19 +472,19 @@ namespace storm {
}
return true;
}
bool PrismParser::isOfBoolType(storm::expressions::Expression const& expression) {
return !this->secondRun || expression.hasBooleanType();
}
bool PrismParser::isOfIntType(storm::expressions::Expression const& expression) {
return !this->secondRun || expression.hasIntegerType();
}
bool PrismParser::isOfNumericalType(storm::expressions::Expression const& expression) {
return !this->secondRun || expression.hasNumericalType();
}
bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialConstruct) {
@ -494,12 +494,12 @@ namespace storm {
globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3));
return true;
}
bool PrismParser::addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation) {
globalProgramInformation.systemCompositionConstruct = storm::prism::SystemCompositionConstruct(composition, this->getFilename(), get_line(qi::_3));
return true;
}
void PrismParser::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) {
STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Program must not set model type multiple times.");
globalProgramInformation.modelType = modelType;
@ -508,27 +508,27 @@ namespace storm {
std::shared_ptr<storm::prism::Composition> PrismParser::createModuleComposition(std::string const& moduleName) const {
return std::make_shared<storm::prism::ModuleComposition>(moduleName);
}
std::shared_ptr<storm::prism::Composition> PrismParser::createRenamingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::map<std::string, std::string> const& renaming) const {
return std::make_shared<storm::prism::RenamingComposition>(subcomposition, renaming);
}
std::shared_ptr<storm::prism::Composition> PrismParser::createHidingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::set<std::string> const& actionsToHide) const {
return std::make_shared<storm::prism::HidingComposition>(subcomposition, actionsToHide);
}
std::shared_ptr<storm::prism::Composition> PrismParser::createSynchronizingParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
return std::make_shared<storm::prism::SynchronizingParallelComposition>(left, right);
}
std::shared_ptr<storm::prism::Composition> PrismParser::createInterleavingParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::shared_ptr<storm::prism::Composition> const& right) const {
return std::make_shared<storm::prism::InterleavingParallelComposition>(left, right);
}
std::shared_ptr<storm::prism::Composition> PrismParser::createRestrictedParallelComposition(std::shared_ptr<storm::prism::Composition> const& left, std::set<std::string> const& synchronizingActions, std::shared_ptr<storm::prism::Composition> const& right) const {
return std::make_shared<storm::prism::RestrictedParallelComposition>(left, synchronizingActions, right);
}
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
if (!this->secondRun) {
try {
@ -540,7 +540,7 @@ namespace storm {
}
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
}
storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
if (!this->secondRun) {
try {
@ -552,7 +552,7 @@ namespace storm {
}
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
}
storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
if (!this->secondRun) {
try {
@ -564,7 +564,7 @@ namespace storm {
}
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
try {
@ -576,7 +576,7 @@ namespace storm {
}
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
try {
@ -588,7 +588,7 @@ namespace storm {
}
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
}
storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
try {
@ -600,7 +600,7 @@ namespace storm {
}
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
}
storm::prism::Formula PrismParser::createFormulaFirstRun(std::string const& formulaName, std::string const& expression) {
// Only store the expression as a string. It will be parsed between first and second run
// This is necessary because the resulting type of the formula is only known after the first run.
@ -608,14 +608,14 @@ namespace storm {
formulaExpressions.push_back(expression);
return storm::prism::Formula(formulaName, this->getFilename());
}
storm::prism::Formula PrismParser::createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression) {
// This is necessary because the resulting type of the formula is only known after the first run.
STORM_LOG_ASSERT(this->secondRun, "This constructor should have only been called during the second run.");
storm::expressions::Expression lhsExpression = *this->identifiers_.find(formulaName);
return storm::prism::Formula(lhsExpression.getBaseExpression().asVariableExpression().getVariable(), expression, this->getFilename());
}
storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const {
return storm::prism::Label(labelName, expression, this->getFilename());
}
@ -623,11 +623,11 @@ namespace storm {
storm::prism::ObservationLabel PrismParser::createObservationLabel(std::string const& labelName, storm::expressions::Expression expression) const {
return storm::prism::ObservationLabel(labelName, expression, this->getFilename());
}
storm::prism::RewardModel PrismParser::createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const {
return storm::prism::RewardModel(rewardModelName, stateRewards, stateActionRewards, transitionRewards, this->getFilename());
}
storm::prism::StateReward PrismParser::createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const {
if (this->secondRun) {
return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename());
@ -635,11 +635,11 @@ namespace storm {
return storm::prism::StateReward();
}
}
storm::prism::StateActionReward PrismParser::createStateActionReward(boost::optional<std::string> const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const {
if (this->secondRun) {
std::string realActionName = actionName ? actionName.get() : "";
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Action reward refers to illegal action '" << realActionName << "'.");
return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename());
@ -647,11 +647,11 @@ namespace storm {
return storm::prism::StateActionReward();
}
}
storm::prism::TransitionReward PrismParser::createTransitionReward(boost::optional<std::string> const& actionName, storm::expressions::Expression sourceStatePredicateExpression, storm::expressions::Expression targetStatePredicateExpression, storm::expressions::Expression rewardValueExpression, GlobalProgramInformation& globalProgramInformation) const {
if (this->secondRun) {
std::string realActionName = actionName ? actionName.get() : "";
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'.");
return storm::prism::TransitionReward(nameIndexPair->second, realActionName, sourceStatePredicateExpression, targetStatePredicateExpression, rewardValueExpression, this->getFilename());
@ -659,22 +659,22 @@ namespace storm {
return storm::prism::TransitionReward();
}
}
storm::prism::Assignment PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const {
return storm::prism::Assignment(manager->getVariable(variableName), assignedExpression, this->getFilename());
}
storm::prism::Update PrismParser::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 PrismParser::createCommand(bool markovian, boost::optional<std::string> const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const {
++globalProgramInformation.currentCommandIndex;
std::string realActionName = actionName ? actionName.get() : "";
uint_fast64_t actionIndex = 0;
// If the action name was not yet seen, record it.
auto nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
@ -686,7 +686,7 @@ namespace storm {
}
return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, markovian, actionIndex, realActionName, guardExpression, updates, this->getFilename());
}
storm::prism::Command PrismParser::createDummyCommand(boost::optional<std::string> const& actionName, GlobalProgramInformation& globalProgramInformation) const {
STORM_LOG_ASSERT(!this->secondRun, "Dummy procedure must not be called in second run.");
std::string realActionName = actionName ? actionName.get() : "";
@ -697,10 +697,10 @@ namespace storm {
std::size_t nextIndex = globalProgramInformation.actionIndices.size();
globalProgramInformation.actionIndices.emplace(realActionName, nextIndex);
}
return storm::prism::Command();
}
storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
try {
@ -716,7 +716,7 @@ namespace storm {
}
return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename());
}
storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
try {
@ -733,7 +733,7 @@ namespace storm {
return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename());
}
storm::prism::ClockVariable PrismParser::createClockVariable(std::string const& variableName) const {
if (!this->secondRun) {
try {
@ -795,18 +795,18 @@ namespace storm {
}
return true;
}
storm::prism::ModuleRenaming PrismParser::createModuleRenaming(std::map<std::string,std::string> const& renaming) const {
return storm::prism::ModuleRenaming(renaming);
}
storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation& globalProgramInformation) const {
// Check whether the module to rename actually exists.
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
auto const& renaming = moduleRenaming.getRenaming();
if (!this->secondRun) {
// Register all (renamed) variables for later use.
// We already checked before, whether the renaiming is valid.
@ -837,7 +837,7 @@ namespace storm {
this->observables.erase(renamingPair->second);
}
}
for (auto const& command : moduleToRename.getCommands()) {
std::string newActionName = command.getActionName();
auto const& renamingPair = renaming.find(command.getActionName());
@ -852,13 +852,13 @@ namespace storm {
globalProgramInformation.actionIndices.emplace(newActionName, nextIndex);
}
}
// Return a dummy module in the first pass.
return storm::prism::Module();
} else {
// Add a mapping from the new module name to its (future) index.
globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
// Create a mapping from identifiers to the expressions they need to be replaced with.
std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
for (auto const& namePair : renaming) {
@ -868,7 +868,7 @@ namespace storm {
expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression);
}
}
// Rename the boolean variables.
std::vector<storm::prism::BooleanVariable> booleanVariables;
for (auto const& variable : moduleToRename.getBooleanVariables()) {
@ -880,7 +880,7 @@ namespace storm {
}
booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), moduleRenaming.getLineNumber()));
}
// Rename the integer variables.
std::vector<storm::prism::IntegerVariable> integerVariables;
for (auto const& variable : moduleToRename.getIntegerVariables()) {
@ -904,13 +904,13 @@ namespace storm {
}
clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), moduleRenaming.getLineNumber()));
}
// Rename invariant (if present)
storm::expressions::Expression invariant;
if (moduleToRename.hasInvariant()) {
invariant = moduleToRename.getInvariant().substitute(expressionRenaming);
}
// Rename commands.
std::vector<storm::prism::Command> commands;
for (auto const& command : moduleToRename.getCommands()) {
@ -928,13 +928,13 @@ namespace storm {
updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), moduleRenaming.getLineNumber());
++globalProgramInformation.currentUpdateIndex;
}
std::string newActionName = command.getActionName();
auto const& renamingPair = renaming.find(command.getActionName());
if (renamingPair != renaming.end()) {
newActionName = renamingPair->second;
}
uint_fast64_t actionIndex = 0;
auto nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
@ -944,22 +944,22 @@ namespace storm {
} else {
actionIndex = nameIndexPair->second;
}
commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), moduleRenaming.getLineNumber());
++globalProgramInformation.currentCommandIndex;
}
return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming);
}
}
storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
storm::prism::Program::ModelType finalModelType = globalProgramInformation.modelType;
if (globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED) {
STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'.");
finalModelType = storm::prism::Program::ModelType::MDP;
}
// make sure formulas are stored in a proper order.
std::vector<storm::prism::Formula> orderedFormulas;
if (this->secondRun) {
@ -971,7 +971,7 @@ namespace storm {
return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, globalProgramInformation.observationLabels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
}
void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {
globalProgramInformation.hasInitialConstruct = false;
}

66
src/storm-parsers/parser/PrismParser.h
View File

@ -20,7 +20,7 @@ namespace storm {
namespace storm {
namespace parser {
class ExpressionParser;
// A class that stores information about the parsed program.
class GlobalProgramInformation {
public:
@ -29,7 +29,7 @@ namespace storm {
// Map the empty action to index 0.
actionIndices.emplace("", 0);
}
void moveToSecondRun() {
// Clear all data except the action to indices mapping.
modelType = storm::prism::Program::ModelType::UNDEFINED;
@ -45,11 +45,11 @@ namespace storm {
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;
@ -81,7 +81,7 @@ namespace storm {
* @return The resulting PRISM program.
*/
static storm::prism::Program parse(std::string const& filename, bool prismCompatability = false);
/*!
* Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax.
*
@ -90,7 +90,7 @@ namespace storm {
* @return The resulting PRISM program.
*/
static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool prismCompatability = false);
private:
struct modelTypeStruct : qi::symbols<char, storm::prism::Program::ModelType> {
modelTypeStruct() {
@ -152,7 +152,7 @@ namespace storm {
std::string filename;
Iterator const first;
};
/*!
* Creates a grammar for the given filename and the iterator to the first input to parse.
*
@ -160,32 +160,32 @@ namespace storm {
* @param first The iterator to the beginning of the input.
*/
PrismParser(std::string const& filename, Iterator first, bool prismCompatibility);
/*!
* Sets an internal flag that indicates the second run is now taking place.
*/
void moveToSecondRun();
/*!
* Parses the stored formula Expressions.
*/
void createFormulaIdentifiers(std::vector<storm::prism::Formula> const& formulas);
// A flag that stores whether the grammar is currently doing the second run.
bool secondRun;
bool prismCompatibility;
/*!
* 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.
*
@ -194,22 +194,22 @@ namespace storm {
std::string const& getFilename() const;
mutable std::set<std::string> observables;
// Store the expressions of formulas. They have to be parsed after the first and before the second run
std::vector<std::string> formulaExpressions;
// Stores a proper order in which formulas can be evaluated. This is necessary since formulas might depend on each other.
// E.g. for "formula x = y; formula y = z;" we have to swap the order of the two formulas.
std::vector<uint64_t> formulaOrder;
// 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(), Skipper> start;
// Rules for model type.
qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;
@ -217,7 +217,7 @@ namespace storm {
qi::rule<Iterator, storm::expressions::Expression(), Skipper> boolExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> intExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> numericalExpression;
// Rules for parsing the program header.
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
@ -227,45 +227,49 @@ namespace storm {
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;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalBooleanVariableDefinition;
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalIntegerVariableDefinition;
// Rules for modules definition.
qi::rule<Iterator, std::string(), Skipper> knownModuleName;
qi::rule<Iterator, std::string(), Skipper> freshModuleName;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>, std::vector<storm::prism::ClockVariable>>, Skipper> moduleDefinition;
qi::rule<Iterator, storm::prism::ModuleRenaming, qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::string, storm::prism::ModuleRenaming>, Skipper> renamedModule;
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&, std::vector<storm::prism::ClockVariable>&), Skipper> variableDefinition;
qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
qi::rule<Iterator, storm::prism::ClockVariable(), qi::locals<storm::expressions::Expression>, Skipper> clockVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<bool>, 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, std::string(), Skipper> freshRewardModelName;
qi::rule<Iterator, storm::prism::RewardModel(GlobalProgramInformation&), qi::locals<std::string, std::vector<storm::prism::StateReward>, std::vector<storm::prism::StateActionReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, storm::prism::StateActionReward(GlobalProgramInformation&), Skipper> stateActionRewardDefinition;
qi::rule<Iterator, storm::prism::TransitionReward(GlobalProgramInformation&), qi::locals<std::string, storm::expressions::Expression, storm::expressions::Expression,storm::expressions::Expression>, Skipper> transitionRewardDefinition;
// Rules for player definitions
qi::rule<Iterator, std::string(), Skipper> commandName;
qi::rule<Iterator, qi::unused_type(), Skipper> playerDefinition;
// Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
// Rules for POMDP observables (standard prism)
qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct;
// Rules for invariant constructs
qi::rule<Iterator, storm::expressions::Expression(), Skipper> invariantConstruct;
@ -294,20 +298,20 @@ namespace storm {
// Rules for formula definitions.
qi::rule<Iterator, std::string(), Skipper> formulaDefinitionRhs;
qi::rule<Iterator, storm::prism::Formula(), Skipper> formulaDefinition;
// Rules for identifier parsing.
qi::rule<Iterator, std::string(), Skipper> identifier;
qi::rule<Iterator, std::string(), Skipper> freshIdentifier;
// Parsers that recognize special keywords and model types.
storm::parser::PrismParser::keywordsStruct keywords_;
storm::parser::PrismParser::modelTypeStruct modelType_;
qi::symbols<char, storm::expressions::Expression> identifiers_;
// Parser and manager used for recognizing expressions.
std::shared_ptr<storm::expressions::ExpressionManager> manager;
std::shared_ptr<storm::parser::ExpressionParser> expressionParser;
// Helper methods used in the grammar.
bool isValidIdentifier(std::string const& identifier);
bool isFreshIdentifier(std::string const& identifier);
@ -323,7 +327,7 @@ namespace storm {
bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
bool addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation);
void setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType);
std::shared_ptr<storm::prism::Composition> createModuleComposition(std::string const& moduleName) const;
std::shared_ptr<storm::prism::Composition> createRenamingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::map<std::string, std::string> const& renaming) const;
std::shared_ptr<storm::prism::Composition> createHidingComposition(std::shared_ptr<storm::prism::Composition> const& subcomposition, std::set<std::string> const& actionsToHide) const;

16
src/storm/generator/NextStateGenerator.h
View File

@ -88,7 +88,7 @@ namespace storm {
* @param remapping The remapping to apply.
*/
void remapStateIds(std::function<StateType(StateType const&)> const& remapping);
protected:
/*!
* Creates the state labeling for the given states using the provided labels and expressions.
@ -100,25 +100,25 @@ namespace storm {
virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const;
void postprocess(StateBehavior<ValueType, StateType>& result);
/// The options to be used for next-state generation.
NextStateGeneratorOptions options;
/// The expression manager used for evaluating expressions.
std::shared_ptr<storm::expressions::ExpressionManager const> expressionManager;
/// The expressions that define terminal states.
std::vector<std::pair<storm::expressions::Expression, bool>> terminalStates;
/// Information about how the variables are packed.
VariableInformation variableInformation;
/// An evaluator used to evaluate expressions.
std::unique_ptr<storm::expressions::ExpressionEvaluator<ValueType>> evaluator;
/// The currently loaded state.
CompressedState const* state;
/// A comparator used to compare constants.
storm::utility::ConstantsComparator<ValueType> comparator;

176
src/storm/generator/PrismNextStateGenerator.cpp
View File

@ -20,24 +20,24 @@
namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : PrismNextStateGenerator<ValueType, StateType>(program.substituteConstantsFormulas(), options, false) {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(program.getManager(), options), program(program), rewardModels(), hasStateActionRewards(false) {
STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program);
STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
// Only after checking validity of the program, we initialize the variable information.
this->checkValid();
this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet());
// Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());
if (this->options.isBuildAllRewardModelsSet()) {
for (auto const& rewardModel : this->program.getRewardModels()) {
rewardModels.push_back(rewardModel);
@ -52,19 +52,19 @@ namespace storm {
STORM_LOG_THROW(this->program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
}
}
// If no reward model was yet added, but there was one that was given in the options, we try to build the
// standard reward model.
if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
rewardModels.push_back(this->program.getRewardModel(0));
}
}
// Determine whether any reward model has state action rewards.
for (auto const& rewardModel : rewardModels) {
hasStateActionRewards |= rewardModel.get().hasStateActionRewards();
}
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
if (this->options.hasTerminalStates()) {
for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
@ -87,7 +87,7 @@ namespace storm {
// We can handle all valid prism programs (except for PTAs)
return program.getModelType() != storm::prism::Program::ModelType::PTA;
}
template<typename ValueType, typename StateType>
void PrismNextStateGenerator<ValueType, StateType>::checkValid() const {
// If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
@ -118,7 +118,7 @@ namespace storm {
}
#endif
}
template<typename ValueType, typename StateType>
ModelType PrismNextStateGenerator<ValueType, StateType>::getModelType() const {
switch (program.getModelType()) {
@ -146,7 +146,7 @@ namespace storm {
bool PrismNextStateGenerator<ValueType, StateType>::isPartiallyObservable() const {
return program.isPartiallyObservable();
}
template<typename ValueType, typename StateType>
std::vector<StateType> PrismNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
std::vector<StateType> initialStateIndices;
@ -162,9 +162,9 @@ namespace storm {
currentIntegerValues.emplace_back(0);
initialState.setFromInt(variable.bitOffset, variable.bitWidth, 0);
}
initialStateIndices.emplace_back(stateToIdCallback(initialState));
bool done = false;
while (!done) {
bool changedBooleanVariable = false;
@ -177,7 +177,7 @@ namespace storm {
initialState.set(booleanVariable.bitOffset, false);
}
}
bool changedIntegerVariable = false;
if (changedBooleanVariable) {
initialStateIndices.emplace_back(stateToIdCallback(initialState));
@ -191,37 +191,37 @@ namespace storm {
currentIntegerValues[integerVariableIndex] = integerVariable.lowerBound;
}
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, currentIntegerValues[integerVariableIndex]);
if (changedIntegerVariable) {
break;
}
}
}
if (changedIntegerVariable) {
initialStateIndices.emplace_back(stateToIdCallback(initialState));
}
done = !changedBooleanVariable && !changedIntegerVariable;
}
STORM_LOG_DEBUG("Enumerated " << initialStateIndices.size() << " initial states using brute force enumeration.");
} else {
// Prepare an SMT solver to enumerate all initial states.
storm::utility::solver::SmtSolverFactory factory;
std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(program.getManager());
std::vector<storm::expressions::Expression> rangeExpressions = program.getAllRangeExpressions();
for (auto const& expression : rangeExpressions) {
solver->add(expression);
}
solver->add(program.getInitialStatesExpression());
// Proceed ss long as the solver can still enumerate initial states.
while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
// Create fresh state.
CompressedState initialState(this->variableInformation.getTotalBitOffset(true));
// Read variable assignment from the solution of the solver. Also, create an expression we can use to
// prevent the variable assignment from being enumerated again.
storm::expressions::Expression blockingExpression;
@ -238,29 +238,29 @@ namespace storm {
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
}
// Register initial state and return it.
StateType id = stateToIdCallback(initialState);
initialStateIndices.push_back(id);
// Block the current initial state to search for the next one.
if (!blockingExpression.isInitialized()) {
break;
}
solver->add(blockingExpression);
}
STORM_LOG_DEBUG("Enumerated " << initialStateIndices.size() << " initial states using SMT solving.");
}
return initialStateIndices;
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;
// First, construct the state rewards, as we may return early if there are no choices later and we already
// need the state rewards then.
for (auto const& rewardModel : rewardModels) {
@ -274,7 +274,7 @@ namespace storm {
}
result.addStateReward(stateRewardValue);
}
// If a terminal expression was set and we must not expand this state, return now.
if (!this->terminalStates.empty()) {
for (auto const& expressionBool : this->terminalStates) {
@ -286,7 +286,7 @@ namespace storm {
// Get all choices for the state.
result.setExpanded();
std::vector<Choice<ValueType>> allChoices;
if (this->getOptions().isApplyMaximalProgressAssumptionSet()) {
// First explore only edges without a rate
@ -301,15 +301,15 @@ namespace storm {
allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
addLabeledChoices(allChoices, *this->state, stateToIdCallback);
}
std::size_t totalNumberOfChoices = allChoices.size();
// If there is not a single choice, we return immediately, because the state has no behavior (other than
// the state reward).
if (totalNumberOfChoices == 0) {
return result;
}
// If the model is a deterministic model, we need to fuse the choices into one.
if (this->isDeterministicModel() && totalNumberOfChoices > 1) {
Choice<ValueType> globalChoice;
@ -317,11 +317,11 @@ namespace storm {
if (this->options.isAddOverlappingGuardLabelSet()) {
this->overlappingGuardStates->push_back(stateToIdCallback(*this->state));
}
// For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
// this is equal to the number of choices, which is why we initialize it like this here.
ValueType totalExitRate = this->isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
// Iterate over all choices and combine the probabilities/rates into one choice.
for (auto const& choice : allChoices) {
for (auto const& stateProbabilityPair : choice) {
@ -331,20 +331,20 @@ namespace storm {
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
}
}
if (hasStateActionRewards && !this->isDiscreteTimeModel()) {
totalExitRate += choice.getTotalMass();
}
if (this->options.isBuildChoiceLabelsSet() && choice.hasLabels()) {
globalChoice.addLabels(choice.getLabels());
}
if (this->options.isBuildChoiceOriginsSet() && choice.hasOriginData()) {
globalChoice.addOriginData(choice.getOriginData());
}
}
// Now construct the state-action reward for all selected reward models.
for (auto const& rewardModel : rewardModels) {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
@ -355,41 +355,41 @@ namespace storm {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
}
}
}
}
if (hasStateActionRewards) {
globalChoice.addReward(stateActionRewardValue / totalExitRate);
}
}
// Move the newly fused choice in place.
allChoices.clear();
allChoices.push_back(std::move(globalChoice));
}
// Move all remaining choices in place.
for (auto& choice : allChoices) {
result.addChoice(std::move(choice));
}
this->postprocess(result);
return result;
}
template<typename ValueType, typename StateType>
CompressedState PrismNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::prism::Update const& update) {
CompressedState newState(state);
// NOTE: the following process assumes that the assignments of the update are ordered in such a way that the
// assignments to boolean variables precede the assignments to all integer variables and that within the
// types, the assignments to variables are ordered (in ascending order) by the expression variables.
// This is guaranteed for PRISM models, by sorting the assignments as soon as an update is created.
auto assignmentIt = update.getAssignments().begin();
auto assignmentIte = update.getAssignments().end();
// Iterate over all boolean assignments and carry them out.
auto boolIt = this->variableInformation.booleanVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) {
@ -398,7 +398,7 @@ namespace storm {
}
newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getExpression()));
}
// Iterate over all integer assignments and carry them out.
auto integerIt = this->variableInformation.integerVariables.begin();
for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) {
@ -417,13 +417,13 @@ namespace storm {
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
}
// Check that we processed all assignments.
STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
return newState;
}
struct ActiveCommandData {
ActiveCommandData(storm::prism::Module const* modulePtr, std::set<uint_fast64_t> const* commandIndicesPtr, typename std::set<uint_fast64_t>::const_iterator currentCommandIndexIt) : modulePtr(modulePtr), commandIndicesPtr(commandIndicesPtr), currentCommandIndexIt(currentCommandIndexIt) {
// Intentionally left empty
@ -432,33 +432,33 @@ namespace storm {
std::set<uint_fast64_t> const* commandIndicesPtr;
typename std::set<uint_fast64_t>::const_iterator currentCommandIndexIt;
};
template<typename ValueType, typename StateType>
boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> PrismNextStateGenerator<ValueType, StateType>::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex, CommandFilter const& commandFilter) {
// First check whether there is at least one enabled command at each module
// This avoids evaluating unnecessarily many guards.
// If we find one module without an enabled command, we return boost::none.
// At the same time, we store pointers to the relevant modules, the relevant command sets and the first enabled command within each set.
// Iterate over all modules.
std::vector<ActiveCommandData> activeCommands;
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
// If the module has no command labeled with the given action, we can skip this module.
if (!module.hasActionIndex(actionIndex)) {
continue;
}
std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
// If the module contains the action, but there is no command in the module that is labeled with
// this action, we don't have any feasible command combinations.
if (commandIndices.empty()) {
return boost::none;
}
// Look up commands by their indices and check if the guard evaluates to true in the given state.
bool hasOneEnabledCommand = false;
for (auto commandIndexIt = commandIndices.begin(), commandIndexIte = commandIndices.end(); commandIndexIt != commandIndexIte; ++commandIndexIt) {
@ -476,23 +476,23 @@ namespace storm {
break;
}
}
if (!hasOneEnabledCommand) {
return boost::none;
}
}
// If we reach this point, there has to be at least one active command for each relevant module.
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> result;
// Iterate over all command sets.
for (auto const& activeCommand : activeCommands) {
std::vector<std::reference_wrapper<storm::prism::Command const>> commands;
auto commandIndexIt = activeCommand.currentCommandIndexIt;
// The command at the current position is already known to be enabled
commands.push_back(activeCommand.modulePtr->getCommand(*commandIndexIt));
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
auto commandIndexIte = activeCommand.commandIndicesPtr->end();
for (++commandIndexIt; commandIndexIt != commandIndexIte; ++commandIndexIt) {
@ -507,29 +507,29 @@ namespace storm {
commands.push_back(command);
}
}
result.push_back(std::move(commands));
}
STORM_LOG_ASSERT(!result.empty(), "Expected non-empty list.");
return result;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> PrismNextStateGenerator<ValueType, StateType>::getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) {
std::vector<Choice<ValueType>> result;
// Iterate over all modules.
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
storm::prism::Module const& module = program.getModule(i);
// Iterate over all commands.
for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
storm::prism::Command const& command = module.getCommand(j);
// Only consider unlabeled commands.
if (command.isLabeled()) continue;
if (commandFilter != CommandFilter::All) {
STORM_LOG_ASSERT(commandFilter == CommandFilter::Markovian || commandFilter == CommandFilter::Probabilistic, "Unexpected command filter.");
if ((commandFilter == CommandFilter::Markovian) != command.isMarkovian()) {
@ -541,16 +541,16 @@ namespace storm {
if (!this->evaluator->asBool(command.getGuardExpression())) {
continue;
}
result.push_back(Choice<ValueType>(command.getActionIndex(), command.isMarkovian()));
Choice<ValueType>& choice = result.back();
// Remember the choice origin only if we were asked to.
if (this->options.isBuildChoiceOriginsSet()) {
CommandSet commandIndex { command.getGlobalIndex() };
choice.addOriginData(boost::any(std::move(commandIndex)));
}
// Iterate over all updates of the current command.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
@ -561,7 +561,7 @@ namespace storm {
// Obtain target state index and add it to the list of known states. If it has not yet been
// seen, we also add it to the set of states that have yet to be explored.
StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
// Update the choice by adding the probability/target state to it.
choice.addProbability(stateIndex, probability);
if (this->options.isExplorationChecksSet()) {
@ -569,7 +569,7 @@ namespace storm {
}
}
}
// Create the state-action reward for the newly created choice.
for (auto const& rewardModel : rewardModels) {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
@ -582,24 +582,24 @@ namespace storm {
}
choice.addReward(stateActionRewardValue);
}
if (this->options.isExplorationChecksSet()) {
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
}
}
}
return result;
}
template<typename ValueType, typename StateType>
void PrismNextStateGenerator<ValueType, StateType>::generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>::const_iterator> const& iteratorList, storm::builder::jit::Distribution<StateType, ValueType>& distribution, StateToIdCallback stateToIdCallback) {
if (storm::utility::isZero<ValueType>(probability)) {
return;
}
if (position >= iteratorList.size()) {
StateType id = stateToIdCallback(state);
distribution.add(id, probability);
@ -611,7 +611,7 @@ namespace storm {
}
}
}
template<typename ValueType, typename StateType>
void PrismNextStateGenerator<ValueType, StateType>::addLabeledChoices(std::vector<Choice<ValueType>>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter) {
@ -702,7 +702,7 @@ namespace storm {
}
}
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
// Gather a vector of labels and their expressions.
@ -720,7 +720,7 @@ namespace storm {
}
}
}
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels);
}
@ -741,22 +741,22 @@ namespace storm {
std::size_t PrismNextStateGenerator<ValueType, StateType>::getNumberOfRewardModels() const {
return rewardModels.size();
}
template<typename ValueType, typename StateType>
storm::builder::RewardModelInformation PrismNextStateGenerator<ValueType, StateType>::getRewardModelInformation(uint64_t const& index) const {
storm::prism::RewardModel const& rewardModel = rewardModels[index].get();
return storm::builder::RewardModelInformation(rewardModel.getName(), rewardModel.hasStateRewards(), rewardModel.hasStateActionRewards(), rewardModel.hasTransitionRewards());
}
template<typename ValueType, typename StateType>
std::shared_ptr<storm::storage::sparse::ChoiceOrigins> PrismNextStateGenerator<ValueType, StateType>::generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const {
if (!this->getOptions().isBuildChoiceOriginsSet()) {
return nullptr;
}
std::vector<uint_fast64_t> identifiers;
identifiers.reserve(dataForChoiceOrigins.size());
std::map<CommandSet, uint_fast64_t> commandSetToIdentifierMap;
// The empty commandset (i.e., the choices without origin) always has to get identifier getIdentifierForChoicesWithNoOrigin() -- which is assumed to be 0
STORM_LOG_ASSERT(storm::storage::sparse::ChoiceOrigins::getIdentifierForChoicesWithNoOrigin() == 0, "The no origin identifier is assumed to be zero");
@ -764,7 +764,7 @@ namespace storm {
uint_fast64_t currentIdentifier = 1;
for (boost::any& originData : dataForChoiceOrigins) {
STORM_LOG_ASSERT(originData.empty() || boost::any_cast<CommandSet>(&originData) != nullptr, "Origin data has unexpected type: " << originData.type().name() << ".");
CommandSet currentCommandSet = originData.empty() ? CommandSet() : boost::any_cast<CommandSet>(std::move(originData));
auto insertionRes = commandSetToIdentifierMap.insert(std::make_pair(std::move(currentCommandSet), currentIdentifier));
identifiers.push_back(insertionRes.first->second);
@ -772,16 +772,16 @@ namespace storm {
++currentIdentifier;
}
}
std::vector<CommandSet> identifierToCommandSetMapping(currentIdentifier);
for (auto const& setIdPair : commandSetToIdentifierMap) {
identifierToCommandSetMapping[setIdPair.second] = setIdPair.first;
}
return std::make_shared<storm::storage::sparse::PrismChoiceOrigins>(std::make_shared<storm::prism::Program>(program), std::move(identifiers), std::move(identifierToCommandSetMapping));
}
template class PrismNextStateGenerator<double>;
#ifdef STORM_HAVE_CARL

40
src/storm/storage/SymbolicModelDescription.cpp
View File

@ -15,37 +15,37 @@
namespace storm {
namespace storage {
SymbolicModelDescription::SymbolicModelDescription(storm::jani::Model const& model) : modelDescription(model) {
// Intentionally left empty.
}
SymbolicModelDescription::SymbolicModelDescription(storm::prism::Program const& program) : modelDescription(program) {
// Intentionally left empty.
}
SymbolicModelDescription& SymbolicModelDescription::operator=(storm::jani::Model const& model) {
this->modelDescription = model;
return *this;
}
SymbolicModelDescription& SymbolicModelDescription::operator=(storm::prism::Program const& program) {
this->modelDescription = program;
return *this;
}
bool SymbolicModelDescription::hasModel() const {
return static_cast<bool>(modelDescription);
}
bool SymbolicModelDescription::isJaniModel() const {
return modelDescription.get().which() == 0;
}
bool SymbolicModelDescription::isPrismProgram() const {
return modelDescription.get().which() == 1;
}
SymbolicModelDescription::ModelType SymbolicModelDescription::getModelType() const {
if (this->isJaniModel()) {
storm::jani::Model const& janiModel = this->asJaniModel();
@ -78,15 +78,15 @@ namespace storm {
return this->asJaniModel().getManager();
}
}
void SymbolicModelDescription::setModel(storm::jani::Model const& model) {
modelDescription = model;
}
void SymbolicModelDescription::setModel(storm::prism::Program const& program) {
modelDescription = program;
}
storm::jani::Model const& SymbolicModelDescription::asJaniModel() const {
STORM_LOG_THROW(isJaniModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type.");
return boost::get<storm::jani::Model>(modelDescription.get());
@ -120,7 +120,7 @@ namespace storm {
}
return result;
}
SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const {
if (this->isJaniModel()) {
return *this;
@ -131,7 +131,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
}
}
std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> SymbolicModelDescription::toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal) const {
if (this->isJaniModel()) {
return std::make_pair(*this, std::vector<storm::jani::Property>());
@ -143,12 +143,12 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
}
}
SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = parseConstantDefinitions(constantDefinitionString);
return preprocess(substitution);
}
SymbolicModelDescription SymbolicModelDescription::preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
if (this->isJaniModel()) {
storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstantsFunctions();
@ -158,7 +158,7 @@ namespace storm {
}
return *this;
}
std::map<storm::expressions::Variable, storm::expressions::Expression> SymbolicModelDescription::parseConstantDefinitions(std::string const& constantDefinitionString) const {
if (this->isJaniModel()) {
return storm::utility::cli::parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString);
@ -166,7 +166,7 @@ namespace storm {
return storm::utility::cli::parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString);
}
}
void SymbolicModelDescription::requireNoUndefinedConstants() const {
if (this->isJaniModel()) {
storm::utility::jani::requireNoUndefinedConstants(this->asJaniModel());
@ -174,7 +174,7 @@ namespace storm {
storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram());
}
}
bool SymbolicModelDescription::hasUndefinedConstants() const {
if (this->isPrismProgram()) {
return this->asPrismProgram().hasUndefinedConstants();
@ -182,7 +182,7 @@ namespace storm {
return this->asJaniModel().hasUndefinedConstants();
}
}
std::vector<storm::expressions::Variable> SymbolicModelDescription::getUndefinedConstants() const {
std::vector<storm::expressions::Variable> result;
if (this->isPrismProgram()) {
@ -198,7 +198,7 @@ namespace storm {
}
return result;
}
std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) {
if (model.isPrismProgram()) {
out << model.asPrismProgram();

10
src/storm/storage/SymbolicModelDescription.h
View File

@ -49,20 +49,20 @@ namespace storm {
* @note The returned property vector might be empty in case no renaming is necessary.
*/
std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal) const;
SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
SymbolicModelDescription preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitions(std::string const& constantDefinitionString) const;
void requireNoUndefinedConstants() const;
bool hasUndefinedConstants() const;
std::vector<storm::expressions::Variable> getUndefinedConstants() const;
private:
boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;
};
std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model);
std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType const& type);

527
src/storm/storage/prism/Program.cpp
File diff suppressed because it is too large
View File

188
src/storm/storage/prism/Program.h
View File

@ -24,7 +24,7 @@ namespace storm {
class Model;
class Property;
}
namespace prism {
class Program : public LocatedInformation {
public:
@ -32,9 +32,9 @@ namespace storm {
* An enum for the different model types.
*/
enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA};
enum class ValidityCheckLevel : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};
/*!
* Creates a program with the given model type, undefined constants, global variables, modules, reward
* models, labels and initial states.
@ -58,7 +58,7 @@ namespace storm {
* @param finalModel If set to true, the program is checked for input-validity, as well as some post-processing.
*/
Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, 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::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, std::vector<ObservationLabel> const& observationLabels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, bool prismCompatibility, std::string const& filename = "", uint_fast64_t lineNumber = 0, bool finalModel = true);
// Provide default implementations for constructors and assignments.
Program() = default;
Program(Program const& other) = default;
@ -72,14 +72,14 @@ namespace storm {
* @return The type of the model.
*/
ModelType getModelType() const;
/*!
* Retrieves whether the model is a discrete-time model, i.e. a DTMC or an MDP.
*
* @return True iff the model is a discrete-time model.
*/
bool isDiscreteTimeModel() const;
/*!
* Retrieves whether the model is one without nondeterministic choices, i.e. a DTMC or a CTMC.
*/
@ -102,10 +102,10 @@ namespace storm {
* That is, undefined constants may only appear in the probability expressions of updates as well as in the
* values in reward models.
*
* @return True iff the undefined constants are graph-preserving.
* @return True iff the undefined constants are graph-preserving.
*/
bool undefinedConstantsAreGraphPreserving() const;
/*!
* Retrieves the undefined constants in the program.
*
@ -127,7 +127,7 @@ namespace storm {
* @return True iff the constant exists in the program.
*/
bool hasConstant(std::string const& constantName) const;
/*!
* Retrieves the constant with the given name if it exists.
*
@ -135,33 +135,33 @@ namespace storm {
* @return The constant with the given name if it exists.
*/
Constant const& getConstant(std::string const& constantName) const;
/*!
* Retrieves a mapping of all defined constants to their defining expressions.
*
* @return A mapping from constants to their 'values'.
*/
std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
/*!
* Retrieves a mapping of all formula variables to their defining expressions.
*
* @return A mapping from constants to their 'values'.
*/
std::map<storm::expressions::Variable, storm::expressions::Expression> getFormulasSubstitution() const;
/*!
* Retrieves a mapping of all defined constants and formula variables to their defining expressions
*
* @return A mapping from constants and formulas to their expressions.
*/
std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsFormulasSubstitution(bool getConstantsSubstitution = true, bool getFormulasSubstitution = true) const;
/*!
* Applies the renaming of a renamed module to the given substitution.
*/
std::map<storm::expressions::Variable, storm::expressions::Expression> getSubstitutionForRenamedModule(Module const& renamedModule, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
/*!
* Gets the renaming of a module after flattening all renamings.
* Note that the base of a renamed module might again be a renamed module.
@ -174,7 +174,7 @@ namespace storm {
* @return The constants defined in the program.
*/
std::vector<Constant> const& getConstants() const;
/*!
* Retrieves the number of all constants defined in the program.
*
@ -195,20 +195,20 @@ namespace storm {
/*!
* Retrieves whether a global Boolean variable with the given name exists
*
*
* @param variableName The name of the variable
* @return true iff a global variable of type Boolean with the given name exists.
*/
bool globalBooleanVariableExists(std::string const& variableName) const;
/**
* Retrieves whether a global Integer variable with the given name exists
*
*
* @param variableName The name of the variable
* @return true iff a global variable of type Integer with the given name exists.
*/
bool globalIntegerVariableExists(std::string const& variableName) const;
/*!
* Retrieves the global boolean variables of the program.
*
@ -223,7 +223,7 @@ namespace storm {
* @return The global boolean variable with the given name.
*/
BooleanVariable const& getGlobalBooleanVariable(std::string const& variableName) const;
/*!
* Retrieves the global integer variables of the program.
*
@ -245,21 +245,21 @@ namespace storm {
* @return The set of expression variables used by this program.
*/
std::set<storm::expressions::Variable> getAllExpressionVariables() const;
/*!
* Retrieves a list of expressions that characterize the legal ranges of all variables.
*
* @return A list of expressions that characterize the legal ranges of all variables.
*/
std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
/*!
* Retrieves the number of global boolean variables of the program.
*
* @return The number of global boolean variables of the program.
*/
std::size_t getNumberOfGlobalBooleanVariables() const;
/*!
* Retrieves the number of global integer variables of the program.
*
@ -273,21 +273,21 @@ namespace storm {
* @return The formulas defined in the program.
*/
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.
*
* @return The number of modules in the program.
*/
std::size_t getNumberOfModules() const;
/*!
* Retrieves the module with the given index.
*
@ -302,7 +302,7 @@ namespace storm {
* @return True iff a module with the given name exists.
*/
bool hasModule(std::string const& moduleName) const;
/*!
* Retrieves the module with the given name.
*
@ -310,26 +310,26 @@ namespace storm {
* @return The module with the given name.
*/
Module const& getModule(std::string const& moduleName) const;
/*!
* Retrieves all modules of the program.
*
* @return All modules of the program.
*/
std::vector<Module> const& getModules() const;
/*!
* Retrieves the mapping of action names to their indices.
*
* @return The mapping of action names to their indices.
*/
std::map<std::string, uint_fast64_t> const& getActionNameToIndexMapping() const;
/*!
* Retrieves whether the program specifies an initial construct.
*/
bool hasInitialConstruct() const;
/*!
* Retrieves the initial construct of the program.
*
@ -350,7 +350,7 @@ namespace storm {
* @return an expression characterizing the initial states.
*/
storm::expressions::Expression getInitialStatesExpression() const;
/*!
* Retrieves whether the program specifies a system composition in terms of process algebra operations over
* the modules.
@ -358,42 +358,42 @@ namespace storm {
* @return True iff the program specifies a system composition.
*/
bool specifiesSystemComposition() const;
/*!
* If the program specifies a system composition construct, this method retrieves it.
*
* @return The system composition construct as specified by the program.
*/
SystemCompositionConstruct const& getSystemCompositionConstruct() const;
/*!
* Retrieves the system composition construct (if any) and none otherwise.
*
* @return The system composition construct specified by the program or none.
*/
boost::optional<SystemCompositionConstruct> getOptionalSystemCompositionConstruct() const;
/*!
* Retrieves the default system composition for this program.
*
* @return The default system composition.
*/
std::shared_ptr<Composition> getDefaultSystemComposition() const;
/*!
* Retrieves the set of actions present in the program.
*
* @return The set of actions present in the program.
*/
std::set<std::string> const& getActions() const;
/*!
* Retrieves the set of synchronizing action indices present in the program.
*
* @return The set of synchronizing action indices present in the program.
*/
std::set<uint_fast64_t> const& getSynchronizingActionIndices() const;
/*!
* Retrieves the action name of the given action index.
*
@ -401,7 +401,7 @@ namespace storm {
* @return The name of the action.
*/
std::string const& getActionName(uint_fast64_t actionIndex) const;
/*!
* Retrieves the index of the action with the given name.
*
@ -409,7 +409,7 @@ namespace storm {
* @return The index of the action.
*/
uint_fast64_t getActionIndex(std::string const& actionName) const;
/*!
* Retrieves whether the program has an action with the given name.
*
@ -423,7 +423,7 @@ namespace storm {
* @return True iff the program has an action with the given index.
*/
bool hasAction(uint_fast64_t const& actionIndex) const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the
* given action.
@ -441,7 +441,7 @@ namespace storm {
* @return A set of indices of all matching modules.
*/
std::set<uint_fast64_t> const& getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const;
/*!
* Retrieves the index of the module in which the given variable name was declared.
*
@ -449,7 +449,7 @@ namespace storm {
* @return The index of the module in which the given variable name was declared.
*/
uint_fast64_t getModuleIndexByVariable(std::string const& variableName) const;
/*!
* Retrieves the index of the module and the (local) index of the command with the given global command index.
*
@ -474,7 +474,7 @@ namespace storm {
* @return True iff the program has at least one reward model.
*/
bool hasRewardModel() const;
/*!
* Retrieves whether the program has a reward model with the given name.
*
@ -482,21 +482,21 @@ namespace storm {
* @return True iff the program has a reward model with the given name.
*/
bool hasRewardModel(std::string const& name) const;
/*!
* Retrieves the reward models of the program.
*
* @return The reward models of the program.
*/
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.
*
@ -504,7 +504,7 @@ namespace storm {
* @return The reward model with the given name.
*/
RewardModel const& getRewardModel(std::string const& rewardModelName) const;
/*!
* Retrieves the reward model with the given index.
*
@ -512,7 +512,7 @@ namespace storm {
* @return The reward model with the given index.
*/
RewardModel const& getRewardModel(uint_fast64_t index) const;
/*!
* Checks whether the program has a label with the given name.
*
@ -520,7 +520,7 @@ namespace storm {
* @return True iff the label of the program.
*/
bool hasLabel(std::string const& labelName) const;
/*!
* Retrieves all labels that are defined by the probabilitic program.
*
@ -535,21 +535,21 @@ namespace storm {
* @return All guards appearing in the program.
*/
std::vector<storm::expressions::Expression> getAllGuards(bool negated = false) const;
/*!
* Retrieves the expression associated with the given label, if it exists.
*
* @param labelName The name of the label to retrieve.
*/
storm::expressions::Expression const& getLabelExpression(std::string const& label) const;
/*!
* Retrieves a mapping from all labels in the program to their defining expressions.
*
* @return A mapping from label names to their expressions.
*/
std::map<std::string, storm::expressions::Expression> getLabelToExpressionMapping() const;
/*!
* Retrieves the number of labels in the program.
*
@ -564,14 +564,14 @@ namespace storm {
* @param statePredicateExpression The predicate that is described by the label.
*/
void addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression);
/*!
* Removes the label with the given name from the program.
*
* @param name The name of a label that exists within the program.
*/
void removeLabel(std::string const& name);
/*!
* Removes all labels that are not contained in the given set from the program. Note: no check is performed
* as to whether or not the given label names actually exist.
@ -595,14 +595,14 @@ namespace storm {
* @return The number of labels in the program.
*/
std::size_t getNumberOfObservationLabels() const;
/*!
* Creates a new program that drops all commands whose indices are not in the given set.
*
* @param indexSet The set of indices for which to keep the commands.
*/
Program restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const;
/*!
* Defines the undefined constants according to the given map and returns the resulting program.
*
@ -612,7 +612,7 @@ namespace storm {
* definitions.
*/
Program defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
/*!
* Substitutes all constants appearing in the expressions of the program by their defining expressions. For
* this to work, all constants need to be defined prior to calling this.
@ -620,7 +620,7 @@ namespace storm {
* @return The resulting program that only contains expressions over variables of the program (and maybe formulas).
*/
Program substituteConstants() const;
/*!
* Substitutes all formulas appearing in the expressions of the program by their defining expressions.
*
@ -628,7 +628,7 @@ namespace storm {
* @return The resulting program that only contains expressions over variables of the program (and maybe constants).
*/
Program substituteFormulas() const;
/*!
* Substitutes all constants and/or formulas appearing in the expressions of the program by their defining expressions. For
* this to work, all constants need to be defined prior to calling this.
@ -636,19 +636,19 @@ namespace storm {
* @return The resulting program that only contains expressions over variables of the program.
*/
Program substituteConstantsFormulas(bool substituteConstants = true, bool substituteFormulas = true) const;
/**
* Entry point for static analysis for simplify. As we use the same expression manager, we recommend to not use the original program any further.
* Entry point for static analysis for simplify. As we use the same expression manager, we recommend to not use the original program any further.
* @return A simplified, equivalent program.
*/
Program simplify();
/*!
* Checks the validity of the program. If the program is not valid, an exception is thrown with a message
* that indicates the source of the problem.
*/
void checkValidity(Program::ValidityCheckLevel lvl = Program::ValidityCheckLevel::READYFORPROCESSING) const;
/*!
* Creates an equivalent program that contains exactly one module.
*
@ -656,16 +656,16 @@ namespace storm {
* @return The resulting program.
*/
Program flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory())) const;
friend std::ostream& operator<<(std::ostream& stream, Program const& program);
/*!
* Retrieves the manager responsible for the expressions of this program.
*
* @return The manager responsible for the expressions of this program.
*/
storm::expressions::ExpressionManager& getManager() const;
std::unordered_map<uint_fast64_t, std::string> buildCommandIndexToActionNameMap() const;
std::unordered_map<uint_fast64_t, uint_fast64_t> buildCommandIndexToActionIndex() const;
@ -676,14 +676,14 @@ namespace storm {
* Converts the PRISM model into an equivalent JANI model.
*/
storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "") const;
/*!
* Converts the PRISM model into an equivalent JANI model and if labels or reward models had
* to be renamed in the process, the renamings are applied to the given properties
* @return The jani model of this and either the new set of properties or an empty vector if no renamings were necessary
*/
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal = true, std::string suffix = "") const;
private:
/*!
* This function builds a command that corresponds to the synchronization of the given list of commands.
@ -696,95 +696,95 @@ namespace storm {
* @return The resulting command.
*/
Command synchronizeCommands(uint_fast64_t newCommandIndex, uint_fast64_t actionIndex, uint_fast64_t firstUpdateIndex, std::string const& actionName, std::vector<std::reference_wrapper<Command const>> const& commands) const;
/*!
* Equips all global variables without initial values with initial values based on their type.
*/
void createMissingInitialValues();
// The manager responsible for the variables/expressions of the program.
std::shared_ptr<storm::expressions::ExpressionManager> manager;
// Creates the internal mappings.
void createMappings();
// The type of the model.
ModelType modelType;
// The constants of the program.
std::vector<Constant> constants;
// A mapping from constant names to their corresponding indices.
std::map<std::string, uint_fast64_t> constantToIndexMap;
// The global boolean variables.
std::vector<BooleanVariable> globalBooleanVariables;
// A mapping from global boolean variable names to their corresponding indices.
std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap;
// The global integer variables.
std::vector<IntegerVariable> globalIntegerVariables;
// A mapping from global integer variable names to their corresponding indices.
std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap;
// The formulas defined in the program.
std::vector<Formula> formulas;
// A mapping of formula names to their corresponding indices.
std::map<std::string, uint_fast64_t> formulaToIndexMap;
// The modules associated with the program.
std::vector<Module> modules;
// A mapping of module names to their indices.
std::map<std::string, uint_fast64_t> moduleToIndexMap;
// The reward models associated with the program.
std::vector<RewardModel> rewardModels;
// A mapping of reward models to their indices.
std::map<std::string, uint_fast64_t> rewardModelToIndexMap;
// The initial construct of the program.
boost::optional<InitialConstruct> initialConstruct;
// If set, this specifies the way the modules are composed to obtain the full system.
boost::optional<SystemCompositionConstruct> systemCompositionConstruct;
// The labels that are defined for this model.
std::vector<Label> labels;
// A mapping from labels to their indices.
std::map<std::string, uint_fast64_t> labelToIndexMap;
// Observation labels
std::vector<ObservationLabel> observationLabels;
// A mapping from action names to their indices.
std::map<std::string, uint_fast64_t> actionToIndexMap;
// A mapping from action indices to their names.
std::map<uint_fast64_t, std::string> indexToActionMap;
// The set of actions present in this program.
std::set<std::string> actions;
// The set of synchronizing actions present in this program.
std::set<uint_fast64_t> synchronizingActionIndices;
// A map of actions to the set of modules containing commands labelled with this action.
std::map<uint_fast64_t, std::set<uint_fast64_t>> actionIndicesToModuleIndexMap;
// A mapping from variable names to the modules in which they were declared.
std::map<std::string, uint_fast64_t> variableToModuleIndexMap;
bool prismCompatibility;
};
std::ostream& operator<<(std::ostream& out, Program::ModelType const& type);
} // namespace prism
} // namespace storm

Write Preview
Loading…
Cancel
Save