diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 1c1d599a5..4f6ab3871 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -190,18 +190,18 @@ namespace storm {
};
template <storm::dd::DdType Type>
- DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
+ DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <storm::dd::DdType Type>
- DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
+ DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
this->setTerminalStatesFromFormula(formula);
}
template <storm::dd::DdType Type>
- DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
+ DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@@ -221,6 +221,9 @@ namespace storm {
if (terminalStates) {
terminalStates.reset();
}
+ if (negatedTerminalStates) {
+ negatedTerminalStates.reset();
+ }
// If we are not required to build all reward models, we determine the reward models we need to build.
if (!buildAllRewardModels) {
@@ -261,10 +264,16 @@ namespace storm {
this->setTerminalStatesFromFormula(sub);
}
} else if (formula.isUntilFormula()) {
- storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+ 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()) {
@@ -1023,16 +1032,33 @@ namespace storm {
storm::dd::Add<Type> stateActionDd = system.stateActionDd;
// If we were asked to treat some states as terminal states, we cut away their transitions now.
- 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());
- terminalExpression = preparedProgram.getLabelExpression(labelName);
+ if (options.terminalStates || options.negatedTerminalStates) {
+ storm::dd::Add<Type> terminalStatesAdd = generationInfo.manager->getAddZero();
+ 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());
+ terminalExpression = preparedProgram.getLabelExpression(labelName);
+ }
+
+ STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
+ terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
}
- STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
- storm::dd::Add<Type> terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
+ if (options.negatedTerminalStates) {
+ storm::expressions::Expression nonTerminalExpression;
+ if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
+ nonTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+ } else {
+ std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+ nonTerminalExpression = preparedProgram.getLabelExpression(labelName);
+ }
+
+ STORM_LOG_TRACE("Making the states *not* satisfying " << nonTerminalExpression << " terminal.");
+ terminalStatesAdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression);
+ }
+
transitionMatrix *= !terminalStatesAdd;
}
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 20f6e76f0..4669432a8 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -99,9 +99,13 @@ namespace storm {
// An optional set of expressions for which labels need to be built.
boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
- // An optional expression or label that characterizes the terminal states of the model. If this is set,
- // the outgoing transitions of these states are replaced with a self-loop.
+ // An optional expression or label that (a subset of) characterizes 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;
};
/*!
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index cf02700eb..cfc7d8577 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -106,17 +106,17 @@ namespace storm {
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
this->preserveFormula(formula);
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@@ -142,10 +142,16 @@ namespace storm {
this->setTerminalStatesFromFormula(sub);
}
} else if (formula.isUntilFormula()) {
- storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+ 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()) {
@@ -160,6 +166,9 @@ namespace storm {
if (terminalStates) {
terminalStates.reset();
}
+ if (negatedTerminalStates) {
+ negatedTerminalStates.reset();
+ }
// If we are not required to build all reward models, we determine the reward models we need to build.
if (!buildAllRewardModels) {
@@ -932,7 +941,8 @@ namespace storm {
rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards());
}
- // If we were asked to treat some states as terminal states, we cut away their transitions now.
+ // If we were asked to treat some states as terminal states, we determine an expression characterizing the
+ // terminal states of the model that we pass on to the matrix building routine.
boost::optional<storm::expressions::Expression> terminalExpression;
if (options.terminalStates) {
if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
@@ -942,9 +952,27 @@ namespace storm {
terminalExpression = program.getLabelExpression(labelName);
}
}
+ if (options.negatedTerminalStates) {
+ if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
+ if (terminalExpression) {
+ terminalExpression = terminalExpression.get() || !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+ } else {
+ terminalExpression = !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+ }
+ } else {
+ std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
+ if (terminalExpression) {
+ terminalExpression = terminalExpression.get() || !program.getLabelExpression(labelName);
+ } else {
+ terminalExpression = !program.getLabelExpression(labelName);
+ }
+ }
+ }
+ if (terminalExpression) {
+ STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
+ }
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
-
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
// Now finalize all reward models.
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index 313b1652c..1356394d8 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -193,9 +193,13 @@ namespace storm {
// An optional set of expressions for which labels need to be built.
boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
- // An optional expression or label that characterizes the terminal states of the model. If this is set,
- // the outgoing transitions of these states are replaced with a self-loop.
+ // An optional expression or label 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;
};
/*!