From cec2fd420ad0fd1a0335fcf3757b9500723acadf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 7 Feb 2020 17:40:47 +0100 Subject: [PATCH 1/9] Fixed compiler warning --- src/test/storm/storage/SparseMatrixTest.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/test/storm/storage/SparseMatrixTest.cpp b/src/test/storm/storage/SparseMatrixTest.cpp index 6d0ea4480..38566112d 100644 --- a/src/test/storm/storage/SparseMatrixTest.cpp +++ b/src/test/storm/storage/SparseMatrixTest.cpp @@ -710,12 +710,12 @@ TEST(SparseMatrix, Permute) { std::vector inversePermutation = {1,4,0,3,2}; storm::storage::SparseMatrix matrixperm = matrix.permuteRows(inversePermutation); - EXPECT_EQ(5, matrixperm.getRowCount()); - EXPECT_EQ(4, matrixperm.getColumnCount()); - EXPECT_EQ(8, matrixperm.getEntryCount()); + EXPECT_EQ(5ul, matrixperm.getRowCount()); + EXPECT_EQ(4ul, matrixperm.getColumnCount()); + EXPECT_EQ(8ul, matrixperm.getEntryCount()); EXPECT_EQ(matrix.getRowSum(1), matrixperm.getRowSum(0)); EXPECT_EQ(matrix.getRowSum(4), matrixperm.getRowSum(1)); EXPECT_EQ(matrix.getRowSum(0), matrixperm.getRowSum(2)); EXPECT_EQ(matrix.getRowSum(3), matrixperm.getRowSum(3)); EXPECT_EQ(matrix.getRowSum(2), matrixperm.getRowSum(4)); -} \ No newline at end of file +} From 6891825803f0732e8047033dbcc05fdfbe90a4fe Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 10 Feb 2020 15:18:39 +0100 Subject: [PATCH 2/9] IterativeMinMaxLinearEquationSolver: Fixed not incrementing an iterator when computing the maximum absolute difference between two values --- src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 37f9c1ab5..df53fb538 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -424,6 +424,7 @@ namespace storm { auto oldValueIt = oldValues.begin(); for (auto value : relevantValues) { result = storm::utility::max(result, storm::utility::abs(allValues[value] - *oldValueIt)); + ++oldValueIt; } return result; } From 5f18704becd096bf6d07fa4d2aa9b86dd1db80af Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 14 Feb 2020 12:30:58 +0100 Subject: [PATCH 3/9] Added makeOptional to arguments of the --qvbs option. --- src/storm/settings/modules/IOSettings.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index b6753760b..7da94b94e 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -97,8 +97,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("model", "The short model name as in the benchmark set.").build()) - .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("instance-index", "The selected instance of this model.").setDefaultValueUnsignedInteger(0).build()) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The comma separated list of property names to check. Omit to check all, \"\" to check none.").setDefaultValueString("").build()) + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("instance-index", "The selected instance of this model.").setDefaultValueUnsignedInteger(0).makeOptional().build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The comma separated list of property names to check. Omit to check all, \"\" to check none.").setDefaultValueString("").makeOptional().build()) .build()); #ifdef STORM_HAVE_QVBS std::string qvbsRootDefault = STORM_QVBS_ROOT; From 9e54ce4e8b938ad764536686364c0865cffed587 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 19 Feb 2020 15:29:37 +0100 Subject: [PATCH 4/9] Improved detection of terminal states for Dd engine. Also reduced code duplication. --- src/storm/builder/BuilderOptions.cpp | 56 +------------ src/storm/builder/DdJaniModelBuilder.cpp | 86 +++++++------------- src/storm/builder/DdJaniModelBuilder.h | 8 +- src/storm/builder/DdPrismModelBuilder.cpp | 90 +++------------------ src/storm/builder/DdPrismModelBuilder.h | 10 +-- src/storm/builder/TerminalStatesGetter.cpp | 94 ++++++++++++++++++++++ src/storm/builder/TerminalStatesGetter.h | 53 ++++++++++++ 7 files changed, 202 insertions(+), 195 deletions(-) create mode 100644 src/storm/builder/TerminalStatesGetter.cpp create mode 100644 src/storm/builder/TerminalStatesGetter.h diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 9a5b4737c..2224efe11 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -1,5 +1,7 @@ #include "storm/builder/BuilderOptions.h" +#include "storm/builder/TerminalStatesGetter.h" + #include "storm/logic/Formulas.h" #include "storm/logic/LiftableTransitionRewardsVisitor.h" @@ -95,58 +97,8 @@ namespace storm { } void BuilderOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - addTerminalExpression(formula.asAtomicExpressionFormula().getExpression(), true); - } else if (formula.isAtomicLabelFormula()) { - addTerminalLabel(formula.asAtomicLabelFormula().getLabel(), true); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); - } else if (left.isAtomicLabelFormula()) { - addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); - } - } else if (formula.isBoundedUntilFormula()) { - storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); - bool hasLowerBound = false; - for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { - if (boundedUntil.hasLowerBound(i) && (boundedUntil.getLowerBound(i).containsVariables() || !storm::utility::isZero(boundedUntil.getLowerBound(i).evaluateAsRational()))) { - hasLowerBound = true; - break; - } - } - if (!hasLowerBound) { - storm::logic::Formula const& right = boundedUntil.getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - } - storm::logic::Formula const& left = boundedUntil.getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); - } else if (left.isAtomicLabelFormula()) { - addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula() || sub.isBoundedUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula()) { - storm::logic::Formula const& sub = formula.asOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } + getTerminalStatesFromFormula(formula, [this](storm::expressions::Expression const& expr, bool inverted){ this->addTerminalExpression(expr, inverted);} + , [this](std::string const& label, bool inverted){ this->addTerminalLabel(label, inverted);}); } std::set const& BuilderOptions::getRewardModelNames() const { diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 5940e4ac3..ff52955ee 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -46,18 +46,18 @@ namespace storm { namespace builder { template - DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions() { // Intentionally left empty. } template - DdJaniModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template - DdJaniModelBuilder::Options::Options(std::vector> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() { + DdJaniModelBuilder::Options::Options(std::vector> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() { if (!formulas.empty()) { for (auto const& formula : formulas) { this->preserveFormula(*formula); @@ -71,12 +71,7 @@ namespace storm { template void DdJaniModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - if (terminalStates) { - terminalStates.reset(); - } - if (negatedTerminalStates) { - negatedTerminalStates.reset(); - } + terminalStates = storm::builder::TerminalStates(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { @@ -93,28 +88,7 @@ namespace storm { template void DdJaniModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - terminalStates = formula.asAtomicExpressionFormula().getExpression(); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } + terminalStates = getTerminalStatesFromFormula(formula); } template @@ -939,13 +913,14 @@ namespace storm { boost::optional previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); STORM_LOG_ASSERT(previousActionPosition, "Inconsistent information about synchronization vector."); AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; - auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())), synchronizationVectorIndex, isCtmc)); + auto precedingActionIndex = actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())); + auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(precedingActionIndex, synchronizationVectorIndex, isCtmc)); uint64_t highestLocalNondeterminismVariable = 0; if (precedingActionIt != previousAutomatonDd.actions.end()) { highestLocalNondeterminismVariable = precedingActionIt->second.getHighestLocalNondeterminismVariable(); } else { - STORM_LOG_WARN("Subcomposition does not have action that is mentioned in parallel composition."); + STORM_LOG_WARN("Subcomposition does not have action" << actionInformation.getActionName(precedingActionIndex) << " that is mentioned in parallel composition."); } actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, highestLocalNondeterminismVariable, isCtmc); } @@ -1870,7 +1845,7 @@ namespace storm { } template - storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { + storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options, std::map const& labelsToExpressionMap) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { storm::dd::Add stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables); @@ -1883,25 +1858,23 @@ namespace storm { } // If we were asked to treat some states as terminal states, we cut away their transitions now. - if (options.terminalStates || options.negatedTerminalStates) { - std::map constantsSubstitution = model.getConstantsSubstitution(); - - storm::dd::Bdd terminalStatesBdd = variables.manager->getBddZero(); - if (options.terminalStates) { - storm::expressions::Expression terminalExpression = options.terminalStates.get().substitute(constantsSubstitution); - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); - terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); - } - if (options.negatedTerminalStates) { - storm::expressions::Expression negatedTerminalExpression = options.negatedTerminalStates.get().substitute(constantsSubstitution); - STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); - terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); - } - + storm::dd::Bdd terminalStatesBdd = variables.manager->getBddZero(); + if (!options.terminalStates.empty()) { + storm::expressions::Expression terminalExpression = options.terminalStates.asExpression([&model, &labelsToExpressionMap](std::string const& labelName) { + auto exprIt = labelsToExpressionMap.find(labelName); + if (exprIt != labelsToExpressionMap.end()) { + return exprIt->second; + } else { + STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + // If the label name is "init" we can abort 'exploration' directly at the initial state. If it is deadlock, we do not have to abort. + return model.getExpressionManager().boolean(labelName == "init"); + } + }); + terminalExpression = terminalExpression.substitute(model.getConstantsSubstitution()); + terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); system.transitions *= (!terminalStatesBdd).template toAdd(); - return terminalStatesBdd; } - return variables.manager->getBddZero(); + return terminalStatesBdd; } template @@ -2095,12 +2068,18 @@ namespace storm { // Postprocess the variables in place. postprocessVariables(preparedModel.getModelType(), system, variables); + // Build the label to expressions mapping. + auto labelsToExpressionMap = buildLabelExpressions(preparedModel, variables, options); + // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off). - storm::dd::Bdd terminalStates = postprocessSystem(preparedModel, system, variables, options); + storm::dd::Bdd terminalStates = postprocessSystem(preparedModel, system, variables, options, labelsToExpressionMap); // Start creating the model components. ModelComponents modelComponents; + // Set the label expressions + modelComponents.labelToExpressionMap = std::move(labelsToExpressionMap); + // Build initial states. modelComponents.initialStates = computeInitialStates(preparedModel, variables); @@ -2128,9 +2107,6 @@ namespace storm { // Build the reward models. modelComponents.rewardModels = buildRewardModels(reachableStatesAdd, modelComponents.transitionMatrix, preparedModel.getModelType(), variables, system, rewardVariables); - // Build the label to expressions mapping. - modelComponents.labelToExpressionMap = buildLabelExpressions(preparedModel, variables, options); - // Finally, create the model. return createModel(preparedModel.getModelType(), variables, modelComponents); } diff --git a/src/storm/builder/DdJaniModelBuilder.h b/src/storm/builder/DdJaniModelBuilder.h index 371b52557..9dfe6f232 100644 --- a/src/storm/builder/DdJaniModelBuilder.h +++ b/src/storm/builder/DdJaniModelBuilder.h @@ -5,6 +5,7 @@ #include "storm/storage/dd/DdType.h" #include "storm/logic/Formula.h" +#include "storm/builder/TerminalStatesGetter.h" namespace storm { @@ -96,13 +97,10 @@ namespace storm { // An optional mapping that, if given, contains defining expressions for undefined constants. boost::optional> constantDefinitions; - // An optional expression or label that (a subset of) characterizes the terminal states of the model. + // An optional set of expression or labels that characterizes (a subset of) the terminal states of the model. // If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional terminalStates; + storm::builder::TerminalStates terminalStates; - // An optional expression or label whose negation characterizes (a subset of) the terminal states of the - // model. If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional negatedTerminalStates; }; /*! diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 1a25bdaa2..0e5a05c9a 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -540,18 +540,18 @@ namespace storm { }; template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() { // Intentionally left empty. } template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set()) { this->preserveFormula(formula); this->setTerminalStatesFromFormula(formula); } template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() { + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() { for (auto const& formula : formulas) { this->preserveFormula(*formula); } @@ -563,12 +563,7 @@ namespace storm { template void DdPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - if (terminalStates) { - terminalStates.reset(); - } - if (negatedTerminalStates) { - negatedTerminalStates.reset(); - } + terminalStates = storm::builder::TerminalStates(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { @@ -588,32 +583,7 @@ namespace storm { template void DdPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - terminalStates = formula.asAtomicExpressionFormula().getExpression(); - } else if (formula.isAtomicLabelFormula()) { - terminalStates = formula.asAtomicLabelFormula().getLabel(); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); - } else if (left.isAtomicLabelFormula()) { - negatedTerminalStates = left.asAtomicLabelFormula().getLabel(); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } + terminalStates = getTerminalStatesFromFormula(formula); } template @@ -1351,52 +1321,18 @@ namespace storm { // If we were asked to treat some states as terminal states, we cut away their transitions now. storm::dd::Bdd terminalStatesBdd = generationInfo.manager->getBddZero(); - if (options.terminalStates || options.negatedTerminalStates) { - std::map constantsSubstitution = program.getConstantsSubstitution(); - - if (options.terminalStates) { - storm::expressions::Expression terminalExpression; - if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { - terminalExpression = boost::get(options.terminalStates.get()); - } else { - std::string const& labelName = boost::get(options.terminalStates.get()); + if (!options.terminalStates.empty()) { + storm::expressions::Expression terminalExpression = options.terminalStates.asExpression([&program](std::string const& labelName) { if (program.hasLabel(labelName)) { - terminalExpression = program.getLabelExpression(labelName); + return program.getLabelExpression(labelName); } else { STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + // If the label name is "init" we can abort 'exploration' directly at the initial state. If it is deadlock, we do not have to abort. + return program.getManager().boolean(labelName == "init"); } - } - - if (terminalExpression.isInitialized()) { - // If the expression refers to constants of the model, we need to substitute them. - terminalExpression = terminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); - terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); - } - } - if (options.negatedTerminalStates) { - storm::expressions::Expression negatedTerminalExpression; - if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) { - negatedTerminalExpression = boost::get(options.negatedTerminalStates.get()); - } else { - std::string const& labelName = boost::get(options.negatedTerminalStates.get()); - if (program.hasLabel(labelName)) { - negatedTerminalExpression = program.getLabelExpression(labelName); - } else { - STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); - } - } - - if (negatedTerminalExpression.isInitialized()) { - // If the expression refers to constants of the model, we need to substitute them. - negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); - terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); - } - } - + }); + terminalExpression = terminalExpression.substitute(program.getConstantsSubstitution()); + terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); transitionMatrix *= (!terminalStatesBdd).template toAdd(); } diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index fb357a6c8..a529f0656 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -7,6 +7,8 @@ #include "storm/storage/prism/Program.h" +#include "storm/builder/TerminalStatesGetter.h" + #include "storm/logic/Formulas.h" #include "storm/adapters/AddExpressionAdapter.h" #include "storm/utility/macros.h" @@ -81,13 +83,9 @@ namespace storm { // An optional set of labels that, if given, restricts the labels that are built. boost::optional> labelsToBuild; - // An optional expression or label that (a subset of) characterizes the terminal states of the model. + // An optional set of expression or labels that characterizes (a subset of) the terminal states of the model. // If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional> terminalStates; - - // An optional expression or label whose negation characterizes (a subset of) the terminal states of the - // model. If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional> negatedTerminalStates; + storm::builder::TerminalStates terminalStates; }; /*! diff --git a/src/storm/builder/TerminalStatesGetter.cpp b/src/storm/builder/TerminalStatesGetter.cpp new file mode 100644 index 000000000..11a4ccb85 --- /dev/null +++ b/src/storm/builder/TerminalStatesGetter.cpp @@ -0,0 +1,94 @@ +#include "storm/builder/TerminalStatesGetter.h" + +#include "storm/storage/expressions/Expression.h" +#include "storm/logic/Formulas.h" + +namespace storm { + namespace builder { + void getTerminalStatesFromFormula(storm::logic::Formula const& formula, std::function const& terminalExpressionCallback, std::function const& terminalLabelCallback) { + if (formula.isAtomicExpressionFormula()) { + terminalExpressionCallback(formula.asAtomicExpressionFormula().getExpression(), true); + } else if (formula.isAtomicLabelFormula()) { + terminalLabelCallback(formula.asAtomicLabelFormula().getLabel(), true); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + getTerminalStatesFromFormula(right, terminalExpressionCallback, terminalLabelCallback); + } + storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + terminalExpressionCallback(left.asAtomicExpressionFormula().getExpression(), false); + } else if (left.isAtomicLabelFormula()) { + terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); + } + } else if (formula.isBoundedUntilFormula()) { + storm::logic::BoundedUntilFormula const& boundedUntil = formula.asBoundedUntilFormula(); + bool hasLowerBound = false; + for (uint64_t i = 0; i < boundedUntil.getDimension(); ++i) { + if (boundedUntil.hasLowerBound(i) && (boundedUntil.getLowerBound(i).containsVariables() || !storm::utility::isZero(boundedUntil.getLowerBound(i).evaluateAsRational()))) { + hasLowerBound = true; + break; + } + } + if (!hasLowerBound) { + storm::logic::Formula const& right = boundedUntil.getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + getTerminalStatesFromFormula(right, terminalExpressionCallback, terminalLabelCallback); + } + } + storm::logic::Formula const& left = boundedUntil.getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + terminalExpressionCallback(left.asAtomicExpressionFormula().getExpression(), false); + } else if (left.isAtomicLabelFormula()) { + terminalLabelCallback(left.asAtomicLabelFormula().getLabel(), false); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula() || sub.isBoundedUntilFormula()) { + getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); + } + } else if (formula.isRewardOperatorFormula() || formula.isTimeOperatorFormula()) { + storm::logic::Formula const& sub = formula.asOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula()) { + getTerminalStatesFromFormula(sub, terminalExpressionCallback, terminalLabelCallback); + } + } + } + + bool TerminalStates::empty() const { + return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty(); + } + + storm::expressions::Expression TerminalStates::asExpression(std::function const& labelToExpressionMap) const { + auto allTerminalExpressions = terminalExpressions; + for (auto const& e : negatedTerminalExpressions) { + allTerminalExpressions.push_back(!e); + } + for (auto const& l : terminalLabels) { + allTerminalExpressions.push_back(labelToExpressionMap(l)); + } + for (auto const& l : negatedTerminalLabels) { + allTerminalExpressions.push_back(!labelToExpressionMap(l)); + } + STORM_LOG_ASSERT(!allTerminalExpressions.empty(), "Unable to convert empty terminal state set to expression"); + return storm::expressions::disjunction(allTerminalExpressions); + } + + TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula) { + TerminalStates result; + getTerminalStatesFromFormula(formula, [&result](storm::expressions::Expression const& expr, bool inverted){ if(inverted) { result.terminalExpressions.push_back(expr);} else {result.negatedTerminalExpressions.push_back(expr);} }, + [&result](std::string const& label, bool inverted){ if(inverted) { result.terminalLabels.push_back(label);} else {result.negatedTerminalLabels.push_back(label);} }); + return result; + } + + + + + + } +} \ No newline at end of file diff --git a/src/storm/builder/TerminalStatesGetter.h b/src/storm/builder/TerminalStatesGetter.h new file mode 100644 index 000000000..c9eb2c6c0 --- /dev/null +++ b/src/storm/builder/TerminalStatesGetter.h @@ -0,0 +1,53 @@ +#pragma once + +#include +#include +#include + +namespace storm { + + namespace expressions { + class Expression; + } + namespace logic { + class Formula; + } + + namespace builder { + + /*! + * Traverses the formula. If an expression (or label) is found such that checking the formula does not require further exploration from a state + * satisfying (or violating) the expression (or label), the corresponding callback function is called. + * @param formula The formula to analyzed + * @param terminalExpressionCallback called on terminal expressions. The corresponding flag indicates whether exploration can stop from states satisfying (true) or violating (false) the expression + * @param terminalLabelCallback called on terminal labels. The corresponding flag indicates whether exploration can stop from states having (true) or not having (false) the label + */ + void getTerminalStatesFromFormula(storm::logic::Formula const& formula, std::function const& terminalExpressionCallback, std::function const& terminalLabelCallback); + + + struct TerminalStates { + std::vector terminalExpressions; // if one of these is true, we can stop exploration + std::vector negatedTerminalExpressions; // if one of these is false, we can stop exploration + std::vector terminalLabels; // if a state has one of these labels, we can stop exploration + std::vector negatedTerminalLabels; // if a state does not have all of these labels, we can stop exploration + + /*! + * True if no terminal states are specified + */ + bool empty() const; + + /*! + * Returns an expression that evaluates to true only if the exploration can stop at the corresponding state + * Should only be called if this is not empty. + */ + storm::expressions::Expression asExpression(std::function const& labelToExpressionMap) const; + }; + + /*! + * Traverses the formula. If an expression (or label) is found such that checking the formula does not require further exploration from a state + * satisfying (or violating) the expression (or label), it is inserted into the returned struct. + */ + TerminalStates getTerminalStatesFromFormula(storm::logic::Formula const& formula); + + } +} \ No newline at end of file From ba6f0c0e877af75d8ed4a967bcbc8edac46ac855 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 20 Feb 2020 12:01:55 +0100 Subject: [PATCH 5/9] BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption. --- CHANGELOG.md | 2 ++ src/storm-cli-utilities/model-handling.h | 13 +++++++++---- src/storm/api/builder.h | 4 +++- src/storm/builder/TerminalStatesGetter.cpp | 7 +++++++ src/storm/builder/TerminalStatesGetter.h | 5 +++++ src/storm/settings/modules/BuildSettings.cpp | 12 ++++++++++++ src/storm/settings/modules/BuildSettings.h | 13 +++++++++++-- 7 files changed, 49 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3a5c36231..df9f29923 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,8 @@ Version 1.4.x ## Version 1.4.2 (under development) - DRN: support import of choice labelling +- Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`). +- Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata) - `storm-pomdp`: Only accept POMDPs that are canonical - `storm-pomdp`: Prism language extended with observable expressions - `storm-pomdp`: Various fixes that prevented usage. diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index a49d244e5..b35b9f0d3 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -260,7 +260,8 @@ namespace storm { template std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule().isBuildFullModelSet()); + auto buildSettings = storm::settings::getModule(); + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(), !buildSettings.isApplyNoMaximumProgressAssumptionSet()); } template @@ -268,19 +269,23 @@ namespace storm { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); - bool buildChoiceOrigins = false; + bool buildChoiceOrigins = buildSettings.isBuildChoiceOriginsSet(); if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { auto counterexampleGeneratorSettings = storm::settings::getModule(); if (counterexampleGeneratorSettings.isCounterexampleSet()) { - buildChoiceOrigins = counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); + buildChoiceOrigins |= counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); } - options.setBuildChoiceOrigins(buildChoiceOrigins); } + options.setBuildChoiceOrigins(buildChoiceOrigins); if (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::POMDP) { options.setBuildChoiceOrigins(true); options.setBuildChoiceLabels(true); } + if (buildSettings.isApplyNoMaximumProgressAssumptionSet()) { + options.setApplyMaximalProgressAssumption(false); + } + options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 0df66c7ff..6be939496 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -43,7 +43,7 @@ namespace storm { } template - std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel = false) { + std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel = false, bool applyMaximumProgress = true) { if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); @@ -51,6 +51,7 @@ namespace storm { if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.terminalStates.clear(); } storm::builder::DdPrismModelBuilder builder; @@ -63,6 +64,7 @@ namespace storm { if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.terminalStates.clear(); } storm::builder::DdJaniModelBuilder builder; diff --git a/src/storm/builder/TerminalStatesGetter.cpp b/src/storm/builder/TerminalStatesGetter.cpp index 11a4ccb85..16779b8d9 100644 --- a/src/storm/builder/TerminalStatesGetter.cpp +++ b/src/storm/builder/TerminalStatesGetter.cpp @@ -60,6 +60,13 @@ namespace storm { } } + void TerminalStates::clear() { + terminalExpressions.clear(); + negatedTerminalExpressions.clear(); + terminalLabels.clear(); + negatedTerminalLabels.clear(); + } + bool TerminalStates::empty() const { return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty(); } diff --git a/src/storm/builder/TerminalStatesGetter.h b/src/storm/builder/TerminalStatesGetter.h index c9eb2c6c0..f41413f28 100644 --- a/src/storm/builder/TerminalStatesGetter.h +++ b/src/storm/builder/TerminalStatesGetter.h @@ -31,6 +31,11 @@ namespace storm { std::vector terminalLabels; // if a state has one of these labels, we can stop exploration std::vector negatedTerminalLabels; // if a state does not have all of these labels, we can stop exploration + /*! + * Clears all terminal states. After calling this, empty() holds. + */ + void clear(); + /*! * True if no terminal states are specified */ diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 3ebc6d109..b460d7ba6 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -29,7 +29,9 @@ namespace storm { const std::string dontFixDeadlockOptionShortName = "ndl"; const std::string noBuildOptionName = "nobuild"; const std::string fullModelBuildOptionName = "buildfull"; + const std::string applyNoMaxProgAssumptionOptionName = "nomaxprog"; const std::string buildChoiceLabelOptionName = "buildchoicelab"; + const std::string buildChoiceOriginsOptionName = "buildchoiceorig"; const std::string buildStateValuationsOptionName = "buildstateval"; const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; @@ -40,7 +42,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, applyNoMaxProgAssumptionOptionName, false, "If set, the maximum progress assumption is not applied while building the model (relevant for MAs)").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceOriginsOptionName, false, "If set, also build information that for each choice indicates the part(s) of the input that yielded the choice.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").setIsAdvanced().build()); @@ -81,9 +85,17 @@ namespace storm { return this->getOption(noBuildOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isApplyNoMaximumProgressAssumptionSet() const { + return this->getOption(applyNoMaxProgAssumptionOptionName).getHasOptionBeenSet(); + } + bool BuildSettings::isBuildChoiceLabelsSet() const { return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); } + + bool BuildSettings::isBuildChoiceOriginsSet() const { + return this->getOption(buildChoiceOriginsOptionName).getHasOptionBeenSet(); + } bool BuildSettings::isBuildStateValuationsSet() const { return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index b80424c7f..274f42da1 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -78,12 +78,21 @@ namespace storm { * @return true iff the full model should be build. */ bool isBuildFullModelSet() const; - + + /*! + * Retrieves whether the maximum progress assumption is to be applied when building the model + */ + bool isApplyNoMaximumProgressAssumptionSet() const; + /*! * Retrieves whether the choice labels should be build - * @return */ bool isBuildChoiceLabelsSet() const; + + /*! + * Retrieves whether the choice origins should be build + */ + bool isBuildChoiceOriginsSet() const; /*! * Retrieves whether the choice labels should be build From f7e2ff08437977187421d92dffbebce3490caea1 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 20 Feb 2020 12:02:32 +0100 Subject: [PATCH 6/9] Apply max. Prog. assumption while building with the dd engine. --- CHANGELOG.md | 1 + src/storm/api/builder.h | 11 ++--- src/storm/builder/DdJaniModelBuilder.cpp | 52 ++++++++++++++++++++--- src/storm/builder/DdJaniModelBuilder.h | 11 +++-- src/storm/builder/DdPrismModelBuilder.cpp | 2 +- 5 files changed, 61 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index df9f29923..d9504338f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,7 @@ Version 1.4.x ## Version 1.4.2 (under development) - DRN: support import of choice labelling - Added option `--build:buildchoiceorig` to build a model (PRISM or JANI) with choice origins (which are exported with, e.g. `--exportscheduler`). +- Apply the maximum progress assumption while building a Markov automata with the Dd engine. - Added option `--build:nomaxprog` to disable applying the maximum progress assumption during model building (for Markov Automata) - `storm-pomdp`: Only accept POMDPs that are canonical - `storm-pomdp`: Prism language extended with observable expressions diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 6be939496..4e22d6662 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -47,7 +47,6 @@ namespace storm { if (model.isPrismProgram()) { typename storm::builder::DdPrismModelBuilder::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; @@ -58,13 +57,15 @@ namespace storm { return builder.build(model.asPrismProgram(), options); } else { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Building symbolic model from this model description is unsupported."); - typename storm::builder::DdJaniModelBuilder::Options options; - options = typename storm::builder::DdJaniModelBuilder::Options(formulas); + typename storm::builder::DdJaniModelBuilder::Options options(formulas); if (buildFullModel) { options.buildAllLabels = true; options.buildAllRewardModels = true; + options.applyMaximumProgressAssumption = false; options.terminalStates.clear(); + } else { + options.applyMaximumProgressAssumption = (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA && applyMaximumProgress); } storm::builder::DdJaniModelBuilder builder; @@ -73,12 +74,12 @@ namespace storm { } template<> - inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel) { + inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool, bool) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational numbers."); } template<> - inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildFullModel) { + inline std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool, bool) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions."); } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index ff52955ee..2175dd2e1 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -46,7 +46,7 @@ namespace storm { namespace builder { template - DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions() { + DdJaniModelBuilder::Options::Options(bool buildAllLabels, bool buildAllRewardModels, bool applyMaximumProgressAssumption) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), applyMaximumProgressAssumption(applyMaximumProgressAssumption), rewardModelsToBuild(), constantDefinitions() { // Intentionally left empty. } @@ -71,7 +71,7 @@ namespace storm { template void DdJaniModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - terminalStates = storm::builder::TerminalStates(); + terminalStates.clear(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { @@ -662,6 +662,19 @@ namespace storm { return ActionDd(newGuard, newTransitions, newTransientEdgeAssignments, newLocalNondeterminismVariables, newVariableToWritingFragment, newIllegalFragment); } + /*! + * Conjuncts the guard of the action with the provided condition, i.e., this action is only enabled if the provided condition is true. + */ + void conjunctGuardWith(storm::dd::Bdd const& condition) { + guard &= condition; + storm::dd::Add conditionAdd = condition.template toAdd(); + transitions *= conditionAdd; + for (auto& t : transientEdgeAssignments) { + t.second *= conditionAdd; + } + illegalFragment &= condition; + } + bool isInputEnabled() const { return inputEnabled; } @@ -670,10 +683,10 @@ namespace storm { inputEnabled = true; } - // A DD that represents all states that have this edge enabled. + // A DD that represents all states that have this action enabled. storm::dd::Bdd guard; - // A DD that represents the transitions of this edge. + // A DD that represents the transitions of this action. storm::dd::Add transitions; // A mapping from transient variables to their assignments. @@ -787,11 +800,12 @@ namespace storm { std::pair localNondeterminismVariables; }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables, bool applyMaximumProgress) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation), applyMaximumProgress(applyMaximumProgress) { // Intentionally left empty. } storm::jani::CompositionInformation const& actionInformation; + bool applyMaximumProgress; ComposerResult compose() override { STORM_LOG_THROW(this->model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions."); @@ -936,6 +950,9 @@ namespace storm { AutomatonDd composeInParallel(std::vector const& subautomata, std::vector const& synchronizationVectors) { AutomatonDd result(this->variables.manager->template getAddOne()); + // Disjunction of all guards of non-markovian actions (only required for maximum progress assumption. + storm::dd::Bdd nonMarkovianActionGuards = this->variables.manager->getBddZero(); + // Build the results of the synchronization vectors. std::unordered_map, ActionIdentificationHash> actions; for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) { @@ -943,6 +960,11 @@ namespace storm { boost::optional synchronizingAction = combineSynchronizingActions(subautomata, synchVector, synchronizationVectorIndex); if (synchronizingAction) { + if (applyMaximumProgress) { + STORM_LOG_ASSERT(this->model.getModelType() == storm::jani::ModelType::MA, "Maximum progress assumption enabled for unexpected model type."); + // By the JANI standard, we can assume that synchronizing actions of MAs are always non-Markovian. + nonMarkovianActionGuards |= synchronizingAction->guard; + } actions[ActionIdentification(actionInformation.getActionIndex(synchVector.getOutput()), this->model.getModelType() == storm::jani::ModelType::CTMC)].emplace_back(synchronizingAction.get()); } } @@ -986,9 +1008,26 @@ namespace storm { auto& allSilentActionDds = actions[silentActionIdentification]; allSilentActionDds.insert(allSilentActionDds.end(), silentActionDds.begin(), silentActionDds.end()); } + + // Add guards of non-markovian actions + if (applyMaximumProgress) { + auto allSilentActionDdsIt = actions.find(silentActionIdentification); + if (allSilentActionDdsIt != actions.end()) { + for (ActionDd const& silentActionDd : allSilentActionDdsIt->second) { + nonMarkovianActionGuards |= silentActionDd.guard; + } + } + } + if (!silentMarkovianActionDds.empty()) { auto& allMarkovianSilentActionDds = actions[silentMarkovianActionIdentification]; allMarkovianSilentActionDds.insert(allMarkovianSilentActionDds.end(), silentMarkovianActionDds.begin(), silentMarkovianActionDds.end()); + if (applyMaximumProgress && !nonMarkovianActionGuards.isZero()) { + auto invertedNonMarkovianGuards = !nonMarkovianActionGuards; + for (ActionDd& markovianActionDd : allMarkovianSilentActionDds) { + markovianActionDd.conjunctGuardWith(invertedNonMarkovianGuards); + } + } } // Finally, combine (potentially) multiple action DDs. @@ -2062,7 +2101,8 @@ namespace storm { std::vector rewardVariables = selectRewardVariables(preparedModel, options); // Create a builder to compose and build the model. - CombinedEdgesSystemComposer composer(preparedModel, actionInformation, variables, rewardVariables); + bool applyMaximumProgress = options.applyMaximumProgressAssumption && model.getModelType() == storm::jani::ModelType::MA; + CombinedEdgesSystemComposer composer(preparedModel, actionInformation, variables, rewardVariables, applyMaximumProgress); ComposerResult system = composer.compose(); // Postprocess the variables in place. diff --git a/src/storm/builder/DdJaniModelBuilder.h b/src/storm/builder/DdJaniModelBuilder.h index 9dfe6f232..23684f4f9 100644 --- a/src/storm/builder/DdJaniModelBuilder.h +++ b/src/storm/builder/DdJaniModelBuilder.h @@ -28,7 +28,7 @@ namespace storm { /*! * Creates an object representing the default building options. */ - Options(bool buildAllLabels = false, bool buildAllRewardModels = false); + Options(bool buildAllLabels = false, bool buildAllRewardModels = false, bool applyMaximumProgressAssumption = true); /*! Creates an object representing the suggested building options assuming that the given formula is the * only one to check. Additional formulas may be preserved by calling preserveFormula. @@ -79,9 +79,6 @@ namespace storm { /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored. bool buildAllLabels; - - /// A set of labels to build. - std::set labelNames; /*! * Retrieves whether the flag to build all reward models is set. @@ -91,6 +88,12 @@ namespace storm { // A flag that indicates whether or not all reward models are to be build. bool buildAllRewardModels; + /// A flag that indicates whether the maximum progress assumption should be applied. + bool applyMaximumProgressAssumption; + + /// A set of labels to build. + std::set labelNames; + // A list of reward models to be build in case not all reward models are to be build. std::set rewardModelsToBuild; diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 0e5a05c9a..4633ebdbc 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -563,7 +563,7 @@ namespace storm { template void DdPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. - terminalStates = storm::builder::TerminalStates(); + terminalStates.clear(); // If we are not required to build all reward models, we determine the reward models we need to build. if (!buildAllRewardModels) { From 141316943cd6ccda9a7787c2524967c37841a579 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 27 Feb 2020 09:06:12 +0100 Subject: [PATCH 7/9] DdJaniModelBuilder: Also apply max. progress if the system consists of just a single automaton. --- src/storm/builder/DdJaniModelBuilder.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 2175dd2e1..0df1fa029 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -887,7 +887,7 @@ namespace storm { inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName)); } - return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast(data), inputEnabledActionIndices); + return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast(data), inputEnabledActionIndices, data.empty()); } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { @@ -1707,10 +1707,13 @@ namespace storm { } } - AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set const& inputEnabledActionIndices) { + AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set const& inputEnabledActionIndices, bool isTopLevelAutomaton) { STORM_LOG_TRACE("Building DD for automaton '" << automatonName << "'."); AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); + // Disjunction of all guards of non-markovian actions (only required for maximum progress assumption). + storm::dd::Bdd nonMarkovianActionGuards = this->variables.manager->getBddZero(); + storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); for (auto const& actionInstantiation : actionInstantiations) { uint64_t actionIndex = actionInstantiation.first; @@ -1727,12 +1730,20 @@ namespace storm { if (inputEnabled) { actionDd.setIsInputEnabled(); } + if (applyMaximumProgress && isTopLevelAutomaton && !instantiation.isMarkovian()) { + nonMarkovianActionGuards |= actionDd.guard; + } STORM_LOG_TRACE("Used local nondeterminism variables are " << actionDd.getLowestLocalNondeterminismVariable() << " to " << actionDd.getHighestLocalNondeterminismVariable() << "."); result.actions[ActionIdentification(actionIndex, instantiation.synchronizationVectorIndex, instantiation.isMarkovian())] = actionDd; result.extendLocalNondeterminismVariables(actionDd.getLocalNondeterminismVariables()); } } + if (applyMaximumProgress && isTopLevelAutomaton) { + ActionIdentification silentMarkovianActionIdentification(storm::jani::Model::SILENT_ACTION_INDEX, true); + result.actions[silentMarkovianActionIdentification].conjunctGuardWith(!nonMarkovianActionGuards); + } + for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) { auto const& location = automaton.getLocation(locationIndex); performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) { From 5d8419336f86084c262a6433d9ea985d887a2b8a Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 2 Mar 2020 06:34:28 +0100 Subject: [PATCH 8/9] InternalAdds: Added a comment related to GitHub issue #64 --- src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 2 ++ src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index d94e6cadc..fe9a85f7e 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -596,6 +596,8 @@ namespace storm { splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } else { + // FIXME: We first traverse the else successor (unlike other variants of this method). + // Otherwise, the GameBasedMdpModelCheckerTest would not terminate. See github issue #64 splitIntoGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 8ede93854..d50b8cc0f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1007,6 +1007,8 @@ namespace storm { bool elseComplemented = mtbdd_hascomp(elseDdNode) ^ negated; bool thenComplemented = mtbdd_hascomp(thenDdNode) ^ negated; + // FIXME: We first traverse the else successor (unlike other variants of this method). + // Otherwise, the GameBasedMdpModelCheckerTest would not terminate. See github issue #64 splitIntoGroupsRec(mtbdd_regular(elseDdNode), elseComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); splitIntoGroupsRec(mtbdd_regular(thenDdNode), thenComplemented, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel); } From 6c095e757a7aaa54f7a7613e1797f0ba77f8a2a3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 4 Mar 2020 18:20:33 +0100 Subject: [PATCH 9/9] Fixed problem with Windows linebreak \r\n, because this is still a problem in 2020 --- src/storm-dft/parser/DFTGalileoParser.cpp | 2 +- src/storm-gspn/api/storm-gspn.cpp | 2 +- .../parser/DirectEncodingParser.cpp | 30 ++++++++----------- src/storm/settings/SettingsManager.cpp | 2 +- src/storm/utility/file.h | 23 ++++++++++++++ src/test/storm/utility/FileTest.cpp | 24 +++++++++++++++ 6 files changed, 63 insertions(+), 20 deletions(-) create mode 100644 src/test/storm/utility/FileTest.cpp diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index e463bed37..b387a1a1a 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -48,7 +48,7 @@ namespace storm { std::string toplevelId = ""; bool comment = false; // Indicates whether the current line is part of a multiline comment try { - while (std::getline(file, line)) { + while (storm::utility::getline(file, line)) { ++lineNo; // First consider comments if (comment) { diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index d11ee28ba..ea4faf9e0 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -94,7 +94,7 @@ namespace storm { storm::utility::openFile(filename, stream); std::string line; - while ( std::getline(stream, line) ) { + while (storm::utility::getline(stream, line)) { std::vector strs; boost::split(strs, line, boost::is_any_of("\t ")); STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs"); diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 4814c77f5..35220498e 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -3,25 +3,21 @@ #include #include #include - - #include #include -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/Ctmc.h" - +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/FileIoException.h" -#include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Ctmc.h" #include "storm/settings/SettingsManager.h" - -#include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/utility/constants.h" #include "storm/utility/builder.h" -#include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/utility/file.h" +#include "storm/utility/macros.h" namespace storm { @@ -48,7 +44,7 @@ namespace storm { std::shared_ptr> modelComponents; // Parse header - while (std::getline(file, line)) { + while (storm::utility::getline(file, line)) { if (line.empty() || boost::starts_with(line, "//")) { continue; } @@ -65,7 +61,7 @@ namespace storm { } else if (line == "@parameters") { // Parse parameters STORM_LOG_THROW(!sawParameters, storm::exceptions::WrongFormatException, "Parameters declared twice"); - std::getline(file, line); + storm::utility::getline(file, line); if (line != "") { std::vector parameters; boost::split(parameters, line, boost::is_any_of(" ")); @@ -78,7 +74,7 @@ namespace storm { } else if (line == "@placeholders") { // Parse placeholders - while (std::getline(file, line)) { + while (storm::utility::getline(file, line)) { size_t posColon = line.find(':'); STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found."); std::string placeName = line.substr(0, posColon - 1); @@ -96,16 +92,16 @@ namespace storm { } else if (line == "@reward_models") { // Parse reward models STORM_LOG_THROW(rewardModelNames.empty(), storm::exceptions::WrongFormatException, "Reward model names declared twice"); - std::getline(file, line); + storm::utility::getline(file, line); boost::split(rewardModelNames, line, boost::is_any_of("\t ")); } else if (line == "@nr_states") { // Parse no. of states STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); - std::getline(file, line); + storm::utility::getline(file, line); nrStates = parseNumber(line); } else if (line == "@nr_choices") { STORM_LOG_THROW(nrChoices == 0, storm::exceptions::WrongFormatException, "Number of actions declared twice"); - std::getline(file, line); + storm::utility::getline(file, line); nrChoices = parseNumber(line); } else if (line == "@model") { // Parse rest of the model @@ -164,7 +160,7 @@ namespace storm { size_t state = 0; bool firstState = true; bool firstActionForState = true; - while (std::getline(file, line)) { + while (storm::utility::getline(file, line)) { STORM_LOG_TRACE("Parsing: " << line); if (boost::starts_with(line, "state ")) { // New state diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 8e278fecb..8736c941e 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -539,7 +539,7 @@ namespace storm { bool globalScope = true; std::string activeModule = ""; uint_fast64_t lineNumber = 1; - for (std::string line; getline(input, line); ++lineNumber) { + for (std::string line; storm::utility::getline(input, line); ++lineNumber) { // If the first character of the line is a "[", we expect the settings of a new module to start and // the line to be of the shape []. if (line.at(0) == '[') { diff --git a/src/storm/utility/file.h b/src/storm/utility/file.h index f5ba06f4a..f4a1cbc96 100644 --- a/src/storm/utility/file.h +++ b/src/storm/utility/file.h @@ -70,5 +70,28 @@ namespace storm { return filestream.good(); } + /*! + * Overloaded getline function which handles different types of newline (\n and \r). + * @param input Input stream. + * @param str Output string. + * @return Remaining stream. + */ + template + inline std::basic_istream& getline(std::basic_istream& input, std::basic_string& str) { + auto& res = std::getline(input, str); + // Remove linebreaks + std::string::reverse_iterator rit = str.rbegin(); + while (rit != str.rend()) { + if (*rit == '\r' || *rit == '\n') { + ++rit; + str.pop_back(); + } else { + break; + } + } + return res; + } + + } } diff --git a/src/test/storm/utility/FileTest.cpp b/src/test/storm/utility/FileTest.cpp new file mode 100644 index 000000000..d804e653e --- /dev/null +++ b/src/test/storm/utility/FileTest.cpp @@ -0,0 +1,24 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/utility/file.h" + +TEST(FileTest, GetLine) { + std::stringstream stream; + stream << "Hello world" << std::endl << "This is a test with n\nThis is a test with rn\r\n\nMore tests"; + + std::string str; + int i = 0; + std::string expected[] = {"Hello world", "This is a test with n", "This is a test with rn", "", "More tests"}; + while (storm::utility::getline(stream, str)) { + EXPECT_EQ(str, expected[i]); + ++i; + } +} + + +TEST(FileTest, GetLineEmpty) { + std::stringstream stream; + std::string str; + EXPECT_FALSE(storm::utility::getline(stream, str)); +}