diff --git a/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp b/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp new file mode 100644 index 000000000..436234668 --- /dev/null +++ b/src/storm-pars/modelchecker/region/monotonicity/Assumption.cpp @@ -0,0 +1,16 @@ +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" + +#include "storm/utility/macros.h" + +namespace storm { +namespace analysis { + +std::ostream& operator<<(std::ostream& out, Assumption const& assumption) { + STORM_LOG_ASSERT(assumption.relation == storm::expressions::RelationType::Greater || assumption.relation == storm::expressions::RelationType::Equal, + "Only Greater or Equal assumptions are supported."); + out << "s" << assumption.state1 << (assumption.relation == storm::expressions::RelationType::Greater ? " > s" : " = s") << assumption.state2; + return out; +} + +} // namespace analysis +} // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/Assumption.h b/src/storm-pars/modelchecker/region/monotonicity/Assumption.h new file mode 100644 index 000000000..cb14a4187 --- /dev/null +++ b/src/storm-pars/modelchecker/region/monotonicity/Assumption.h @@ -0,0 +1,24 @@ +#pragma once + +#include +#include + +#include "storm/storage/expressions/BinaryRelationType.h" + +namespace storm { +namespace analysis { + +/*! + * A candidate relation between two states of a reachability order: either state1 > state2 + * (Greater) or state1 == state2 (Equal). Only these two relation types are supported. + */ +struct Assumption { + uint64_t state1; + uint64_t state2; + storm::expressions::RelationType relation; +}; + +std::ostream& operator<<(std::ostream& out, Assumption const& assumption); + +} // namespace analysis +} // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp index 3ce3de928..68042435c 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.cpp @@ -9,8 +9,6 @@ #include "storm/solver/Z3SmtSolver.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/RationalFunctionToExpression.h" -#include "storm/storage/expressions/SimpleValuation.h" -#include "storm/storage/expressions/VariableExpression.h" #include "storm/utility/solver.h" namespace storm { @@ -73,22 +71,21 @@ AssumptionChecker::AssumptionChecker(std::shared_ptr -AssumptionStatus AssumptionChecker::validateAssumption(uint_fast64_t val1, uint_fast64_t val2, - std::shared_ptr assumption, - std::shared_ptr order, storage::ParameterRegion region, +AssumptionStatus AssumptionChecker::validateAssumption(Assumption const& assumption, std::shared_ptr order, + storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { // First check if based on sample points the assumption can be discharged - assert(val1 == std::stoull(assumption->getFirstOperand()->asVariableExpression().getVariableName())); - assert(val2 == std::stoull(assumption->getSecondOperand()->asVariableExpression().getVariableName())); AssumptionStatus result = AssumptionStatus::UNKNOWN; if (useSamples) { result = checkOnSamples(assumption); } - assert(result != AssumptionStatus::VALID); + STORM_LOG_ASSERT(result != AssumptionStatus::VALID, "Sample-based checking should never conclude VALID by itself."); if (minValues.size() != 0) { - if (assumption->getRelationType() == expressions::RelationType::Greater) { + auto const val1 = assumption.state1; + auto const val2 = assumption.state2; + if (assumption.relation == expressions::RelationType::Greater) { if (minValues[val1] > maxValues[val2]) { return AssumptionStatus::VALID; } else if (minValues[val1] == maxValues[val2] && minValues[val1] == maxValues[val1] && minValues[val2] == maxValues[val2]) { @@ -109,31 +106,22 @@ AssumptionStatus AssumptionChecker::validateAssumption( if (result == AssumptionStatus::UNKNOWN) { // If result from sample checking was unknown, the assumption might hold - std::set vars = std::set({}); - assumption->gatherVariables(vars); - - STORM_LOG_THROW( - assumption->getRelationType() == expressions::RelationType::Greater || assumption->getRelationType() == expressions::RelationType::Equal, - exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported."); - result = validateAssumptionSMTSolver(val1, val2, assumption, order, region, minValues, maxValues); + STORM_LOG_THROW(assumption.relation == expressions::RelationType::Greater || assumption.relation == expressions::RelationType::Equal, + exceptions::NotSupportedException, "Only Greater Or Equal assumptions supported"); + result = validateAssumptionSMTSolver(assumption, order, region, minValues, maxValues); } return result; } template -AssumptionStatus AssumptionChecker::checkOnSamples(std::shared_ptr assumption) const { +AssumptionStatus AssumptionChecker::checkOnSamples(Assumption const& assumption) const { + STORM_LOG_ASSERT(assumption.relation == expressions::RelationType::Greater || assumption.relation == expressions::RelationType::Equal, + "Only Greater or Equal assumptions are supported."); auto result = AssumptionStatus::UNKNOWN; - std::set vars = std::set({}); - assumption->gatherVariables(vars); - for (auto values : samples) { - auto valuation = expressions::SimpleValuation(assumption->getManager().getSharedPointer()); - for (auto var : vars) { - auto index = std::stoi(var.getName()); - valuation.setRationalValue(var, utility::convertNumber(values[index])); - } - - assert(assumption->hasBooleanType()); - if (!assumption->evaluateAsBool(&valuation)) { + for (auto const& values : samples) { + bool holds = assumption.relation == expressions::RelationType::Greater ? values[assumption.state1] > values[assumption.state2] + : values[assumption.state1] == values[assumption.state2]; + if (!holds) { result = AssumptionStatus::INVALID; break; } @@ -142,19 +130,19 @@ AssumptionStatus AssumptionChecker::checkOnSamples(std: } template -AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver( - uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr assumption, std::shared_ptr order, - storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { - std::shared_ptr smtSolverFactory = std::make_shared(); +AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(Assumption const& assumption, std::shared_ptr order, + storage::ParameterRegion region, + std::vector const minValues, + std::vector const maxValues) const { std::shared_ptr manager(new expressions::ExpressionManager()); AssumptionStatus result = AssumptionStatus::UNKNOWN; - auto var1 = assumption->getFirstOperand()->asVariableExpression().getVariableName(); - auto var2 = assumption->getSecondOperand()->asVariableExpression().getVariableName(); + uint_fast64_t val1 = assumption.state1; + uint_fast64_t val2 = assumption.state2; auto row1 = matrix.getRow(val1); auto row2 = matrix.getRow(val2); bool orderKnown = true; - // if the state with number var1 (var2) occurs in the successors of the state with number var2 (var1) we need to add var1 == expr1 (var2 == expr2) to the + // if the state with number val1 (val2) occurs in the successors of the state with number val2 (val1) we need to add val1 == expr1 (val2 == expr2) to the // bounds bool addVar1 = false; bool addVar2 = false; @@ -165,7 +153,7 @@ AssumptionStatus AssumptionChecker::validateAssumptionS std::set topVariables; std::set bottomVariables; for (auto itr1 = row1.begin(); orderKnown && itr1 != row1.end(); ++itr1) { - addVar2 |= std::to_string(itr1->getColumn()) == var2; + addVar2 |= itr1->getColumn() == val2; auto varname1 = "s" + std::to_string(itr1->getColumn()); if (!manager->hasVariable(varname1)) { if (order->isTopState(itr1->getColumn())) { @@ -178,7 +166,7 @@ AssumptionStatus AssumptionChecker::validateAssumptionS } for (auto itr2 = row2.begin(); orderKnown && itr2 != row2.end(); ++itr2) { - addVar1 |= std::to_string(itr2->getColumn()) == var1; + addVar1 |= itr2->getColumn() == val1; if (itr1->getColumn() != itr2->getColumn()) { auto varname2 = "s" + std::to_string(itr2->getColumn()); if (!manager->hasVariable(varname2)) { @@ -248,10 +236,10 @@ AssumptionStatus AssumptionChecker::validateAssumptionS // It is the negation of actual assumption expressions::Expression exprToCheck; - if (assumption->getRelationType() == expressions::RelationType::Greater) { + if (assumption.relation == expressions::RelationType::Greater) { exprToCheck = expr1 <= expr2; } else { - assert(assumption->getRelationType() == expressions::RelationType::Equal); + STORM_LOG_ASSERT(assumption.relation == expressions::RelationType::Equal, "Only Greater and Equal assumptions are supported."); exprToCheck = expr1 != expr2; } @@ -259,10 +247,10 @@ AssumptionStatus AssumptionChecker::validateAssumptionS // Bounds for the state probabilities and parameters expressions::Expression exprBounds = manager->boolean(true); if (addVar1) { - exprBounds = exprBounds && (manager->getVariable("s" + var1) == expr1); + exprBounds = exprBounds && (manager->getVariable("s" + std::to_string(val1)) == expr1); } if (addVar2) { - exprBounds = exprBounds && (manager->getVariable("s" + var2) == expr2); + exprBounds = exprBounds && (manager->getVariable("s" + std::to_string(val2)) == expr2); } for (auto var : variables) { if (find(stateVariables.begin(), stateVariables.end(), var) != stateVariables.end()) { @@ -297,7 +285,6 @@ AssumptionStatus AssumptionChecker::validateAssumptionS if (s.check() == solver::SmtSolver::CheckResult::Unsat) { return AssumptionStatus::INVALID; } - assert(s.check() != solver::SmtSolver::CheckResult::Unsat); s.add(exprToCheck); auto smtRes = s.check(); @@ -312,13 +299,10 @@ AssumptionStatus AssumptionChecker::validateAssumptionS } template -AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, - std::shared_ptr order, +AssumptionStatus AssumptionChecker::validateAssumption(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region) const { - auto var1 = std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()); - auto var2 = std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()); std::vector vals; - return validateAssumption(var1, var2, assumption, order, region, vals, vals); + return validateAssumption(assumption, order, region, vals, vals); } template class AssumptionChecker; diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h index 3d7bf0408..255ac2e21 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h @@ -1,13 +1,14 @@ #pragma once -#include "Order.h" -#include "storm-pars/storage/ParameterRegion.h" #include "storm/environment/Environment.h" #include "storm/logic/Formula.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" + +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" +#include "storm-pars/modelchecker/region/monotonicity/Order.h" +#include "storm-pars/storage/ParameterRegion.h" namespace storm { namespace analysis { @@ -69,11 +70,9 @@ class AssumptionChecker { * @param region The region of the considered model. * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID */ - AssumptionStatus validateAssumption(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr assumption, - std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, - std::vector const maxValue) const; - AssumptionStatus validateAssumption(std::shared_ptr assumption, std::shared_ptr order, - storage::ParameterRegion region) const; + AssumptionStatus validateAssumption(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region, + std::vector const minValues, std::vector const maxValue) const; + AssumptionStatus validateAssumption(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region) const; private: bool useSamples; @@ -82,11 +81,10 @@ class AssumptionChecker { storage::SparseMatrix matrix; - AssumptionStatus validateAssumptionSMTSolver(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr assumption, - std::shared_ptr order, storage::ParameterRegion region, + AssumptionStatus validateAssumptionSMTSolver(Assumption const& assumption, std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, std::vector const maxValue) const; - AssumptionStatus checkOnSamples(std::shared_ptr assumption) const; + AssumptionStatus checkOnSamples(Assumption const& assumption) const; }; } // namespace analysis } // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp index 135450a0b..ef3b1000b 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.cpp @@ -6,15 +6,11 @@ namespace storm { namespace analysis { template AssumptionMaker::AssumptionMaker(storage::SparseMatrix matrix) : assumptionChecker(matrix) { - numberOfStates = matrix.getColumnCount(); - expressionManager = std::make_shared(expressions::ExpressionManager()); - for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { - expressionManager->declareRationalVariable(std::to_string(i)); - } + // Intentionally left empty. } template -std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumptions( +std::vector> AssumptionMaker::createAndCheckAssumptions( uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region) const { auto vec1 = std::vector(); auto vec2 = std::vector(); @@ -22,49 +18,51 @@ std::map, AssumptionStatu } template -std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumptions( +std::vector> AssumptionMaker::createAndCheckAssumptions( uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { - std::map, AssumptionStatus> result; + std::vector> result; STORM_LOG_INFO("Creating assumptions for " << val1 << " and " << val2); - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); auto assumption = createAndCheckAssumption(val1, val2, expressions::RelationType::Greater, order, region, minValues, maxValues); if (assumption.second != AssumptionStatus::INVALID) { - result.insert(assumption); + result.push_back(assumption); if (assumption.second == AssumptionStatus::VALID) { - assert(createAndCheckAssumption(val2, val1, expressions::RelationType::Greater, order, region, minValues, maxValues).second != - AssumptionStatus::VALID && - createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != - AssumptionStatus::VALID); + STORM_LOG_ASSERT(createAndCheckAssumption(val2, val1, expressions::RelationType::Greater, order, region, minValues, maxValues).second != + AssumptionStatus::VALID && + createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != + AssumptionStatus::VALID, + "At most one of the three candidate assumptions may be valid."); STORM_LOG_INFO("Assumption " << assumption.first << "is valid\n"); return result; } } - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); assumption = createAndCheckAssumption(val2, val1, expressions::RelationType::Greater, order, region, minValues, maxValues); if (assumption.second != AssumptionStatus::INVALID) { if (assumption.second == AssumptionStatus::VALID) { result.clear(); - result.insert(assumption); - assert(createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != - AssumptionStatus::VALID); + result.push_back(assumption); + STORM_LOG_ASSERT( + createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues).second != AssumptionStatus::VALID, + "At most one of the three candidate assumptions may be valid."); STORM_LOG_INFO("Assumption " << assumption.first << "is valid\n"); return result; } - result.insert(assumption); + result.push_back(assumption); } - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); assumption = createAndCheckAssumption(val1, val2, expressions::RelationType::Equal, order, region, minValues, maxValues); if (assumption.second != AssumptionStatus::INVALID) { if (assumption.second == AssumptionStatus::VALID) { result.clear(); - result.insert(assumption); + result.push_back(assumption); STORM_LOG_INFO("Assumption " << assumption.first << "is valid\n"); return result; } - result.insert(assumption); + result.push_back(assumption); } - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); STORM_LOG_INFO("None of the assumptions is valid, number of possible assumptions: " << result.size() << '\n'); return result; } @@ -82,17 +80,13 @@ void AssumptionMaker::setSampleValues(std::vector -std::pair, AssumptionStatus> AssumptionMaker::createAndCheckAssumption( +std::pair AssumptionMaker::createAndCheckAssumption( uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, std::shared_ptr order, storage::ParameterRegion region, std::vector const minValues, std::vector const maxValues) const { - assert(val1 != val2); - expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); - expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); - auto assumption = std::make_shared( - expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), var1.getExpression().getBaseExpressionPointer(), - var2.getExpression().getBaseExpressionPointer(), relationType)); - AssumptionStatus validationResult = assumptionChecker.validateAssumption(val1, val2, assumption, order, region, minValues, maxValues); - return std::pair, AssumptionStatus>(assumption, validationResult); + STORM_LOG_ASSERT(val1 != val2, "An assumption must relate two distinct states."); + Assumption assumption{val1, val2, relationType}; + AssumptionStatus validationResult = assumptionChecker.validateAssumption(assumption, order, region, minValues, maxValues); + return {assumption, validationResult}; } template class AssumptionMaker; diff --git a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h index d261cea62..09ca0b9ba 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h +++ b/src/storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h @@ -1,19 +1,17 @@ #pragma once -#include "AssumptionChecker.h" -#include "Order.h" - #include "storm/storage/SparseMatrix.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/BinaryRelationType.h" + +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" +#include "storm-pars/modelchecker/region/monotonicity/AssumptionChecker.h" +#include "storm-pars/modelchecker/region/monotonicity/Order.h" namespace storm { namespace analysis { template class AssumptionMaker { - typedef std::shared_ptr AssumptionType; - public: /*! * Constructs AssumptionMaker based on the matrix of the model. @@ -31,13 +29,15 @@ class AssumptionMaker { * @param val2 Second state number. * @param order The order on which the assumptions are checked. * @param region The region for the parameters. - * @return Map with at most three assumptions, and the validation. + * @return At most three (assumption, status) candidates, in the order they were tried + * (val1 > val2, val2 > val1, val1 == val2). */ - std::map, AssumptionStatus> createAndCheckAssumptions( - uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region) const; - std::map, AssumptionStatus> createAndCheckAssumptions( - uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, storage::ParameterRegion region, - std::vector const minValues, std::vector const maxValue) const; + std::vector> createAndCheckAssumptions(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, + storage::ParameterRegion region) const; + std::vector> createAndCheckAssumptions(uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr order, + storage::ParameterRegion region, + std::vector const minValues, + std::vector const maxValue) const; /*! * Initializes the given number of sample points for a given model, formula and region. @@ -58,15 +58,11 @@ class AssumptionMaker { void setSampleValues(std::vector> const& samples); private: - std::pair, AssumptionStatus> createAndCheckAssumption( - uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, std::shared_ptr order, - storage::ParameterRegion region, std::vector const minValues, std::vector const maxValue) const; + std::pair createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, expressions::RelationType relationType, + std::shared_ptr order, storage::ParameterRegion region, + std::vector const minValues, std::vector const maxValue) const; AssumptionChecker assumptionChecker; - - std::shared_ptr expressionManager; - - uint_fast64_t numberOfStates; }; } // namespace analysis } // namespace storm diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp index d5d708909..65c8e04c6 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp @@ -62,7 +62,7 @@ MonotonicityHelper::MonotonicityHelper(std::shared_ptr< checkSamples = false; } - this->extender = new analysis::OrderExtender(model, formulas[0]); + this->extender = std::make_unique>(model, formulas[0]); for (uint_fast64_t i = 0; i < matrix.getRowCount(); ++i) { std::set occurringVariables; @@ -78,8 +78,8 @@ MonotonicityHelper::MonotonicityHelper(std::shared_ptr< /*** Public methods ***/ template -std::map, std::pair::VariableType>>, - std::vector>>> +std::map, + std::pair::VariableType>>, std::vector>> MonotonicityHelper::checkMonotonicityInBuild(std::ostream& outfile, bool usePLA, std::string dotOutfileName) { if (usePLA) { storm::utility::Stopwatch plaWatch(true); @@ -111,7 +111,7 @@ MonotonicityHelper::checkMonotonicityInBuild(std::ostre << " "; first = false; } - outfile << *assumption; + outfile << assumption; } if (!first) { outfile << '\n'; @@ -178,21 +178,13 @@ void MonotonicityHelper::createOrder() { auto monRes = std::make_shared>(MonotonicityResult()); criticalTuple = extender->toOrder(region, monRes); // Continue based on not (yet) sorted states - std::map, std::vector>> result; - auto val1 = std::get<1>(criticalTuple); auto val2 = std::get<2>(criticalTuple); auto numberOfStates = model->getNumberOfStates(); - std::vector> assumptions; + std::vector assumptions; if (val1 == numberOfStates && val2 == numberOfStates) { - auto resAssumptionPair = - std::pair>, std::vector>>(monRes, - assumptions); - monResults.insert( - std::pair, - std::pair>, std::vector>>>( - std::get<0>(criticalTuple), resAssumptionPair)); + monResults.insert({std::get<0>(criticalTuple), {monRes, assumptions}}); } else if (val1 != numberOfStates && val2 != numberOfStates) { extendOrderWithAssumptions(std::get<0>(criticalTuple), val1, val2, assumptions, monRes); } else { @@ -202,74 +194,87 @@ void MonotonicityHelper::createOrder() { template void MonotonicityHelper::extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, - std::vector> assumptions, + std::vector assumptions, std::shared_ptr> monRes) { - std::map, std::vector>> result; - if (order->isInvalid()) { - // We don't add anything as the order we created with assumptions turns out to be invalid - STORM_LOG_INFO(" The order was invalid, so we stop here"); - return; - } - auto numberOfStates = model->getNumberOfStates(); - if (val1 == numberOfStates || val2 == numberOfStates) { - assert(val1 == val2); - assert(order->getNumberOfAddedStates() == order->getNumberOfStates()); - auto resAssumptionPair = - std::pair>, std::vector>>(monRes, - assumptions); - monResults.insert( - std::pair, - std::pair>, std::vector>>>( - std::move(order), std::move(resAssumptionPair))); - } else { + // Algorithm 2 spawns up to three branches per unresolved (val1, val2) pair, one per candidate + // assumption. The worklist keeps this iterative so that pMCs chaining many such ambiguities + // cannot overflow the call stack. Branches are pushed in reverse so popping (LIFO) visits + // them depth-first, left to right. + struct PendingBranch { + std::shared_ptr order; + uint_fast64_t val1; + uint_fast64_t val2; + std::vector assumptions; + std::shared_ptr> monRes; + }; + std::vector worklist; + worklist.push_back({std::move(order), val1, val2, std::move(assumptions), std::move(monRes)}); + + auto const numberOfStates = model->getNumberOfStates(); + while (!worklist.empty()) { + PendingBranch current = std::move(worklist.back()); + worklist.pop_back(); + + if (current.order->isInvalid()) { + // We don't add anything as the order we created with assumptions turns out to be invalid + STORM_LOG_INFO(" The order was invalid, so we stop here"); + continue; + } + if (current.val1 == numberOfStates || current.val2 == numberOfStates) { + assert(current.val1 == current.val2); + assert(current.order->getNumberOfAddedStates() == current.order->getNumberOfStates()); + monResults.insert({current.order, {current.monRes, current.assumptions}}); + continue; + } + // Make the three assumptions - STORM_LOG_INFO("Creating assumptions for " << val1 << " and " << val2 << ". "); - auto newAssumptions = assumptionMaker.createAndCheckAssumptions(val1, val2, order, region); + STORM_LOG_INFO("Creating assumptions for " << current.val1 << " and " << current.val2 << ". "); + auto newAssumptions = assumptionMaker.createAndCheckAssumptions(current.val1, current.val2, current.order, region); assert(newAssumptions.size() <= 3); - auto itr = newAssumptions.begin(); - if (newAssumptions.size() == 0) { - monRes = std::make_shared>(MonotonicityResult()); + + if (newAssumptions.empty()) { + auto fallbackMonRes = std::make_shared>(MonotonicityResult()); for (auto& entry : occuringStatesAtVariable) { for (auto& state : entry.second) { - extender->checkParOnStateMonRes(state, order, entry.first, monRes); - if (monRes->getMonotonicity(entry.first) == Monotonicity::Unknown) { + extender->checkParOnStateMonRes(state, current.order, entry.first, fallbackMonRes); + if (fallbackMonRes->getMonotonicity(entry.first) == Monotonicity::Unknown) { break; } } - monRes->setDoneForVar(entry.first); + fallbackMonRes->setDoneForVar(entry.first); } - monResults.insert({order, {monRes, assumptions}}); + monResults.insert({current.order, {fallbackMonRes, current.assumptions}}); STORM_LOG_INFO(" None of the assumptions were valid, we stop exploring the current order"); - } else { - STORM_LOG_INFO(" Created " << newAssumptions.size() << " assumptions, we continue extending the current order"); + continue; } + STORM_LOG_INFO(" Created " << newAssumptions.size() << " assumptions, we continue extending the current order"); - while (itr != newAssumptions.end()) { - auto assumption = *itr; - ++itr; - if (assumption.second != AssumptionStatus::INVALID) { - if (itr != newAssumptions.end()) { - // We make a copy of the order and the assumptions - auto orderCopy = order->copy(); - auto assumptionsCopy = std::vector>(assumptions); - auto monResCopy = monRes->copy(); - - if (assumption.second == AssumptionStatus::UNKNOWN) { - // only add assumption to the set of assumptions if it is unknown whether it holds or not - assumptionsCopy.push_back(std::move(assumption.first)); - } - auto criticalTuple = extender->extendOrder(orderCopy, region, monResCopy, assumption.first); - extendOrderWithAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptionsCopy, monResCopy); - } else { - // It is the last one, so we don't need to create a copy. - if (assumption.second == AssumptionStatus::UNKNOWN) { - // only add assumption to the set of assumptions if it is unknown whether it holds or not - assumptions.push_back(std::move(assumption.first)); - } - auto criticalTuple = extender->extendOrder(order, region, monRes, assumption.first); - extendOrderWithAssumptions(std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions, monRes); - } + // Candidates 0..size-2 each get an independent copy of current.order/monRes, so extending + // one cannot affect another; the last candidate reuses current.order/monRes in place. + // That in-place mutation must happen last, after every other candidate has already taken + // its copy from the still-pristine original. + std::vector preparedBranches; + preparedBranches.reserve(newAssumptions.size()); + for (size_t i = 0; i < newAssumptions.size(); ++i) { + auto const& assumption = newAssumptions[i]; + bool const isLastCandidate = (i == newAssumptions.size() - 1); + + std::shared_ptr branchOrder = isLastCandidate ? current.order : current.order->copy(); + std::shared_ptr> branchMonRes = isLastCandidate ? current.monRes : current.monRes->copy(); + std::vector branchAssumptions = current.assumptions; + + if (assumption.second == AssumptionStatus::UNKNOWN) { + // only add assumption to the set of assumptions if it is unknown whether it holds or not + branchAssumptions.push_back(assumption.first); } + auto criticalTuple = extender->extendOrder(branchOrder, region, branchMonRes, assumption.first); + preparedBranches.push_back( + {std::get<0>(criticalTuple), std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::move(branchAssumptions), branchMonRes}); + } + // Pushed in reverse so the first-prepared branch ends up on top of the stack and is + // explored first, i.e., depth-first, left to right. + for (auto it = preparedBranches.rbegin(); it != preparedBranches.rend(); ++it) { + worklist.push_back(std::move(*it)); } } } diff --git a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h index 07d2eadbf..0142b6cae 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h +++ b/src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h @@ -1,11 +1,6 @@ #pragma once #include -#include "AssumptionMaker.h" -#include "LocalMonotonicityResult.h" -#include "MonotonicityResult.h" -#include "Order.h" -#include "OrderExtender.h" #include "storm/logic/Formula.h" @@ -16,13 +11,18 @@ #include "storm/solver/Z3SmtSolver.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/RationalFunctionToExpression.h" #include "storm/utility/constants.h" #include "storm-pars/api/region.h" +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" +#include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h" +#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h" +#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" +#include "storm-pars/modelchecker/region/monotonicity/Order.h" +#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" namespace storm { namespace analysis { @@ -57,47 +57,7 @@ class MonotonicityHelper { * @return pair of bools, >= 0 and <= 0 */ static std::pair checkDerivative(ValueType derivative, storage::ParameterRegion reg) { - bool monIncr = false; - bool monDecr = false; - - if (derivative.isZero()) { - monIncr = true; - monDecr = true; - } else if (derivative.isConstant()) { - monIncr = derivative.constantPart() >= 0; - monDecr = derivative.constantPart() <= 0; - } else { - std::shared_ptr smtSolverFactory = std::make_shared(); - std::shared_ptr manager(new expressions::ExpressionManager()); - solver::Z3SmtSolver s(*manager); - std::set variables = derivative.gatherVariables(); - - expressions::Expression exprBounds = manager->boolean(true); - for (auto variable : variables) { - auto managerVariable = manager->declareRationalVariable(variable.name()); - auto lb = utility::convertNumber(reg.getLowerBoundary(variable)); - auto ub = utility::convertNumber(reg.getUpperBoundary(variable)); - exprBounds = exprBounds && manager->rational(lb) < managerVariable && managerVariable < manager->rational(ub); - } - - auto converter = expressions::RationalFunctionToExpression(manager); - - // < 0, so not monotone increasing. If this is unsat, then it should be monotone increasing. - expressions::Expression exprToCheck = converter.toExpression(derivative) < manager->rational(0); - s.add(exprBounds); - s.add(exprToCheck); - monIncr = s.check() == solver::SmtSolver::CheckResult::Unsat; - - // > 0, so not monotone decreasing. If this is unsat it should be monotone decreasing. - exprToCheck = converter.toExpression(derivative) > manager->rational(0); - s.reset(); - s.add(exprBounds); - s.add(exprToCheck); - monDecr = s.check() == solver::SmtSolver::CheckResult::Unsat; - } - assert(!(monIncr && monDecr) || derivative.isZero()); - - return std::pair(monIncr, monDecr); + return MonotonicityChecker::checkDerivative(derivative, reg); } /*! @@ -107,9 +67,8 @@ class MonotonicityHelper { * @param dotOutfileName Name for the files of the dot outputs should they be generated * @return Map which maps each order to its Reachability Order and used assumptions. */ - std::map, - std::pair>, std::vector>>> - checkMonotonicityInBuild(std::ostream& outfile, bool usePLA = false, std::string dotOutfileName = "dotOutput"); + std::map, std::pair>, std::vector>> checkMonotonicityInBuild( + std::ostream& outfile, bool usePLA = false, std::string dotOutfileName = "dotOutput"); /*! * Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity. @@ -125,8 +84,7 @@ class MonotonicityHelper { void checkMonotonicityOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); - void extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, - std::vector> assumptions, + void extendOrderWithAssumptions(std::shared_ptr order, uint_fast64_t val1, uint_fast64_t val2, std::vector assumptions, std::shared_ptr> monRes); std::shared_ptr model; @@ -143,11 +101,9 @@ class MonotonicityHelper { std::map> occuringStatesAtVariable; - std::map, - std::pair>, std::vector>>> - monResults; + std::map, std::pair>, std::vector>> monResults; - OrderExtender* extender; + std::unique_ptr> extender; ConstantType precision; diff --git a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp index 6cdc09fa5..a0446859c 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Order.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/Order.cpp @@ -27,8 +27,9 @@ Order::Order(storm::storage::BitVector const& topStates, storm::storage::BitVect this->nodes[i] = bottom; numberOfAddedStates++; } - assert(numberOfAddedStates <= numberOfStates); - assert(doneStates.getNumberOfSetBits() == (topStates.getNumberOfSetBits() + bottomStates.getNumberOfSetBits())); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); + STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == (topStates.getNumberOfSetBits() + bottomStates.getNumberOfSetBits()), + "Number of done states does not match the number of given top and bottom states."); if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } @@ -50,10 +51,10 @@ Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t nu this->bottom->states.insert(bottomState); this->nodes[bottomState] = bottom; this->numberOfAddedStates = 2; - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); this->statesSorted = statesSorted; - assert(doneStates.getNumberOfSetBits() == 2); + STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == 2, "Expected exactly the given top and bottom state to be done."); if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } @@ -63,10 +64,70 @@ Order::Order() { this->invalid = false; } +Order::Order(Order const& other) + : invalid(other.invalid), + doneBuilding(other.doneBuilding), + onlyBottomTopOrder(other.onlyBottomTopOrder), + doneStates(other.doneStates), + trivialStates(other.trivialStates), + nodes(other.numberOfStates, nullptr), + statesToHandle(other.statesToHandle), + top(nullptr), + bottom(nullptr), + numberOfStates(other.numberOfStates), + numberOfAddedStates(other.numberOfAddedStates), + statesSorted(other.statesSorted) { + storm::storage::BitVector seenStates(numberOfStates, false); + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + Node* oldNode = other.nodes.at(state); + if (oldNode != nullptr && !seenStates[*(oldNode->states.begin())]) { + Node* newNode = allocateNode(); + if (oldNode == other.top) { + top = newNode; + } else if (oldNode == other.bottom) { + bottom = newNode; + } + newNode->statesAbove = oldNode->statesAbove; + for (auto const& i : oldNode->states) { + newNode->states.insert(i); + seenStates.set(i); + nodes[i] = newNode; + } + } + } +} + +Order& Order::operator=(Order other) { + swap(*this, other); + return *this; +} + +void swap(Order& first, Order& second) noexcept { + using std::swap; + swap(first.invalid, second.invalid); + swap(first.doneBuilding, second.doneBuilding); + swap(first.onlyBottomTopOrder, second.onlyBottomTopOrder); + swap(first.doneStates, second.doneStates); + swap(first.trivialStates, second.trivialStates); + swap(first.nodes, second.nodes); + swap(first.nodeStorage, second.nodeStorage); + swap(first.statesToHandle, second.statesToHandle); + swap(first.top, second.top); + swap(first.bottom, second.bottom); + swap(first.numberOfStates, second.numberOfStates); + swap(first.numberOfAddedStates, second.numberOfAddedStates); + swap(first.statesSorted, second.statesSorted); +} + +Order::Node* Order::allocateNode() { + nodeStorage.push_back(std::make_unique()); + return nodeStorage.back().get(); +} + /*** Modifying the order ***/ void Order::add(uint_fast64_t state) { - assert(nodes[state] == nullptr); + STORM_LOG_ASSERT(nodes[state] == nullptr, "State " << state << " is already in the order."); addBetween(state, top, bottom); addStateToHandle(state); } @@ -74,8 +135,8 @@ void Order::add(uint_fast64_t state) { void Order::addAbove(uint_fast64_t state, Node* node) { STORM_LOG_INFO("Add " << state << " above " << *node->states.begin() << '\n'); - assert(nodes[state] == nullptr); - Node* newNode = new Node(); + STORM_LOG_ASSERT(nodes[state] == nullptr, "State " << state << " is already in the order."); + Node* newNode = allocateNode(); nodes[state] = newNode; newNode->states.insert(state); @@ -94,8 +155,8 @@ void Order::addAbove(uint_fast64_t state, Node* node) { void Order::addBelow(uint_fast64_t state, Node* node) { STORM_LOG_INFO("Add " << state << " below " << *node->states.begin() << '\n'); - assert(nodes[state] == nullptr); - Node* newNode = new Node(); + STORM_LOG_ASSERT(nodes[state] == nullptr, "State " << state << " is already in the order."); + Node* newNode = allocateNode(); nodes[state] = newNode; newNode->states.insert(state); newNode->statesAbove = storm::storage::BitVector((node->statesAbove)); @@ -108,17 +169,17 @@ void Order::addBelow(uint_fast64_t state, Node* node) { if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); } void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { STORM_LOG_INFO("Add " << state << " between (above) " << *above->states.begin() << " and " << *below->states.begin() << '\n'); - assert(compare(above, below) == ABOVE); - assert(above != nullptr && below != nullptr); + STORM_LOG_ASSERT(compare(above, below) == ABOVE, "Expected the first node/state to be above the second."); + STORM_LOG_ASSERT(above != nullptr && below != nullptr, "Both nodes must exist."); if (nodes[state] == nullptr) { // State is not in the order yet - Node* newNode = new Node(); + Node* newNode = allocateNode(); nodes[state] = newNode; newNode->states.insert(state); @@ -132,7 +193,7 @@ void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); } else { // State is in the order already, so we add the new relations addRelationNodes(above, nodes[state]); @@ -141,20 +202,19 @@ void Order::addBetween(uint_fast64_t state, Node* above, Node* below) { } void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { - assert(compare(above, below) == ABOVE); - assert(getNode(below)->states.find(below) != getNode(below)->states.end()); - assert(getNode(above)->states.find(above) != getNode(above)->states.end()); + STORM_LOG_ASSERT(getNode(below)->states.find(below) != getNode(below)->states.end(), "State " << below << " is not in its own node."); + STORM_LOG_ASSERT(getNode(above)->states.find(above) != getNode(above)->states.end(), "State " << above << " is not in its own node."); addBetween(state, getNode(above), getNode(below)); } void Order::addRelation(uint_fast64_t above, uint_fast64_t below, bool allowMerge) { - assert(getNode(above) != nullptr && getNode(below) != nullptr); + STORM_LOG_ASSERT(getNode(above) != nullptr && getNode(below) != nullptr, "Both states must already be in the order."); addRelationNodes(getNode(above), getNode(below), allowMerge); } void Order::addRelationNodes(Order::Node* above, Order::Node* below, bool allowMerge) { - assert(allowMerge || compare(above, below) != BELOW); + STORM_LOG_ASSERT(allowMerge || compare(above, below) != BELOW, "The first node/state is already known to be below the second."); STORM_LOG_INFO("Add relation between (above) " << *above->states.begin() << " and " << *below->states.begin() << '\n'); @@ -168,7 +228,7 @@ void Order::addRelationNodes(Order::Node* above, Order::Node* below, bool allowM for (auto const& state : above->states) { below->statesAbove.set(state); } - assert(compare(above, below) == ABOVE); + STORM_LOG_ASSERT(compare(above, below) == ABOVE, "Expected the first node/state to be above the second."); } void Order::addToNode(uint_fast64_t state, Node* node) { @@ -182,7 +242,7 @@ void Order::addToNode(uint_fast64_t state, Node* node) { if (numberOfAddedStates == numberOfStates) { doneBuilding = doneStates.full(); } - assert(numberOfAddedStates <= numberOfStates); + STORM_LOG_ASSERT(numberOfAddedStates <= numberOfStates, "More states were added to the order than it has room for."); } else { // State is in the order already, so we merge the nodes @@ -216,7 +276,13 @@ bool Order::mergeNodes(storm::analysis::Order::Node* node1, storm::analysis::Ord } } for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + if (nodes[i] == nullptr) { + continue; + } for (uint_fast64_t j = i + 1; j < numberOfStates; ++j) { + if (nodes[j] == nullptr) { + continue; + } auto comp1 = compare(i, j); auto comp2 = compare(j, i); if (!((comp1 == BELOW && comp2 == ABOVE) || (comp1 == ABOVE && comp2 == BELOW) || (comp1 == UNKNOWN && comp2 == UNKNOWN) || @@ -272,7 +338,9 @@ Order::NodeComparison Order::compare(Node* node1, Node* node2, NodeComparison hy return comp; } if ((hypothesis == UNKNOWN || hypothesis == ABOVE) && above(node1, node2)) { - assert(!above(node2, node1)); + // This does not require !above(node2, node1): mergeNodes calls compare() on every + // pair in both directions to detect exactly that antisymmetry violation and reject + // the merge, so this function must tolerate it transiently rather than fail here. return ABOVE; } @@ -296,7 +364,8 @@ Order::Node* Order::getBottom() const { } bool Order::getDoneBuilding() const { - assert(!doneStates.full() || numberOfAddedStates == numberOfStates); + STORM_LOG_ASSERT(!doneStates.full() || numberOfAddedStates == numberOfStates, + "All states are marked done, but not all states have been added to the order."); return doneStates.full(); } @@ -344,7 +413,7 @@ bool Order::isOnlyBottomTopOrder() const { } std::vector Order::sortStates(std::vector* states) { - assert(states != nullptr); + STORM_LOG_ASSERT(states != nullptr, "States to sort must be given."); uint_fast64_t numberOfStatesToSort = states->size(); std::vector result; // Go over all states @@ -377,7 +446,7 @@ std::vector Order::sortStates(std::vector* states) while (result.size() < numberOfStatesToSort) { result.push_back(numberOfStates); } - assert(result.size() == numberOfStatesToSort); + STORM_LOG_ASSERT(result.size() == numberOfStatesToSort, "Not all states could be sorted (or padded with the sentinel value)."); return result; } @@ -425,17 +494,18 @@ std::pair, std::vector> O } } if (!unknown && oneUnknown) { - assert(statesSorted.size() == states.size()); + STORM_LOG_ASSERT(statesSorted.size() == states.size(), "Expected all but the single unresolved state to have been sorted."); s2 = numberOfStates; } - assert(s1 == numberOfStates || (s1 != numberOfStates && s2 == numberOfStates && statesSorted.size() == states.size()) || - (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size())); + STORM_LOG_ASSERT(s1 == numberOfStates || (s1 != numberOfStates && s2 == numberOfStates && statesSorted.size() == states.size()) || + (s1 != numberOfStates && s2 != numberOfStates && statesSorted.size() < states.size()), + "Inconsistent result: (s1, s2) and the number of sorted states must agree on how far sorting got."); return {{s1, s2}, statesSorted}; } std::pair, std::vector> Order::sortStatesUnorderedPair(const std::vector* states) { - assert(states != nullptr); + STORM_LOG_ASSERT(states != nullptr, "States to sort must be given."); [[maybe_unused]] uint_fast64_t numberOfStatesToSort = states->size(); std::vector result; // Go over all states @@ -465,7 +535,7 @@ std::pair, std::vector> O } } - assert(result.size() == numberOfStatesToSort); + STORM_LOG_ASSERT(result.size() == numberOfStatesToSort, "Not all states could be sorted."); return {{numberOfStates, numberOfStates}, std::move(result)}; } @@ -502,54 +572,15 @@ std::vector Order::sortStates(storm::storage::BitVector* states) while (result.size() < numberOfStatesToSort) { result.push_back(numberOfStates); } - assert(result.size() == numberOfStatesToSort); + STORM_LOG_ASSERT(result.size() == numberOfStatesToSort, "Not all states could be sorted (or padded with the sentinel value)."); return result; } /*** Checking on helpfunctionality for building of order ***/ std::shared_ptr Order::copy() const { - assert(!isInvalid()); - std::shared_ptr copiedOrder = std::make_shared(); - copiedOrder->nodes = std::vector(numberOfStates, nullptr); - copiedOrder->onlyBottomTopOrder = this->isOnlyBottomTopOrder(); - copiedOrder->numberOfStates = this->getNumberOfStates(); - copiedOrder->statesSorted = std::vector(this->statesSorted); - copiedOrder->statesToHandle = std::vector(this->statesToHandle); - copiedOrder->trivialStates = storm::storage::BitVector(trivialStates); - copiedOrder->doneStates = storm::storage::BitVector(doneStates); - copiedOrder->numberOfAddedStates = this->numberOfAddedStates; - copiedOrder->doneBuilding = this->doneBuilding; - - auto seenStates = storm::storage::BitVector(numberOfStates, false); - // copy nodes - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - Node* oldNode = nodes.at(state); - if (oldNode != nullptr) { - if (!seenStates[*(oldNode->states.begin())]) { - Node* newNode = new Node(); - if (oldNode == this->getTop()) { - copiedOrder->top = newNode; - } else if (oldNode == this->getBottom()) { - copiedOrder->bottom = newNode; - } - newNode->statesAbove = storm::storage::BitVector(oldNode->statesAbove); - for (size_t i = 0; i < oldNode->statesAbove.size(); ++i) { - assert(newNode->statesAbove[i] == oldNode->statesAbove[i]); - } - for (auto const& i : oldNode->states) { - assert(!seenStates[i]); - newNode->states.insert(i); - seenStates.set(i); - copiedOrder->nodes[i] = newNode; - } - } - } else { - assert(copiedOrder->nodes[state] == nullptr); - } - } - - return copiedOrder; + STORM_LOG_ASSERT(!isInvalid(), "Cannot copy an invalid order."); + return std::make_shared(*this); } /*** Setters ***/ @@ -657,7 +688,7 @@ void Order::init(uint_fast64_t numberOfStates, storage::Decompositioninvalid = false; this->nodes = std::vector(numberOfStates, nullptr); this->doneStates = storm::storage::BitVector(numberOfStates, false); - assert(doneStates.getNumberOfSetBits() == 0); + STORM_LOG_ASSERT(doneStates.getNumberOfSetBits() == 0, "A freshly initialized order must not have any done states yet."); if (decomposition.size() == 0) { this->trivialStates = storm::storage::BitVector(numberOfStates, true); } else { @@ -668,8 +699,8 @@ void Order::init(uint_fast64_t numberOfStates, storage::Decompositiontop = new Node(); - this->bottom = new Node(); + this->top = allocateNode(); + this->bottom = allocateNode(); this->top->statesAbove = storm::storage::BitVector(numberOfStates, false); this->bottom->statesAbove = storm::storage::BitVector(numberOfStates, false); this->doneBuilding = doneBuilding; @@ -763,7 +794,7 @@ std::pair Order::getNextStateNumber() { } std::pair Order::getStateToHandle() { - assert(existsStateToHandle()); + STORM_LOG_ASSERT(existsStateToHandle(), "No state to handle exists."); auto state = statesToHandle.back(); statesToHandle.pop_back(); return {state, false}; diff --git a/src/storm-pars/modelchecker/region/monotonicity/Order.h b/src/storm-pars/modelchecker/region/monotonicity/Order.h index 1a6334981..cf25c1126 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/Order.h +++ b/src/storm-pars/modelchecker/region/monotonicity/Order.h @@ -57,6 +57,18 @@ class Order { */ Order(); + /*! + * Constructs a deep copy of the given Order. Every Node is reallocated; no state is shared + * with other. + */ + Order(Order const& other); + + Order(Order&&) noexcept = default; + + Order& operator=(Order other); + + friend void swap(Order& first, Order& second) noexcept; + /*! * Adds state between the top and bottom node of the order. * @@ -318,6 +330,12 @@ class Order { void init(uint_fast64_t numberOfStates, storage::Decomposition, bool doneBuilding = false); + /*! + * Allocates a new Node owned by this Order (in nodeStorage) and returns an observer pointer to + * it. + */ + Node* allocateNode(); + std::string nodeName(Node n) const; std::string nodeLabel(Node n) const; @@ -333,6 +351,10 @@ class Order { std::vector nodes; + // Sole owner of every Node allocated for this Order; `nodes`, `top` and `bottom` are + // non-owning observer pointers into this storage. + std::vector> nodeStorage; + std::vector statesToHandle; Node* top; diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp index 9ac9edf87..f7d8b5572 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.cpp @@ -102,7 +102,7 @@ void OrderBasedMonotonicityBackend::initializeMono if (useBounds) { STORM_LOG_ASSERT(plaBoundFunction, "PLA bound function not registered."); orderExtender->setMaxValuesInit(plaBoundFunction(env, region, storm::solver::OptimizationDirection::Maximize)); - orderExtender->setMaxValuesInit(plaBoundFunction(env, region, storm::solver::OptimizationDirection::Minimize)); + orderExtender->setMinValuesInit(plaBoundFunction(env, region, storm::solver::OptimizationDirection::Minimize)); } typename MonotonicityAnnotation::OrderBasedMonotonicityAnnotation annotation; annotation.stateOrder = detail::extendOrder(*this->orderExtender, nullptr, region.region); @@ -128,11 +128,9 @@ void OrderBasedMonotonicityBackend::updateMonotoni // Copy order only if it will potentially change and if it is shared with another region bool const changeOrder = !annotation->stateOrder->getDoneBuilding() && orderExtender->isHope(annotation->stateOrder); if (changeOrder && annotation->stateOrder.use_count() > 1) { - // TODO: orderExtender currently uses shared_ptr which likely interferes with the use_count() > 1 check above // TODO: Make sure that only annotated regions own the order auto newOrder = annotation->stateOrder->copy(); - orderExtender->setUnknownStates(annotation->stateOrder, newOrder); - orderExtender->copyMinMax(annotation->stateOrder, newOrder); + orderExtender->copyContext(annotation->stateOrder, newOrder); annotation->stateOrder = newOrder; } if (changeOrder) { diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp index 9a1aed027..c9b1db1fc 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp @@ -1,4 +1,4 @@ -#include "OrderExtender.h" +#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" #include #include "storm/exceptions/NotSupportedException.h" @@ -27,7 +27,7 @@ OrderExtender::OrderExtender(std::shared_ptrmatrix = model->getTransitionMatrix(); this->numberOfStates = this->model->getNumberOfStates(); this->formula = formula; - this->assumptionMaker = new analysis::AssumptionMaker(matrix); + this->assumptionMaker = std::make_unique>(matrix); } template @@ -37,13 +37,22 @@ OrderExtender::OrderExtender(storm::storage::BitVector this->matrix = matrix; this->model = nullptr; this->monotonicityChecker = MonotonicityChecker(matrix); + this->numberOfStates = matrix.getColumnCount(); + + this->bottomTopOrder = computeInitialOrder(topStates, bottomStates, matrix, /*addStatesWithDirectBoundaryTransition=*/true); + this->assumptionMaker = std::make_unique>(matrix); +} + +template +std::shared_ptr OrderExtender::computeInitialOrder(storm::storage::BitVector const& topStates, + storm::storage::BitVector const& bottomStates, + storm::storage::SparseMatrix const& matrix, + bool addStatesWithDirectBoundaryTransition) { storm::storage::StronglyConnectedComponentDecompositionOptions options; options.forceTopologicalSort(); - this->numberOfStates = matrix.getColumnCount(); std::vector firstStates; - storm::storage::BitVector subStates(topStates.size(), true); for (auto state : topStates) { firstStates.push_back(state); @@ -60,7 +69,7 @@ OrderExtender::OrderExtender(storm::storage::BitVector } auto statesSorted = storm::utility::graph::getTopologicalSort(matrix.transpose(), firstStates); - this->bottomTopOrder = std::make_shared(topStates, bottomStates, numberOfStates, std::move(decomposition), std::move(statesSorted)); + auto order = std::make_shared(topStates, bottomStates, numberOfStates, std::move(decomposition), std::move(statesSorted)); // Build stateMap for (uint_fast64_t state = 0; state < numberOfStates; ++state) { @@ -71,8 +80,8 @@ OrderExtender::OrderExtender(storm::storage::BitVector for (auto& entry : matrix.getRow(state)) { // ignore self-loops when there are more transitions if (state != entry.getColumn() || row.getNumberOfEntries() == 1) { - if (!subStates[entry.getColumn()] && !bottomTopOrder->contains(state)) { - bottomTopOrder->add(state); + if (addStatesWithDirectBoundaryTransition && !subStates[entry.getColumn()] && !order->contains(state)) { + order->add(state); } stateMap[state].push_back(entry.getColumn()); } @@ -88,19 +97,19 @@ OrderExtender::OrderExtender(storm::storage::BitVector occuringVariablesAtState.push_back(std::move(occurringVariables)); } - this->assumptionMaker = new analysis::AssumptionMaker(matrix); + return order; } template std::shared_ptr OrderExtender::getBottomTopOrder() { if (bottomTopOrder == nullptr) { - assert(model != nullptr); + STORM_LOG_ASSERT(model != nullptr, "Cannot lazily build the bottom-top order without a model."); STORM_LOG_THROW(matrix.getRowCount() == matrix.getColumnCount(), exceptions::NotSupportedException, "Creating order not supported for non-square matrix."); modelchecker::SparsePropositionalModelChecker> propositionalChecker(*model); storage::BitVector phiStates; storage::BitVector psiStates; - assert(formula->isProbabilityOperatorFormula()); + STORM_LOG_ASSERT(formula->isProbabilityOperatorFormula(), "Expected a probability operator formula."); if (formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { phiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula()) ->template asExplicitQualitativeCheckResult() @@ -109,7 +118,7 @@ std::shared_ptr OrderExtender::getBottomTopOrder ->template asExplicitQualitativeCheckResult() .getTruthValuesVector(); } else { - assert(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + STORM_LOG_ASSERT(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula(), "Expected an eventually formula."); phiStates = storage::BitVector(numberOfStates, true); psiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()) ->template asExplicitQualitativeCheckResult() @@ -123,89 +132,57 @@ std::shared_ptr OrderExtender::getBottomTopOrder STORM_LOG_THROW(topStates.begin() != topStates.end(), exceptions::NotSupportedException, "Formula yields to no 1 states."); STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), exceptions::NotSupportedException, "Formula yields to no zero states."); - auto& matrix = this->model->getTransitionMatrix(); - std::vector firstStates; - - storm::storage::BitVector subStates(topStates.size(), true); - for (auto state : topStates) { - firstStates.push_back(state); - subStates.set(state, false); - } - for (auto state : bottomStates) { - firstStates.push_back(state); - subStates.set(state, false); - } - cyclic = storm::utility::graph::hasCycle(matrix, subStates); - storm::storage::StronglyConnectedComponentDecomposition decomposition; - if (cyclic) { - storm::storage::StronglyConnectedComponentDecompositionOptions options; - options.forceTopologicalSort(); - decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); - } - auto statesSorted = storm::utility::graph::getTopologicalSort(matrix.transpose(), firstStates); - bottomTopOrder = std::make_shared(topStates, bottomStates, numberOfStates, std::move(decomposition), std::move(statesSorted)); - - // Build stateMap - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - auto const& row = matrix.getRow(state); - stateMap[state] = std::vector(); - std::set occurringVariables; - - for (auto& entry : matrix.getRow(state)) { - // ignore self-loops when there are more transitions - if (state != entry.getColumn() || row.getNumberOfEntries() == 1) { - // if (!subStates[entry.getColumn()] && !bottomTopOrder->contains(state)) { - // bottomTopOrder->add(state); - // } - stateMap[state].push_back(entry.getColumn()); - } - storm::utility::parametric::gatherOccurringVariables(entry.getValue(), occurringVariables); - } - if (occurringVariables.empty()) { - nonParametricStates.insert(state); - } - for (auto& var : occurringVariables) { - occuringStatesAtVariable[var].push_back(state); - } - occuringVariablesAtState.push_back(std::move(occurringVariables)); - } + // Unlike the BitVector-matrix constructor, this path does not pre-add states with a direct + // transition to a top/bottom state to the order ahead of the main construction loop. + bottomTopOrder = computeInitialOrder(topStates, bottomStates, this->model->getTransitionMatrix(), /*addStatesWithDirectBoundaryTransition=*/false); } if (minValuesInit && maxValuesInit) { - continueExtending[bottomTopOrder] = true; - usePLA[bottomTopOrder] = true; - minValues[bottomTopOrder] = std::move(minValuesInit.get()); - maxValues[bottomTopOrder] = std::move(maxValuesInit.get()); + auto& ctx = context(bottomTopOrder); + ctx.continueExtending = true; + ctx.usePLA = true; + ctx.minValues = std::move(minValuesInit.get()); + ctx.maxValues = std::move(maxValuesInit.get()); } else { - usePLA[bottomTopOrder] = false; + context(bottomTopOrder).usePLA = false; } return bottomTopOrder; } +template +typename OrderExtender::Context& OrderExtender::context(std::shared_ptr const& order) { + auto result = contexts.try_emplace(order); + if (result.second) { + result.first->second.unknownStates = {numberOfStates, numberOfStates}; + } + return result.first->second; +} + +template +typename OrderExtender::Context const& OrderExtender::contextAt(std::shared_ptr const& order) const { + auto it = contexts.find(order); + STORM_LOG_ASSERT(it != contexts.end(), "No context set for this order."); + return it->second; +} + template std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender::toOrder( storage::ParameterRegion region, std::shared_ptr> monRes) { - return this->extendOrder(nullptr, region, monRes, nullptr); + return this->extendOrder(nullptr, region, monRes, std::nullopt); } template -void OrderExtender::handleAssumption(std::shared_ptr order, - std::shared_ptr assumption) const { - assert(assumption != nullptr); - assert(assumption->getFirstOperand()->isVariable() && assumption->getSecondOperand()->isVariable()); - - expressions::Variable var1 = assumption->getFirstOperand()->asVariableExpression().getVariable(); - expressions::Variable var2 = assumption->getSecondOperand()->asVariableExpression().getVariable(); - auto const& val1 = std::stoul(var1.getName(), nullptr, 0); - auto const& val2 = std::stoul(var2.getName(), nullptr, 0); +void OrderExtender::handleAssumption(std::shared_ptr order, Assumption const& assumption) const { + uint_fast64_t val1 = assumption.state1; + uint_fast64_t val2 = assumption.state2; - assert(order->compare(val1, val2) == Order::UNKNOWN); + STORM_LOG_ASSERT(order->compare(val1, val2) == Order::UNKNOWN, "The assumption's states are already ordered; handling it again is redundant."); Order::Node* n1 = order->getNode(val1); Order::Node* n2 = order->getNode(val2); - if (assumption->getRelationType() == expressions::RelationType::Equal) { + if (assumption.relation == expressions::RelationType::Equal) { if (n1 != nullptr && n2 != nullptr) { order->mergeNodes(n1, n2); } else if (n1 != nullptr) { @@ -217,7 +194,7 @@ void OrderExtender::handleAssumption(std::shared_ptraddToNode(val2, order->getNode(val1)); } } else { - assert(assumption->getRelationType() == expressions::RelationType::Greater); + STORM_LOG_ASSERT(assumption.relation == expressions::RelationType::Greater, "Only Equal and Greater assumptions are supported."); if (n1 != nullptr && n2 != nullptr) { order->addRelationNodes(n1, n2); } else if (n1 != nullptr) { @@ -234,13 +211,14 @@ void OrderExtender::handleAssumption(std::shared_ptr std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender::extendOrder( std::shared_ptr order, storm::storage::ParameterRegion region, std::shared_ptr> monRes, - std::shared_ptr assumption) { + std::optional assumption) { this->region = region; if (order == nullptr) { order = getBottomTopOrder(); - if (usePLA[order]) { - auto& min = minValues[order]; - auto& max = maxValues[order]; + auto& initialContext = context(order); + if (initialContext.usePLA) { + auto& min = initialContext.minValues; + auto& max = initialContext.maxValues; // Try to make the order as complete as possible based on pla results auto& statesSorted = order->getStatesSorted(); auto itr = statesSorted.begin(); @@ -276,9 +254,11 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtenderaddToNode(state1, order->getNode(state2)); } else if (!order->contains(state2)) { order->addToNode(state2, order->getNode(state1)); - } else { - order->merge(state1, state2); - assert(!order->isInvalid()); + } else if (!order->merge(state1, state2)) { + // The PLA-bound-based conclusion that state1 and state2 are equal + // contradicts what the order already knows about them. Bail out here + // rather than continuing to build on top of an inconsistent order. + return std::make_tuple(order, numberOfStates, numberOfStates); } } else { all = false; @@ -291,54 +271,68 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender std::tuple, uint_fast64_t, uint_fast64_t> OrderExtender::extendOrder( - std::shared_ptr order, std::shared_ptr> monRes, std::shared_ptr assumption) { - if (assumption != nullptr) { + std::shared_ptr order, std::shared_ptr> monRes, std::optional assumption) { + if (assumption.has_value()) { STORM_LOG_INFO("Handling assumption " << *assumption << '\n'); - handleAssumption(order, assumption); + handleAssumption(order, *assumption); + if (order->isInvalid()) { + // The assumption led to a mathematically inconsistent order (a merge of two states that + // should stay distinct). Bail out here rather than continuing to build on top of it. + return std::make_tuple(order, numberOfStates, numberOfStates); + } } auto currentStateMode = getNextState(order, numberOfStates, false); while (currentStateMode.first != numberOfStates) { - assert(currentStateMode.first < numberOfStates); + STORM_LOG_ASSERT(currentStateMode.first < numberOfStates, "Expected a valid state, not the sentinel value."); auto& currentState = currentStateMode.first; auto& successors = stateMap[currentState]; std::pair result = {numberOfStates, numberOfStates}; if (successors.size() == 1) { - assert(order->contains(successors[0])); + STORM_LOG_ASSERT(order->contains(successors[0]), "The single successor of a state must already be in the order."); handleOneSuccessor(order, currentState, successors[0]); } else if (!successors.empty()) { if (order->isOnlyBottomTopOrder()) { order->add(currentState); if (!order->isTrivial(currentState)) { // This state is part of an scc, therefore, we could do forward reasoning here - result = extendByForwardReasoning(order, currentState, successors, assumption != nullptr); + result = extendByForwardReasoning(order, currentState, successors, assumption.has_value()); } else { result = {numberOfStates, numberOfStates}; } } else { - result = extendNormal(order, currentState, successors, assumption != nullptr); + result = extendNormal(order, currentState, successors, assumption.has_value()); } } + if (order->isInvalid()) { + // A merge performed while extending this state (directly, or via forward/backward + // reasoning) produced a mathematically inconsistent order. Bail out here rather than + // continuing to build on top of it. + return std::make_tuple(order, numberOfStates, numberOfStates); + } + if (result.first == numberOfStates) { // We did extend the order - assert(result.second == numberOfStates); - assert(order->sortStates(&successors).size() == successors.size()); - assert(order->contains(currentState) && order->getNode(currentState) != nullptr); + STORM_LOG_ASSERT(result.second == numberOfStates, "Expected both entries of result to be the sentinel value."); + STORM_LOG_ASSERT(order->sortStates(&successors).size() == successors.size(), "Expected all successors to be sortable at this point."); + STORM_LOG_ASSERT(order->contains(currentState) && order->getNode(currentState) != nullptr, + "The current state should have been placed in the order."); if (monRes != nullptr) { for (auto& param : occuringVariablesAtState[currentState]) { @@ -348,12 +342,15 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtendercompare(result.first, result.second) == Order::UNKNOWN); - assert(order->compare(result.second, result.first) == Order::UNKNOWN); + STORM_LOG_ASSERT(result.first < numberOfStates, "Expected a valid state, not the sentinel value."); + STORM_LOG_ASSERT(result.second < numberOfStates, "Expected a valid state, not the sentinel value."); + STORM_LOG_ASSERT(order->compare(result.first, result.second) == Order::UNKNOWN, "Expected the unresolved pair to indeed be unordered."); + STORM_LOG_ASSERT(order->compare(result.second, result.first) == Order::UNKNOWN, "Expected the unresolved pair to indeed be unordered."); // Try to add states based on min/max and assumptions, only if we are not in statesToHandle mode if (currentStateMode.second && extendByAssumption(order, result.first, result.second)) { + if (order->isInvalid()) { + return std::make_tuple(order, numberOfStates, numberOfStates); + } continue; } // We couldn't extend the order @@ -373,15 +370,14 @@ std::tuple, uint_fast64_t, uint_fast64_t> OrderExtenderaddStateSorted(currentState); - continueExtending[order] = false; + context(order).continueExtending = false; return {order, result.first, result.second}; } } } - assert(order->sortStates(&successors).size() == successors.size()); } - assert(order->getDoneBuilding()); + STORM_LOG_ASSERT(order->getDoneBuilding(), "Expected the order to be fully built at this point."); if (monRes != nullptr) { // monotonicity result for the in-build checking of monotonicity monRes->setDone(); @@ -397,7 +393,8 @@ std::pair OrderExtender:: // Try to extend the order for this scc return extendByForwardReasoning(order, currentState, successors, allowMerge); } else { - assert(order->isTrivial(currentState) || !order->contains(currentState)); + STORM_LOG_ASSERT(order->isTrivial(currentState) || !order->contains(currentState), + "A non-trivial (SCC) state that is already in the order should use forward reasoning, not backward reasoning."); // Do backward reasoning, all successor states must be in the order return extendByBackwardReasoning(order, currentState, successors, allowMerge); } @@ -405,7 +402,7 @@ std::pair OrderExtender:: template void OrderExtender::handleOneSuccessor(std::shared_ptr order, uint_fast64_t currentState, uint_fast64_t successor) { - assert(order->contains(successor)); + STORM_LOG_ASSERT(order->contains(successor), "The successor must already be in the order."); if (currentState != successor) { if (order->contains(currentState)) { order->merge(currentState, successor); @@ -420,13 +417,14 @@ std::pair OrderExtender:: uint_fast64_t currentState, std::vector const& successors, bool allowMerge) { - assert(!order->isOnlyBottomTopOrder()); - assert(successors.size() > 1); + STORM_LOG_ASSERT(!order->isOnlyBottomTopOrder(), "Backward reasoning requires the order to have grown beyond just top and bottom."); + STORM_LOG_ASSERT(successors.size() > 1, "Backward reasoning is only needed for states with more than one successor."); - bool pla = (usePLA.find(order) != usePLA.end() && usePLA.at(order)); + auto& ctx = context(order); + bool pla = ctx.usePLA; std::vector sortedSuccs; - if (pla && (continueExtending.find(order) == continueExtending.end() || continueExtending.at(order))) { + if (pla && ctx.continueExtending) { for (auto& state1 : successors) { if (sortedSuccs.size() == 0) { sortedSuccs.push_back(state1); @@ -448,7 +446,7 @@ std::pair OrderExtender:: added = true; break; } else if (compareRes == Order::NodeComparison::UNKNOWN) { - continueExtending[order] = false; + ctx.continueExtending = false; return {state1, state2}; } } @@ -474,13 +472,13 @@ std::pair OrderExtender:: } } else { if (!order->contains(sortedSuccs[0])) { - assert(order->isBottomState(sortedSuccs[sortedSuccs.size() - 1])); - assert(sortedSuccs.size() == 2); + STORM_LOG_ASSERT(order->isBottomState(sortedSuccs[sortedSuccs.size() - 1]), "Expected the other successor to be a bottom state."); + STORM_LOG_ASSERT(sortedSuccs.size() == 2, "Expected exactly two successors in this case."); order->addAbove(sortedSuccs[0], order->getBottom()); } if (!order->contains(sortedSuccs[sortedSuccs.size() - 1])) { - assert(order->isTopState(sortedSuccs[0])); - assert(sortedSuccs.size() == 2); + STORM_LOG_ASSERT(order->isTopState(sortedSuccs[0]), "Expected the other successor to be a top state."); + STORM_LOG_ASSERT(sortedSuccs.size() == 2, "Expected exactly two successors in this case."); order->addBelow(sortedSuccs[sortedSuccs.size() - 1], order->getTop()); } // sortedSuccs[0] is highest @@ -491,8 +489,9 @@ std::pair OrderExtender:: order->addRelation(currentState, sortedSuccs[sortedSuccs.size() - 1], allowMerge); } } - assert(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && - order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW); + STORM_LOG_ASSERT(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && + order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, + "The current state should have ended up strictly between top and bottom in the order."); return {numberOfStates, numberOfStates}; } @@ -501,13 +500,13 @@ std::pair OrderExtender:: uint_fast64_t currentState, std::vector const& successors, bool allowMerge) { - assert(successors.size() > 1); - assert(order->contains(currentState)); - assert(cyclic); + STORM_LOG_ASSERT(successors.size() > 1, "Forward reasoning is only needed for states with more than one successor."); + STORM_LOG_ASSERT(order->contains(currentState), "The current state must already be in the order before doing forward reasoning on it."); + STORM_LOG_ASSERT(cyclic, "Forward reasoning is only applicable to cyclic pMCs."); std::vector statesSorted; statesSorted.push_back(currentState); - bool pla = (usePLA.find(order) != usePLA.end() && usePLA.at(order)); + bool pla = context(order).usePLA; // Go over all states bool oneUnknown = false; bool unknown = false; @@ -555,12 +554,12 @@ std::pair OrderExtender:: } } if (!unknown && oneUnknown) { - assert(statesSorted.size() == successors.size()); + STORM_LOG_ASSERT(statesSorted.size() == successors.size(), "Expected all but the single unresolved successor to have been sorted."); s2 = numberOfStates; } if (s1 == numberOfStates) { - assert(statesSorted.size() == successors.size() + 1); + STORM_LOG_ASSERT(statesSorted.size() == successors.size() + 1, "Expected all successors (plus the current state) to have been sorted."); // all could be sorted, no need to do anything } else if (s2 == numberOfStates) { if (!order->contains(s1)) { @@ -569,19 +568,25 @@ std::pair OrderExtender:: if (statesSorted[0] == currentState) { order->addRelation(s1, statesSorted[0], allowMerge); - assert((order->compare(s1, statesSorted[0]) == Order::ABOVE) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + // Fallback checks statesSorted[0]: that's the element the addRelation call just above + // related (and, if allowMerge applies, may have merged) s1 with. + STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::ABOVE) || (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), + "Expected s1 to end up above (or, if merged, equal to) statesSorted[0]."); order->addRelation(s1, statesSorted[statesSorted.size() - 1], allowMerge); - assert((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::ABOVE) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + STORM_LOG_ASSERT((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::ABOVE) || + (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), + "Expected s1 to end up above (or, if merged, equal to) the lowest sorted successor."); order->addStateToHandle(s1); } else if (statesSorted[statesSorted.size() - 1] == currentState) { order->addRelation(statesSorted[0], s1, allowMerge); - assert((order->compare(s1, statesSorted[0]) == Order::BELOW) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + // Fallback checks statesSorted[0]: that's the element the addRelation call just above + // related (and, if allowMerge applies, may have merged) s1 with. + STORM_LOG_ASSERT((order->compare(s1, statesSorted[0]) == Order::BELOW) || (allowMerge && (order->compare(s1, statesSorted[0]) == Order::SAME)), + "Expected s1 to end up below (or, if merged, equal to) statesSorted[0]."); order->addRelation(statesSorted[statesSorted.size() - 1], s1, allowMerge); - assert((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::BELOW) || - (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME))); + STORM_LOG_ASSERT((order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::BELOW) || + (allowMerge && (order->compare(s1, statesSorted[statesSorted.size() - 1]) == Order::SAME)), + "Expected s1 to end up below (or, if merged, equal to) the highest sorted successor."); order->addStateToHandle(s1); } else { bool continueSearch = true; @@ -603,17 +608,18 @@ std::pair OrderExtender:: } else { return {s1, s2}; } - assert(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && - order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW); + STORM_LOG_ASSERT(order->contains(currentState) && order->compare(order->getNode(currentState), order->getBottom()) == Order::ABOVE && + order->compare(order->getNode(currentState), order->getTop()) == Order::BELOW, + "The current state should have ended up strictly between top and bottom in the order."); return {numberOfStates, numberOfStates}; } template bool OrderExtender::extendByAssumption(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) { - bool usePLANow = usePLA.find(order) != usePLA.end() && usePLA[order]; - assert(order->compare(state1, state2) == Order::UNKNOWN); - auto assumptions = usePLANow ? assumptionMaker->createAndCheckAssumptions(state1, state2, order, region, minValues[order], maxValues[order]) - : assumptionMaker->createAndCheckAssumptions(state1, state2, order, region); + auto& ctx = context(order); + STORM_LOG_ASSERT(order->compare(state1, state2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); + auto assumptions = ctx.usePLA ? assumptionMaker->createAndCheckAssumptions(state1, state2, order, region, ctx.minValues, ctx.maxValues) + : assumptionMaker->createAndCheckAssumptions(state1, state2, order, region); if (assumptions.size() == 1 && assumptions.begin()->second == AssumptionStatus::VALID) { handleAssumption(order, assumptions.begin()->first); // Assumptions worked, we continue @@ -625,15 +631,19 @@ bool OrderExtender::extendByAssumption(std::shared_ptr< template Order::NodeComparison OrderExtender::addStatesBasedOnMinMax(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) const { - assert(order->compareFast(state1, state2) == Order::UNKNOWN); - assert(minValues.find(order) != minValues.end()); - std::vector const& mins = minValues.at(order); - std::vector const& maxs = maxValues.at(order); + STORM_LOG_ASSERT(order->compareFast(state1, state2) == Order::UNKNOWN, "Expected the given pair to indeed be unordered."); + auto const& ctx = contextAt(order); + std::vector const& mins = ctx.minValues; + std::vector const& maxs = ctx.maxValues; if (mins[state1] == maxs[state1] && mins[state2] == maxs[state2] && mins[state1] == mins[state2]) { if (order->contains(state1)) { if (order->contains(state2)) { - order->merge(state1, state2); - assert(!order->isInvalid()); + if (!order->merge(state1, state2)) { + // The min/max-based conclusion that state1 and state2 are equal contradicts + // what the order already knows about them; treat it as unresolved rather than + // silently building on top of an inconsistent order. + return Order::UNKNOWN; + } } else { order->addToNode(state2, order->getNode(state1)); } @@ -647,8 +657,8 @@ Order::NodeComparison OrderExtender::addStatesBasedOnMi if (!order->contains(state2)) { order->add(state2); } - assert(order->compare(state1, state2) != Order::BELOW); - assert(order->compare(state1, state2) != Order::SAME); + STORM_LOG_ASSERT(order->compare(state1, state2) != Order::BELOW, "min/max values say state1 is above state2, contradicting the order."); + STORM_LOG_ASSERT(order->compare(state1, state2) != Order::SAME, "min/max values say state1 is strictly above state2, contradicting the order."); order->addRelation(state1, state2); return Order::ABOVE; @@ -660,8 +670,8 @@ Order::NodeComparison OrderExtender::addStatesBasedOnMi if (!order->contains(state2)) { order->add(state2); } - assert(order->compare(state2, state1) != Order::BELOW); - assert(order->compare(state2, state1) != Order::SAME); + STORM_LOG_ASSERT(order->compare(state2, state1) != Order::BELOW, "min/max values say state2 is above state1, contradicting the order."); + STORM_LOG_ASSERT(order->compare(state2, state1) != Order::SAME, "min/max values say state2 is strictly above state1, contradicting the order."); order->addRelation(state2, state1); return Order::BELOW; } else { @@ -697,82 +707,70 @@ void OrderExtender::initializeMinMaxValues(storage::Par plaModelChecker.check(env, annotatedRegion, solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult(); minValuesInit = minCheck.getValueVector(); maxValuesInit = maxCheck.getValueVector(); - assert(minValuesInit->size() == numberOfStates); - assert(maxValuesInit->size() == numberOfStates); + STORM_LOG_ASSERT(minValuesInit->size() == numberOfStates, "Expected one lower bound per state."); + STORM_LOG_ASSERT(maxValuesInit->size() == numberOfStates, "Expected one upper bound per state."); } } template void OrderExtender::setMinMaxValues(std::shared_ptr order, std::vector&& minValues, std::vector&& maxValues) { - assert(minValues.size() == numberOfStates); - assert(maxValues.size() == numberOfStates); - usePLA[order] = true; - if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - auto& unknownStates = unknownStatesMap[order]; - if (unknownStates.first != numberOfStates) { - continueExtending[order] = - minValues[unknownStates.first] >= maxValues[unknownStates.second] || minValues[unknownStates.second] >= maxValues[unknownStates.first]; - } else { - continueExtending[order] = true; - } + STORM_LOG_ASSERT(minValues.size() == numberOfStates, "Expected one lower bound per state."); + STORM_LOG_ASSERT(maxValues.size() == numberOfStates, "Expected one upper bound per state."); + auto& ctx = context(order); + ctx.usePLA = true; + if (ctx.unknownStates.first != numberOfStates) { + ctx.continueExtending = minValues[ctx.unknownStates.first] >= maxValues[ctx.unknownStates.second] || + minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; } else { - continueExtending[order] = true; + ctx.continueExtending = true; } - this->minValues[order] = std::move(minValues); - this->maxValues[order] = std::move(maxValues); + ctx.minValues = std::move(minValues); + ctx.maxValues = std::move(maxValues); } template void OrderExtender::setMinValues(std::shared_ptr order, std::vector&& minValues) { - assert(minValues.size() == numberOfStates); - auto& maxValues = this->maxValues[order]; - usePLA[order] = this->maxValues.find(order) != this->maxValues.end(); - if (maxValues.size() == 0) { - continueExtending[order] = false; - } else if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - auto& unknownStates = unknownStatesMap[order]; - if (unknownStates.first != numberOfStates) { - continueExtending[order] = - minValues[unknownStates.first] >= maxValues[unknownStates.second] || minValues[unknownStates.second] >= maxValues[unknownStates.first]; - } else { - continueExtending[order] = true; - } + STORM_LOG_ASSERT(minValues.size() == numberOfStates, "Expected one lower bound per state."); + auto& ctx = context(order); + // usePLA becomes true unconditionally here (unlike setMaxValues, which checks whether the other + // bound is already known): accessing ctx.maxValues below always makes it "known", even if empty. + ctx.usePLA = true; + if (ctx.maxValues.size() == 0) { + ctx.continueExtending = false; + } else if (ctx.unknownStates.first != numberOfStates) { + ctx.continueExtending = minValues[ctx.unknownStates.first] >= ctx.maxValues[ctx.unknownStates.second] || + minValues[ctx.unknownStates.second] >= ctx.maxValues[ctx.unknownStates.first]; } else { - continueExtending[order] = true; + ctx.continueExtending = true; } - this->minValues[order] = std::move(minValues); + ctx.minValues = std::move(minValues); } template void OrderExtender::setMaxValues(std::shared_ptr order, std::vector&& maxValues) { - assert(maxValues.size() == numberOfStates); - usePLA[order] = this->minValues.find(order) != this->minValues.end(); - auto& minValues = this->minValues[order]; - if (minValues.size() == 0) { - continueExtending[order] = false; - } else if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - auto& unknownStates = unknownStatesMap[order]; - if (unknownStates.first != numberOfStates) { - continueExtending[order] = - minValues[unknownStates.first] >= maxValues[unknownStates.second] || minValues[unknownStates.second] >= maxValues[unknownStates.first]; - } else { - continueExtending[order] = true; - } + STORM_LOG_ASSERT(maxValues.size() == numberOfStates, "Expected one upper bound per state."); + auto& ctx = context(order); + ctx.usePLA = !ctx.minValues.empty(); + if (ctx.minValues.size() == 0) { + ctx.continueExtending = false; + } else if (ctx.unknownStates.first != numberOfStates) { + ctx.continueExtending = ctx.minValues[ctx.unknownStates.first] >= maxValues[ctx.unknownStates.second] || + ctx.minValues[ctx.unknownStates.second] >= maxValues[ctx.unknownStates.first]; } else { - continueExtending[order] = true; + ctx.continueExtending = true; } - this->maxValues[order] = std::move(maxValues); // maxCheck->asExplicitQuantitativeCheckResult().getValueVector(); + ctx.maxValues = std::move(maxValues); } template void OrderExtender::setMinValuesInit(std::vector&& minValues) { - assert(minValues.size() == numberOfStates); + STORM_LOG_ASSERT(minValues.size() == numberOfStates, "Expected one lower bound per state."); this->minValuesInit = std::move(minValues); } template void OrderExtender::setMaxValuesInit(std::vector&& maxValues) { - assert(maxValues.size() == numberOfStates); + STORM_LOG_ASSERT(maxValues.size() == numberOfStates, "Expected one upper bound per state."); this->maxValuesInit = std::move(maxValues); // maxCheck->asExplicitQuantitativeCheckResult().getValueVector(); } @@ -786,33 +784,23 @@ void OrderExtender::checkParOnStateMonRes(uint_fast64_t template void OrderExtender::setUnknownStates(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) { - assert(state1 != numberOfStates && state2 != numberOfStates); - unknownStatesMap[order] = {state1, state2}; + STORM_LOG_ASSERT(state1 != numberOfStates && state2 != numberOfStates, "Expected two actual states, not the sentinel value."); + context(order).unknownStates = {state1, state2}; } template std::pair OrderExtender::getUnknownStates(std::shared_ptr order) const { - if (unknownStatesMap.find(order) != unknownStatesMap.end()) { - return unknownStatesMap.at(order); + auto it = contexts.find(order); + if (it != contexts.end()) { + return it->second.unknownStates; } return {numberOfStates, numberOfStates}; } template -void OrderExtender::setUnknownStates(std::shared_ptr orderOriginal, std::shared_ptr orderCopy) { - assert(unknownStatesMap.find(orderCopy) == unknownStatesMap.end()); - unknownStatesMap.insert({orderCopy, {unknownStatesMap[orderOriginal].first, unknownStatesMap[orderOriginal].second}}); -} - -template -void OrderExtender::copyMinMax(std::shared_ptr orderOriginal, std::shared_ptr orderCopy) { - usePLA[orderCopy] = usePLA[orderOriginal]; - if (usePLA[orderCopy]) { - minValues[orderCopy] = minValues[orderOriginal]; - assert(maxValues.find(orderOriginal) != maxValues.end()); - maxValues[orderCopy] = maxValues[orderOriginal]; - } - continueExtending[orderCopy] = continueExtending[orderOriginal]; +void OrderExtender::copyContext(std::shared_ptr orderOriginal, std::shared_ptr orderCopy) { + STORM_LOG_ASSERT(contexts.find(orderCopy) == contexts.end(), "The copy must not already have a context set."); + contexts[orderCopy] = contextAt(orderOriginal); } template @@ -834,11 +822,10 @@ std::pair OrderExtender::getNextSt template bool OrderExtender::isHope(std::shared_ptr order) { - assert(unknownStatesMap.find(order) != unknownStatesMap.end()); - assert(!order->getDoneBuilding()); + STORM_LOG_ASSERT(contexts.find(order) != contexts.end(), "Expected a context to be set for this order."); + STORM_LOG_ASSERT(!order->getDoneBuilding(), "Asking for hope on an order that is already fully built is meaningless."); // First check if bounds helped us - bool yesThereIsHope = continueExtending[order]; - return yesThereIsHope; + return context(order).continueExtending; } template MonotonicityChecker& OrderExtender::getMonotoncityChecker() { diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h index b552abd94..27d802057 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h @@ -1,12 +1,12 @@ #pragma once #include +#include #include "storm/logic/Formula.h" #include "storm/models/sparse/Model.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/expressions/VariableExpression.h" #include "storm/utility/Stopwatch.h" +#include "storm-pars/modelchecker/region/monotonicity/Assumption.h" #include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityChecker.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" @@ -63,7 +63,7 @@ class OrderExtender { std::tuple, uint_fast64_t, uint_fast64_t> extendOrder(std::shared_ptr order, storm::storage::ParameterRegion region, std::shared_ptr> monRes = nullptr, - std::shared_ptr assumption = nullptr); + std::optional assumption = std::nullopt); void setMinMaxValues(std::shared_ptr order, std::vector&& minValues, std::vector&& maxValues); void setMinValues(std::shared_ptr order, std::vector&& minValues); @@ -74,8 +74,7 @@ class OrderExtender { void setUnknownStates(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2); std::pair getUnknownStates(std::shared_ptr order) const; - void setUnknownStates(std::shared_ptr orderOriginal, std::shared_ptr orderCopy); - void copyMinMax(std::shared_ptr orderOriginal, std::shared_ptr orderCopy); + void copyContext(std::shared_ptr orderOriginal, std::shared_ptr orderCopy); void initializeMinMaxValues(storage::ParameterRegion region); void checkParOnStateMonRes(uint_fast64_t s, std::shared_ptr order, typename OrderExtender::VariableType param, std::shared_ptr> monResult); @@ -89,7 +88,7 @@ class OrderExtender { Order::NodeComparison addStatesBasedOnMinMax(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2) const; std::tuple, uint_fast64_t, uint_fast64_t> extendOrder(std::shared_ptr order, std::shared_ptr> monRes, - std::shared_ptr assumption = nullptr); + std::optional assumption = std::nullopt); std::pair extendNormal(std::shared_ptr order, uint_fast64_t currentState, std::vector const& successors, bool allowMerge); std::pair extendByBackwardReasoning(std::shared_ptr order, uint_fast64_t currentState, @@ -99,26 +98,38 @@ class OrderExtender { bool extendByAssumption(std::shared_ptr order, uint_fast64_t state1, uint_fast64_t state2); void handleOneSuccessor(std::shared_ptr order, uint_fast64_t currentState, uint_fast64_t successor); - void handleAssumption(std::shared_ptr order, std::shared_ptr assumption) const; + void handleAssumption(std::shared_ptr order, Assumption const& assumption) const; std::pair getNextState(std::shared_ptr order, uint_fast64_t stateNumber, bool done); + std::shared_ptr computeInitialOrder(storm::storage::BitVector const& topStates, storm::storage::BitVector const& bottomStates, + storm::storage::SparseMatrix const& matrix, bool addStatesWithDirectBoundaryTransition); std::shared_ptr getBottomTopOrder(); std::shared_ptr bottomTopOrder = nullptr; - std::map, std::vector> minValues; + // Per-in-progress-order bookkeeping used while extending an order (PLA bounds, whether PLA is + // usable/worth continuing, and the pair of states this order got stuck on, if any). Keyed by + // weak_ptr so this bookkeeping neither keeps an order alive nor inflates its use_count() + // while the order is still being extended. + struct Context { + std::vector minValues; + std::vector maxValues; + bool usePLA = false; + bool continueExtending = true; + std::pair unknownStates; + }; + Context& context(std::shared_ptr const& order); + Context const& contextAt(std::shared_ptr const& order) const; + std::map, Context, std::owner_less>> contexts; + boost::optional> minValuesInit; boost::optional> maxValuesInit; - std::map, std::vector> maxValues; storage::SparseMatrix matrix; std::shared_ptr> model; std::map> stateMap; - std::map, std::pair> unknownStatesMap; - std::map, bool> usePLA; - std::map, bool> continueExtending; bool cyclic; std::shared_ptr formula; @@ -127,7 +138,7 @@ class OrderExtender { uint_fast64_t numberOfStates; - analysis::AssumptionMaker* assumptionMaker; + std::unique_ptr> assumptionMaker; boost::container::flat_set nonParametricStates; diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp index 6e6aa753e..c319410f8 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp @@ -19,8 +19,6 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" -#include "storm/storage/expressions/BinaryRelationExpression.h" -#include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/graph.h" class AssumptionCheckerTest : public ::testing::Test { @@ -59,9 +57,6 @@ TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) { auto region = storm::api::parseRegion("0.00001 <= pK <= 0.00001, 0.00001 <= pL <= 0.99999", vars); auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("7"); - expressionManager->declareRationalVariable("5"); storm::storage::BitVector above(193); above.set(0); storm::storage::BitVector below(193); @@ -74,35 +69,23 @@ TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) { auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); auto dummyOrder = std::shared_ptr(new storm::analysis::Order(above, below, 193, decomposition, statesSorted)); - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{7, 5, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{5, 7, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{7, 5, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{7, 5, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{5, 7, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{7, 5, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder, region)); } @@ -133,9 +116,6 @@ TEST_F(AssumptionCheckerTest, Simple1) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); storm::storage::StronglyConnectedComponentDecompositionOptions options; options.forceTopologicalSort(); auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), options); @@ -148,35 +128,23 @@ TEST_F(AssumptionCheckerTest, Simple1) { auto order = std::shared_ptr(new storm::analysis::Order(above, below, 5, decomposition, statesSorted)); // Validating - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); region = storm::api::parseRegion("0.51 <= p <= 0.99", vars); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } @@ -207,10 +175,6 @@ TEST_F(AssumptionCheckerTest, Casestudy1) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); - storm::storage::BitVector above(5); above.set(3); storm::storage::BitVector below(5); @@ -223,35 +187,23 @@ TEST_F(AssumptionCheckerTest, Casestudy1) { auto order = std::shared_ptr(new storm::analysis::Order(above, below, 5, decomposition, statesSorted)); // Validating - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } @@ -282,10 +234,6 @@ TEST_F(AssumptionCheckerTest, Casestudy2) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); - storm::storage::BitVector above(6); above.set(4); storm::storage::BitVector below(6); @@ -299,19 +247,13 @@ TEST_F(AssumptionCheckerTest, Casestudy2) { order->add(3); // Checking on samples and validate - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } @@ -342,10 +284,6 @@ TEST_F(AssumptionCheckerTest, Casestudy3) { auto checker = storm::analysis::AssumptionChecker(dtmc->getTransitionMatrix()); - auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); - expressionManager->declareRationalVariable("1"); - expressionManager->declareRationalVariable("2"); - // Order storm::storage::BitVector above(5); above.set(3); @@ -357,35 +295,23 @@ TEST_F(AssumptionCheckerTest, Casestudy3) { auto statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); auto order = std::shared_ptr(new storm::analysis::Order(above, below, 5, decomposition, statesSorted)); - auto assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + storm::analysis::Assumption assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); checker.initializeCheckingOnSamples(formulas[0], dtmc, region, 3); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Greater)); + assumption = storm::analysis::Assumption{2, 1, storm::expressions::RelationType::Greater}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); - assumption = std::make_shared(storm::expressions::BinaryRelationExpression( - *expressionManager, expressionManager->getBooleanType(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), - expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::RelationType::Equal)); + assumption = storm::analysis::Assumption{1, 2, storm::expressions::RelationType::Equal}; EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order, region)); } diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp index d6d68716c..e7559d46c 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp @@ -67,20 +67,29 @@ TEST_F(AssumptionMakerTest, Brp_without_bisimulation) { for (auto res : result) { EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, res.second); - EXPECT_EQ(true, res.first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, res.first->getSecondOperand()->isVariable()); } + // Regression test: when more than one candidate survives, they must be returned in construction + // order (val1 > val2, val2 > val1, val1 == val2), not e.g. heap-address order of some internal + // representation. + EXPECT_EQ(183ul, result[0].first.state1); + EXPECT_EQ(186ul, result[0].first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, result[0].first.relation); + EXPECT_EQ(186ul, result[1].first.state1); + EXPECT_EQ(183ul, result[1].first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, result[1].first.relation); + EXPECT_EQ(183ul, result[2].first.state1); + EXPECT_EQ(186ul, result[2].first.state2); + EXPECT_EQ(storm::expressions::RelationType::Equal, result[2].first.relation); + assumptionMaker.initializeCheckingOnSamples(formulas[0], model, region, 10); result = assumptionMaker.createAndCheckAssumptions(std::get<1>(criticalTuple), std::get<2>(criticalTuple), std::get<0>(criticalTuple), region); EXPECT_EQ(1ul, result.size()); auto itr = result.begin(); EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, itr->second); - EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); - EXPECT_EQ("186", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ("183", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType()); + EXPECT_EQ(186ul, itr->first.state1); + EXPECT_EQ(183ul, itr->first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first.relation); } TEST_F(AssumptionMakerTest, Simple1) { @@ -129,11 +138,9 @@ TEST_F(AssumptionMakerTest, Simple1) { EXPECT_EQ(1ul, result.size()); auto itr = result.begin(); EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second); - EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); - EXPECT_EQ("1", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType()); + EXPECT_EQ(1ul, itr->first.state1); + EXPECT_EQ(2ul, itr->first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first.relation); } TEST_F(AssumptionMakerTest, Casestudy1) { @@ -175,9 +182,7 @@ TEST_F(AssumptionMakerTest, Casestudy1) { EXPECT_EQ(1ul, result.size()); auto itr = result.begin(); EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, itr->second); - EXPECT_EQ(true, itr->first->getFirstOperand()->isVariable()); - EXPECT_EQ(true, itr->first->getSecondOperand()->isVariable()); - EXPECT_EQ("1", itr->first->getFirstOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ("2", itr->first->getSecondOperand()->asVariableExpression().getVariable().getName()); - EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first->getRelationType()); + EXPECT_EQ(1ul, itr->first.state1); + EXPECT_EQ(2ul, itr->first.state2); + EXPECT_EQ(storm::expressions::RelationType::Greater, itr->first.relation); } diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp index 7c6c5c8e5..db6fe869e 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/OrderTest.cpp @@ -152,6 +152,53 @@ TEST(OrderTest, copy_order) { EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5, 6)); } +TEST(OrderTest, copy_is_deep) { + // Regression test: Order's copy constructor must deep-copy every Node, not alias the + // original's nodes. Mutating one Order (adding states, merging nodes) must not affect the + // other. + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + storm::storage::SparseMatrixBuilder matrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1)); + matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1)); + storm::storage::StronglyConnectedComponentDecompositionOptions options; + options.forceTopologicalSort(); + auto matrix = matrixBuilder.build(); + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + auto statesSorted = storm::utility::graph::getTopologicalSort(matrix); + auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted); + order.add(2); + order.add(3); + order.addToNode(4, order.getNode(2)); + + auto orderCopy = storm::analysis::Order(order); + + // Mutating the copy (adding a new state) must not be visible in the original. + orderCopy.addBetween(5, orderCopy.getNode(0), orderCopy.getNode(3)); + EXPECT_TRUE(orderCopy.contains(5)); + EXPECT_FALSE(order.contains(5)); + + // Mutating the original (adding a different state) must not be visible in the copy. + order.addBetween(6, order.getNode(0), order.getNode(3)); + EXPECT_TRUE(order.contains(6)); + EXPECT_FALSE(orderCopy.contains(6)); + + // Merging nodes in the copy must not merge the corresponding nodes in the original: states 2 + // and 3 stay unrelated in the original, even after they are merged in the copy. + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3)); + orderCopy.mergeNodes(orderCopy.getNode(2), orderCopy.getNode(3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2, 3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2, 3)); + + // Node pointers themselves must not be shared between the two Orders. + EXPECT_NE(order.getNode(0), orderCopy.getNode(0)); + EXPECT_NE(order.getTop(), orderCopy.getTop()); + EXPECT_NE(order.getBottom(), orderCopy.getBottom()); +} + TEST(OrderTest, merge_nodes) { auto numberOfStates = 7; auto above = storm::storage::BitVector(numberOfStates); @@ -192,6 +239,47 @@ TEST(OrderTest, merge_nodes) { EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1, 5)); } +TEST(OrderTest, merge_nodes_inconsistent) { + // Regression test: forcing a merge that contradicts an already-established chain of relations + // must be reported gracefully (mergeNodes returns false, isInvalid() becomes true) rather than + // crashing on an internal assertion when a later compare() call discovers the resulting cycle. + auto numberOfStates = 6; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + storm::storage::SparseMatrixBuilder matrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 0, storm::RationalFunction(1)); + matrixBuilder.addNextValue(1, 1, storm::RationalFunction(1)); + storm::storage::StronglyConnectedComponentDecompositionOptions options; + options.forceTopologicalSort(); + auto matrix = matrixBuilder.build(); + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options); + auto statesSorted = storm::utility::graph::getTopologicalSort(matrix); + auto order = storm::analysis::Order(above, below, numberOfStates, decomposition, statesSorted); + + // Build a strict chain: top(0) > 3 > 4 > 5 > 2 > bottom(1). + order.add(2); + order.addBetween(3, order.getNode(0), order.getNode(2)); + order.addBetween(4, order.getNode(3), order.getNode(2)); + order.addBetween(5, order.getNode(4), order.getNode(2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(3, 2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(3, 4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4, 5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5, 2)); + + // Forcing 3 and 2 to be equal directly contradicts 3 > 4 > 5 > 2: mergeNodes must refuse this + // (returning false, marking the order invalid) instead of leaving the order in a state where a + // later compare() call would discover a state both above and below another. + EXPECT_FALSE(order.mergeNodes(order.getNode(3), order.getNode(2))); + EXPECT_TRUE(order.isInvalid()); + + // Further compare() calls on the now-invalid order must not crash. + EXPECT_NO_FATAL_FAILURE(order.compare(4, 5)); + EXPECT_NO_FATAL_FAILURE(order.compare(3, 4)); + EXPECT_NO_FATAL_FAILURE(order.compare(0, 1)); +} + TEST(OrderTest, sort_states) { auto numberOfStates = 7; auto above = storm::storage::BitVector(numberOfStates);