diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h
index 946fb0a97..e82c1fb31 100644
--- a/src/storm/abstraction/MenuGameAbstractor.h
+++ b/src/storm/abstraction/MenuGameAbstractor.h
@@ -48,6 +48,9 @@ namespace storm {
/// Exports a representation of the current abstraction state in the dot format.
virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const = 0;
+ /// Retrieves the number of predicates currently in use.
+ virtual uint64_t getNumberOfPredicates() const = 0;
+
protected:
void exportToDot(storm::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const;
};
diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 642cb83fb..e139a357f 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -390,7 +390,7 @@ namespace storm {
storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract);
- bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
+ bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero() && !lowerChoice1.isZero() && !lowerChoice2.isZero();
if (lowerChoicesDifferent) {
STORM_LOG_TRACE("Deriving predicate based on lower choice.");
predicates = derivePredicatesFromDifferingChoices((pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
@@ -405,7 +405,7 @@ namespace storm {
storm::dd::Bdd<Type> upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract);
storm::dd::Bdd<Type> upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract);
- bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
+ bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero() && !upperChoice1.isZero() && !upperChoice2.isZero();
if (upperChoicesDifferent) {
STORM_LOG_TRACE("Deriving predicate based on upper choice.");
additionalPredicates = derivePredicatesFromDifferingChoices((pivotState && maxPlayer1Strategy).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
@@ -476,12 +476,26 @@ namespace storm {
// Retrieve the variable updates that the predecessor needs to perform to get to the current state.
auto variableUpdates = abstractor.get().getVariableUpdates(std::get<1>(decodedPredecessor), std::get<2>(decodedPredecessor));
- for (auto const& update : variableUpdates) {
- storm::expressions::Variable newVariable = oldToNewVariables.at(update.first);
- if (update.second.hasBooleanType()) {
- predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(oldToNewVariables.at(update.first)), update.second.changeManager(expressionManager).substitute(substitution)));
+ for (auto const& oldNewVariablePair : oldToNewVariables) {
+ storm::expressions::Variable const& newVariable = oldNewVariablePair.second;
+
+ // If the variable was set, use its update expression.
+ auto updateIt = variableUpdates.find(oldNewVariablePair.first);
+ if (updateIt != variableUpdates.end()) {
+ auto const& update = *updateIt;
+
+ if (update.second.hasBooleanType()) {
+ predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(newVariable), update.second.changeManager(expressionManager).substitute(substitution)));
+ } else {
+ predicates.back().push_back(lastSubstitution.at(newVariable) == update.second.changeManager(expressionManager).substitute(substitution));
+ }
} else {
- predicates.back().push_back(lastSubstitution.at(oldToNewVariables.at(update.first)) == update.second.changeManager(expressionManager).substitute(substitution));
+ // Otherwise, make sure that the new variable maintains the old value.
+ if (newVariable.hasBooleanType()) {
+ predicates.back().push_back(storm::expressions::iff(lastSubstitution.at(newVariable), substitution.at(newVariable)));
+ } else {
+ predicates.back().push_back(lastSubstitution.at(newVariable) == substitution.at(newVariable));
+ }
}
}
@@ -581,6 +595,7 @@ namespace storm {
// Redirect all player 1 choices of the min strategy to that of the max strategy if this leads to a player 2
// state that is also a prob 0 state.
+ auto oldMinPlayer1Strategy = minPlayer1Strategy;
minPlayer1Strategy = (maxPlayer1Strategy && qualitativeResult.prob0Min.getPlayer2States()).existsAbstract(game.getPlayer1Variables()).ite(maxPlayer1Strategy, minPlayer1Strategy);
// Compute all reached pivot states.
@@ -597,7 +612,49 @@ namespace storm {
// Now that we have the pivot state candidates, we need to pick one.
PivotStateResult<Type, ValueType> pivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none);
-
+
+// // SANITY CHECK TO MAKE SURE OUR STRATEGIES ARE NOT BROKEN.
+// // FIXME.
+// auto min1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
+// STORM_LOG_ASSERT(!min1ChoiceInPivot.isZero(), "wth?");
+// bool min1ChoiceInPivotIsProb0Min = !(min1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero();
+// bool min1ChoiceInPivotIsProb0Max = !(min1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero();
+// bool min1ChoiceInPivotIsProb1Min = !(min1ChoiceInPivot && qualitativeResult.prob1Min.getPlayer2States()).isZero();
+// bool min1ChoiceInPivotIsProb1Max = !(min1ChoiceInPivot && qualitativeResult.prob1Max.getPlayer2States()).isZero();
+// std::cout << "after redirection (min)" << std::endl;
+// std::cout << "min choice is prob0 in min? " << min1ChoiceInPivotIsProb0Min << ", max? " << min1ChoiceInPivotIsProb0Max << std::endl;
+// std::cout << "min choice is prob1 in min? " << min1ChoiceInPivotIsProb1Min << ", max? " << min1ChoiceInPivotIsProb1Max << std::endl;
+// std::cout << "min" << std::endl;
+// for (auto const& e : (min1ChoiceInPivot && minPlayer2Strategy).template toAdd<ValueType>()) {
+// std::cout << e.first << " -> " << e.second << std::endl;
+// }
+// std::cout << "max" << std::endl;
+// for (auto const& e : (min1ChoiceInPivot && maxPlayer2Strategy).template toAdd<ValueType>()) {
+// std::cout << e.first << " -> " << e.second << std::endl;
+// }
+// bool different = (min1ChoiceInPivot && minPlayer2Strategy) != (min1ChoiceInPivot && maxPlayer2Strategy);
+// std::cout << "min/max choice of player 2 is different? " << different << std::endl;
+// bool min1MinPlayer2Choice = !(min1ChoiceInPivot && minPlayer2Strategy).isZero();
+// bool min1MaxPlayer2Choice = !(min1ChoiceInPivot && maxPlayer2Strategy).isZero();
+// std::cout << "max/min choice there? " << min1MinPlayer2Choice << std::endl;
+// std::cout << "max/max choice there? " << min1MaxPlayer2Choice << std::endl;
+//
+// auto max1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
+// STORM_LOG_ASSERT(!max1ChoiceInPivot.isZero(), "wth?");
+// bool max1ChoiceInPivotIsProb0Min = !(max1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero();
+// bool max1ChoiceInPivotIsProb0Max = !(max1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero();
+// bool max1ChoiceInPivotIsProb1Min = !(max1ChoiceInPivot && qualitativeResult.prob1Min.getPlayer2States()).isZero();
+// bool max1ChoiceInPivotIsProb1Max = !(max1ChoiceInPivot && qualitativeResult.prob1Max.getPlayer2States()).isZero();
+// std::cout << "after redirection (max)" << std::endl;
+// std::cout << "max choice is prob0 in min? " << max1ChoiceInPivotIsProb0Min << ", max? " << max1ChoiceInPivotIsProb0Max << std::endl;
+// std::cout << "max choice is prob1 in min? " << max1ChoiceInPivotIsProb1Min << ", max? " << max1ChoiceInPivotIsProb1Max << std::endl;
+// different = (max1ChoiceInPivot && minPlayer2Strategy) != (max1ChoiceInPivot && maxPlayer2Strategy);
+// std::cout << "min/max choice of player 2 is different? " << different << std::endl;
+// bool max1MinPlayer2Choice = !(max1ChoiceInPivot && minPlayer2Strategy).isZero();
+// bool max1MaxPlayer2Choice = !(max1ChoiceInPivot && maxPlayer2Strategy).isZero();
+// std::cout << "max/min choice there? " << max1MinPlayer2Choice << std::endl;
+// std::cout << "max/max choice there? " << max1MaxPlayer2Choice << std::endl;
+
boost::optional<RefinementPredicates> predicates;
if (useInterpolation) {
predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
index b3c7a755a..a3900ab80 100644
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
@@ -208,6 +208,11 @@ namespace storm {
this->exportToDot(*currentGame, filename, highlightStates, filter);
}
+ template <storm::dd::DdType DdType, typename ValueType>
+ uint64_t JaniMenuGameAbstractor<DdType, ValueType>::getNumberOfPredicates() const {
+ return abstractionInformation.getNumberOfPredicates();
+ }
+
// Explicitly instantiate the class.
template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
index 3a478fcb0..0a4cc36ed 100644
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
+++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h
@@ -109,6 +109,8 @@ namespace storm {
*/
void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
+ virtual uint64_t getNumberOfPredicates() const override;
+
protected:
using MenuGameAbstractor<DdType, ValueType>::exportToDot;
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
index 4cb3d46eb..a93e62e67 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
@@ -203,6 +203,11 @@ namespace storm {
this->exportToDot(*currentGame, filename, highlightStates, filter);
}
+ template <storm::dd::DdType DdType, typename ValueType>
+ uint64_t PrismMenuGameAbstractor<DdType, ValueType>::getNumberOfPredicates() const {
+ return abstractionInformation.getNumberOfPredicates();
+ }
+
// Explicitly instantiate the class.
template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
template class PrismMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
index 49dc8e9dc..931170df9 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
@@ -109,6 +109,8 @@ namespace storm {
*/
virtual void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
+ virtual uint64_t getNumberOfPredicates() const override;
+
protected:
using MenuGameAbstractor<DdType, ValueType>::exportToDot;
diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h
index 357c482b3..4b4d7cb57 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.h
+++ b/src/storm/adapters/MathsatExpressionAdapter.h
@@ -116,6 +116,8 @@ namespace storm {
msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
msat_term rightResult = boost::any_cast<msat_term>(expression.getSecondOperand()->accept(*this, data));
+ msat_term result = leftResult;
+ int_fast64_t exponent;
switch (expression.getOperatorType()) {
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus:
return msat_make_plus(env, leftResult, rightResult);
@@ -124,11 +126,21 @@ namespace storm {
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times:
return msat_make_times(env, leftResult, rightResult);
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide:
- STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unsupported numerical binary operator: '/' (division) in expression.");
+ return msat_make_divide(env, leftResult, rightResult);
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
return msat_make_term_ite(env, msat_make_leq(env, leftResult, rightResult), leftResult, rightResult);
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max:
return msat_make_term_ite(env, msat_make_leq(env, leftResult, rightResult), rightResult, leftResult);
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power:
+ exponent = expression.getSecondOperand()->evaluateAsInt();
+ STORM_LOG_THROW(exponent >= 0, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression with negative exponent.");
+ --exponent;
+ if (exponent > 0) {
+ for (; exponent > 0; --exponent) {
+ result = msat_make_times(env, result, leftResult);
+ }
+ }
+ return result;
default:
STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Cannot evaluate expression: unknown numerical binary operator '" << static_cast<uint_fast64_t>(expression.getOperatorType()) << "' in expression " << expression << ".");
}
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 36af17be0..6a42b6530 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -131,7 +131,7 @@ namespace storm {
std::unique_ptr<CheckResult> result;
if (checkTask.isBoundSet()) {
- // Despite having a bound, we create a quanitative result so that the next layer can perform the comparison.
+ // Despite having a bound, we create a quantitative result so that the next layer can perform the comparison.
if (player2Direction == storm::OptimizationDirection::Minimize) {
if (storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
@@ -361,7 +361,7 @@ namespace storm {
auto abstractionStart = std::chrono::high_resolution_clock::now();
storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
auto abstractionEnd = std::chrono::high_resolution_clock::now();
- STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
+ STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
// (2) Prepare transition matrix BDD and target state BDD for later use.
storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp
index 4835019d4..fd384321f 100644
--- a/src/storm/settings/modules/AbstractionSettings.cpp
+++ b/src/storm/settings/modules/AbstractionSettings.cpp
@@ -25,7 +25,7 @@ namespace storm {
AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "Sets which abstraction-refinement method to use.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of themethod to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods))
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods))
.setDefaultValueString("bisim").build())
.build());