diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3a5c36231..d9504338f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,9 @@ 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
- `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 <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
- return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule<storm::settings::modules::BuildSettings>().isBuildFullModelSet());
+ auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
+ return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties), buildSettings.isBuildFullModelSet(), !buildSettings.isApplyNoMaximumProgressAssumptionSet());
}
template <typename ValueType>
@@ -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<storm::settings::modules::CounterexampleGeneratorSettings>();
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-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<std::string> 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 <iostream>
#include <string>
#include <regex>
-
-
#include <boost/algorithm/string.hpp>
#include <boost/algorithm/string/predicate.hpp>
-#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<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> 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<std::string> 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<size_t>(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<size_t>(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/api/builder.h b/src/storm/api/builder.h
index 0df66c7ff..4e22d6662 100644
--- a/src/storm/api/builder.h
+++ b/src/storm/api/builder.h
@@ -43,26 +43,29 @@ namespace storm {
}
template<storm::dd::DdType LibraryType, typename ValueType>
- std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false) {
+ std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false, bool applyMaximumProgress = true) {
if (model.isPrismProgram()) {
typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
-
if (buildFullModel) {
options.buildAllLabels = true;
options.buildAllRewardModels = true;
+ options.terminalStates.clear();
}
storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
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<LibraryType, ValueType>::Options options;
- options = typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options(formulas);
+ typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::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<LibraryType, ValueType> builder;
@@ -71,12 +74,12 @@ namespace storm {
}
template<>
- inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalNumber>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel) {
+ inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalNumber>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool, bool) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational numbers.");
}
template<>
- inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalFunction>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel) {
+ inline std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, storm::RationalFunction>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool, bool) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions.");
}
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<std::string> const& BuilderOptions::getRewardModelNames() const {
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index 5940e4ac3..0df1fa029 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -46,18 +46,18 @@ namespace storm {
namespace builder {
template <storm::dd::DdType Type, typename ValueType>
- DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+ DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels, bool applyMaximumProgressAssumption) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), applyMaximumProgressAssumption(applyMaximumProgressAssumption), rewardModelsToBuild(), constantDefinitions() {
// Intentionally left empty.
}
template <storm::dd::DdType Type, typename ValueType>
- DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+ DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions() {
this->preserveFormula(formula);
this->setTerminalStatesFromFormula(formula);
}
template <storm::dd::DdType Type, typename ValueType>
- DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+ DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> 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 <storm::dd::DdType Type, typename ValueType>
void DdJaniModelBuilder<Type, ValueType>::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.clear();
// 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 <storm::dd::DdType Type, typename ValueType>
void DdJaniModelBuilder<Type, ValueType>::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 <storm::dd::DdType Type, typename ValueType>
@@ -688,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<Type> const& condition) {
+ guard &= condition;
+ storm::dd::Add<Type, ValueType> conditionAdd = condition.template toAdd<ValueType>();
+ transitions *= conditionAdd;
+ for (auto& t : transientEdgeAssignments) {
+ t.second *= conditionAdd;
+ }
+ illegalFragment &= condition;
+ }
+
bool isInputEnabled() const {
return inputEnabled;
}
@@ -696,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<Type> guard;
- // A DD that represents the transitions of this edge.
+ // A DD that represents the transitions of this action.
storm::dd::Add<Type, ValueType> transitions;
// A mapping from transient variables to their assignments.
@@ -813,11 +800,12 @@ namespace storm {
std::pair<uint64_t, uint64_t> localNondeterminismVariables;
};
- CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) {
+ CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables, bool applyMaximumProgress) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation), applyMaximumProgress(applyMaximumProgress) {
// Intentionally left empty.
}
storm::jani::CompositionInformation const& actionInformation;
+ bool applyMaximumProgress;
ComposerResult<Type, ValueType> compose() override {
STORM_LOG_THROW(this->model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions.");
@@ -899,7 +887,7 @@ namespace storm {
inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName));
}
- return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast<ActionInstantiations const&>(data), inputEnabledActionIndices);
+ return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast<ActionInstantiations const&>(data), inputEnabledActionIndices, data.empty());
}
boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
@@ -939,13 +927,14 @@ namespace storm {
boost::optional<uint64_t> 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);
}
@@ -961,6 +950,9 @@ namespace storm {
AutomatonDd composeInParallel(std::vector<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) {
AutomatonDd result(this->variables.manager->template getAddOne<ValueType>());
+ // Disjunction of all guards of non-markovian actions (only required for maximum progress assumption.
+ storm::dd::Bdd<Type> nonMarkovianActionGuards = this->variables.manager->getBddZero();
+
// Build the results of the synchronization vectors.
std::unordered_map<ActionIdentification, std::vector<ActionDd>, ActionIdentificationHash> actions;
for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) {
@@ -968,6 +960,11 @@ namespace storm {
boost::optional<ActionDd> 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());
}
}
@@ -1011,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.
@@ -1693,10 +1707,13 @@ namespace storm {
}
}
- AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set<uint64_t> const& inputEnabledActionIndices) {
+ AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set<uint64_t> 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<Type> nonMarkovianActionGuards = this->variables.manager->getBddZero();
+
storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
for (auto const& actionInstantiation : actionInstantiations) {
uint64_t actionIndex = actionInstantiation.first;
@@ -1713,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) {
@@ -1870,7 +1895,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
- storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
+ storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options, std::map<std::string, storm::expressions::Expression> 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<Type, ValueType> stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables);
@@ -1883,25 +1908,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<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = model.getConstantsSubstitution();
-
- storm::dd::Bdd<Type> 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<Type> 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<ValueType>();
- return terminalStatesBdd;
}
- return variables.manager->getBddZero();
+ return terminalStatesBdd;
}
template <storm::dd::DdType Type, typename ValueType>
@@ -2089,18 +2112,25 @@ namespace storm {
std::vector<storm::expressions::Variable> rewardVariables = selectRewardVariables<Type, ValueType>(preparedModel, options);
// Create a builder to compose and build the model.
- CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables);
+ bool applyMaximumProgress = options.applyMaximumProgressAssumption && model.getModelType() == storm::jani::ModelType::MA;
+ CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables, applyMaximumProgress);
ComposerResult<Type, ValueType> system = composer.compose();
// 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<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options);
+ storm::dd::Bdd<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options, labelsToExpressionMap);
// Start creating the model components.
ModelComponents<Type, ValueType> modelComponents;
+ // Set the label expressions
+ modelComponents.labelToExpressionMap = std::move(labelsToExpressionMap);
+
// Build initial states.
modelComponents.initialStates = computeInitialStates(preparedModel, variables);
@@ -2128,9 +2158,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..23684f4f9 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 {
@@ -27,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 <code>preserveFormula</code>.
@@ -78,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<std::string> labelNames;
/*!
* Retrieves whether the flag to build all reward models is set.
@@ -90,19 +88,22 @@ 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<std::string> labelNames;
+
// A list of reward models to be build in case not all reward models are to be build.
std::set<std::string> rewardModelsToBuild;
// An optional mapping that, if given, contains defining expressions for undefined constants.
boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> 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<storm::expressions::Expression> 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<storm::expressions::Expression> negatedTerminalStates;
};
/*!
diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp
index 1a25bdaa2..4633ebdbc 100644
--- a/src/storm/builder/DdPrismModelBuilder.cpp
+++ b/src/storm/builder/DdPrismModelBuilder.cpp
@@ -540,18 +540,18 @@ namespace storm {
};
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() {
// Intentionally left empty.
}
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(std::set<std::string>()) {
this->preserveFormula(formula);
this->setTerminalStatesFromFormula(formula);
}
template <storm::dd::DdType Type, typename ValueType>
- DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild(), terminalStates(), negatedTerminalStates() {
+ DdPrismModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), buildAllLabels(false), labelsToBuild() {
for (auto const& formula : formulas) {
this->preserveFormula(*formula);
}
@@ -563,12 +563,7 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
void DdPrismModelBuilder<Type, ValueType>::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.clear();
// 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 <storm::dd::DdType Type, typename ValueType>
void DdPrismModelBuilder<Type, ValueType>::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 <storm::dd::DdType Type, typename ValueType>
@@ -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<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
- if (options.terminalStates || options.negatedTerminalStates) {
- std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = program.getConstantsSubstitution();
-
- if (options.terminalStates) {
- storm::expressions::Expression terminalExpression;
- if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
- terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
- } else {
- std::string const& labelName = boost::get<std::string>(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<storm::expressions::Expression>(options.negatedTerminalStates.get());
- } else {
- std::string const& labelName = boost::get<std::string>(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<ValueType>();
}
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<std::set<std::string>> 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<boost::variant<storm::expressions::Expression, std::string>> 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<boost::variant<storm::expressions::Expression, std::string>> 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..16779b8d9
--- /dev/null
+++ b/src/storm/builder/TerminalStatesGetter.cpp
@@ -0,0 +1,101 @@
+#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<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback, std::function<void(std::string const&, bool)> 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);
+ }
+ }
+ }
+
+ void TerminalStates::clear() {
+ terminalExpressions.clear();
+ negatedTerminalExpressions.clear();
+ terminalLabels.clear();
+ negatedTerminalLabels.clear();
+ }
+
+ bool TerminalStates::empty() const {
+ return terminalExpressions.empty() && negatedTerminalExpressions.empty() && terminalLabels.empty() && negatedTerminalLabels.empty();
+ }
+
+ storm::expressions::Expression TerminalStates::asExpression(std::function<storm::expressions::Expression(std::string const&)> 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..f41413f28
--- /dev/null
+++ b/src/storm/builder/TerminalStatesGetter.h
@@ -0,0 +1,58 @@
+#pragma once
+
+#include <functional>
+#include <string>
+#include <vector>
+
+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<void(storm::expressions::Expression const&, bool)> const& terminalExpressionCallback, std::function<void(std::string const&, bool)> const& terminalLabelCallback);
+
+
+ struct TerminalStates {
+ std::vector<storm::expressions::Expression> terminalExpressions; // if one of these is true, we can stop exploration
+ std::vector<storm::expressions::Expression> negatedTerminalExpressions; // if one of these is false, we can stop exploration
+ std::vector<std::string> terminalLabels; // if a state has one of these labels, we can stop exploration
+ std::vector<std::string> 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
+ */
+ 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<storm::expressions::Expression(std::string const&)> 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
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 [<module>].
if (line.at(0) == '[') {
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
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;
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<ValueType>(result, storm::utility::abs<ValueType>(allValues[value] - *oldValueIt));
+ ++oldValueIt;
}
return result;
}
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);
}
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<class CharT, class Traits, class Allocator>
+ inline std::basic_istream<CharT, Traits>& getline(std::basic_istream<CharT, Traits>& input, std::basic_string<CharT, Traits, Allocator>& 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/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<uint64_t> inversePermutation = {1,4,0,3,2};
storm::storage::SparseMatrix<double> 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
+}
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));
+}