diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp
index c95c42af2..624dda819 100644
--- a/src/storm-parsers/parser/PrismParser.cpp
+++ b/src/storm-parsers/parser/PrismParser.cpp
@@ -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("]"))
|
@@ -272,20 +272,37 @@ namespace storm {
// We first check for a module renaming, i.e., for this rule we certainly have to see a module definition
moduleDefinition = ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)];
moduleDefinition.name("module definition");
-
+
+ freshPlayerName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshPlayerName, phoenix::ref(*this), qi::_1)];
+ freshPlayerName.name("fresh player name");
+
+ commandName = (qi::lit("[") >> identifier >> qi::lit("]"))[qi::_val = qi::_1];
+ commandName.name("command name");
+
+ moduleName = identifier[qi::_val = qi::_1];
+ moduleName.name("module name");
+
+ playerDefinition = (qi::lit("player") > freshPlayerName[qi::_a = qi::_1]
+ > +( (commandName[phoenix::push_back(qi::_c, qi::_1)]
+ | moduleName[phoenix::push_back(qi::_b, qi::_1)]) % ','
+ )
+ > qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParser::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
+ playerDefinition.name("player definition");
+
moduleRenaming = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = phoenix::bind(&PrismParser::createModuleRenaming, phoenix::ref(*this), qi::_a)];
moduleRenaming.name("Module renaming list");
-
+
renamedModule = (((qi::lit("module") > freshModuleName) >> qi::lit("="))
> knownModuleName[qi::_a = qi::_1]
> (moduleRenaming[qi::_b = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isValidModuleRenaming, phoenix::ref(*this), qi::_a, qi::_b, qi::_r1)]
> qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_r1)];
renamedModule.name("module definition via renaming");
-
+
start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]
> modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)]
> -observablesConstruct
> *( definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
+ | playerDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::players, phoenix::ref(globalProgramInformation)), qi::_1)]
| undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)]
| formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)]
| globalVariableDefinition(phoenix::ref(globalProgramInformation))
@@ -298,7 +315,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 +337,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 +367,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 +414,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 +437,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 +445,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 +453,7 @@ namespace storm {
}
return true;
}
-
+
bool PrismParser::isFreshLabelName(std::string const& labelName) {
if (!this->secondRun) {
for (auto const& existingLabel : this->globalProgramInformation.labels) {
@@ -460,7 +477,7 @@ namespace storm {
}
return true;
}
-
+
bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) {
if (!this->secondRun) {
for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) {
@@ -472,19 +489,23 @@ namespace storm {
}
return true;
}
-
+
+ bool PrismParser::isFreshPlayerName(std::string const& playerName) {
+ 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 +515,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 +529,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 +561,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 +573,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 +585,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 +597,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 +609,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 +621,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 +629,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 +644,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 +656,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 +668,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 +680,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 +707,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 +718,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 +737,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 +754,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 {
@@ -755,12 +776,53 @@ namespace storm {
this->observables.insert(observables.begin(), observables.end());
// We need this list to be filled in both runs.
}
-
+
storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
- globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
+ if (!this->secondRun) {
+ globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
+ } else {
+ STORM_LOG_THROW(globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(), storm::exceptions::WrongFormatException, "Internal error while parsing: the index for module " << moduleName << " does not match the on in the first run.");
+ }
return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
}
-
+
+ storm::prism::Player PrismParser::createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames, std::vector<std::string> const & actionNames) {
+ if (this->secondRun) {
+ std::map<std::string, uint_fast64_t> controlledModuleIndices;
+ std::map<std::string, uint_fast64_t> controlledActionIndices;
+ for(std::string moduleName : moduleNames) {
+ auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(moduleName);
+ if (moduleIndexPair != globalProgramInformation.moduleToIndexMap.end()) {
+ controlledModuleIndices.insert(std::pair<std::string, uint_fast64_t>(moduleIndexPair->first, moduleIndexPair->second));
+ if (std::find(globalProgramInformation.playerControlledModules.begin(), globalProgramInformation.playerControlledModules.end(), moduleName) != globalProgramInformation.playerControlledModules.end()) {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Module '" << moduleName << "' already controlled by another player.");
+ } else {
+ globalProgramInformation.playerControlledModules.push_back(moduleName);
+ }
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": No module named '" << moduleName << "' present.");
+ }
+ }
+ for(std::string actionName : actionNames) {
+ auto const& actionIndexPair = globalProgramInformation.actionIndices.find(actionName);
+ if (actionIndexPair != globalProgramInformation.actionIndices.end()) {
+ controlledActionIndices.insert(std::pair<std::string, uint_fast64_t>(actionIndexPair->first, actionIndexPair->second));
+ if (std::find(globalProgramInformation.playerControlledCommands.begin(), globalProgramInformation.playerControlledCommands.end(), actionName) != globalProgramInformation.playerControlledCommands.end()) {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": Command '" << actionName << "' already controlled by another player.");
+ } else {
+ globalProgramInformation.playerControlledCommands.push_back(actionName);
+ }
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << " for player " << playerName << ": No action named '" << actionName << "' present.");
+ }
+ }
+ STORM_LOG_DEBUG("PLAYER created:" << playerName);
+ return storm::prism::Player(playerName, controlledModuleIndices, controlledActionIndices);
+ } else {
+ return storm::prism::Player();
+ }
+ }
+
bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const {
if (!this->secondRun) {
auto const& renaming = moduleRenaming.getRenaming();
@@ -795,18 +857,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 +899,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 +914,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 +930,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 +942,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 +966,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 +990,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 +1006,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) {
@@ -969,9 +1031,9 @@ 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);
+ return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.players, 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;
}
diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h
index 2668dcb68..9153f64bd 100644
--- a/src/storm-parsers/parser/PrismParser.h
+++ b/src/storm-parsers/parser/PrismParser.h
@@ -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;
@@ -38,6 +38,9 @@ namespace storm {
globalBooleanVariables.clear();
globalIntegerVariables.clear();
moduleToIndexMap.clear();
+ players.clear();
+ playerControlledModules.clear();
+ playerControlledCommands.clear();
modules.clear();
rewardModels.clear();
labels.clear();
@@ -45,11 +48,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;
@@ -62,11 +65,16 @@ namespace storm {
std::vector<storm::prism::RewardModel> rewardModels;
std::vector<storm::prism::Label> labels;
std::vector<storm::prism::ObservationLabel> observationLabels;
+ std::vector<storm::prism::Player> players;
+
+ std::vector<std::string> playerControlledModules;
+ std::vector<std::string> playerControlledCommands;
+
bool hasInitialConstruct;
storm::prism::InitialConstruct initialConstruct;
boost::optional<storm::prism::SystemCompositionConstruct> systemCompositionConstruct;
-
+
// Counters to provide unique indexing for commands and updates.
uint_fast64_t currentCommandIndex;
uint_fast64_t currentUpdateIndex;
@@ -81,7 +89,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 +98,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() {
@@ -101,10 +109,11 @@ namespace storm {
("ctmdp", storm::prism::Program::ModelType::CTMDP)
("ma", storm::prism::Program::ModelType::MA)
("pomdp", storm::prism::Program::ModelType::POMDP)
- ("pta", storm::prism::Program::ModelType::PTA);
+ ("pta", storm::prism::Program::ModelType::PTA)
+ ("smg", storm::prism::Program::ModelType::SMG);
}
};
-
+
struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
keywordsStruct() {
add
@@ -131,19 +140,21 @@ namespace storm {
("init", 21)
("endinit", 22)
("invariant", 23)
- ("endinvariant", 24);
+ ("endinvariant", 24)
+ ("smg", 25)
+ ("endplayer", 26);
}
};
-
+
// Functor used for annotating entities with line number information.
class PositionAnnotation {
public:
typedef void result_type;
-
+
PositionAnnotation(Iterator first) : first(first) {
// Intentionally left empty.
}
-
+
template<typename Entity, typename First, typename Last>
result_type operator()(Entity& entity, First f, Last) const {
entity.setLineNumber(get_line(f));
@@ -152,7 +163,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 +171,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 +205,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 +228,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 +238,51 @@ 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> freshPlayerName;
+ qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> commandName;
+ qi::rule<Iterator, std::string(), qi::locals<std::string>, Skipper> moduleName;
+ qi::rule<Iterator, storm::prism::Player(GlobalProgramInformation&), qi::locals<std::string, std::vector<std::string>, std::vector<std::string>>, 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 +311,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);
@@ -316,6 +333,7 @@ namespace storm {
bool isFreshLabelName(std::string const& moduleName);
bool isFreshObservationLabelName(std::string const& labelName);
bool isFreshRewardModelName(std::string const& moduleName);
+ bool isFreshPlayerName(std::string const& playerName);
bool isOfBoolType(storm::expressions::Expression const& expression);
bool isOfIntType(storm::expressions::Expression const& expression);
bool isOfNumericalType(storm::expressions::Expression const& expression);
@@ -323,7 +341,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;
@@ -355,12 +373,13 @@ namespace storm {
storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::ModuleRenaming createModuleRenaming(std::map<std::string,std::string> const& renaming) const;
storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& renaming, GlobalProgramInformation& globalProgramInformation) const;
+ storm::prism::Player createPlayer(std::string const& playerName, std::vector<std::string> const& moduleNames, std::vector<std::string> const & commandNames);
storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
void createObservablesList(std::vector<std::string> const& observables);
void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const;
-
+
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
};
@@ -368,4 +387,3 @@ namespace storm {
} // namespace storm
#endif /* STORM_PARSER_PRISMPARSER_H_ */
-
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 8fedf075b..10e0c8927 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -49,26 +49,26 @@ namespace storm {
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::BuildSettings>().getExplorationOrder()) {
// Intentionally left empty.
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::ExplicitModelBuilder(std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> const& generator, Options const& options) : generator(generator), options(options), stateStorage(generator->getStateSize()) {
// Intentionally left empty.
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, StateType>>(program, generatorOptions), builderOptions) {
// Intentionally left empty.
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, StateType>>(model, generatorOptions), builderOptions) {
// Intentionally left empty.
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitModelBuilder<ValueType, RewardModelType, StateType>::build() {
STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder);
-
+
switch (generator->getModelType()) {
case storm::generator::ModelType::DTMC:
return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Dtmc, buildModelComponents());
@@ -80,22 +80,24 @@ namespace storm {
return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Pomdp, buildModelComponents());
case storm::generator::ModelType::MA:
return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents());
+ case storm::generator::ModelType::SMG:
+ return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Smg, buildModelComponents());
default:
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type.");
}
-
+
return nullptr;
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
StateType ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
StateType newIndex = static_cast<StateType>(stateStorage.getNumberOfStates());
-
+
// Check, if the state was already registered.
std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
-
+
StateType actualIndex = actualIndexBucketPair.first;
-
+
if (actualIndex == newIndex) {
if (options.explorationOrder == ExplorationOrder::Dfs) {
statesToExplore.emplace_front(state, actualIndex);
@@ -108,7 +110,7 @@ namespace storm {
STORM_LOG_ASSERT(false, "Invalid exploration order.");
}
}
-
+
return actualIndex;
}
@@ -118,24 +120,30 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename StateType>
- void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
-
+ void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<std::vector<uint_fast32_t>> playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
+
// Create markovian states bit vector, if required.
if (generator->getModelType() == storm::generator::ModelType::MA) {
// The bit vector will be resized when the correct size is known.
markovianStates = storm::storage::BitVector(1000);
}
+ // Create the player indices vector, if required.
+ if (generator->getModelType() == storm::generator::ModelType::SMG) {
+ playerActionIndices = std::vector<uint_fast32_t>{};
+ playerActionIndices.get().reserve(1000);
+ }
+
// Create a callback for the next-state generator to enable it to request the index of states.
std::function<StateType (CompressedState const&)> stateToIdCallback = std::bind(&ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex, this, std::placeholders::_1);
-
+
// If the exploration order is something different from breadth-first, we need to keep track of the remapping
// from state ids to row groups. For this, we actually store the reversed mapping of row groups to state-ids
// and later reverse it.
if (options.explorationOrder != ExplorationOrder::Bfs) {
stateRemapping = std::vector<uint_fast64_t>();
}
-
+
// Let the generator create all initial states.
this->stateStorage.initialStateIndices = generator->getInitialStates(stateToIdCallback);
STORM_LOG_THROW(!this->stateStorage.initialStateIndices.empty(), storm::exceptions::WrongFormatException, "The model does not have a single initial state.");
@@ -148,30 +156,30 @@ namespace storm {
auto timeOfLastMessage = std::chrono::high_resolution_clock::now();
uint64_t numberOfExploredStates = 0;
uint64_t numberOfExploredStatesSinceLastMessage = 0;
-
+
// Perform a search through the model.
while (!statesToExplore.empty()) {
// Get the first state in the queue.
CompressedState currentState = statesToExplore.front().first;
StateType currentIndex = statesToExplore.front().second;
statesToExplore.pop_front();
-
+
// If the exploration order differs from breadth-first, we remember that this row group was actually
// filled with the transitions of a different state.
if (options.explorationOrder != ExplorationOrder::Bfs) {
stateRemapping.get()[currentIndex] = currentRowGroup;
}
-
+
if (currentIndex % 100000 == 0) {
STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
}
-
+
generator->load(currentState);
if (stateValuationsBuilder) {
generator->addStateValuation(currentIndex, stateValuationsBuilder.get());
}
storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
-
+
// If there is no behavior, we might have to introduce a self-loop.
if (behavior.empty()) {
if (!storm::settings::getModule<storm::settings::modules::BuildSettings>().isDontFixDeadlocksSet() || !behavior.wasExpanded()) {
@@ -179,28 +187,33 @@ namespace storm {
if (behavior.wasExpanded()) {
this->stateStorage.deadlockStateIndices.push_back(currentIndex);
}
-
+
if (markovianStates) {
markovianStates.get().grow(currentRowGroup + 1, false);
markovianStates.get().set(currentRowGroup);
}
-
+
if (!generator->isDeterministicModel()) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
-
+
transitionMatrixBuilder.addNextValue(currentRow, currentIndex, storm::utility::one<ValueType>());
-
+
for (auto& rewardModelBuilder : rewardModelBuilders) {
if (rewardModelBuilder.hasStateRewards()) {
rewardModelBuilder.addStateReward(storm::utility::zero<ValueType>());
}
-
+
if (rewardModelBuilder.hasStateActionRewards()) {
rewardModelBuilder.addStateActionReward(storm::utility::zero<ValueType>());
}
}
-
+
+ if (playerActionIndices) {
+ // TODO change this to storm::utility::infinity<ValueType>() ?
+ playerActionIndices.get().push_back(-1);
+ }
+
++currentRow;
++currentRowGroup;
} else {
@@ -215,15 +228,15 @@ namespace storm {
}
++stateRewardIt;
}
-
+
// If the model is nondeterministic, we need to open a row group.
if (!generator->isDeterministicModel()) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
-
+
// Now add all choices.
for (auto const& choice : behavior) {
-
+
// add the generated choice information
if (choice.hasLabels()) {
for (auto const& label : choice.getLabels()) {
@@ -233,18 +246,18 @@ namespace storm {
if (choice.hasOriginData()) {
choiceInformationBuilder.addOriginData(choice.getOriginData(), currentRow);
}
-
+
// If we keep track of the Markovian choices, store whether the current one is Markovian.
if (markovianStates && choice.isMarkovian()) {
markovianStates.get().grow(currentRowGroup + 1, false);
markovianStates.get().set(currentRowGroup);
}
-
+
// Add the probabilistic behavior to the matrix.
for (auto const& stateProbabilityPair : choice) {
transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
}
-
+
// Add the rewards to the reward models.
auto choiceRewardIt = choice.getRewards().begin();
for (auto& rewardModelBuilder : rewardModelBuilders) {
@@ -255,6 +268,10 @@ namespace storm {
}
++currentRow;
}
+
+ if (playerActionIndices) {
+ playerActionIndices.get().push_back(behavior.getChoices().at(0).getPlayerIndex());
+ }
++currentRowGroup;
}
@@ -280,24 +297,28 @@ namespace storm {
break;
}
}
-
+
if (markovianStates) {
// Since we now know the correct size, cut the bit vector to the correct length.
markovianStates->resize(currentRowGroup, false);
}
+ if (playerActionIndices) {
+ playerActionIndices.get().shrink_to_fit();
+ }
+
// If the exploration order was not breadth-first, we need to fix the entries in the matrix according to
// (reversed) mapping of row groups to indices.
if (options.explorationOrder != ExplorationOrder::Bfs) {
STORM_LOG_ASSERT(stateRemapping, "Unable to fix columns without mapping.");
std::vector<uint_fast64_t> const& remapping = stateRemapping.get();
-
+
// We need to fix the following entities:
// (a) the transition matrix
// (b) the initial states
// (c) the hash map storing the mapping states -> ids
// (d) fix remapping for state-generation labels
-
+
// Fix (a).
transitionMatrixBuilder.replaceColumns(remapping, 0);
@@ -306,21 +327,21 @@ namespace storm {
std::transform(this->stateStorage.initialStateIndices.begin(), this->stateStorage.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } );
std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end());
this->stateStorage.initialStateIndices = std::move(newInitialStateIndices);
-
+
// Fix (c).
this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } );
this->generator->remapStateIds([&remapping] (StateType const& state) { return remapping[state]; });
}
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildModelComponents() {
-
+
// Determine whether we have to combine different choices to one or whether this model can have more than
// one choice per state.
bool deterministicModel = generator->isDeterministicModel();
-
+
// Prepare the component builders
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
std::vector<RewardModelBuilder<typename RewardModelType::ValueType>> rewardModelBuilders;
@@ -329,25 +350,26 @@ namespace storm {
}
ChoiceInformationBuilder choiceInformationBuilder;
boost::optional<storm::storage::BitVector> markovianStates;
-
+ boost::optional<std::vector<uint_fast32_t>> playerActionIndices;
+
// If we need to build state valuations, initialize them now.
boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder;
if (generator->getOptions().isBuildStateValuationsSet()) {
stateValuationsBuilder = generator->initializeStateValuationsBuilder();
}
-
- buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder);
-
+
+ buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, playerActionIndices, stateValuationsBuilder);
+
// Initialize the model components with the obtained information.
- storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
-
+ storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates), /* player1Matrix = */ boost::none, std::move(playerActionIndices));
+
// Now finalize all reward models.
for (auto& rewardModelBuilder : rewardModelBuilders) {
modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));
}
// Build the choice labeling
modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
-
+
// If requested, build the state valuations and choice origins
if (stateValuationsBuilder) {
modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount());
@@ -372,12 +394,12 @@ namespace storm {
}
return modelComponents;
}
-
+
template <typename ValueType, typename RewardModelType, typename StateType>
storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
}
-
+
// Explicitly instantiate the class.
template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
template class ExplicitStateLookup<uint32_t>;
diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h
index 132345075..af068b3fa 100644
--- a/src/storm/builder/ExplicitModelBuilder.h
+++ b/src/storm/builder/ExplicitModelBuilder.h
@@ -131,40 +131,40 @@ namespace storm {
* @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
* @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states
*/
- void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
-
+ void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<std::vector<uint_fast32_t>> playerActionIndices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
+
/*!
* Explores the state space of the given program and returns the components of the model as a result.
*
* @return A structure containing the components of the resulting model.
*/
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents();
-
+
/*!
* Builds the state labeling for the given program.
*
* @return The state labeling of the given program.
*/
storm::models::sparse::StateLabeling buildStateLabeling();
-
+
/// The generator to use for the building process.
std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> generator;
-
+
/// The options to be used for the building process.
Options options;
/// Internal information about the states that were explored.
storm::storage::sparse::StateStorage<StateType> stateStorage;
-
+
/// A set of states that still need to be explored.
std::deque<std::pair<CompressedState, StateType>> statesToExplore;
-
+
/// An optional mapping from state indices to the row groups in which they actually reside. This needs to be
/// built in case the exploration order is not BFS.
boost::optional<std::vector<uint_fast64_t>> stateRemapping;
};
-
+
} // namespace adapters
} // namespace storm
diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp
index 5d69c98ab..517dffd6c 100644
--- a/src/storm/generator/Choice.cpp
+++ b/src/storm/generator/Choice.cpp
@@ -81,17 +81,32 @@ namespace storm {
labels = newLabels;
}
}
-
+
template<typename ValueType, typename StateType>
bool Choice<ValueType, StateType>::hasLabels() const {
return labels.is_initialized();
}
-
+
template<typename ValueType, typename StateType>
std::set<std::string> const& Choice<ValueType, StateType>::getLabels() const {
return labels.get();
}
-
+
+ template<typename ValueType, typename StateType>
+ void Choice<ValueType, StateType>::setPlayerIndex(uint_fast32_t playerIndex) {
+ this->playerIndex = playerIndex;
+ }
+
+ template<typename ValueType, typename StateType>
+ bool Choice<ValueType, StateType>::hasPlayerIndex() const {
+ return playerIndex.is_initialized();
+ }
+
+ template<typename ValueType, typename StateType>
+ uint_fast32_t const& Choice<ValueType, StateType>::getPlayerIndex() const {
+ return playerIndex.get();
+ }
+
template<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::addOriginData(boost::any const& data) {
if (!this->originData || this->originData->empty()) {
diff --git a/src/storm/generator/Choice.h b/src/storm/generator/Choice.h
index 1dbc41760..80f8f7031 100644
--- a/src/storm/generator/Choice.h
+++ b/src/storm/generator/Choice.h
@@ -64,118 +64,140 @@ namespace storm {
*/
template<typename ValueTypePrime, typename StateTypePrime>
friend std::ostream& operator<<(std::ostream& out, Choice<ValueTypePrime, StateTypePrime> const& choice);
-
+
/*!
* Adds the given label to the labels associated with this choice.
*
* @param label The label to associate with this choice.
*/
void addLabel(std::string const& label);
-
+
/*!
* Adds the given label set to the labels associated with this choice.
*
* @param labelSet The label set to associate with this choice.
*/
void addLabels(std::set<std::string> const& labels);
-
+
/*!
* Returns whether there are labels defined for this choice
*/
bool hasLabels() const;
-
+
/*!
* Retrieves the set of labels associated with this choice.
*
* @return The set of labels associated with this choice.
*/
std::set<std::string> const& getLabels() const;
-
+
+ /*!
+ * Sets the players index
+ *
+ * @param The player index associated with this choice.
+ */
+ void setPlayerIndex(uint_fast32_t playerIndex);
+
+ /*!
+ * Returns whether there is an index for the player defined for this choice.
+ */
+ bool hasPlayerIndex() const;
+
+ /*!
+ * Retrieves the players index associated with this choice
+ *
+ * @return The player index associated with this choice.
+ */
+ uint_fast32_t const& getPlayerIndex() const;
+
/*!
* Adds the given data that specifies the origin of this choice w.r.t. the model specification
*/
void addOriginData(boost::any const& data);
-
+
/*!
* Returns whether there is origin data defined for this choice
*/
bool hasOriginData() const;
-
+
/*!
* Returns the origin data associated with this choice.
*/
boost::any const& getOriginData() const;
-
+
/*!
* Retrieves the index of the action of this choice.
*
* @return The index of the action of this choice.
*/
uint_fast64_t getActionIndex() const;
-
+
/*!
* Retrieves the total mass of this choice.
*
* @return The total mass.
*/
ValueType getTotalMass() const;
-
+
/*!
* Adds the given probability value to the given state in the underlying distribution.
*/
void addProbability(StateType const& state, ValueType const& value);
-
+
/*!
* Adds the given value to the reward associated with this choice.
*/
void addReward(ValueType const& value);
-
+
/*!
* Adds the given choices rewards to this choice.
*/
void addRewards(std::vector<ValueType>&& values);
-
+
/*!
* Retrieves the rewards for this choice under selected reward models.
*/
std::vector<ValueType> const& getRewards() const;
-
+
/*!
* Retrieves whether the choice is Markovian.
*/
bool isMarkovian() const;
-
+
/*!
* Retrieves the size of the distribution associated with this choice.
*/
std::size_t size() const;
-
+
/*!
* If the size is already known, reserves space in the underlying distribution.
*/
void reserve(std::size_t const& size);
-
+
private:
// A flag indicating whether this choice is Markovian or not.
bool markovian;
// The action index associated with this choice.
uint_fast64_t actionIndex;
-
+
// The distribution that is associated with the choice.
storm::storage::Distribution<ValueType, StateType> distribution;
-
+
// The total probability mass (or rates) of this choice.
ValueType totalMass;
-
+
// The reward values associated with this choice.
std::vector<ValueType> rewards;
-
+
// The data that stores what part of the model specification induced this choice
boost::optional<boost::any> originData;
-
+
// The labels of this choice
boost::optional<std::set<std::string>> labels;
+
+ // The playerIndex of this choice
+ boost::optional<uint_fast32_t> playerIndex = boost::none;
};
template<typename ValueType, typename StateType>
diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h
index 126d0fa5a..671158870 100644
--- a/src/storm/generator/NextStateGenerator.h
+++ b/src/storm/generator/NextStateGenerator.h
@@ -24,44 +24,45 @@
namespace storm {
namespace generator {
typedef storm::builder::BuilderOptions NextStateGeneratorOptions;
-
+
enum class ModelType {
DTMC,
CTMC,
MDP,
MA,
- POMDP
+ POMDP,
+ SMG
};
-
+
template<typename ValueType, typename StateType = uint32_t>
class NextStateGenerator {
public:
typedef std::function<StateType (CompressedState const&)> StateToIdCallback;
NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options);
-
+
/*!
* Creates a new next state generator. This version of the constructor default-constructs the variable information.
* Hence, the subclass is responsible for suitably initializing it in its constructor.
*/
NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options);
-
+
virtual ~NextStateGenerator() = default;
-
+
uint64_t getStateSize() const;
virtual ModelType getModelType() const = 0;
virtual bool isDeterministicModel() const = 0;
virtual bool isDiscreteTimeModel() const = 0;
virtual bool isPartiallyObservable() const = 0;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
-
+
/// Initializes a builder for state valuations by adding the appropriate variables.
virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const;
-
+
void load(CompressedState const& state);
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
bool satisfies(storm::expressions::Expression const& expression) const;
-
+
/// Adds the valuation for the currently loaded state to the given builder
virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const;
/// Adds the valuation for the currently loaded state
@@ -69,7 +70,7 @@ namespace storm {
virtual std::size_t getNumberOfRewardModels() const = 0;
virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
-
+
std::string stateToString(CompressedState const& state) const;
uint32_t observabilityClass(CompressedState const& state) const;
@@ -88,7 +89,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.
@@ -109,25 +110,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;
diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp
index 6bec68bed..03b4975a6 100644
--- a/src/storm/generator/PrismNextStateGenerator.cpp
+++ b/src/storm/generator/PrismNextStateGenerator.cpp
@@ -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()) {
@@ -80,6 +80,18 @@ namespace storm {
}
}
}
+
+ if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
+ for (auto const& player : program.getPlayers()) {
+ uint_fast32_t playerIndex = program.getIndexOfPlayer(player.getName());
+ for (auto const& moduleIndexPair : player.getModules()) {
+ moduleIndexToPlayerIndexMap[moduleIndexPair.second] = playerIndex;
+ }
+ for (auto const& commandIndexPair : player.getCommands()) {
+ commandIndexToPlayerIndexMap[commandIndexPair.second] = playerIndex;
+ }
+ }
+ }
}
template<typename ValueType, typename StateType>
@@ -87,7 +99,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 +130,7 @@ namespace storm {
}
#endif
}
-
+
template<typename ValueType, typename StateType>
ModelType PrismNextStateGenerator<ValueType, StateType>::getModelType() const {
switch (program.getModelType()) {
@@ -127,16 +139,17 @@ namespace storm {
case storm::prism::Program::ModelType::MDP: return ModelType::MDP;
case storm::prism::Program::ModelType::MA: return ModelType::MA;
case storm::prism::Program::ModelType::POMDP: return ModelType::POMDP;
+ case storm::prism::Program::ModelType::SMG: return ModelType::SMG;
default:
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type.");
}
}
-
+
template<typename ValueType, typename StateType>
bool PrismNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
return program.isDeterministicModel();
}
-
+
template<typename ValueType, typename StateType>
bool PrismNextStateGenerator<ValueType, StateType>::isDiscreteTimeModel() const {
return program.isDiscreteTimeModel();
@@ -146,7 +159,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 +175,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 +190,7 @@ namespace storm {
initialState.set(booleanVariable.bitOffset, false);
}
}
-
+
bool changedIntegerVariable = false;
if (changedBooleanVariable) {
initialStateIndices.emplace_back(stateToIdCallback(initialState));
@@ -191,37 +204,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 +251,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 +287,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 +299,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 +314,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 +330,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 +344,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 +368,54 @@ 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));
}
-
+
+ if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
+ uint_fast32_t statePlayerIndex = allChoices.at(0).getPlayerIndex();
+ for(auto& choice : allChoices) {
+ if (allChoices.size() == 1) break;
+ // getPlayerIndex().is_initialized()?
+ if (choice.hasPlayerIndex()) {
+ STORM_LOG_ASSERT(choice.getPlayerIndex() == statePlayerIndex, "State '" << this->stateToString(*this->state) << "' comprises choices for different players.");
+ } else {
+ STORM_LOG_WARN("State '" << this->stateToString(*this->state) << "' features a choice without player index.");
+ }
+ }
+ }
+
// 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 +424,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 +443,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 +458,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 +502,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 +533,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 +567,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 +587,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 +595,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 +608,30 @@ namespace storm {
}
choice.addReward(stateActionRewardValue);
}
-
+
+ if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
+ // Can we trust the model ordering here?
+ // I.e. is i the correct moduleIndex set in Program.cpp:805? TODO
+ choice.setPlayerIndex(moduleIndexToPlayerIndexMap[i]);
+ }
+
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 +643,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) {
@@ -645,6 +677,10 @@ namespace storm {
// Now create the actual distribution.
Choice<ValueType>& choice = choices.back();
+ if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
+ choice.setPlayerIndex(commandIndexToPlayerIndexMap[actionIndex]);
+ }
+
// Remember the choice label and origins only if we were asked to.
if (this->options.isBuildChoiceLabelsSet()) {
choice.addLabel(program.getActionName(actionIndex));
@@ -702,7 +738,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 +756,7 @@ namespace storm {
}
}
}
-
+
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels);
}
@@ -741,22 +777,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 +800,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 +808,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
diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h
index e302fd02e..dc9564dd8 100644
--- a/src/storm/generator/PrismNextStateGenerator.h
+++ b/src/storm/generator/PrismNextStateGenerator.h
@@ -111,17 +111,21 @@ namespace storm {
* A recursive helper function to generate a synchronziing distribution.
*/
void 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);
-
+
// The program used for the generation of next states.
storm::prism::Program program;
-
+
// The reward models that need to be considered.
std::vector<std::reference_wrapper<storm::prism::RewardModel const>> rewardModels;
-
+
// A flag that stores whether at least one of the selected reward models has state-action rewards.
bool hasStateActionRewards;
+
+ // A mapping from modules/commands to the programs players
+ std::map<uint_fast32_t, uint_fast32_t> moduleIndexToPlayerIndexMap;
+ std::map<uint_fast32_t, uint_fast32_t> commandIndexToPlayerIndexMap;
};
-
+
}
}
diff --git a/src/storm/models/ModelType.cpp b/src/storm/models/ModelType.cpp
index d556448bb..1e89ec163 100644
--- a/src/storm/models/ModelType.cpp
+++ b/src/storm/models/ModelType.cpp
@@ -19,6 +19,8 @@ namespace storm {
return ModelType::S2pg;
} else if (type == "POMDP") {
return ModelType::Pomdp;
+ } else if (type == "SMG") {
+ return ModelType::Smg;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type " << type << "not known.");
}
@@ -44,6 +46,9 @@ namespace storm {
case ModelType::Pomdp:
os << "POMDP";
break;
+ case ModelType::Smg:
+ os << "Smg";
+ break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unknown model type.");
}
diff --git a/src/storm/models/ModelType.h b/src/storm/models/ModelType.h
index b183a598d..d9d7b0dc8 100644
--- a/src/storm/models/ModelType.h
+++ b/src/storm/models/ModelType.h
@@ -7,11 +7,11 @@ namespace storm {
namespace models {
// All supported model types.
enum class ModelType {
- Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp
+ Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg, Pomdp, Smg
};
ModelType getModelType(std::string const& type);
-
+
std::ostream& operator<<(std::ostream& os, ModelType const& type);
}
}
diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index bf9d69d4c..b1e80ab8b 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/src/storm/models/sparse/Model.cpp
@@ -62,14 +62,17 @@ namespace storm {
STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of row groups (" << this->getTransitionMatrix().getRowGroupCount() << ") of transition matrix does not match state count (" << stateCount << ").");
STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of columns of transition matrix does not match state count.");
STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored).");
- } else {
- STORM_LOG_THROW(this->isOfType(ModelType::S2pg), storm::exceptions::IllegalArgumentException, "Invalid model type.");
+ } else if (this->isOfType(ModelType::S2pg)) {
STORM_LOG_THROW(components.player1Matrix.is_initialized(), storm::exceptions::IllegalArgumentException, "No player 1 matrix given for stochastic game.");
STORM_LOG_ASSERT(components.player1Matrix->isProbabilistic(), "Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry.");
STORM_LOG_THROW(stateCount == components.player1Matrix->getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p1 matrix does not match state count.");
STORM_LOG_THROW(this->getTransitionMatrix().getRowGroupCount() == components.player1Matrix->getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p2 matrix does not match column count of p1 matrix.");
+ } else if (this->isOfType(ModelType::Smg)) {
+ STORM_LOG_DEBUG("Smg parsed");
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Invalid model type.");
}
-
+
// Branch on continuous/discrete timing
if (this->isOfType(ModelType::Ctmc) || this->isOfType(ModelType::MarkovAutomaton)) {
STORM_LOG_THROW(components.rateTransitions || components.exitRates.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create continuous time model: no rates are given.");
diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp
new file mode 100644
index 000000000..e0419844c
--- /dev/null
+++ b/src/storm/models/sparse/Smg.cpp
@@ -0,0 +1,49 @@
+#include "storm/models/sparse/Smg.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/vector.h"
+#include "storm/adapters/RationalFunctionAdapter.h"
+
+#include "storm/models/sparse/StandardRewardModel.h"
+
+namespace storm {
+ namespace models {
+ namespace sparse {
+
+ template <typename ValueType, typename RewardModelType>
+ Smg<ValueType, RewardModelType>::Smg(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
+ std::unordered_map<std::string, RewardModelType> const& rewardModels, ModelType type)
+ : Smg<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(transitionMatrix, stateLabeling, rewardModels), type) {
+ // Intentionally left empty
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ Smg<ValueType, RewardModelType>::Smg(storm::storage::SparseMatrix<ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
+ std::unordered_map<std::string, RewardModelType>&& rewardModels, ModelType type)
+ : Smg<ValueType, RewardModelType>(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)), type) {
+ // Intentionally left empty
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ Smg<ValueType, RewardModelType>::Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components, ModelType type)
+ : NondeterministicModel<ValueType, RewardModelType>(type, components) {
+ assert(type == storm::models::ModelType::Smg);
+ // Intentionally left empty
+ }
+
+ template <typename ValueType, typename RewardModelType>
+ Smg<ValueType, RewardModelType>::Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components, ModelType type)
+ : NondeterministicModel<ValueType, RewardModelType>(type, std::move(components)) {
+ assert(type == storm::models::ModelType::Smg);
+ // Intentionally left empty
+ }
+
+ template class Smg<double>;
+ template class Smg<storm::RationalNumber>;
+
+ template class Smg<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+ template class Smg<storm::RationalFunction>;
+ } // namespace sparse
+ } // namespace models
+} // namespace storm
diff --git a/src/storm/models/sparse/Smg.h b/src/storm/models/sparse/Smg.h
new file mode 100644
index 000000000..663817418
--- /dev/null
+++ b/src/storm/models/sparse/Smg.h
@@ -0,0 +1,57 @@
+#ifndef STORM_MODELS_SPARSE_SMG_H_
+#define STORM_MODELS_SPARSE_SMG_H_
+
+#include "storm/models/sparse/NondeterministicModel.h"
+
+namespace storm {
+ namespace models {
+ namespace sparse {
+
+ /*!
+ * This class represents a stochastic multiplayer game.
+ */
+ template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
+ class Smg : public NondeterministicModel<ValueType, RewardModelType> {
+ public:
+ /*!
+ * Constructs a model from the given data.
+ *
+ * @param transitionMatrix The matrix representing the transitions in the model.
+ * @param stateLabeling The labeling of the states.
+ * @param rewardModels A mapping of reward model names to reward models.
+ */
+ Smg(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
+ storm::models::sparse::StateLabeling const& stateLabeling,
+ std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>(), ModelType type = ModelType::Smg);
+
+ /*!
+ * Constructs a model by moving the given data.
+ *
+ * @param transitionMatrix The matrix representing the transitions in the model.
+ * @param stateLabeling The labeling of the states.
+ * @param rewardModels A mapping of reward model names to reward models.
+ */
+ Smg(storm::storage::SparseMatrix<ValueType>&& transitionMatrix,
+ storm::models::sparse::StateLabeling&& stateLabeling,
+ std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), ModelType type = ModelType::Smg);
+
+ /*!
+ * Constructs a model from the given data.
+ *
+ * @param components The components for this model.
+ */
+ Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components, ModelType type = ModelType::Smg);
+ Smg(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components, ModelType type = ModelType::Smg);
+
+ Smg(Smg<ValueType, RewardModelType> const& other) = default;
+ Smg& operator=(Smg<ValueType, RewardModelType> const& other) = default;
+
+ Smg(Smg<ValueType, RewardModelType>&& other) = default;
+ Smg& operator=(Smg<ValueType, RewardModelType>&& other) = default;
+ };
+
+ } // namespace sparse
+ } // namespace models
+} // namespace storm
+
+#endif /* STORM_MODELS_SPARSE_SMG_H_ */
diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp
index 3e59f4090..abf9aa340 100644
--- a/src/storm/storage/SymbolicModelDescription.cpp
+++ b/src/storm/storage/SymbolicModelDescription.cpp
@@ -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();
@@ -65,12 +65,13 @@ namespace storm {
case storm::prism::Program::ModelType::MDP: return SymbolicModelDescription::ModelType::MDP;
case storm::prism::Program::ModelType::POMDP: return SymbolicModelDescription::ModelType::POMDP;
case storm::prism::Program::ModelType::MA: return SymbolicModelDescription::ModelType::MA;
+ case storm::prism::Program::ModelType::SMG: return SymbolicModelDescription::ModelType::SMG;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Expected other PRISM model type.");
}
}
}
-
+
storm::expressions::ExpressionManager& SymbolicModelDescription::getManager() const {
if (this->isPrismProgram()) {
return this->asPrismProgram().getManager();
@@ -78,15 +79,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 +121,7 @@ namespace storm {
}
return result;
}
-
+
SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const {
if (this->isJaniModel()) {
return *this;
@@ -131,7 +132,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 +144,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 +159,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 +167,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 +175,7 @@ namespace storm {
storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram());
}
}
-
+
bool SymbolicModelDescription::hasUndefinedConstants() const {
if (this->isPrismProgram()) {
return this->asPrismProgram().hasUndefinedConstants();
@@ -182,7 +183,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 +199,7 @@ namespace storm {
}
return result;
}
-
+
std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) {
if (model.isPrismProgram()) {
out << model.asPrismProgram();
diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h
index da07e10f8..495091755 100644
--- a/src/storm/storage/SymbolicModelDescription.h
+++ b/src/storm/storage/SymbolicModelDescription.h
@@ -7,39 +7,39 @@
namespace storm {
namespace storage {
-
+
class SymbolicModelDescription {
public:
enum class ModelType {
- DTMC, CTMC, MDP, MA, POMDP
+ DTMC, CTMC, MDP, MA, POMDP, SMG
};
-
+
SymbolicModelDescription() = default;
SymbolicModelDescription(storm::jani::Model const& model);
SymbolicModelDescription(storm::prism::Program const& program);
SymbolicModelDescription& operator=(storm::jani::Model const& model);
SymbolicModelDescription& operator=(storm::prism::Program const& program);
-
+
bool hasModel() const;
bool isJaniModel() const;
bool isPrismProgram() const;
-
+
ModelType getModelType() const;
storm::expressions::ExpressionManager& getManager() const;
void setModel(storm::jani::Model const& model);
void setModel(storm::prism::Program const& program);
-
+
storm::jani::Model const& asJaniModel() const;
storm::jani::Model& asJaniModel();
storm::prism::Program const& asPrismProgram() const;
storm::prism::Program& asPrismProgram();
-
+
std::vector<std::string> getParameterNames() const;
-
+
SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
-
+
/*!
* Ensures that this model is a JANI model by, e.g., converting prism to jani.
* If labels or reward models had to be converted during conversion, the renamings are applied to the given properties
@@ -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);
diff --git a/src/storm/storage/prism/Player.cpp b/src/storm/storage/prism/Player.cpp
new file mode 100644
index 000000000..f2e30d3ad
--- /dev/null
+++ b/src/storm/storage/prism/Player.cpp
@@ -0,0 +1,37 @@
+#include "storm/storage/prism/Player.h"
+
+namespace storm {
+ namespace prism {
+ Player::Player(std::string const& playerName, std::map<std::string, uint_fast32_t> const& controlledModules, std::map<std::string, uint_fast32_t> const& controlledCommands, std::string const& filename, uint_fast32_t lineNumber) : LocatedInformation(filename, lineNumber), playerName(playerName), controlledModules(controlledModules), controlledCommands(controlledCommands) {
+ // Nothing to do here.
+ }
+
+ std::string const& Player::getName() const {
+ return this->playerName;
+ }
+
+ std::map<std::string, uint_fast32_t> const& Player::getModules() const {
+ return this->controlledModules;
+ }
+
+ std::map<std::string, uint_fast32_t> const& Player::getCommands() const {
+ return this->controlledCommands;
+ }
+
+ std::ostream& operator<<(std::ostream& stream, Player const& player) {
+ stream << "player";
+ if (player.getName() != "") {
+ stream << " " << player.getName();
+ }
+ stream << std::endl;
+ for (auto const& module : player.getModules()) {
+ stream << "\t" << module.first << std::endl;
+ }
+ for (auto const& command : player.getCommands()) {
+ stream << "\t[" << command.first << "]" << std::endl;
+ }
+ stream << "endplayer" << std::endl;
+ return stream;
+ }
+ } // namespace prism
+} // namespace storm
diff --git a/src/storm/storage/prism/Player.h b/src/storm/storage/prism/Player.h
new file mode 100644
index 000000000..7d9437f7f
--- /dev/null
+++ b/src/storm/storage/prism/Player.h
@@ -0,0 +1,72 @@
+#ifndef STORM_STORAGE_PRISM_PLAYER_H_
+#define STORM_STORAGE_PRISM_PLAYER_H_
+
+#include <string>
+#include <vector>
+
+#include "storm/storage/prism/Module.h"
+#include "storm/storage/prism/Command.h"
+
+// needed?
+#include "storm/storage/BoostTypes.h"
+#include "storm/utility/OsDetection.h"
+
+namespace storm {
+ namespace prism {
+ class Player : public LocatedInformation {
+ public:
+ /*!
+ * Creates a player with the given name, controlled modules and actions.
+ *
+ * @param playerName The name of the player.
+ * @param controlledModules The controlled modules.
+ * @param controlledCommands The controlled actions.
+ * @param filename The filename in which the player is defined.
+ * @param lineNumber The line number in which the player is defined.
+ */
+ Player(std::string const& playerName, std::map<std::string, uint_fast32_t> const& controlledModules, std::map<std::string, uint_fast32_t> const& controlledCommands, std::string const& filename = "", uint_fast32_t lineNumber = 0);
+
+ // Create default implementations of constructors/assignment.
+ Player() = default;
+ Player(Player const& other) = default;
+ Player& operator=(Player const& other) = default;
+ Player(Player&& other) = default;
+ Player& operator=(Player&& other) = default;
+
+ /*!
+ * Retrieves the name of the player.
+ *
+ * @return The name of the player.
+ */
+ std::string const& getName() const;
+
+ /*!
+ * Retrieves all controlled Modules of the player.
+ *
+ * @return The modules controlled by the player.
+ */
+ std::map<std::string, uint_fast32_t> const& getModules() const; // TODO
+
+ /*!
+ * Retrieves all controlled Commands of the player.
+ *
+ * @return The commands controlled by the player.
+ */
+ std::map<std::string, uint_fast32_t> const& getCommands() const;
+
+ friend std::ostream& operator<<(std::ostream& stream, Player const& player);
+ private:
+ // The name of the player.
+ std::string playerName;
+
+ // The modules associated with this player.
+ std::map<std::string, uint_fast32_t> controlledModules;
+
+ // The commands associated with this player.
+ std::map<std::string, uint_fast32_t> controlledCommands;
+ };
+
+ } // namespace prism
+} // namespace storm
+
+#endif /* STORM_STORAGE_PRISM_PLAYER_H_ */
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index cdd41f7c3..3acef442e 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -32,14 +32,14 @@ namespace storm {
CompositionValidityChecker(storm::prism::Program const& program) : program(program) {
// Intentionally left empty.
}
-
+
void check(Composition const& composition) {
composition.accept(*this, boost::any());
if (appearingModules.size() != program.getNumberOfModules()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Not every module is used in the system composition.");
}
}
-
+
virtual boost::any visit(ModuleComposition const& composition, boost::any const&) override {
bool isValid = program.hasModule(composition.getModuleName());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist.");
@@ -49,10 +49,10 @@ namespace storm {
std::set<uint_fast64_t> synchronizingActionIndices = program.getModule(composition.getModuleName()).getSynchronizingActionIndices();
return synchronizingActionIndices;
}
-
+
virtual boost::any visit(RenamingComposition const& composition, boost::any const& data) override {
std::set<uint_fast64_t> subSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getSubcomposition().accept(*this, data));
-
+
std::set<uint_fast64_t> newSynchronizingActionIndices = subSynchronizingActionIndices;
for (auto const& namePair : composition.getActionRenaming()) {
if (!program.hasAction(namePair.first)) {
@@ -68,14 +68,14 @@ namespace storm {
newSynchronizingActionIndices.insert(toIndex);
}
}
-
-
+
+
return newSynchronizingActionIndices;
}
-
+
virtual boost::any visit(HidingComposition const& composition, boost::any const& data) override {
std::set<uint_fast64_t> subSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getSubcomposition().accept(*this, data));
-
+
for (auto const& action : composition.getActionsToHide()) {
if (!program.hasAction(action)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'.");
@@ -86,34 +86,34 @@ namespace storm {
subSynchronizingActionIndices.erase(it);
}
}
-
+
return subSynchronizingActionIndices;
}
-
+
virtual boost::any visit(SynchronizingParallelComposition const& composition, boost::any const& data) override {
std::set<uint_fast64_t> leftSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
std::set<uint_fast64_t> rightSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
-
+
std::set<uint_fast64_t> synchronizingActionIndices;
std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
-
+
return synchronizingActionIndices;
}
-
+
virtual boost::any visit(InterleavingParallelComposition const& composition, boost::any const& data) override {
std::set<uint_fast64_t> leftSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
std::set<uint_fast64_t> rightSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
-
+
std::set<uint_fast64_t> synchronizingActionIndices;
std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
-
+
return synchronizingActionIndices;
}
-
+
virtual boost::any visit(RestrictedParallelComposition const& composition, boost::any const& data) override {
std::set<uint_fast64_t> leftSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getLeftSubcomposition().accept(*this, data));
std::set<uint_fast64_t> rightSynchronizingActionIndices = boost::any_cast<std::set<uint_fast64_t>>(composition.getRightSubcomposition().accept(*this, data));
-
+
for (auto const& action : composition.getSynchronizingActions()) {
if (!program.hasAction(action)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'.");
@@ -125,32 +125,32 @@ namespace storm {
STORM_LOG_THROW(it != rightSynchronizingActionIndices.end(), storm::exceptions::WrongFormatException, "Cannot synchronize on action '" << action << "', because module '" << composition.getRightSubcomposition() << " does not have this action.");
}
}
-
+
std::set<uint_fast64_t> synchronizingActionIndices;
std::set_union(leftSynchronizingActionIndices.begin(), leftSynchronizingActionIndices.end(), rightSynchronizingActionIndices.begin(), rightSynchronizingActionIndices.end(), std::inserter(synchronizingActionIndices, synchronizingActionIndices.begin()));
-
+
return synchronizingActionIndices;
}
-
+
private:
storm::prism::Program const& program;
std::set<std::string> appearingModules;
};
-
- Program::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, bool finalModel)
+
+ Program::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<Player> const& players, 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, bool finalModel)
: LocatedInformation(filename, lineNumber), manager(manager),
modelType(modelType), constants(constants), constantToIndexMap(),
globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(),
globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(),
- formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(),
+ formulas(formulas), formulaToIndexMap(), players(players), modules(modules), moduleToIndexMap(),
rewardModels(rewardModels), rewardModelToIndexMap(), systemCompositionConstruct(compositionConstruct),
labels(labels), labelToIndexMap(), observationLabels(observationLabels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(),
synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap(), prismCompatibility(prismCompatibility)
{
-
+
// Start by creating the necessary mappings from the given ones.
this->createMappings();
-
+
// Set the initial construct if given.
if (initialConstruct) {
this->initialConstruct = initialConstruct.get();
@@ -161,7 +161,7 @@ namespace storm {
modules.createMissingInitialValues();
}
}
-
+
if (finalModel) {
// If the model is supposed to be a CTMC, but contains probabilistic commands, we transform them to Markovian
// commands and issue a warning.
@@ -181,15 +181,15 @@ namespace storm {
this->checkValidity(Program::ValidityCheckLevel::VALIDINPUT);
}
}
-
+
Program::ModelType Program::getModelType() const {
return modelType;
}
-
+
bool Program::isDiscreteTimeModel() const {
- return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP;
+ return modelType == ModelType::DTMC || modelType == ModelType::MDP || modelType == ModelType::POMDP || modelType == ModelType::SMG;
}
-
+
bool Program::isDeterministicModel() const {
return modelType == ModelType::DTMC || modelType == ModelType::CTMC;
}
@@ -206,7 +206,7 @@ namespace storm {
}
return res;
}
-
+
bool Program::hasUndefinedConstants() const {
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {
@@ -215,12 +215,12 @@ namespace storm {
}
return false;
}
-
+
bool Program::undefinedConstantsAreGraphPreserving() const {
if (!this->hasUndefinedConstants()) {
return true;
}
-
+
// Gather the variables of all undefined constants.
std::set<storm::expressions::Variable> undefinedConstantVariables;
for (auto const& constant : this->getConstants()) {
@@ -228,7 +228,7 @@ namespace storm {
undefinedConstantVariables.insert(constant.getExpressionVariable());
}
}
-
+
// Start by checking the defining expressions of all defined constants. If it contains a currently undefined
// constant, we need to mark the target constant as undefined as well.
for (auto const& constant : this->getConstants()) {
@@ -238,7 +238,7 @@ namespace storm {
}
}
}
-
+
// Now check initial value and range expressions of global variables.
for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
if (booleanVariable.hasInitialValue()) {
@@ -260,7 +260,7 @@ namespace storm {
return false;
}
}
-
+
// Proceed by checking each of the modules.
for (auto const& module : this->getModules()) {
@@ -268,29 +268,29 @@ namespace storm {
return false;
}
}
-
+
// Check the reward models.
for (auto const& rewardModel : this->getRewardModels()) {
rewardModel.containsVariablesOnlyInRewardValueExpressions(undefinedConstantVariables);
}
-
+
// Initial construct.
if (this->hasInitialConstruct()) {
if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
-
+
// Labels.
for (auto const& label : this->getLabels()) {
if (label.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
-
+
return true;
}
-
+
std::vector<std::reference_wrapper<storm::prism::Constant const>> Program::getUndefinedConstants() const {
std::vector<std::reference_wrapper<storm::prism::Constant const>> result;
for (auto const& constant : this->getConstants()) {
@@ -300,7 +300,7 @@ namespace storm {
}
return result;
}
-
+
std::string Program::getUndefinedConstantsAsString() const {
std::stringstream stream;
bool printComma = false;
@@ -315,28 +315,28 @@ namespace storm {
stream << ".";
return stream.str();
}
-
+
bool Program::hasConstant(std::string const& constantName) const {
return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end();
}
-
+
Constant const& Program::getConstant(std::string const& constantName) const {
auto const& constantIndexPair = this->constantToIndexMap.find(constantName);
return this->getConstants()[constantIndexPair->second];
}
-
+
std::vector<Constant> const& Program::getConstants() const {
return this->constants;
}
-
+
std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsSubstitution() const {
return getConstantsFormulasSubstitution(true, false);
}
-
+
std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getFormulasSubstitution() const {
return getConstantsFormulasSubstitution(false, true);
}
-
+
std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsFormulasSubstitution(bool getConstantsSubstitution, bool getFormulasSubstitution) const {
std::map<storm::expressions::Variable, storm::expressions::Expression> result;
if (getConstantsSubstitution) {
@@ -353,7 +353,7 @@ namespace storm {
}
return result;
}
-
+
std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getSubstitutionForRenamedModule(Module const& renamedModule, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
auto renaming = getFinalRenamingOfModule(renamedModule);
std::map<storm::expressions::Variable, storm::expressions::Expression> renamingAsSubstitution;
@@ -363,7 +363,7 @@ namespace storm {
renamingAsSubstitution.emplace(getManager().getVariable(renamingPair.first), getManager().getVariableExpression(renamingPair.second));
}
}
-
+
std::map<storm::expressions::Variable, storm::expressions::Expression> newSubstitution;
for (auto const& substVarExpr : substitution) {
newSubstitution.emplace(substVarExpr.first, storm::jani::substituteJaniExpression(substVarExpr.second, renamingAsSubstitution));
@@ -376,7 +376,7 @@ namespace storm {
while (moduleStack.back()->isRenamedFromModule()) {
moduleStack.push_back(&getModule(moduleStack.back()->getBaseModule()));
}
-
+
assert(!moduleStack.back()->isRenamedFromModule());
moduleStack.pop_back();
assert(moduleStack.empty() || moduleStack.back()->isRenamedFromModule());
@@ -399,23 +399,23 @@ namespace storm {
return currentRenaming;
}
-
-
+
+
std::size_t Program::getNumberOfConstants() const {
return this->getConstants().size();
}
-
+
std::vector<BooleanVariable> const& Program::getGlobalBooleanVariables() const {
return this->globalBooleanVariables;
}
-
+
std::vector<IntegerVariable> const& Program::getGlobalIntegerVariables() const {
return this->globalIntegerVariables;
}
std::set<storm::expressions::Variable> Program::getAllExpressionVariables() const {
std::set<storm::expressions::Variable> result;
-
+
for (auto const& constant : constants) {
result.insert(constant.getExpressionVariable());
}
@@ -429,28 +429,28 @@ namespace storm {
auto const& moduleVariables = module.getAllExpressionVariables();
result.insert(moduleVariables.begin(), moduleVariables.end());
}
-
+
return result;
}
-
+
std::vector<storm::expressions::Expression> Program::getAllRangeExpressions() const {
std::vector<storm::expressions::Expression> result;
for (auto const& globalIntegerVariable : this->globalIntegerVariables) {
result.push_back(globalIntegerVariable.getRangeExpression());
}
-
+
for (auto const& module : modules) {
std::vector<storm::expressions::Expression> moduleRangeExpressions = module.getAllRangeExpressions();
result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end());
}
-
+
return result;
}
-
+
bool Program::globalBooleanVariableExists(std::string const& variableName) const {
return this->globalBooleanVariableToIndexMap.count(variableName) > 0;
}
-
+
bool Program::globalIntegerVariableExists(std::string const& variableName) const {
return this->globalIntegerVariableToIndexMap.count(variableName) > 0;
}
@@ -460,51 +460,63 @@ namespace storm {
STORM_LOG_THROW(nameIndexPair != this->globalBooleanVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown boolean variable '" << variableName << "'.");
return this->getGlobalBooleanVariables()[nameIndexPair->second];
}
-
+
IntegerVariable const& Program::getGlobalIntegerVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->globalIntegerVariableToIndexMap.find(variableName);
STORM_LOG_THROW(nameIndexPair != this->globalIntegerVariableToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown integer variable '" << variableName << "'.");
return this->getGlobalIntegerVariables()[nameIndexPair->second];
}
-
+
std::size_t Program::getNumberOfGlobalBooleanVariables() const {
return this->getGlobalBooleanVariables().size();
}
-
+
std::size_t Program::getNumberOfGlobalIntegerVariables() const {
return this->getGlobalIntegerVariables().size();
}
-
+
std::vector<Formula> const& Program::getFormulas() const {
return this->formulas;
}
-
+
+ std::vector<Player> const& Program::getPlayers() const {
+ return this->players;
+ }
+
std::size_t Program::getNumberOfFormulas() const {
return this->getFormulas().size();
}
-
+
std::size_t Program::getNumberOfModules() const {
return this->getModules().size();
}
-
+
+ std::size_t Program::getNumberOfPlayers() const {
+ return this->getPlayers().size();
+ }
+
storm::prism::Module const& Program::getModule(uint_fast64_t index) const {
return this->modules[index];
}
-
+
bool Program::hasModule(std::string const& moduleName) const {
return this->moduleToIndexMap.find(moduleName) != this->moduleToIndexMap.end();
}
-
+
Module const& Program::getModule(std::string const& moduleName) const {
auto const& nameIndexPair = this->moduleToIndexMap.find(moduleName);
STORM_LOG_THROW(nameIndexPair != this->moduleToIndexMap.end(), storm::exceptions::OutOfRangeException, "Unknown module '" << moduleName << "'.");
return this->getModules()[nameIndexPair->second];
}
-
+
std::vector<storm::prism::Module> const& Program::getModules() const {
return this->modules;
}
-
+
+ uint_fast32_t const& Program::getIndexOfPlayer(std::string playerName) const {
+ return this->playerToIndexMap.at(playerName);
+ }
+
std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
return actionToIndexMap;
}
@@ -520,15 +532,15 @@ namespace storm {
bool Program::hasInitialConstruct() const {
return static_cast<bool>(initialConstruct);
}
-
+
storm::prism::InitialConstruct const& Program::getInitialConstruct() const {
return this->initialConstruct.get();
}
-
+
boost::optional<InitialConstruct> const& Program::getOptionalInitialConstruct() const {
return this->initialConstruct;
}
-
+
storm::expressions::Expression Program::getInitialStatesExpression() const {
// If there is an initial construct, return its expression. If not, we construct the expression from the
// initial values of the variables (which have to exist).
@@ -536,7 +548,7 @@ namespace storm {
return this->getInitialConstruct().getInitialStatesExpression();
} else {
storm::expressions::Expression result;
-
+
for (auto const& variable : this->getGlobalBooleanVariables()) {
if (result.isInitialized()) {
result = result && storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
@@ -567,86 +579,86 @@ namespace storm {
}
}
}
-
+
// If there are no variables, there is no restriction on the initial states.
if (!result.isInitialized()) {
result = manager->boolean(true);
}
-
+
return result;
}
}
-
+
bool Program::specifiesSystemComposition() const {
return static_cast<bool>(systemCompositionConstruct);
}
-
+
SystemCompositionConstruct const& Program::getSystemCompositionConstruct() const {
return systemCompositionConstruct.get();
}
-
+
boost::optional<SystemCompositionConstruct> Program::getOptionalSystemCompositionConstruct() const {
return systemCompositionConstruct;
}
-
+
std::shared_ptr<Composition> Program::getDefaultSystemComposition() const {
std::shared_ptr<Composition> current = std::make_shared<ModuleComposition>(this->modules.front().getName());
-
+
for (uint_fast64_t index = 1; index < this->modules.size(); ++index) {
std::shared_ptr<Composition> newComposition = std::make_shared<SynchronizingParallelComposition>(current, std::make_shared<ModuleComposition>(this->modules[index].getName()));
current = newComposition;
}
-
-
+
+
return current;
}
-
+
std::set<std::string> const& Program::getActions() const {
return this->actions;
}
-
+
std::set<uint_fast64_t> const& Program::getSynchronizingActionIndices() const {
return this->synchronizingActionIndices;
}
-
+
std::string const& Program::getActionName(uint_fast64_t actionIndex) const {
auto const& indexNamePair = this->indexToActionMap.find(actionIndex);
STORM_LOG_THROW(indexNamePair != this->indexToActionMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action index " << actionIndex << ".");
return indexNamePair->second;
}
-
+
uint_fast64_t Program::getActionIndex(std::string const& actionName) const {
auto const& nameIndexPair = this->actionToIndexMap.find(actionName);
STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action name '" << actionName << "'.");
return nameIndexPair->second;
}
-
+
bool Program::hasAction(std::string const& actionName) const {
return this->actionToIndexMap.find(actionName) != this->actionToIndexMap.end();
}
-
+
bool Program::hasAction(uint_fast64_t const& actionIndex) const {
return this->indexToActionMap.find(actionIndex) != this->indexToActionMap.end();
}
-
+
std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
auto const& nameIndexPair = this->actionToIndexMap.find(action);
STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
return this->getModuleIndicesByActionIndex(nameIndexPair->second);
}
-
+
std::set<uint_fast64_t> const& Program::getModuleIndicesByActionIndex(uint_fast64_t actionIndex) const {
auto const& actionModuleSetPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
STORM_LOG_THROW(actionModuleSetPair != this->actionIndicesToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << actionIndex << "' does not exist.");
return actionModuleSetPair->second;
}
-
+
uint_fast64_t Program::getModuleIndexByVariable(std::string const& variableName) const {
auto const& variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName);
STORM_LOG_THROW(variableNameToModuleIndexPair != this->variableToModuleIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' does not exist.");
return variableNameToModuleIndexPair->second;
}
-
+
std::pair<uint_fast64_t, uint_fast64_t> Program::getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const {
uint_fast64_t moduleIndex = 0;
for (auto const& module : modules) {
@@ -663,44 +675,44 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::OutOfRangeException, "Global command index '" << globalCommandIndex << "' does not exist.");
return std::pair<uint_fast64_t, uint_fast64_t>(0, 0);
}
-
+
bool Program::hasRewardModel() const {
return !this->rewardModels.empty();
}
-
+
bool Program::hasRewardModel(std::string const& name) const {
auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
return nameIndexPair != this->rewardModelToIndexMap.end();
}
-
+
std::vector<storm::prism::RewardModel> const& Program::getRewardModels() const {
return this->rewardModels;
}
-
+
std::size_t Program::getNumberOfRewardModels() const {
return this->getRewardModels().size();
}
-
+
storm::prism::RewardModel const& Program::getRewardModel(std::string const& name) const {
auto const& nameIndexPair = this->rewardModelToIndexMap.find(name);
STORM_LOG_THROW(nameIndexPair != this->rewardModelToIndexMap.end(), storm::exceptions::OutOfRangeException, "Reward model '" << name << "' does not exist.");
return this->getRewardModels()[nameIndexPair->second];
}
-
+
RewardModel const& Program::getRewardModel(uint_fast64_t index) const {
STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist.");
return this->rewardModels[index];
}
-
+
bool Program::hasLabel(std::string const& labelName) const {
auto it = std::find_if(labels.begin(), labels.end(), [&labelName] (storm::prism::Label const& label) { return label.getName() == labelName; } );
return it != labels.end();
}
-
+
std::vector<Label> const& Program::getLabels() const {
return this->labels;
}
-
+
std::vector<storm::expressions::Expression> Program::getAllGuards(bool negated) const {
std::vector<storm::expressions::Expression> allGuards;
for (auto const& module : modules) {
@@ -710,13 +722,13 @@ namespace storm {
}
return allGuards;
}
-
+
storm::expressions::Expression const& Program::getLabelExpression(std::string const& label) const {
auto const& labelIndexPair = labelToIndexMap.find(label);
STORM_LOG_THROW(labelIndexPair != labelToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve expression for unknown label '" << label << "'.");
return this->labels[labelIndexPair->second].getStatePredicateExpression();
}
-
+
std::map<std::string, storm::expressions::Expression> Program::getLabelToExpressionMapping() const {
std::map<std::string, storm::expressions::Expression> result;
for (auto const& label : labels) {
@@ -724,17 +736,17 @@ namespace storm {
}
return result;
}
-
+
std::size_t Program::getNumberOfLabels() const {
return this->getLabels().size();
}
-
+
void Program::addLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression) {
auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name] (storm::prism::Label const& label) { return label.getName() == name; });
STORM_LOG_THROW(it == this->labels.end(), storm::exceptions::InvalidArgumentException, "Cannot add a label '" << name << "', because a label with that name already exists.");
this->labels.emplace_back(name, statePredicateExpression);
}
-
+
void Program::removeLabel(std::string const& name) {
auto it = std::find_if(this->labels.begin(), this->labels.end(), [&name] (storm::prism::Label const& label) { return label.getName() == name; });
STORM_LOG_THROW(it != this->labels.end(), storm::exceptions::InvalidArgumentException, "Canno remove unknown label '" << name << "'.");
@@ -745,11 +757,11 @@ namespace storm {
this->rewardModels.clear();
this->rewardModelToIndexMap.clear();
}
-
+
void Program::filterLabels(std::set<std::string> const& labelSet) {
std::vector<storm::prism::Label> newLabels;
newLabels.reserve(labelSet.size());
-
+
// Now filter the labels by the criterion whether or not their name appears in the given label set.
for (auto it = labels.begin(), ite = labels.end(); it != ite; ++it) {
auto setIt = labelSet.find(it->getName());
@@ -757,7 +769,7 @@ namespace storm {
newLabels.emplace_back(*it);
}
}
-
+
// Move the new labels in place.
this->labels = std::move(newLabels);
}
@@ -769,18 +781,18 @@ namespace storm {
std::size_t Program::getNumberOfObservationLabels() const {
return this->observationLabels.size();
}
-
+
Program Program::restrictCommands(storm::storage::FlatSet<uint_fast64_t> const& indexSet) const {
std::vector<storm::prism::Module> newModules;
newModules.reserve(this->getNumberOfModules());
-
+
for (auto const& module : this->getModules()) {
newModules.push_back(module.restrictCommands(indexSet));
}
-
- return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+
+ return Program(this->manager, this->getModelType(), this->getConstants(), this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
-
+
void Program::createMappings() {
// Build the mappings for constants, global variables, formulas, modules, reward models and labels.
for (uint_fast64_t constantIndex = 0; constantIndex < this->getNumberOfConstants(); ++constantIndex) {
@@ -801,24 +813,27 @@ namespace storm {
for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
}
+ for (uint_fast64_t playerIndex = 0; playerIndex < this->getNumberOfPlayers(); ++playerIndex) {
+ this->playerToIndexMap[this->getPlayers()[playerIndex].getName()] = playerIndex;
+ }
for (uint_fast64_t rewardModelIndex = 0; rewardModelIndex < this->getNumberOfRewardModels(); ++rewardModelIndex) {
this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
}
-
+
for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
this->actions.insert(actionIndexPair.first);
this->indexToActionMap.emplace(actionIndexPair.second, actionIndexPair.first);
-
+
// Only let all non-zero indices be synchronizing.
if (actionIndexPair.second != 0) {
this->synchronizingActionIndices.insert(actionIndexPair.second);
}
}
-
+
// Build the mapping from action names to module indices so that the lookup can later be performed quickly.
for (unsigned int moduleIndex = 0; moduleIndex < this->getNumberOfModules(); moduleIndex++) {
Module const& module = this->getModule(moduleIndex);
-
+
for (auto const& actionIndex : module.getSynchronizingActionIndices()) {
auto const& actionModuleIndicesPair = this->actionIndicesToModuleIndexMap.find(actionIndex);
if (actionModuleIndicesPair == this->actionIndicesToModuleIndexMap.end()) {
@@ -826,7 +841,7 @@ namespace storm {
}
this->actionIndicesToModuleIndexMap[actionIndex].insert(moduleIndex);
}
-
+
// Put in the appropriate entries for the mapping from variable names to module index.
for (auto const& booleanVariable : module.getBooleanVariables()) {
this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
@@ -838,13 +853,13 @@ namespace storm {
this->variableToModuleIndexMap[clockVariable.getName()] = moduleIndex;
}
}
-
+
}
-
+
Program Program::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
// For sanity checking, we keep track of all undefined constants that we define in the course of this procedure.
std::set<storm::expressions::Variable> definedUndefinedConstants;
-
+
std::vector<Constant> newConstants;
newConstants.reserve(this->getNumberOfConstants());
for (auto const& constant : this->getConstants()) {
@@ -853,72 +868,72 @@ namespace storm {
if (constant.isDefined()) {
// Make sure we are not trying to define an already defined constant.
STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
-
+
// Now replace the occurrences of undefined constants in its defining expression.
newConstants.emplace_back(constant.getExpressionVariable(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
} else {
auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
-
+
// If the constant is not defined by the mapping, we leave it like it is.
if (variableExpressionPair == constantDefinitions.end()) {
newConstants.emplace_back(constant);
} else {
// Otherwise, we add it to the defined constants and assign it the appropriate expression.
definedUndefinedConstants.insert(constant.getExpressionVariable());
-
+
// Make sure the type of the constant is correct.
STORM_LOG_THROW(variableExpressionPair->second.getType() == constant.getType(), storm::exceptions::InvalidArgumentException, "Illegal type of expression defining constant '" << constant.getName() << "'.");
-
+
// Now create the defined constant.
newConstants.emplace_back(constant.getExpressionVariable(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
}
}
}
-
- return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+
+ return Program(this->manager, this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getPlayers(), this->getModules(), this->getActionNameToIndexMapping(), this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
-
+
Program Program::substituteConstants() const {
return substituteConstantsFormulas(true, false);
}
-
+
Program Program::substituteFormulas() const {
return substituteConstantsFormulas(false, true);
}
-
+
Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const {
// Formulas need to be substituted first. otherwise, constants appearing in formula expressions can not be handled properly
if (substituteConstants && substituteFormulas) {
return this->substituteFormulas().substituteConstants();
}
-
+
// We start by creating the appropriate substitution.
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = getConstantsFormulasSubstitution(substituteConstants, substituteFormulas);
-
+
std::vector<Constant> newConstants;
newConstants.reserve(this->getNumberOfConstants());
for (auto const& oldConstant : this->getConstants()) {
newConstants.push_back(oldConstant.substitute(substitution));
}
-
+
std::vector<Formula> newFormulas;
newFormulas.reserve(this->getNumberOfFormulas());
for (auto const& oldFormula : this->getFormulas()) {
newFormulas.emplace_back(oldFormula.substitute(substitution));
}
-
+
std::vector<BooleanVariable> newBooleanVariables;
newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
newBooleanVariables.emplace_back(booleanVariable.substitute(substitution));
}
-
+
std::vector<IntegerVariable> newIntegerVariables;
newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
newIntegerVariables.emplace_back(integerVariable.substitute(substitution));
}
-
+
std::vector<Module> newModules;
newModules.reserve(this->getNumberOfModules());
for (auto const& module : this->getModules()) {
@@ -930,18 +945,18 @@ namespace storm {
newModules.emplace_back(module.substitute(substitution));
}
}
-
+
std::vector<RewardModel> newRewardModels;
newRewardModels.reserve(this->getNumberOfRewardModels());
for (auto const& rewardModel : this->getRewardModels()) {
newRewardModels.emplace_back(rewardModel.substitute(substitution));
}
-
+
boost::optional<storm::prism::InitialConstruct> newInitialConstruct;
if (this->hasInitialConstruct()) {
newInitialConstruct = this->getInitialConstruct().substitute(substitution);
}
-
+
std::vector<Label> newLabels;
newLabels.reserve(this->getNumberOfLabels());
for (auto const& label : this->getLabels()) {
@@ -953,12 +968,12 @@ namespace storm {
for (auto const& label : this->getObservationLabels()) {
newObservationLabels.emplace_back(label.substitute(substitution));
}
-
- return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+
+ return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, this->getPlayers(), newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newObservationLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
-
+
void Program::checkValidity(Program::ValidityCheckLevel lvl) const {
-
+
// Start by checking the constant declarations.
std::set<storm::expressions::Variable> all;
std::set<storm::expressions::Variable> allGlobals;
@@ -971,7 +986,7 @@ namespace storm {
std::set<storm::expressions::Variable> illegalVariables;
std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
bool isValid = illegalVariables.empty();
-
+
if (!isValid) {
std::vector<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
@@ -980,25 +995,25 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
}
-
+
// Record the new identifier for future checks.
constants.insert(constant.getExpressionVariable());
all.insert(constant.getExpressionVariable());
allGlobals.insert(constant.getExpressionVariable());
}
-
+
// Now we check the variable declarations. We start with the global variables.
std::set<storm::expressions::Variable> variables;
for (auto const& variable : this->getGlobalBooleanVariables()) {
if (variable.hasInitialValue()) {
STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present.");
-
+
// Check the initial value of the variable.
std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
std::set<storm::expressions::Variable> illegalVariables;
std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
bool isValid = illegalVariables.empty();
-
+
if (!isValid) {
std::vector<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
@@ -1007,7 +1022,7 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
}
-
+
// Record the new identifier for future checks.
variables.insert(variable.getExpressionVariable());
all.insert(variable.getExpressionVariable());
@@ -1020,7 +1035,7 @@ namespace storm {
std::set<storm::expressions::Variable> illegalVariables;
std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
bool isValid = illegalVariables.empty();
-
+
if (!isValid) {
std::vector<std::string> illegalVariableNames;
for (auto const& var : illegalVariables) {
@@ -1028,7 +1043,7 @@ namespace storm {
}
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
-
+
containedVariables = variable.getLowerBoundExpression().getVariables();
std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
isValid = illegalVariables.empty();
@@ -1039,7 +1054,7 @@ namespace storm {
}
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
-
+
if (variable.hasInitialValue()) {
STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present.");
@@ -1055,14 +1070,14 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
}
-
+
// Record the new identifier for future checks.
variables.insert(variable.getExpressionVariable());
all.insert(variable.getExpressionVariable());
allGlobals.insert(variable.getExpressionVariable());
globalVariables.insert(variable.getExpressionVariable());
}
-
+
// Now go through the variables of the modules.
for (auto const& module : this->getModules()) {
for (auto const& variable : module.getBooleanVariables()) {
@@ -1082,7 +1097,7 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
}
-
+
// Record the new identifier for future checks.
variables.insert(variable.getExpressionVariable());
all.insert(variable.getExpressionVariable());
@@ -1100,7 +1115,7 @@ namespace storm {
}
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
-
+
containedVariables = variable.getLowerBoundExpression().getVariables();
illegalVariables.clear();
std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
@@ -1112,7 +1127,7 @@ namespace storm {
}
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
-
+
if (variable.hasInitialValue()) {
STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": illegal to specify initial value if an initial construct is present.");
@@ -1129,23 +1144,23 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
}
-
+
// Record the new identifier for future checks.
variables.insert(variable.getExpressionVariable());
all.insert(variable.getExpressionVariable());
}
-
+
for (auto const& variable : module.getClockVariables()) {
// Record the new identifier for future checks.
variables.insert(variable.getExpressionVariable());
all.insert(variable.getExpressionVariable());
}
}
-
+
// Create the set of valid identifiers for future checks.
std::set<storm::expressions::Variable> variablesAndConstants;
std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
-
+
// Collect the formula placeholders and check formulas
for (auto const& formula : this->getFormulas()) {
std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
@@ -1156,7 +1171,7 @@ namespace storm {
variablesAndConstants.insert(formula.getExpressionVariable());
}
}
-
+
// Check the commands and invariants of the modules.
bool hasProbabilisticCommand = false;
bool hasMarkovianCommand = false;
@@ -1173,7 +1188,7 @@ namespace storm {
for (auto const& variable : module.getClockVariables()) {
legalVariables.insert(variable.getExpressionVariable());
}
-
+
if (module.hasInvariant()) {
std::set<storm::expressions::Variable> containedVariables = module.getInvariant().getVariables();
std::set<storm::expressions::Variable> illegalVariables;
@@ -1188,7 +1203,7 @@ namespace storm {
}
STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant() << " must evaluate to type 'bool'.");
}
-
+
for (auto& command : module.getCommands()) {
// Check the guard.
std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
@@ -1203,20 +1218,20 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": guard " << command.getGuardExpression() << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
STORM_LOG_THROW(command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": expression for guard must evaluate to type 'bool'.");
-
+
// Record which types of commands were seen.
if (command.isMarkovian()) {
hasMarkovianCommand = true;
} else {
hasProbabilisticCommand = true;
}
-
+
// If the command is Markovian and labeled, we throw an error or raise a warning, depending on
// whether or not the PRISM compatibility mode was enabled.
if (command.isMarkovian() && command.isLabeled()) {
hasLabeledMarkovianCommand = true;
}
-
+
// Check all updates.
for (auto const& update : command.getUpdates()) {
containedVariables = update.getLikelihoodExpression().getVariables();
@@ -1230,12 +1245,12 @@ namespace storm {
}
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": likelihood expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
-
+
// Check all assignments.
std::set<storm::expressions::Variable> alreadyAssignedVariables;
for (auto const& assignment : update.getAssignments()) {
storm::expressions::Variable assignedVariable = manager->getVariable(assignment.getVariableName());
-
+
if (legalVariables.find(assignedVariable) == legalVariables.end()) {
if (all.find(assignedVariable) != all.end()) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assignment illegally refers to variable '" << assignment.getVariableName() << "'.");
@@ -1245,14 +1260,14 @@ namespace storm {
}
STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() || (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'.");
-
+
if (command.isLabeled() && globalVariables.find(assignedVariable) != globalVariables.end()) {
std::pair<storm::expressions::Variable, uint64_t>variableActionIndexPair(assignedVariable, command.getActionIndex());
std::pair<uint64_t,std::string> lineModuleNamePair(command.getLineNumber(), module.getName());
auto insertionResult = writtenGlobalVariables.emplace(variableActionIndexPair, lineModuleNamePair);
STORM_LOG_THROW(insertionResult.second || insertionResult.first->second.second == module.getName(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": Syncronizing command with action label '" << command.getActionName() << "' illegally assigns a value to global variable '" << assignedVariable.getName() << "'. Previous assignment to the variable at line " << insertionResult.first->second.first << " in module '" << insertionResult.first->second.second << "'.");
}
-
+
containedVariables = assignment.getExpression().getVariables();
illegalVariables.clear();
std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
@@ -1264,14 +1279,14 @@ namespace storm {
}
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": assigned expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
}
-
+
// Add the current variable to the set of assigned variables (of this update).
alreadyAssignedVariables.insert(assignedVariable);
}
}
}
}
-
+
if (hasLabeledMarkovianCommand) {
if (prismCompatibility) {
STORM_LOG_WARN_COND(false, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
@@ -1279,13 +1294,13 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
}
}
-
+
if (this->getModelType() == Program::ModelType::DTMC || this->getModelType() == Program::ModelType::MDP) {
STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException, "Discrete-time model must not have Markovian commands.");
} else if (this->getModelType() == Program::ModelType::CTMC) {
STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn on the PRISM compatibility mode using the flag '-pc'.");
}
-
+
// Now check the reward models.
for (auto const& rewardModel : this->getRewardModels()) {
for (auto const& stateReward : rewardModel.getStateRewards()) {
@@ -1293,57 +1308,57 @@ namespace storm {
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
STORM_LOG_THROW(stateReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
-
+
containedVariables = stateReward.getRewardValueExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException, "Error in " << stateReward.getFilename() << ", line " << stateReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
}
-
+
for (auto const& stateActionReward : rewardModel.getStateActionRewards()) {
std::set<storm::expressions::Variable> containedVariables = stateActionReward.getStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
STORM_LOG_THROW(stateActionReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
-
+
containedVariables = stateActionReward.getRewardValueExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
STORM_LOG_THROW(stateActionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException, "Error in " << stateActionReward.getFilename() << ", line " << stateActionReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
}
-
+
for (auto const& transitionReward : rewardModel.getTransitionRewards()) {
std::set<storm::expressions::Variable> containedVariables = transitionReward.getSourceStatePredicateExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
STORM_LOG_THROW(transitionReward.getSourceStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
-
+
containedVariables = transitionReward.getTargetStatePredicateExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward expression refers to unknown identifiers.");
STORM_LOG_THROW(transitionReward.getTargetStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state predicate must evaluate to type 'bool'.");
-
-
+
+
containedVariables = transitionReward.getRewardValueExpression().getVariables();
isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": state reward value expression refers to unknown identifiers.");
STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException, "Error in " << transitionReward.getFilename() << ", line " << transitionReward.getLineNumber() << ": reward value expression must evaluate to numerical type.");
}
}
-
+
// Check the initial states expression.
if (this->hasInitialConstruct()) {
std::set<storm::expressions::Variable> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getInitialConstruct().getFilename() << ", line " << this->getInitialConstruct().getLineNumber() << ": initial construct refers to unknown identifiers.");
}
-
+
// Check the system composition if given.
if (systemCompositionConstruct) {
CompositionValidityChecker checker(*this);
checker.check(systemCompositionConstruct.get().getSystemComposition());
}
-
+
// Check the labels.
for (auto const& label : this->getLabels()) {
std::set<storm::expressions::Variable> containedVariables = label.getStatePredicateExpression().getVariables();
@@ -1351,7 +1366,7 @@ namespace storm {
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
}
-
+
if(lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
// We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
@@ -1385,21 +1400,21 @@ namespace storm {
}
}
}
-
+
Program Program::simplify() {
// Start by substituting the constants, because this will potentially erase some commands or even actions.
Program substitutedProgram = this->substituteConstantsFormulas();
-
+
// As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
// maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]
// commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will
// remove the forced synchronization that was there before.
std::set<uint_fast64_t> actionIndicesToDelete;
-
+
std::vector<Module> newModules;
std::vector<Constant> newConstants = substitutedProgram.getConstants();
for (auto const& module : substitutedProgram.getModules()) {
-
+
// Discard all commands with a guard equivalent to false and remove identity assignments from the updates.
std::vector<Command> newCommands;
for (auto const& command : module.getCommands()) {
@@ -1407,7 +1422,7 @@ namespace storm {
newCommands.emplace_back(command.simplify());
}
}
-
+
// Substitute variables by global constants if possible.
std::map<storm::expressions::Variable, storm::expressions::Expression> booleanVars;
std::map<storm::expressions::Variable, storm::expressions::Expression> integerVars;
@@ -1417,7 +1432,7 @@ namespace storm {
for (auto const& variable : module.getIntegerVariables()) {
integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression());
}
-
+
// Collect all variables that are being written. These variables cannot be turned to constants.
for (auto const& command : newCommands) {
// Check all updates.
@@ -1438,7 +1453,7 @@ namespace storm {
}
}
}
-
+
std::vector<storm::prism::BooleanVariable> newBooleanVars;
for (auto const& variable : module.getBooleanVariables()) {
if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) {
@@ -1451,7 +1466,7 @@ namespace storm {
newIntegerVars.push_back(variable);
}
}
-
+
for (auto const& variable : module.getBooleanVariables()) {
if (booleanVars.find(variable.getExpressionVariable()) != booleanVars.end()) {
if (variable.hasInitialValue()) {
@@ -1470,36 +1485,36 @@ namespace storm {
}
}
}
-
+
// we currently do not simplify clock variables or invariants
newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, module.getClockVariables(), module.getInvariant(), newCommands);
-
+
// Determine the set of action indices that have been deleted entirely.
std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
}
-
+
// If we have to delete whole actions, do so now.
std::map<std::string, uint_fast64_t> newActionToIndexMap;
std::vector<RewardModel> newRewardModels;
if (!actionIndicesToDelete.empty()) {
storm::storage::FlatSet<uint_fast64_t> actionsToKeep;
std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin()));
-
+
// Insert the silent action as this is not contained in the synchronizing action indices.
actionsToKeep.insert(0);
-
+
std::vector<Module> cleanedModules;
cleanedModules.reserve(newModules.size());
for (auto const& module : newModules) {
cleanedModules.emplace_back(module.restrictActionIndices(actionsToKeep));
}
newModules = std::move(cleanedModules);
-
+
newRewardModels.reserve(substitutedProgram.getNumberOfRewardModels());
for (auto const& rewardModel : substitutedProgram.getRewardModels()) {
newRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep));
}
-
+
for (auto const& entry : this->getActionNameToIndexMapping()) {
if (actionsToKeep.find(entry.second) != actionsToKeep.end()) {
newActionToIndexMap.emplace(entry.first, entry.second);
@@ -1512,22 +1527,22 @@ namespace storm {
newLabels.emplace_back(label.getName(), label.getStatePredicateExpression().simplify());
}
- return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+ return Program(this->manager, modelType, newConstants, getGlobalBooleanVariables(), getGlobalIntegerVariables(), getFormulas(), this->getPlayers(), newModules, actionIndicesToDelete.empty() ? getActionNameToIndexMapping() : newActionToIndexMap, actionIndicesToDelete.empty() ? this->getRewardModels() : newRewardModels, newLabels, getObservationLabels(), getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility);
}
-
+
Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
// If the current program has only one module, we can simply return a copy.
if (this->getNumberOfModules() == 1) {
return Program(*this);
}
-
+
STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException, "Unable to flatten modules for model of type '" << this->getModelType() << "'.");
-
+
// Otherwise, we need to actually flatten the contained modules.
-
+
// Get an SMT solver for computing the possible guard combinations.
std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*manager);
-
+
// Set up the data we need to gather to create the flat module.
std::stringstream newModuleName;
std::vector<storm::prism::BooleanVariable> allBooleanVariables;
@@ -1536,7 +1551,7 @@ namespace storm {
std::vector<storm::prism::Command> newCommands;
uint_fast64_t nextCommandIndex = 0;
uint_fast64_t nextUpdateIndex = 0;
-
+
// Assert the values of the constants.
for (auto const& constant : this->getConstants()) {
if (constant.isDefined()) {
@@ -1547,19 +1562,19 @@ namespace storm {
}
}
}
-
+
// Assert the bounds of the global variables.
for (auto const& variable : this->getGlobalIntegerVariables()) {
solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
}
-
+
// Make the global variables local, such that the resulting module covers all occurring variables. Note that
// this is just for simplicity and is not needed.
allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
storm::expressions::Expression newInvariant;
-
+
// Now go through the modules, gather the variables, construct the name of the new module and assert the
// bounds of the discovered variables.
for (auto const& module : this->getModules()) {
@@ -1567,76 +1582,76 @@ namespace storm {
allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
-
+
for (auto const& variable : module.getIntegerVariables()) {
solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
}
-
+
if (module.hasInvariant()) {
newInvariant = newInvariant.isInitialized() ? (newInvariant && module.getInvariant()) : module.getInvariant();
}
-
+
// The commands without a synchronizing action name, can simply be copied (plus adjusting the global
// indices of the command and its updates).
for (auto const& command : module.getCommands()) {
if (!command.isLabeled()) {
std::vector<storm::prism::Update> updates;
updates.reserve(command.getUpdates().size());
-
+
for (auto const& update : command.getUpdates()) {
updates.push_back(storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
++nextUpdateIndex;
}
-
+
newCommands.push_back(storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find("")->second, "", command.getGuardExpression(), updates, command.getFilename(), 0));
++nextCommandIndex;
}
}
}
-
+
// Save state of solver so that we can always restore the point where we have exactly the constant values
// and variables bounds on the assertion stack.
solver->push();
-
+
// Now we need to enumerate all possible combinations of synchronizing commands. For this, we iterate over
// all actions and let the solver enumerate the possible combinations of commands that can be enabled together.
for (auto const& actionIndex : this->getSynchronizingActionIndices()) {
bool noCombinationsForAction = false;
-
+
// Prepare the list that stores for each module the list of commands with the given action.
std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
-
+
for (auto const& module : this->getModules()) {
// If the module has no command with this action, we can skip it.
if (!module.hasActionIndex(actionIndex)) {
continue;
}
-
+
std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
-
+
// If there is no command even though the module has this action, there is no valid command
// combination with this action.
if (commandIndices.empty()) {
noCombinationsForAction = true;
break;
}
-
+
// Prepare empty list of commands for this module.
possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
-
+
// Add references to the commands labeled with the current action.
for (auto const& commandIndex : commandIndices) {
possibleCommands.back().push_back(module.getCommand(commandIndex));
}
}
-
+
// If there are no valid combinations for the action, we need to skip the generation of synchronizing
// commands.
if (!noCombinationsForAction) {
// Save the solver state to be able to restore it when this action index is done.
solver->push();
-
+
// Start by creating a fresh auxiliary variable for each command and link it with the guard.
std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
std::vector<storm::expressions::Variable> allCommandVariables;
@@ -1647,14 +1662,14 @@ namespace storm {
allCommandVariables.push_back(commandVariables[outerIndex].back());
solver->add(implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
}
-
+
storm::expressions::Expression atLeastOneCommandFromModule = manager->boolean(false);
for (auto const& commandVariable : commandVariables[outerIndex]) {
atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
}
solver->add(atLeastOneCommandFromModule);
}
-
+
// Now we are in a position to start the enumeration over all command variables. While doing so, we
// keep track of previously seen command combinations, because the AllSat procedures are not
// always guaranteed to only provide distinct models.
@@ -1662,7 +1677,7 @@ namespace storm {
solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
// Now we need to reconstruct the chosen commands from the valuation of the command variables.
std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
-
+
for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) {
@@ -1670,14 +1685,14 @@ namespace storm {
}
}
}
-
+
// Now that we have retrieved the commands, we need to build their synchronizations and add them
// to the flattened module.
std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
for (auto const& element : chosenCommands) {
iterators.push_back(element.begin());
}
-
+
bool movedAtLeastOneIterator = false;
std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
std::vector<uint_fast64_t> commandCombinationIndices(iterators.size());
@@ -1686,7 +1701,7 @@ namespace storm {
commandCombination[index] = *iterators[index];
commandCombinationIndices[index] = commandCombination[index].get().getGlobalIndex();
}
-
+
// Only add the command combination if it was not previously seen.
auto seenIt = seenCommandCombinations.find(commandCombinationIndices);
if (seenIt == seenCommandCombinations.end()) {
@@ -1697,7 +1712,7 @@ namespace storm {
++nextCommandIndex;
nextUpdateIndex += newCommands.back().getNumberOfUpdates();
}
-
+
movedAtLeastOneIterator = false;
for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
++iterators[index];
@@ -1709,18 +1724,18 @@ namespace storm {
}
}
} while (movedAtLeastOneIterator);
-
+
return true;
});
-
+
solver->pop();
}
}
-
+
// Finally, we can create the module and the program and return it.
storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands, this->getFilename(), 0);
-
- return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
+
+ return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
}
std::vector<Constant> Program::usedConstants() const {
@@ -1804,7 +1819,7 @@ namespace storm {
}
return res;
}
-
+
std::unordered_map<uint_fast64_t, std::string> Program::buildActionIndexToActionNameMap() const {
std::unordered_map<uint_fast64_t, std::string> res;
for(auto const& nameIndexPair : actionToIndexMap) {
@@ -1812,7 +1827,7 @@ namespace storm {
}
return res;
}
-
+
std::unordered_map<uint_fast64_t, uint_fast64_t> Program::buildCommandIndexToActionIndex() const {
std::unordered_map<uint_fast64_t, uint_fast64_t> res;
for(auto const& m : this->modules) {
@@ -1821,9 +1836,9 @@ namespace storm {
}
}
return res;
-
+
}
-
+
Command Program::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 {
// To construct the synchronous product of the commands, we need to store a list of its updates.
std::vector<storm::prism::Update> newUpdates;
@@ -1832,13 +1847,13 @@ namespace storm {
numberOfUpdates *= commands[i].get().getNumberOfUpdates();
}
newUpdates.reserve(numberOfUpdates);
-
+
// Initialize all update iterators.
std::vector<std::vector<storm::prism::Update>::const_iterator> updateIterators;
for (uint_fast64_t i = 0; i < commands.size(); ++i) {
updateIterators.push_back(commands[i].get().getUpdates().cbegin());
}
-
+
bool doneUpdates = false;
do {
// We create the new likelihood expression by multiplying the particapting updates' expressions.
@@ -1846,17 +1861,17 @@ namespace storm {
for (uint_fast64_t i = 1; i < updateIterators.size(); ++i) {
newLikelihoodExpression = newLikelihoodExpression * updateIterators[i]->getLikelihoodExpression();
}
-
+
// Now concatenate all assignments of all participating updates.
std::vector<storm::prism::Assignment> newAssignments;
for (uint_fast64_t i = 0; i < updateIterators.size(); ++i) {
newAssignments.insert(newAssignments.end(), updateIterators[i]->getAssignments().begin(), updateIterators[i]->getAssignments().end());
}
-
+
// Then we are ready to create the new update.
newUpdates.push_back(storm::prism::Update(firstUpdateIndex, newLikelihoodExpression, newAssignments, this->getFilename(), 0));
++firstUpdateIndex;
-
+
// Now check whether there is some update combination we have not yet explored.
bool movedIterator = false;
for (int_fast64_t j = updateIterators.size() - 1; j >= 0; --j) {
@@ -1869,18 +1884,18 @@ namespace storm {
updateIterators[j] = commands[j].get().getUpdates().cbegin();
}
}
-
+
doneUpdates = !movedIterator;
} while (!doneUpdates);
-
+
storm::expressions::Expression newGuard = commands[0].get().getGuardExpression();
for (uint_fast64_t i = 1; i < commands.size(); ++i) {
newGuard = newGuard && commands[i].get().getGuardExpression();
}
-
+
return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
}
-
+
storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
ToJaniConverter converter;
auto janiModel = converter.convert(*this, allVariablesGlobal, {}, suffix);
@@ -1903,7 +1918,7 @@ namespace storm {
if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
newProperties = converter.applyRenaming(properties);
} else {
- newProperties = properties; // Nothing to be done here. Notice that the copy operation is suboptimal.
+ newProperties = properties; // Nothing to be done here. Notice that the copy operation is suboptimal.
}
return std::make_pair(janiModel, newProperties);
}
@@ -1911,7 +1926,7 @@ namespace storm {
storm::expressions::ExpressionManager& Program::getManager() const {
return *this->manager;
}
-
+
void Program::createMissingInitialValues() {
for (auto& variable : globalBooleanVariables) {
if (!variable.hasInitialValue()) {
@@ -1924,7 +1939,7 @@ namespace storm {
}
}
}
-
+
std::ostream& operator<<(std::ostream& out, Program::ModelType const& type) {
switch (type) {
case Program::ModelType::UNDEFINED: out << "undefined"; break;
@@ -1935,17 +1950,22 @@ namespace storm {
case Program::ModelType::MA: out << "ma"; break;
case Program::ModelType::POMDP: out << "pomdp"; break;
case Program::ModelType::PTA: out << "pta"; break;
+ case Program::ModelType::SMG: out << "smg"; break;
}
return out;
}
-
+
std::ostream& operator<<(std::ostream& stream, Program const& program) {
stream << program.getModelType() << std::endl;
for (auto const& constant : program.getConstants()) {
stream << constant << std::endl;
}
stream << std::endl;
-
+
+ for (auto const& player : program.getPlayers()) {
+ stream << player << std::endl;
+ }
+
for (auto const& variable : program.getGlobalBooleanVariables()) {
stream << "global " << variable << std::endl;
}
@@ -1953,36 +1973,36 @@ namespace storm {
stream << "global " << variable << std::endl;
}
stream << std::endl;
-
+
for (auto const& formula : program.getFormulas()) {
stream << formula << std::endl;
}
stream << std::endl;
-
+
for (auto const& module : program.getModules()) {
stream << module << std::endl;
}
-
+
for (auto const& rewardModel : program.getRewardModels()) {
stream << rewardModel << std::endl;
}
-
+
for (auto const& label : program.getLabels()) {
stream << label << std::endl;
}
-
+
if (program.hasInitialConstruct()) {
stream << program.getInitialConstruct() << std::endl;
}
-
+
if (program.specifiesSystemComposition()) {
stream << program.getSystemCompositionConstruct();
}
-
+
return stream;
}
-
-
-
+
+
+
} // namespace prism
} // namepsace storm
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index 0860dd913..095f164ff 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -15,6 +15,7 @@
#include "storm/storage/prism/SystemCompositionConstruct.h"
#include "storm/storage/prism/InitialConstruct.h"
#include "storm/storage/prism/Composition.h"
+#include "storm/storage/prism/Player.h"
#include "storm/storage/BoostTypes.h"
#include "storm/utility/solver.h"
#include "storm/utility/OsDetection.h"
@@ -24,17 +25,17 @@ namespace storm {
class Model;
class Property;
}
-
+
namespace prism {
class Program : public LocatedInformation {
public:
/*!
* An enum for the different model types.
*/
- enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA};
-
+ enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA, SMG};
+
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.
@@ -57,8 +58,8 @@ namespace storm {
* @param lineNumber The line number in which the program is defined.
* @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);
-
+ 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<Player> const& players, 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 +73,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 +103,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 +128,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 +136,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 +175,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 +196,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 +224,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 +246,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 +274,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 +303,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 +311,47 @@ 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 players of the program.
+ *
+ * @return The players of the program.
+ */
+ std::vector<Player> const& getPlayers() const;
+
+ /*!
+ * Retrieves the number of players in the program.
+ *
+ * @return The number of players in the program.
+ */
+ std::size_t getNumberOfPlayers() const;
+
+ /*!
+ * Retrieves the index of the player in the program.
+ *
+ * @return The index of the player in the program.
+ */
+ uint_fast32_t const& getIndexOfPlayer(std::string playerName) 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 +372,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 +380,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 +423,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 +431,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 +445,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 +463,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 +471,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 +496,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 +504,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 +526,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 +534,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 +542,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 +557,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 +586,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 +617,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 +634,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 +642,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 +650,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 +658,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 +678,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 +698,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 +718,101 @@ 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 players associated with the program.
+ std::vector<Player> players;
+
+ // A mapping of player names to their indices.
+ std::map<std::string, uint_fast64_t> playerToIndexMap;
+
// 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
diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h
index ca325b73c..29ae3d14b 100644
--- a/src/storm/storage/sparse/ModelComponents.h
+++ b/src/storm/storage/sparse/ModelComponents.h
@@ -21,35 +21,37 @@
namespace storm {
namespace storage {
namespace sparse {
-
+
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
struct ModelComponents {
-
+
ModelComponents(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
storm::models::sparse::StateLabeling const& stateLabeling = storm::models::sparse::StateLabeling(),
std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>(),
bool rateTransitions = false,
boost::optional<storm::storage::BitVector> const& markovianStates = boost::none,
- boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none)
- : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) {
+ boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none,
+ boost::optional<std::vector<uint_fast32_t>> const& playerActionIndices = boost::none)
+ : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix), playerActionIndices(playerActionIndices) {
// Intentionally left empty
}
-
+
ModelComponents(storm::storage::SparseMatrix<ValueType>&& transitionMatrix = storm::storage::SparseMatrix<ValueType>(),
storm::models::sparse::StateLabeling&& stateLabeling = storm::models::sparse::StateLabeling(),
std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(),
bool rateTransitions = false,
boost::optional<storm::storage::BitVector>&& markovianStates = boost::none,
- boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none)
- : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)) {
+ boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none,
+ boost::optional<std::vector<uint_fast32_t>>&& playerActionIndices = boost::none)
+ : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)), playerActionIndices(std::move(playerActionIndices)) {
// Intentionally left empty
}
-
-
-
-
+
+
+
+
// General components (applicable for all model types):
-
+
// The transition matrix.
storm::storage::SparseMatrix<ValueType> transitionMatrix;
// The state labeling.
@@ -80,7 +82,11 @@ namespace storm {
// Stochastic two player game specific components:
// The matrix of player 1 choices (needed for stochastic two player games
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> player1Matrix;
+
+ // Stochastic multiplayer game specific components:
+ // The vector mapping state choices to players
+ boost::optional<std::vector<uint_fast32_t>> playerActionIndices;
};
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp
index 481ed8020..0caa0edb3 100644
--- a/src/storm/utility/builder.cpp
+++ b/src/storm/utility/builder.cpp
@@ -6,13 +6,14 @@
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Smg.h"
#include "storm/exceptions/InvalidModelException.h"
namespace storm {
namespace utility {
namespace builder {
-
+
template<typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) {
switch (modelType) {
@@ -28,10 +29,12 @@ namespace storm {
return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components));
case storm::models::ModelType::S2pg:
return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<ValueType, RewardModelType>>(std::move(components));
+ case storm::models::ModelType::Smg:
+ return std::make_shared<storm::models::sparse::Smg<ValueType, RewardModelType>>(std::move(components));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidModelException, "Unknown model type");
}
-
+
template std::shared_ptr<storm::models::sparse::Model<double>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double>&& components);
template std::shared_ptr<storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<storm::Interval>>&& components);
template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<storm::RationalNumber>&& components);