diff --git a/src/storm-pars/analysis/AssumptionChecker.cpp b/src/storm-pars/analysis/AssumptionChecker.cpp index 5fe86eff5..43d0e75e4 100644 --- a/src/storm-pars/analysis/AssumptionChecker.cpp +++ b/src/storm-pars/analysis/AssumptionChecker.cpp @@ -130,7 +130,7 @@ namespace storm { } template - AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, Lattice* lattice) { + AssumptionStatus AssumptionChecker::validateAssumption(std::shared_ptr assumption, Order* order) { // First check if based on sample points the assumption can be discharged auto result = checkOnSamples(assumption); assert (result != AssumptionStatus::VALID); @@ -156,7 +156,7 @@ namespace storm { std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName())); if (row1.getNumberOfEntries() == 2 && row2.getNumberOfEntries() == 2) { - // If the states have the same successors for which we know the position in the lattice + // If the states have the same successors for which we know the position in the order // We can check with a function if the assumption holds auto state1succ1 = row1.begin(); @@ -171,12 +171,12 @@ namespace storm { if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) { if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Greater - && lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Lattice::NodeComparison::UNKNOWN) { + && order->compare(state1succ1->getColumn(), state1succ2->getColumn()) != Order::NodeComparison::UNKNOWN) { // The assumption should be the greater assumption // If the result is unknown, we cannot compare, also SMTSolver will not help - result = validateAssumptionSMTSolver(assumption, lattice); + result = validateAssumptionSMTSolver(assumption, order); -// result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1, +// result = validateAssumptionFunction(order, state1succ1, state1succ2, state2succ1, // state2succ2); } else if (assumption->getRelationType() == expressions::BinaryRelationExpression::RelationType::Equal) { // The assumption is equal, the successors are the same, @@ -188,17 +188,17 @@ namespace storm { result = AssumptionStatus::UNKNOWN; } } else { - result = validateAssumptionSMTSolver(assumption, lattice); + result = validateAssumptionSMTSolver(assumption, order); } } else { - result = validateAssumptionSMTSolver(assumption, lattice); + result = validateAssumptionSMTSolver(assumption, order); } } return result; } template - AssumptionStatus AssumptionChecker::validateAssumptionFunction(Lattice* lattice, + AssumptionStatus AssumptionChecker::validateAssumptionFunction(Order* order, typename storage::SparseMatrix::iterator state1succ1, typename storage::SparseMatrix::iterator state1succ2, typename storage::SparseMatrix::iterator state2succ1, @@ -212,11 +212,11 @@ namespace storm { // Calculate the difference in probability for the "highest" successor state ValueType prob; - auto comp = lattice->compare(state1succ1->getColumn(), state1succ2->getColumn()); - assert (comp == Lattice::NodeComparison::ABOVE || comp == Lattice::NodeComparison::BELOW); - if (comp == Lattice::NodeComparison::ABOVE) { + auto comp = order->compare(state1succ1->getColumn(), state1succ2->getColumn()); + assert (comp == Order::NodeComparison::ABOVE || comp == Order::NodeComparison::BELOW); + if (comp == Order::NodeComparison::ABOVE) { prob = state1succ1->getValue() - state2succ1->getValue(); - } else if (comp == Lattice::NodeComparison::BELOW) { + } else if (comp == Order::NodeComparison::BELOW) { prob = state1succ2->getValue() - state2succ2->getValue(); } @@ -246,7 +246,7 @@ namespace storm { template - AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(std::shared_ptr assumption, Lattice* lattice) { + AssumptionStatus AssumptionChecker::validateAssumptionSMTSolver(std::shared_ptr assumption, Order* order) { std::shared_ptr smtSolverFactory = std::make_shared(); std::shared_ptr manager(new expressions::ExpressionManager()); @@ -272,14 +272,14 @@ namespace storm { if (!manager->hasVariable(varname2)) { stateVariables.insert(manager->declareRationalVariable(varname2)); } - auto comp = lattice->compare(itr1->getColumn(), itr2->getColumn()); - if (comp == Lattice::NodeComparison::ABOVE) { + auto comp = order->compare(itr1->getColumn(), itr2->getColumn()); + if (comp == Order::NodeComparison::ABOVE) { exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) <= manager->getVariable(varname2)); - } else if (comp == Lattice::NodeComparison::BELOW) { + } else if (comp == Order::NodeComparison::BELOW) { exprOrderSucc = exprOrderSucc && !(manager->getVariable(varname1) >= manager->getVariable(varname2)); - } else if (comp == Lattice::NodeComparison::SAME) { + } else if (comp == Order::NodeComparison::SAME) { exprOrderSucc = exprOrderSucc && (manager->getVariable(varname1) = manager->getVariable(varname2)); } else { @@ -331,7 +331,7 @@ namespace storm { s.add(exprOrderSucc); s.add(exprBounds); - // assert that sorting of successors in the lattice and the bounds on the expression are at least satisfiable + // assert that sorting of successors in the order and the bounds on the expression are at least satisfiable assert (s.check() == solver::SmtSolver::CheckResult::Sat); s.add(exprToCheck); auto smtRes = s.check(); diff --git a/src/storm-pars/analysis/AssumptionChecker.h b/src/storm-pars/analysis/AssumptionChecker.h index c1e58dd69..802291291 100644 --- a/src/storm-pars/analysis/AssumptionChecker.h +++ b/src/storm-pars/analysis/AssumptionChecker.h @@ -7,7 +7,7 @@ #include "storm/environment/Environment.h" #include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm-pars/storage/ParameterRegion.h" -#include "Lattice.h" +#include "Order.h" namespace storm { namespace analysis { @@ -50,22 +50,22 @@ namespace storm { AssumptionStatus checkOnSamples(std::shared_ptr assumption); /*! - * Tries to validate an assumption based on the lattice and underlying transition matrix. + * Tries to validate an assumption based on the order and underlying transition matrix. * * @param assumption The assumption to validate. - * @param lattice The lattice. + * @param order The order. * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID */ - AssumptionStatus validateAssumption(std::shared_ptr assumption, Lattice* lattice); + AssumptionStatus validateAssumption(std::shared_ptr assumption, Order* order); /*! - * Tries to validate an assumption based on the lattice, and SMT solving techniques + * Tries to validate an assumption based on the order, and SMT solving techniques * * @param assumption The assumption to validate. - * @param lattice The lattice. + * @param order The order. * @return AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID */ - AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr assumption, Lattice* lattice); + AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr assumption, Order* order); private: std::shared_ptr formula; @@ -76,7 +76,7 @@ namespace storm { void createSamples(); - AssumptionStatus validateAssumptionFunction(Lattice* lattice, + AssumptionStatus validateAssumptionFunction(Order* order, typename storage::SparseMatrix::iterator state1succ1, typename storage::SparseMatrix::iterator state1succ2, typename storage::SparseMatrix::iterator state2succ1, diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 78cebe88e..d889e3f13 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -16,7 +16,7 @@ namespace storm { template - std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) { + std::map, AssumptionStatus> AssumptionMaker::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order) { std::map, AssumptionStatus> result; expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); @@ -29,7 +29,7 @@ namespace storm { AssumptionStatus result2; AssumptionStatus result3; if (validate) { - result1 = assumptionChecker->validateAssumption(assumption1, lattice); + result1 = assumptionChecker->validateAssumption(assumption1, order); } else { result1 = AssumptionStatus::UNKNOWN; } @@ -42,7 +42,7 @@ namespace storm { expressions::BinaryRelationExpression::RelationType::Greater)); if (validate) { - result2 = assumptionChecker->validateAssumption(assumption2, lattice); + result2 = assumptionChecker->validateAssumption(assumption2, order); } else { result2 = AssumptionStatus::UNKNOWN; } @@ -53,7 +53,7 @@ namespace storm { var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), expressions::BinaryRelationExpression::RelationType::Equal)); if (validate) { - result3 = assumptionChecker->validateAssumption(assumption3, lattice); + result3 = assumptionChecker->validateAssumption(assumption3, order); } else { result3 = AssumptionStatus::UNKNOWN; } diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 42710fcc6..41643fb5a 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -2,8 +2,8 @@ #define STORM_ASSUMPTIONMAKER_H #include "AssumptionChecker.h" -#include "Lattice.h" -#include "LatticeExtender.h" +#include "Order.h" +#include "OrderExtender.h" #include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm-pars/utility/ModelInstantiator.h" @@ -16,9 +16,9 @@ namespace storm { typedef std::shared_ptr AssumptionType; public: /*! - * Constructs AssumptionMaker based on the lattice extender, the assumption checker and number of states of the mode + * Constructs AssumptionMaker based on the order extender, the assumption checker and number of states of the mode * - * @param latticeExtender The LatticeExtender which needs the assumptions made by the AssumptionMaker. + * @param orderExtender The OrderExtender which needs the assumptions made by the AssumptionMaker. * @param checker The AssumptionChecker which checks the assumptions at sample points. * @param numberOfStates The number of states of the model. */ @@ -31,10 +31,10 @@ namespace storm { * * @param val1 First state number * @param val2 Second state number - * @param lattice The lattice on which the assumptions are checked + * @param order The order on which the assumptions are checked * @return Map with three assumptions, and the validation */ - std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice); + std::map, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order); private: AssumptionChecker* assumptionChecker; diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h deleted file mode 100644 index cc4e7370f..000000000 --- a/src/storm-pars/analysis/LatticeExtender.h +++ /dev/null @@ -1,83 +0,0 @@ -#ifndef STORM_LATTICEEXTENDER_H -#define STORM_LATTICEEXTENDER_H - -#include -#include "storm/models/sparse/Dtmc.h" -#include "storm-pars/analysis/Lattice.h" -#include "storm/api/storm.h" -#include "storm-pars/storage/ParameterRegion.h" -#include "storm/storage/StronglyConnectedComponentDecomposition.h" -#include "storm/storage/StronglyConnectedComponent.h" - - - -namespace storm { - namespace analysis { - - - template - class LatticeExtender { - - public: - /*! - * Constructs LatticeExtender which can extend a lattice - * - * @param model The model for which the lattice should be extended. - */ - LatticeExtender(std::shared_ptr> model); - - /*! - * Creates a lattice based on the given formula. - * - * @param formulas The formulas based on which the lattice is created, only the first is used. - * @return A triple with a pointer to the lattice and two states of which the current place in the lattice - * is unknown but needed. When the states have as number the number of states, no states are - * unplaced but needed. - */ - std::tuple toLattice(std::vector> formulas); - - /*! - * Creates a lattice based on the given extremal values. - * - * @return A triple with a pointer to the lattice and two states of which the current place in the lattice - * is unknown but needed. When the states have as number the number of states, no states are - * unplaced but needed. - */ - std::tuple toLattice(std::vector> formulas, std::vector minValues, std::vector maxValues); - - - /*! - * Extends the lattice based on the given assumption. - * - * @param lattice The lattice. - * @param assumption The assumption on states. - * @return A triple with a pointer to the lattice and two states of which the current place in the lattice - * is unknown but needed. When the states have as number the number of states, no states are - * unplaced but needed. - */ - std::tuple extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr assumption = nullptr); - - - private: - std::shared_ptr> model; - - std::map stateMap; - - bool acyclic; - - bool assumptionSeen; - - storm::storage::StronglyConnectedComponentDecomposition sccs; - - storm::storage::SparseMatrix matrix; - - void handleAssumption(Lattice* lattice, std::shared_ptr assumption); - - std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); - - std::tuple allSuccAdded(Lattice* lattice, uint_fast64_t stateNumber); - }; - } -} - -#endif //STORM_LATTICEEXTENDER_H diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 8565d97d3..1137d8ce1 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -1,8 +1,8 @@ #include "MonotonicityChecker.h" #include "storm-pars/analysis/AssumptionMaker.h" #include "storm-pars/analysis/AssumptionChecker.h" -#include "storm-pars/analysis/Lattice.h" -#include "storm-pars/analysis/LatticeExtender.h" +#include "storm-pars/analysis/Order.h" +#include "storm-pars/analysis/OrderExtender.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" @@ -64,28 +64,28 @@ namespace storm { region = storm::storage::ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); } - this->extender = new storm::analysis::LatticeExtender(sparseModel); + this->extender = new storm::analysis::OrderExtender(sparseModel); } template - std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity() { - auto map = createLattice(); + std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity() { + auto map = createOrder(); std::shared_ptr> sparseModel = model->as>(); auto matrix = sparseModel->getTransitionMatrix(); return checkMonotonicity(map, matrix); } template - std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { + std::map::type, std::pair>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { storm::utility::Stopwatch monotonicityCheckWatch(true); - std::map::type, std::pair>> result; + std::map::type, std::pair>> result; outfile.open(filename, std::ios_base::app); if (map.size() == 0) { // Nothing is known outfile << " No assumptions -"; - STORM_PRINT("No valid assumptions, couldn't build a sufficient lattice"); + STORM_PRINT("No valid assumptions, couldn't build a sufficient order"); if (resultCheckOnSamples.size() != 0) { STORM_PRINT("\n" << "Based results on samples"); } else { @@ -107,11 +107,11 @@ namespace storm { } else { auto i = 0; for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) { - auto lattice = itr->first; + auto order = itr->first; - auto addedStates = lattice->getAddedStates()->getNumberOfSetBits(); - assert (addedStates == lattice->getAddedStates()->size()); - std::map::type, std::pair> varsMonotone = analyseMonotonicity(i, lattice, + auto addedStates = order->getAddedStates()->getNumberOfSetBits(); + assert (addedStates == order->getAddedStates()->size()); + std::map::type, std::pair> varsMonotone = analyseMonotonicity(i, order, matrix); auto assumptions = itr->second; @@ -157,8 +157,8 @@ namespace storm { } } result.insert( - std::pair::type, std::pair>>( - lattice, varsMonotone)); + std::pair::type, std::pair>>( + order, varsMonotone)); } ++i; outfile << ";"; @@ -172,11 +172,11 @@ namespace storm { } template - std::map>> MonotonicityChecker::createLattice() { - // Transform to Lattices - storm::utility::Stopwatch latticeWatch(true); + std::map>> MonotonicityChecker::createOrder() { + // Transform to Orders + storm::utility::Stopwatch orderWatch(true); - // Use parameter lifting modelchecker to get initial min/max values for lattice creation + // Use parameter lifting modelchecker to get initial min/max values for order creation storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> plaModelChecker; std::unique_ptr checkResult; auto env = Environment(); @@ -195,12 +195,12 @@ namespace storm { std::vector minValues = minRes.getValueVector(); std::vector maxValues = maxRes.getValueVector(); - // Create initial lattice - std::tuple criticalTuple = extender->toLattice(formulas, minValues, maxValues); + // Create initial order + std::tuple criticalTuple = extender->toOrder(formulas, minValues, maxValues); // Continue based on not (yet) sorted states - std::map>> result; + std::map>> result; auto val1 = std::get<1>(criticalTuple); auto val2 = std::get<2>(criticalTuple); @@ -208,7 +208,7 @@ namespace storm { std::vector> assumptions; if (val1 == numberOfStates && val2 == numberOfStates) { - result.insert(std::pair>>(std::get<0>(criticalTuple), assumptions)); + result.insert(std::pair>>(std::get<0>(criticalTuple), assumptions)); } else if (val1 != numberOfStates && val2 != numberOfStates) { storm::analysis::AssumptionChecker *assumptionChecker; @@ -223,26 +223,26 @@ namespace storm { "Unable to perform monotonicity analysis on the provided model type."); } auto assumptionMaker = new storm::analysis::AssumptionMaker(assumptionChecker, numberOfStates, validate); - result = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, val1, val2, assumptions); + result = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, val1, val2, assumptions); } else { assert(false); } - latticeWatch.stop(); + orderWatch.stop(); return result; } template - std::map>> MonotonicityChecker::extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions) { - std::map>> result; + std::map>> MonotonicityChecker::extendOrderWithAssumptions(storm::analysis::Order* order, storm::analysis::AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions) { + std::map>> result; auto numberOfStates = model->getNumberOfStates(); if (val1 == numberOfStates || val2 == numberOfStates) { assert (val1 == val2); - assert (lattice->getAddedStates()->size() == lattice->getAddedStates()->getNumberOfSetBits()); - result.insert(std::pair>>(lattice, assumptions)); + assert (order->getAddedStates()->size() == order->getAddedStates()->getNumberOfSetBits()); + result.insert(std::pair>>(order, assumptions)); } else { // Make the three assumptions - auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, lattice); + auto assumptionTriple = assumptionMaker->createAndCheckAssumption(val1, val2, order); assert (assumptionTriple.size() == 3); auto itr = assumptionTriple.begin(); auto assumption1 = *itr; @@ -252,7 +252,7 @@ namespace storm { auto assumption3 = *itr; if (assumption1.second != AssumptionStatus::INVALID) { - auto latticeCopy = new Lattice(lattice); + auto orderCopy = new Order(order); auto assumptionsCopy = std::vector>(assumptions); if (assumption1.second == AssumptionStatus::UNKNOWN) { @@ -260,9 +260,9 @@ namespace storm { assumptionsCopy.push_back(assumption1.first); } - auto criticalTuple = extender->extendLattice(latticeCopy, assumption1.first); + auto criticalTuple = extender->extendOrder(orderCopy, assumption1.first); if (somewhereMonotonicity(std::get<0>(criticalTuple))) { - auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptionsCopy); result.insert(map.begin(), map.end()); @@ -270,16 +270,16 @@ namespace storm { } if (assumption2.second != AssumptionStatus::INVALID) { - auto latticeCopy = new Lattice(lattice); + auto orderCopy = new Order(order); auto assumptionsCopy = std::vector>(assumptions); if (assumption2.second == AssumptionStatus::UNKNOWN) { assumptionsCopy.push_back(assumption2.first); } - auto criticalTuple = extender->extendLattice(latticeCopy, assumption2.first); + auto criticalTuple = extender->extendOrder(orderCopy, assumption2.first); if (somewhereMonotonicity(std::get<0>(criticalTuple))) { - auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptionsCopy); result.insert(map.begin(), map.end()); @@ -287,14 +287,14 @@ namespace storm { } if (assumption3.second != AssumptionStatus::INVALID) { - // Here we can use the original lattice and assumptions set + // Here we can use the original order and assumptions set if (assumption3.second == AssumptionStatus::UNKNOWN) { assumptions.push_back(assumption3.first); } - auto criticalTuple = extender->extendLattice(lattice, assumption3.first); + auto criticalTuple = extender->extendOrder(order, assumption3.first); if (somewhereMonotonicity(std::get<0>(criticalTuple))) { - auto map = extendLatticeWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, + auto map = extendOrderWithAssumptions(std::get<0>(criticalTuple), assumptionMaker, std::get<1>(criticalTuple), std::get<2>(criticalTuple), assumptions); result.insert(map.begin(), map.end()); @@ -317,7 +317,7 @@ namespace storm { } template - std::map::type, std::pair> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix matrix) { + std::map::type, std::pair> MonotonicityChecker::analyseMonotonicity(uint_fast64_t j, storm::analysis::Order* order, storm::storage::SparseMatrix matrix) { std::map::type, std::pair> varsMonotone; // go over all rows, check for each row local monotonicity @@ -365,8 +365,8 @@ namespace storm { - // Sort the states based on the lattice - auto sortedStates = lattice->sortStates(states); + // Sort the states based on the order + auto sortedStates = order->sortStates(states); if (sortedStates[sortedStates.size() - 1] == matrix.getColumnCount()) { // If the states are not all sorted, we still might obtain some monotonicity for (auto var: vars) { @@ -383,16 +383,16 @@ namespace storm { auto derivative2 = getDerivative(itr2->second, var); auto derivative3 = getDerivative(itr3->second, var); - auto compare = lattice->compare(itr2->first, itr3->first); + auto compare = order->compare(itr2->first, itr3->first); - if (compare == Lattice::ABOVE) { + if (compare == Order::ABOVE) { // As the first state (itr2) is above the second state (itr3) it // is sufficient to look at the derivative of itr2. std::pair mon2; mon2 = checkDerivative(derivative2, region); value->first &= mon2.first; value->second &= mon2.second; - } else if (compare == Lattice::BELOW) { + } else if (compare == Order::BELOW) { // As the second state (itr3) is above the first state (itr2) it // is sufficient to look at the derivative of itr3. std::pair mon3; @@ -400,7 +400,7 @@ namespace storm { mon3 = checkDerivative(derivative3, region); value->first &= mon3.first; value->second &= mon3.second; - } else if (compare == Lattice::SAME) { + } else if (compare == Order::SAME) { // Behaviour doesn't matter, as the states are at the same level. } else { // only if derivatives are the same we can continue @@ -447,7 +447,7 @@ namespace storm { } template - bool MonotonicityChecker::somewhereMonotonicity(Lattice* lattice) { + bool MonotonicityChecker::somewhereMonotonicity(Order* order) { std::shared_ptr> sparseModel = model->as>(); auto matrix = sparseModel->getTransitionMatrix(); @@ -501,16 +501,16 @@ namespace storm { auto derivative2 = getDerivative(itr2->second, var); auto derivative3 = getDerivative(itr3->second, var); - auto compare = lattice->compare(itr2->first, itr3->first); + auto compare = order->compare(itr2->first, itr3->first); - if (compare == Lattice::ABOVE) { + if (compare == Order::ABOVE) { // As the first state (itr2) is above the second state (itr3) it // is sufficient to look at the derivative of itr2. std::pair mon2; mon2 = checkDerivative(derivative2, region); value->first &= mon2.first; value->second &= mon2.second; - } else if (compare == Lattice::BELOW) { + } else if (compare == Order::BELOW) { // As the second state (itr3) is above the first state (itr2) it // is sufficient to look at the derivative of itr3. std::pair mon3; @@ -518,7 +518,7 @@ namespace storm { mon3 = checkDerivative(derivative3, region); value->first &= mon3.first; value->second &= mon3.second; - } else if (compare == Lattice::SAME) { + } else if (compare == Order::SAME) { // Behaviour doesn't matter, as the states are at the same level. } else { // As the relation between the states is unknown, we don't do anything diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index 0ef738154..5d32ecf70 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -2,8 +2,8 @@ #define STORM_MONOTONICITYCHECKER_H #include -#include "Lattice.h" -#include "LatticeExtender.h" +#include "Order.h" +#include "OrderExtender.h" #include "AssumptionMaker.h" #include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -41,12 +41,12 @@ namespace storm { /*! * Checks for model and formula as provided in constructor for monotonicity */ - std::map::type, std::pair>> checkMonotonicity(); + std::map::type, std::pair>> checkMonotonicity(); /*! - * Checks if monotonicity can be found in this lattice. Unordered states are not checked + * Checks if monotonicity can be found in this order. Unordered states are not checked */ - bool somewhereMonotonicity(storm::analysis::Lattice* lattice) ; + bool somewhereMonotonicity(storm::analysis::Order* order) ; /*! * Checks if a derivative >=0 or/and <=0 @@ -113,11 +113,11 @@ namespace storm { } private: - std::map::type, std::pair>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); + std::map::type, std::pair>> checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix); - std::map::type, std::pair> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix matrix) ; + std::map::type, std::pair> analyseMonotonicity(uint_fast64_t i, Order* order, storm::storage::SparseMatrix matrix) ; - std::map>> createLattice(); + std::map>> createOrder(); std::map::type, std::pair> checkOnSamples(std::shared_ptr> model, uint_fast64_t numberOfSamples); @@ -127,7 +127,7 @@ namespace storm { ValueType getDerivative(ValueType function, typename utility::parametric::VariableType::type var); - std::map>> extendLatticeWithAssumptions(Lattice* lattice, AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); + std::map>> extendOrderWithAssumptions(Order* order, AssumptionMaker* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector> assumptions); std::shared_ptr model; @@ -139,7 +139,7 @@ namespace storm { std::map::type, std::pair> resultCheckOnSamples; - LatticeExtender *extender; + OrderExtender *extender; std::ofstream outfile; diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Order.cpp similarity index 81% rename from src/storm-pars/analysis/Lattice.cpp rename to src/storm-pars/analysis/Order.cpp index 3253a7d44..fe8b94233 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Order.cpp @@ -1,10 +1,10 @@ #include #include -#include "Lattice.h" +#include "Order.h" namespace storm { namespace analysis { - Lattice::Lattice(storm::storage::BitVector* topStates, + Order::Order(storm::storage::BitVector* topStates, storm::storage::BitVector* bottomStates, storm::storage::BitVector* initialMiddleStates, uint_fast64_t numberOfStates, @@ -41,7 +41,7 @@ namespace storm { } } - Lattice::Lattice(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates, std::vector* statesSorted) { + Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates, std::vector* statesSorted) { nodes = std::vector(numberOfStates); this->numberOfStates = numberOfStates; @@ -67,13 +67,13 @@ namespace storm { assert (addedStates->getNumberOfSetBits() == 2); } - Lattice::Lattice(Lattice* lattice) { - numberOfStates = lattice->getAddedStates()->size(); + Order::Order(Order* order) { + numberOfStates = order->getAddedStates()->size(); nodes = std::vector(numberOfStates); addedStates = new storm::storage::BitVector(numberOfStates); - this->doneBuilding = lattice->getDoneBuilding(); + this->doneBuilding = order->getDoneBuilding(); - auto oldNodes = lattice->getNodes(); + auto oldNodes = order->getNodes(); // Create nodes for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { Node *oldNode = (*itr); @@ -84,14 +84,14 @@ namespace storm { addedStates->set(i); nodes[i] = newNode; } - if (oldNode == lattice->getTop()) { + if (oldNode == order->getTop()) { top = newNode; - } else if (oldNode == lattice->getBottom()) { + } else if (oldNode == order->getBottom()) { bottom = newNode; } } } - assert(*addedStates == *(lattice->getAddedStates())); + assert(*addedStates == *(order->getAddedStates())); // set all states above and below for (auto itr = oldNodes.begin(); itr != oldNodes.end(); ++itr) { @@ -102,11 +102,11 @@ namespace storm { } } - this->statesSorted = lattice->statesSorted; - this->statesToHandle = lattice->statesToHandle; + this->statesSorted = order->statesSorted; + this->statesToHandle = order->statesToHandle; } - void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { + void Order::addBetween(uint_fast64_t state, Node *above, Node *below) { assert(!(*addedStates)[state]); assert(compare(above, below) == ABOVE); @@ -122,7 +122,7 @@ namespace storm { addedStates->set(state); } - void Lattice::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { + void Order::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) { assert(!(*addedStates)[state]); assert(compare(above, below) == ABOVE); @@ -132,19 +132,19 @@ namespace storm { } - void Lattice::addToNode(uint_fast64_t state, Node *node) { + void Order::addToNode(uint_fast64_t state, Node *node) { assert(!(*addedStates)[state]); node->states.insert(state); nodes[state] = node; addedStates->set(state); } - void Lattice::add(uint_fast64_t state) { + void Order::add(uint_fast64_t state) { assert(!(*addedStates)[state]); addBetween(state, top, bottom); } - void Lattice::addRelationNodes(Lattice::Node *above, Lattice::Node * below) { + void Order::addRelationNodes(Order::Node *above, Order::Node * below) { assert (compare(above, below) == UNKNOWN); for (auto const& state : above->states) { below->statesAbove.set(state); @@ -153,15 +153,15 @@ namespace storm { assert (compare(above, below) == ABOVE); } - void Lattice::addRelation(uint_fast64_t above, uint_fast64_t below) { + void Order::addRelation(uint_fast64_t above, uint_fast64_t below) { addRelationNodes(getNode(above), getNode(below)); } - Lattice::NodeComparison Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { + Order::NodeComparison Order::compare(uint_fast64_t state1, uint_fast64_t state2) { return compare(getNode(state1), getNode(state2)); } - Lattice::NodeComparison Lattice::compare(Node* node1, Node* node2) { + Order::NodeComparison Order::compare(Node* node1, Node* node2) { if (node1 != nullptr && node2 != nullptr) { if (node1 == node2) { return SAME; @@ -194,39 +194,39 @@ namespace storm { } - bool Lattice::contains(uint_fast64_t state) { + bool Order::contains(uint_fast64_t state) { return state >= 0 && state < addedStates->size() && addedStates->get(state); } - Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { + Order::Node *Order::getNode(uint_fast64_t stateNumber) { return nodes.at(stateNumber); } - Lattice::Node *Lattice::getTop() { + Order::Node *Order::getTop() { return top; } - Lattice::Node *Lattice::getBottom() { + Order::Node *Order::getBottom() { return bottom; } - std::vector Lattice::getNodes() { + std::vector Order::getNodes() { return nodes; } - storm::storage::BitVector* Lattice::getAddedStates() { + storm::storage::BitVector* Order::getAddedStates() { return addedStates; } - bool Lattice::getDoneBuilding() { + bool Order::getDoneBuilding() { return doneBuilding; } - void Lattice::setDoneBuilding(bool done) { + void Order::setDoneBuilding(bool done) { doneBuilding = done; } - std::vector Lattice::sortStates(storm::storage::BitVector* states) { + std::vector Order::sortStates(storm::storage::BitVector* states) { auto numberOfSetBits = states->getNumberOfSetBits(); auto stateSize = states->size(); auto result = std::vector(numberOfSetBits, stateSize); @@ -273,11 +273,11 @@ namespace storm { return result; } - void Lattice::toString(std::ostream &out) { + void Order::toString(std::ostream &out) { } - bool Lattice::above(Node *node1, Node *node2) { + bool Order::above(Node *node1, Node *node2) { bool found = false; for (auto const& state : node1->states) { found = ((node2->statesAbove))[state]; @@ -304,8 +304,8 @@ namespace storm { return found; } - bool Lattice::above(storm::analysis::Lattice::Node *node1, storm::analysis::Lattice::Node *node2, - storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen) { + bool Order::above(storm::analysis::Order::Node *node1, storm::analysis::Order::Node *node2, + storm::analysis::Order::Node *nodePrev, storm::storage::BitVector *statesSeen) { bool found = false; for (auto const& state : node1->states) { found = ((node2->statesAbove))[state]; @@ -333,7 +333,7 @@ namespace storm { return found; } - void Lattice::mergeNodes(storm::analysis::Lattice::Node *node1, storm::analysis::Lattice::Node *node2) { + void Order::mergeNodes(storm::analysis::Order::Node *node1, storm::analysis::Order::Node *node2) { // Merges node2 into node 1 // everything above n2 also above n1 node1->statesAbove|=((node2->statesAbove)); @@ -347,7 +347,7 @@ namespace storm { } } - void Lattice::merge(uint_fast64_t var1, uint_fast64_t var2) { + void Order::merge(uint_fast64_t var1, uint_fast64_t var2) { mergeNodes(getNode(var1), getNode(var2)); } } diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Order.h similarity index 82% rename from src/storm-pars/analysis/Lattice.h rename to src/storm-pars/analysis/Order.h index 9de5ed07b..bd5270e30 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Order.h @@ -1,5 +1,5 @@ -#ifndef LATTICE_LATTICE_H -#define LATTICE_LATTICE_H +#ifndef ORDER_ORDER_H +#define ORDER_ORDER_H #include #include @@ -12,7 +12,7 @@ namespace storm { namespace analysis { - class Lattice { + class Order { public: /*! @@ -30,35 +30,35 @@ namespace storm { }; /*! - * Constructs a lattice with the given top node and bottom node. + * Constructs an order with the given top node and bottom node. * - * @param topNode The top node of the resulting lattice. - * @param bottomNode The bottom node of the resulting lattice. + * @param topNode The top node of the resulting order. + * @param bottomNode The bottom node of the resulting order. */ - Lattice(storm::storage::BitVector* topStates, + Order(storm::storage::BitVector* topStates, storm::storage::BitVector* bottomStates, storm::storage::BitVector* initialMiddleStates, uint_fast64_t numberOfStates, std::vector* statesSorted); /*! - * Constructs a lattice with the given top state and bottom state. + * Constructs an order with the given top state and bottom state. * - * @param top The top state of the resulting lattice. - * @param bottom The bottom state of the resulting lattice. - * @param numberOfStates Max number of states in endlattice. + * @param top The top state of the resulting order. + * @param bottom The bottom state of the resulting order. + * @param numberOfStates Max number of states in order. */ - Lattice(uint_fast64_t top, + Order(uint_fast64_t top, uint_fast64_t bottom, uint_fast64_t numberOfStates, std::vector* statesSorted); /*! - * Constructs a copy of the given lattice. + * Constructs a copy of the given order. * - * @param lattice The original lattice. + * @param order The original order. */ - Lattice(Lattice* lattice); + Order(Order* order); /*! * Adds a node with the given state below node1 and above node2. @@ -85,39 +85,39 @@ namespace storm { void addToNode(uint_fast64_t state, Node *node); /*! - * Adds state between the top and bottom node of the lattice + * Adds state between the top and bottom node of the order * @param state The given state */ void add(uint_fast64_t state); /*! - * Adds a new relation between two nodes to the lattice - * @param above The node closest to the top Node of the Lattice. - * @param below The node closest to the bottom Node of the Lattice. + * Adds a new relation between two nodes to the order + * @param above The node closest to the top Node of the Order. + * @param below The node closest to the bottom Node of the Order. */ - void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below); + void addRelationNodes(storm::analysis::Order::Node *above, storm::analysis::Order::Node * below); /*! - * Adds a new relation between two states to the lattice - * @param above The state closest to the top Node of the Lattice. - * @param below The state closest to the bottom Node of the Lattice. + * Adds a new relation between two states to the order + * @param above The state closest to the top Node of the Order. + * @param below The state closest to the bottom Node of the Order. */ void addRelation(uint_fast64_t above, uint_fast64_t below); /*! * Compares the level of the nodes of the states. - * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice. + * Behaviour unknown when one or more of the states doesnot occur at any Node in the Order. * @param state1 The first state. * @param state2 The second state. * @return SAME if the nodes are on the same level; * ABOVE if the node of the first state is closer to top then the node of the second state; * BELOW if the node of the second state is closer to top then the node of the first state; - * UNKNOWN if it is unclear from the structure of the lattice how the nodes relate. + * UNKNOWN if it is unclear from the structure of the order how the nodes relate. */ - Lattice::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); + Order::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); /*! - * Check if state is already in lattice + * Check if state is already in order * @param state * @return */ @@ -133,25 +133,25 @@ namespace storm { Node *getNode(uint_fast64_t state); /*! - * Retrieves the top node of the lattice. + * Retrieves the top node of the order. * * @return The top node. */ Node* getTop(); /*! - * Retrieves the bottom node of the lattice. + * Retrieves the bottom node of the order. * * @return The bottom node. */ Node* getBottom(); /*! - * Returns the vector with the nodes of the lattice. + * Returns the vector with the nodes of the order. * Each index in the vector refers to a state. * When the state is not yet added at a node, it will contain the nullptr. * - * @return The vector with nodes of the lattice. + * @return The vector with nodes of the order. */ std::vector getNodes(); @@ -163,13 +163,13 @@ namespace storm { storm::storage::BitVector* getAddedStates(); /*! - * Returns true if done building the lattice. + * Returns true if done building the order. * @return */ bool getDoneBuilding(); /*! - * Compares two nodes in the lattice + * Compares two nodes in the order * @param node1 * @param node2 * @return BELOW, ABOVE, SAME or UNKNOWN @@ -186,12 +186,12 @@ namespace storm { std::vector sortStates(storm::storage::BitVector* states); /*! - * If the lattice is fully build, this can be set to true. + * If the order is fully build, this can be set to true. */ void setDoneBuilding(bool done); /*! - * Prints a string representation of the lattice to the output stream. + * Prints a string representation of the order to the output stream. * * @param out The stream to output to. */ @@ -227,10 +227,10 @@ namespace storm { bool above(Node * node1, Node * node2); - bool above(Node * node1, Node * node2, storm::analysis::Lattice::Node *nodePrev, storm::storage::BitVector *statesSeen); + bool above(Node * node1, Node * node2, storm::analysis::Order::Node *nodePrev, storm::storage::BitVector *statesSeen); bool doneBuilding; }; } } -#endif //LATTICE_LATTICE_H +#endif //ORDER_ORDER_H diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/OrderExtender.cpp similarity index 70% rename from src/storm-pars/analysis/LatticeExtender.cpp rename to src/storm-pars/analysis/OrderExtender.cpp index b36230492..6662e2757 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/OrderExtender.cpp @@ -2,7 +2,7 @@ // Created by Jip Spel on 28.08.18. // -#include "LatticeExtender.h" +#include "OrderExtender.h" #include "storm/utility/macros.h" #include "storm/utility/graph.h" #include "storm/storage/SparseMatrix.h" @@ -31,7 +31,7 @@ namespace storm { namespace analysis { template - LatticeExtender::LatticeExtender(std::shared_ptr> model) { + OrderExtender::OrderExtender(std::shared_ptr> model) { this->model = model; this->matrix = model->getTransitionMatrix(); this->assumptionSeen = false; @@ -61,7 +61,7 @@ namespace storm { } template - std::tuple LatticeExtender::toLattice(std::vector> formulas) { + std::tuple OrderExtender::toOrder(std::vector> formulas) { STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() @@ -90,14 +90,14 @@ namespace storm { STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states"); STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); - // Transform to Lattice + // Transform to Order auto matrix = this->model->getTransitionMatrix(); auto initialMiddleStates = storm::storage::BitVector(numberOfStates); // Check if MC contains cycles storm::storage::StronglyConnectedComponentDecompositionOptions const options; - // Create the Lattice + // Create the Order if (!acyclic) { for (auto i = 0; i < sccs.size(); ++i) { @@ -121,14 +121,14 @@ namespace storm { } } std::vector statesSorted = storm::utility::graph::getTopologicalSort(matrix); - Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates, &statesSorted); + Order *order = new Order(&topStates, &bottomStates, &initialMiddleStates, numberOfStates, &statesSorted); - return this->extendLattice(lattice); + return this->extendOrder(order); } template - std::tuple LatticeExtender::toLattice(std::vector> formulas, std::vector minValues, std::vector maxValues) { + std::tuple OrderExtender::toOrder(std::vector> formulas, std::vector minValues, std::vector maxValues) { uint_fast64_t numberOfStates = this->model->getNumberOfStates(); // Compare min/max for all states @@ -159,12 +159,12 @@ namespace storm { uint_fast64_t bottom = bottomStates.getNextSetIndex(0); uint_fast64_t top = topStates.getNextSetIndex(0); std::vector statesSorted = storm::utility::graph::getTopologicalSort(matrix); - Lattice *lattice = new Lattice(top, bottom, numberOfStates, &statesSorted); + Order *order = new Order(top, bottom, numberOfStates, &statesSorted); - for (auto state : *(lattice->statesSorted)) { + for (auto state : *(order->statesSorted)) { if (state != bottom && state != top) { - assert (lattice != nullptr); + assert (order != nullptr); auto successors = stateMap[state]; if (successors->size() > 1) { uint_fast64_t min = numberOfStates; @@ -190,32 +190,32 @@ namespace storm { } if (allSorted && min != max) { - if (lattice->contains(min) && lattice->contains(max)) { - assert (lattice->compare(min,max) == Lattice::UNKNOWN || lattice->compare(min,max) == Lattice::BELOW); - if (lattice->compare(min, max) == Lattice::UNKNOWN) { - lattice->addRelation(max, min); + if (order->contains(min) && order->contains(max)) { + assert (order->compare(min,max) == Order::UNKNOWN || order->compare(min,max) == Order::BELOW); + if (order->compare(min, max) == Order::UNKNOWN) { + order->addRelation(max, min); } } - if (!lattice->contains(min)) { - if (lattice->contains(max)) { - lattice->addBetween(min, lattice->getNode(max), lattice->getBottom()); + if (!order->contains(min)) { + if (order->contains(max)) { + order->addBetween(min, order->getNode(max), order->getBottom()); } else { - lattice->add(min); + order->add(min); } } - if (!lattice->contains(max)) { - // Because of construction min is in the lattice - lattice->addBetween(max, lattice->getNode(min), lattice->getTop()); + if (!order->contains(max)) { + // Because of construction min is in the order + order->addBetween(max, order->getNode(min), order->getTop()); } - assert (lattice->compare(max, min) == Lattice::ABOVE); - lattice->addBetween(state, max, min); + assert (order->compare(max, min) == Order::ABOVE); + order->addBetween(state, max, min); } } } } // Handle sccs - auto addedStates = lattice->getAddedStates(); + auto addedStates = order->getAddedStates(); for (auto scc : sccs) { if (scc.size() > 1) { auto states = scc.getStates(); @@ -224,7 +224,7 @@ namespace storm { if (addedStates->get(state)) { candidate = -1; break; - // if there is a state of the scc already present in the lattice, there is no need to add one. + // if there is a state of the scc already present in the order, there is no need to add one. } auto successors = stateMap[state]; if (candidate == -1 && successors->getNumberOfSetBits() == 2) { @@ -236,17 +236,17 @@ namespace storm { } } if (candidate != -1) { - lattice->add(candidate); - lattice->statesToHandle->set(candidate); + order->add(candidate); + order->statesToHandle->set(candidate); } } } - return this->extendLattice(lattice); + return this->extendOrder(order); } template - void LatticeExtender::handleAssumption(Lattice* lattice, std::shared_ptr assumption) { + void OrderExtender::handleAssumption(Order* order, std::shared_ptr assumption) { assert (assumption != nullptr); assumptionSeen = true; @@ -260,21 +260,21 @@ namespace storm { storm::expressions::Variable var2 = expr.getSecondOperand()->asVariableExpression().getVariable(); auto val1 = std::stoul(var1.getName(), nullptr, 0); auto val2 = std::stoul(var2.getName(), nullptr, 0); - auto comp = lattice->compare(val1, val2); + auto comp = order->compare(val1, val2); - assert (comp == Lattice::UNKNOWN); - Lattice::Node *n1 = lattice->getNode(val1); - Lattice::Node *n2 = lattice->getNode(val2); + assert (comp == Order::UNKNOWN); + Order::Node *n1 = order->getNode(val1); + Order::Node *n2 = order->getNode(val2); if (n1 != nullptr && n2 != nullptr) { - lattice->mergeNodes(n1,n2); + order->mergeNodes(n1,n2); } else if (n1 != nullptr) { - lattice->addToNode(val2, n1); + order->addToNode(val2, n1); } else if (n2 != nullptr) { - lattice->addToNode(val1, n2); + order->addToNode(val1, n2); } else { - lattice->add(val1); - lattice->addToNode(val2, lattice->getNode(val1)); + order->add(val1); + order->addToNode(val2, order->getNode(val1)); } } else { assert (expr.getFirstOperand()->isVariable() && expr.getSecondOperand()->isVariable()); @@ -282,59 +282,59 @@ namespace storm { storm::expressions::Variable smallest = expr.getSecondOperand()->asVariableExpression().getVariable(); auto val1 = std::stoul(largest.getName(), nullptr, 0); auto val2 = std::stoul(smallest.getName(), nullptr, 0); - auto compareRes = lattice->compare(val1, val2); + auto compareRes = order->compare(val1, val2); - assert(compareRes == Lattice::UNKNOWN); - Lattice::Node *n1 = lattice->getNode(val1); - Lattice::Node *n2 = lattice->getNode(val2); + assert(compareRes == Order::UNKNOWN); + Order::Node *n1 = order->getNode(val1); + Order::Node *n2 = order->getNode(val2); if (n1 != nullptr && n2 != nullptr) { - lattice->addRelationNodes(n1, n2); + order->addRelationNodes(n1, n2); } else if (n1 != nullptr) { - lattice->addBetween(val2, n1, lattice->getBottom()); + order->addBetween(val2, n1, order->getBottom()); } else if (n2 != nullptr) { - lattice->addBetween(val1, lattice->getTop(), n2); + order->addBetween(val1, order->getTop(), n2); } else { - lattice->add(val1); - lattice->addBetween(val2, lattice->getNode(val1), lattice->getBottom()); + order->add(val1); + order->addBetween(val2, order->getNode(val1), order->getBottom()); } } } template - std::tuple LatticeExtender::extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors) { + std::tuple OrderExtender::extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors) { auto numberOfStates = successors->size(); - assert (lattice->getAddedStates()->size() == numberOfStates); + assert (order->getAddedStates()->size() == numberOfStates); if (successors->getNumberOfSetBits() == 1) { // As there is only one successor the current state and its successor must be at the same nodes. - lattice->addToNode(stateNumber, lattice->getNode(successors->getNextSetIndex(0))); + order->addToNode(stateNumber, order->getNode(successors->getNextSetIndex(0))); } else if (successors->getNumberOfSetBits() == 2) { // Otherwise, check how the two states compare, and add if the comparison is possible. uint_fast64_t successor1 = successors->getNextSetIndex(0); uint_fast64_t successor2 = successors->getNextSetIndex(successor1 + 1); - int compareResult = lattice->compare(successor1, successor2); - if (compareResult == Lattice::ABOVE) { + int compareResult = order->compare(successor1, successor2); + if (compareResult == Order::ABOVE) { // successor 1 is closer to top than successor 2 - lattice->addBetween(stateNumber, lattice->getNode(successor1), - lattice->getNode(successor2)); - } else if (compareResult == Lattice::BELOW) { + order->addBetween(stateNumber, order->getNode(successor1), + order->getNode(successor2)); + } else if (compareResult == Order::BELOW) { // successor 2 is closer to top than successor 1 - lattice->addBetween(stateNumber, lattice->getNode(successor2), - lattice->getNode(successor1)); - } else if (compareResult == Lattice::SAME) { + order->addBetween(stateNumber, order->getNode(successor2), + order->getNode(successor1)); + } else if (compareResult == Order::SAME) { // the successors are at the same level - lattice->addToNode(stateNumber, lattice->getNode(successor1)); + order->addToNode(stateNumber, order->getNode(successor1)); } else { - assert(lattice->compare(successor1, successor2) == Lattice::UNKNOWN); - return std::make_tuple(lattice, successor1, successor2); + assert(order->compare(successor1, successor2) == Order::UNKNOWN); + return std::make_tuple(order, successor1, successor2); } } else if (successors->getNumberOfSetBits() > 2) { for (auto const& i : *successors) { for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { - if (lattice->compare(i,j) == Lattice::UNKNOWN) { - return std::make_tuple(lattice, i, j); + if (order->compare(i,j) == Order::UNKNOWN) { + return std::make_tuple(order, i, j); } } } @@ -342,53 +342,53 @@ namespace storm { auto highest = successors->getNextSetIndex(0); auto lowest = highest; for (auto i = successors->getNextSetIndex(highest+1); i < numberOfStates; i = successors->getNextSetIndex(i+1)) { - if (lattice->compare(i, highest) == Lattice::ABOVE) { + if (order->compare(i, highest) == Order::ABOVE) { highest = i; } - if (lattice->compare(lowest, i) == Lattice::ABOVE) { + if (order->compare(lowest, i) == Order::ABOVE) { lowest = i; } } if (lowest == highest) { - lattice->addToNode(stateNumber, lattice->getNode(highest)); + order->addToNode(stateNumber, order->getNode(highest)); } else { - lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); + order->addBetween(stateNumber, order->getNode(highest), order->getNode(lowest)); } } - return std::make_tuple(lattice, numberOfStates, numberOfStates); + return std::make_tuple(order, numberOfStates, numberOfStates); } template - std::tuple LatticeExtender::extendLattice(Lattice* lattice, std::shared_ptr assumption) { + std::tuple OrderExtender::extendOrder(Order* order, std::shared_ptr assumption) { auto numberOfStates = this->model->getNumberOfStates(); if (assumption != nullptr) { - handleAssumption(lattice, assumption); + handleAssumption(order, assumption); } - auto statesSorted = lattice->statesSorted; + auto statesSorted = order->statesSorted; auto oldNumberSet = numberOfStates; - while (oldNumberSet != lattice->getAddedStates()->getNumberOfSetBits()) { - oldNumberSet = lattice->getAddedStates()->getNumberOfSetBits(); + while (oldNumberSet != order->getAddedStates()->getNumberOfSetBits()) { + oldNumberSet = order->getAddedStates()->getNumberOfSetBits(); // Forward reasoning for cycles; if (!acyclic) { - auto statesToHandle = lattice->statesToHandle; + auto statesToHandle = order->statesToHandle; auto stateNumber = statesToHandle->getNextSetIndex(0); while (stateNumber != numberOfStates) { storm::storage::BitVector *successors = stateMap[stateNumber]; - // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet + // Checking for states which are already added to the order, and only have one successor left which haven't been added yet auto succ1 = successors->getNextSetIndex(0); auto succ2 = successors->getNextSetIndex(succ1 + 1); - assert (lattice->contains(stateNumber)); + assert (order->contains(stateNumber)); if (successors->getNumberOfSetBits() == 1) { - if (!lattice->contains(succ1)) { - lattice->addToNode(succ1, lattice->getNode(stateNumber)); + if (!order->contains(succ1)) { + order->addToNode(succ1, order->getNode(stateNumber)); statesToHandle->set(succ1, true); auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ1); if (itr != statesSorted->end()) { @@ -398,29 +398,29 @@ namespace storm { statesToHandle->set(stateNumber, false); stateNumber = statesToHandle->getNextSetIndex(0); } else if (successors->getNumberOfSetBits() == 2 - && ((lattice->contains(succ1) && !lattice->contains(succ2)) - || (!lattice->contains(succ1) && lattice->contains(succ2)))) { + && ((order->contains(succ1) && !order->contains(succ2)) + || (!order->contains(succ1) && order->contains(succ2)))) { - if (!lattice->contains(succ1)) { + if (!order->contains(succ1)) { std::swap(succ1, succ2); } - auto compare = lattice->compare(stateNumber, succ1); - if (compare == Lattice::ABOVE) { + auto compare = order->compare(stateNumber, succ1); + if (compare == Order::ABOVE) { auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ2); if (itr != statesSorted->end()) { statesSorted->erase(itr); } - lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); + order->addBetween(succ2, order->getTop(), order->getNode(stateNumber)); statesToHandle->set(succ2); statesToHandle->set(stateNumber, false); stateNumber = statesToHandle->getNextSetIndex(0); - } else if (compare == Lattice::BELOW) { + } else if (compare == Order::BELOW) { auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ2); if (itr != statesSorted->end()) { statesSorted->erase(itr); } - lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); + order->addBetween(succ2, order->getNode(stateNumber), order->getBottom()); statesToHandle->set(succ2); statesToHandle->set(stateNumber, false); stateNumber = statesToHandle->getNextSetIndex(0); @@ -430,8 +430,8 @@ namespace storm { stateNumber = statesToHandle->getNextSetIndex(0); } - } else if (!((lattice->contains(succ1) && !lattice->contains(succ2)) - || (!lattice->contains(succ1) && lattice->contains(succ2)))) { + } else if (!((order->contains(succ1) && !order->contains(succ2)) + || (!order->contains(succ1) && order->contains(succ2)))) { stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1); } else { statesToHandle->set(stateNumber, false); @@ -444,56 +444,56 @@ namespace storm { // Normal backwardreasoning if (statesSorted->size() > 0) { auto stateNumber = *(statesSorted->begin()); - while (lattice->contains(stateNumber) && statesSorted->size() > 1) { + while (order->contains(stateNumber) && statesSorted->size() > 1) { // states.size()>1 such that there is at least one state left after erase statesSorted->erase(statesSorted->begin()); stateNumber = *(statesSorted->begin()); - if (lattice->contains(stateNumber)) { - auto resAllAdded = allSuccAdded(lattice, stateNumber); + if (order->contains(stateNumber)) { + auto resAllAdded = allSuccAdded(order, stateNumber); if (!std::get<0>(resAllAdded)) { - return std::make_tuple(lattice, std::get<1>(resAllAdded), std::get<2>(resAllAdded)); + return std::make_tuple(order, std::get<1>(resAllAdded), std::get<2>(resAllAdded)); } } } - if (!lattice->contains(stateNumber)) { + if (!order->contains(stateNumber)) { auto successors = stateMap[stateNumber]; - auto result = extendAllSuccAdded(lattice, stateNumber, successors); + auto result = extendAllSuccAdded(order, stateNumber, successors); if (std::get<1>(result) != numberOfStates) { // So we don't know the relation between all successor states return result; } else { - assert (lattice->getNode(stateNumber) != nullptr); + assert (order->getNode(stateNumber) != nullptr); if (!acyclic) { - lattice->statesToHandle->set(stateNumber); + order->statesToHandle->set(stateNumber); } statesSorted->erase(statesSorted->begin()); } } - assert (lattice->getNode(stateNumber) != nullptr); - assert (lattice->contains(stateNumber)); + assert (order->getNode(stateNumber) != nullptr); + assert (order->contains(stateNumber)); } } - assert (lattice->getAddedStates()->getNumberOfSetBits() == numberOfStates); - lattice->setDoneBuilding(true); - return std::make_tuple(lattice, numberOfStates, numberOfStates); + assert (order->getAddedStates()->getNumberOfSetBits() == numberOfStates); + order->setDoneBuilding(true); + return std::make_tuple(order, numberOfStates, numberOfStates); } template - std::tuple LatticeExtender::allSuccAdded(storm::analysis::Lattice *lattice, uint_fast64_t stateNumber) { + std::tuple OrderExtender::allSuccAdded(storm::analysis::Order *order, uint_fast64_t stateNumber) { auto successors = stateMap[stateNumber]; auto numberOfStates = successors->size(); if (successors->getNumberOfSetBits() == 1) { auto succ = successors->getNextSetIndex(0); - return std::make_tuple(lattice->contains(succ), succ, succ); + return std::make_tuple(order->contains(succ), succ, succ); } else if (successors->getNumberOfSetBits() > 2) { for (auto const& i : *successors) { for (auto j = successors->getNextSetIndex(i+1); j < numberOfStates; j = successors->getNextSetIndex(j+1)) { - if (lattice->compare(i,j) == Lattice::UNKNOWN) { + if (order->compare(i,j) == Order::UNKNOWN) { return std::make_tuple(false, i, j); } } @@ -503,6 +503,6 @@ namespace storm { } - template class LatticeExtender; + template class OrderExtender; } } diff --git a/src/storm-pars/analysis/OrderExtender.h b/src/storm-pars/analysis/OrderExtender.h new file mode 100644 index 000000000..30d3d4137 --- /dev/null +++ b/src/storm-pars/analysis/OrderExtender.h @@ -0,0 +1,83 @@ +#ifndef STORM_LATTICEEXTENDER_H +#define STORM_LATTICEEXTENDER_H + +#include +#include "storm/models/sparse/Dtmc.h" +#include "storm-pars/analysis/Order.h" +#include "storm/api/storm.h" +#include "storm-pars/storage/ParameterRegion.h" +#include "storm/storage/StronglyConnectedComponentDecomposition.h" +#include "storm/storage/StronglyConnectedComponent.h" + + + +namespace storm { + namespace analysis { + + + template + class OrderExtender { + + public: + /*! + * Constructs OrderExtender which can extend an order + * + * @param model The model for which the order should be extended. + */ + OrderExtender(std::shared_ptr> model); + + /*! + * Creates an order based on the given formula. + * + * @param formulas The formulas based on which the order is created, only the first is used. + * @return A triple with a pointer to the order and two states of which the current place in the order + * is unknown but needed. When the states have as number the number of states, no states are + * unplaced but needed. + */ + std::tuple toOrder(std::vector> formulas); + + /*! + * Creates an order based on the given extremal values. + * + * @return A triple with a pointer to the order and two states of which the current place in the order + * is unknown but needed. When the states have as number the number of states, no states are + * unplaced but needed. + */ + std::tuple toOrder(std::vector> formulas, std::vector minValues, std::vector maxValues); + + + /*! + * Extends the order based on the given assumption. + * + * @param order The order. + * @param assumption The assumption on states. + * @return A triple with a pointer to the order and two states of which the current place in the order + * is unknown but needed. When the states have as number the number of states, no states are + * unplaced but needed. + */ + std::tuple extendOrder(storm::analysis::Order* order, std::shared_ptr assumption = nullptr); + + + private: + std::shared_ptr> model; + + std::map stateMap; + + bool acyclic; + + bool assumptionSeen; + + storm::storage::StronglyConnectedComponentDecomposition sccs; + + storm::storage::SparseMatrix matrix; + + void handleAssumption(Order* order, std::shared_ptr assumption); + + std::tuple extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); + + std::tuple allSuccAdded(Order* order, uint_fast64_t stateNumber); + }; + } +} + +#endif //STORM_ORDEREXTENDER_H diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp index 987ef4ef7..e08e4287e 100644 --- a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -13,7 +13,7 @@ #include "storm/api/builder.h" #include "storm-pars/analysis/AssumptionChecker.h" -#include "storm-pars/analysis/Lattice.h" +#include "storm-pars/analysis/Order.h" #include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" #include "storm-pars/storage/ParameterRegion.h" @@ -90,9 +90,9 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); - auto dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 8, &statesSorted); + auto dummyOrder = new storm::analysis::Order(&above, &below, &initialMiddle, 8, &statesSorted); // Validate assumption - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyLattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder)); // EXPECT_FALSE(checker.validated(assumption)); expressionManager->declareRationalVariable("6"); @@ -108,9 +108,9 @@ TEST(AssumptionCheckerTest, Brp_no_bisimulation) { below.set(9); initialMiddle = storm::storage::BitVector(13); - dummyLattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 13, &statesSorted); + dummyOrder = new storm::analysis::Order(&above, &below, &initialMiddle, 13, &statesSorted); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyLattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, dummyOrder)); // EXPECT_EQ(checker.validated(assumption)); // EXPECT_FALSE(checker.valid(assumption)); } @@ -204,7 +204,7 @@ TEST(AssumptionCheckerTest, Simple2) { std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); - auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted); + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); // Checking on samples and validate auto assumption = std::make_shared( @@ -213,7 +213,7 @@ TEST(AssumptionCheckerTest, Simple2) { expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), @@ -221,7 +221,7 @@ TEST(AssumptionCheckerTest, Simple2) { expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); assumption = std::make_shared( @@ -230,7 +230,7 @@ TEST(AssumptionCheckerTest, Simple2) { expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Equal)); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); } TEST(AssumptionCheckerTest, Simple3) { @@ -270,8 +270,8 @@ TEST(AssumptionCheckerTest, Simple3) { std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); - auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 6, &statesSorted); - lattice->add(3); + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 6, &statesSorted); + order->add(3); // Checking on samples and validate auto assumption = std::make_shared( @@ -280,8 +280,8 @@ TEST(AssumptionCheckerTest, Simple3) { expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, lattice)); - EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, order)); assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), @@ -289,8 +289,8 @@ TEST(AssumptionCheckerTest, Simple3) { expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), @@ -298,8 +298,8 @@ TEST(AssumptionCheckerTest, Simple3) { expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Equal)); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); } TEST(AssumptionCheckerTest, Simple4) { @@ -331,7 +331,7 @@ TEST(AssumptionCheckerTest, Simple4) { expressionManager->declareRationalVariable("1"); expressionManager->declareRationalVariable("2"); - // Lattice + // Order storm::storage::BitVector above(5); above.set(3); storm::storage::BitVector below(5); @@ -339,7 +339,7 @@ TEST(AssumptionCheckerTest, Simple4) { storm::storage::BitVector initialMiddle(5); std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); - auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted); + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); auto assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), @@ -347,8 +347,8 @@ TEST(AssumptionCheckerTest, Simple4) { expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), @@ -356,8 +356,8 @@ TEST(AssumptionCheckerTest, Simple4) { expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); EXPECT_EQ(storm::analysis::AssumptionStatus::UNKNOWN, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, lattice)); - EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::VALID, checker.validateAssumptionSMTSolver(assumption, order)); assumption = std::make_shared( storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), @@ -365,8 +365,8 @@ TEST(AssumptionCheckerTest, Simple4) { expressionManager->getVariable("2").getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Equal)); EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.checkOnSamples(assumption)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, lattice)); - EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, lattice)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumption(assumption, order)); + EXPECT_EQ(storm::analysis::AssumptionStatus::INVALID, checker.validateAssumptionSMTSolver(assumption, order)); diff --git a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp index 7268d0c5f..7ede1cc08 100644 --- a/src/test/storm-pars/analysis/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/analysis/AssumptionMakerTest.cpp @@ -17,10 +17,10 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/api/builder.h" -#include "storm-pars/analysis/Lattice.h" +#include "storm-pars/analysis/Order.h" #include "storm-pars/analysis/AssumptionMaker.h" #include "storm-pars/analysis/AssumptionChecker.h" -#include "storm-pars/analysis/LatticeExtender.h" +#include "storm-pars/analysis/OrderExtender.h" #include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" #include "storm-pars/api/storm-pars.h" @@ -51,8 +51,8 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation) { ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); - auto *extender = new storm::analysis::LatticeExtender(dtmc); - auto criticalTuple = extender->toLattice(formulas); + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); ASSERT_EQ(183, std::get<1>(criticalTuple)); ASSERT_EQ(186, std::get<2>(criticalTuple)); @@ -121,8 +121,8 @@ TEST(AssumptionMakerTest, Brp_without_bisimulation_no_validation) { ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); - auto *extender = new storm::analysis::LatticeExtender(dtmc); - auto criticalTuple = extender->toLattice(formulas); + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); ASSERT_EQ(183, std::get<1>(criticalTuple)); ASSERT_EQ(186, std::get<2>(criticalTuple)); @@ -198,11 +198,11 @@ TEST(AssumptionMakerTest, Simple1) { storm::storage::BitVector initialMiddle(5); std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); - auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted); + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); - auto result = assumptionMaker.createAndCheckAssumption(1, 2, lattice); + auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); EXPECT_EQ(3, result.size()); @@ -271,11 +271,11 @@ TEST(AssumptionMakerTest, Simple2) { std::vector statesSorted = storm::utility::graph::getTopologicalSort(model->getTransitionMatrix()); - auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5, &statesSorted); + auto order = new storm::analysis::Order(&above, &below, &initialMiddle, 5, &statesSorted); auto assumptionChecker = storm::analysis::AssumptionChecker(formulas[0], dtmc, region, 3); auto assumptionMaker = storm::analysis::AssumptionMaker(&assumptionChecker, dtmc->getNumberOfStates(), true); - auto result = assumptionMaker.createAndCheckAssumption(1, 2, lattice); + auto result = assumptionMaker.createAndCheckAssumption(1, 2, order); auto itr = result.begin(); diff --git a/src/test/storm-pars/analysis/LatticeTest.cpp b/src/test/storm-pars/analysis/LatticeTest.cpp deleted file mode 100644 index 3b9011b04..000000000 --- a/src/test/storm-pars/analysis/LatticeTest.cpp +++ /dev/null @@ -1,170 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "test/storm_gtest.h" -#include "storm-pars/analysis/Lattice.h" -#include "storm/storage/BitVector.h" - -TEST(LatticeTest, Simple) { - auto numberOfStates = 7; - auto above = storm::storage::BitVector(numberOfStates); - above.set(0); - auto below = storm::storage::BitVector(numberOfStates); - below.set(1); - auto initialMiddle = storm::storage::BitVector(numberOfStates); - - auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates, nullptr); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,0)); - EXPECT_EQ(nullptr, lattice.getNode(2)); - - lattice.add(2); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(2,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(2,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,2)); - - lattice.add(3); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(2,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(3,2)); - - lattice.addToNode(4, lattice.getNode(2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(2,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(4,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(4,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(4,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(4,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(3,4)); - - lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(5,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(5,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(5,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(5,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(2,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(5,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(4,5)); - - lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(6,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(6,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(2,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(6,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(5,6)); - - lattice.addRelationNodes(lattice.getNode(6), lattice.getNode(4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(4,6)); - -} - -TEST(LatticeTest, copy_lattice) { - auto numberOfStates = 7; - auto above = storm::storage::BitVector(numberOfStates); - above.set(0); - auto below = storm::storage::BitVector(numberOfStates); - below.set(1); - auto initialMiddle = storm::storage::BitVector(numberOfStates); - - auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates, nullptr); - lattice.add(2); - lattice.add(3); - lattice.addToNode(4, lattice.getNode(2)); - lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3)); - lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); - - - - auto latticeCopy = storm::analysis::Lattice(lattice); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,0)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(2,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(2,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,2)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(2,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(3,2)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, latticeCopy.compare(2,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, latticeCopy.compare(4,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(4,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(4,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(4,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(3,4)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(5,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(5,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(3,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(5,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, latticeCopy.compare(5,4)); - - lattice.addRelationNodes(lattice.getNode(6), lattice.getNode(4)); - latticeCopy = storm::analysis::Lattice(lattice); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(6,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(0,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,1)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(1,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(2,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,3)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(3,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(4,6)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, latticeCopy.compare(6,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, latticeCopy.compare(5,6)); -} - -TEST(LatticeTest, merge_nodes) { - auto numberOfStates = 7; - auto above = storm::storage::BitVector(numberOfStates); - above.set(0); - auto below = storm::storage::BitVector(numberOfStates); - below.set(1); - auto initialMiddle = storm::storage::BitVector(numberOfStates); - - auto lattice = storm::analysis::Lattice(&above, &below, &initialMiddle, numberOfStates, nullptr); - lattice.add(2); - lattice.add(3); - lattice.addToNode(4, lattice.getNode(2)); - lattice.addBetween(5, lattice.getNode(0), lattice.getNode(3)); - lattice.addBetween(6, lattice.getNode(5), lattice.getNode(3)); - - lattice.mergeNodes(lattice.getNode(4), lattice.getNode(5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(2,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::SAME, lattice.compare(2,5)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice.compare(0,4)); - - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(6,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(3,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,2)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,4)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::BELOW, lattice.compare(1,5)); -} diff --git a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp b/src/test/storm-pars/analysis/OrderExtenderTest.cpp similarity index 80% rename from src/test/storm-pars/analysis/LatticeExtenderTest.cpp rename to src/test/storm-pars/analysis/OrderExtenderTest.cpp index cda1d7233..e9c0c2115 100644 --- a/src/test/storm-pars/analysis/LatticeExtenderTest.cpp +++ b/src/test/storm-pars/analysis/OrderExtenderTest.cpp @@ -12,8 +12,8 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/api/builder.h" -#include "storm-pars/analysis/Lattice.h" -#include "storm-pars/analysis/LatticeExtender.h" +#include "storm-pars/analysis/Order.h" +#include "storm-pars/analysis/OrderExtender.h" #include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" #include "storm-pars/api/storm-pars.h" @@ -21,7 +21,7 @@ #include "storm-parsers/api/storm-parsers.h" -TEST(LatticeExtenderTest, Brp_with_bisimulation) { +TEST(OrderExtenderTest, Brp_with_bisimulation) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; std::string formulaAsString = "P=? [F s=4 & i=N ]"; std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 @@ -47,25 +47,25 @@ TEST(LatticeExtenderTest, Brp_with_bisimulation) { ASSERT_EQ(dtmc->getNumberOfStates(), 99ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 195ull); - auto *extender = new storm::analysis::LatticeExtender(dtmc); - auto criticalTuple = extender->toLattice(formulas); + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); EXPECT_EQ(dtmc->getNumberOfStates(), std::get<1>(criticalTuple)); EXPECT_EQ(dtmc->getNumberOfStates(), std::get<2>(criticalTuple)); - auto lattice = std::get<0>(criticalTuple); + auto order = std::get<0>(criticalTuple); for (auto i = 0; i < dtmc->getNumberOfStates(); ++i) { - EXPECT_TRUE((*lattice->getAddedStates())[i]); + EXPECT_TRUE((*order->getAddedStates())[i]); } // Check on some nodes - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(1,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(1,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(5,0)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::ABOVE, lattice->compare(94,5)); - EXPECT_EQ(storm::analysis::Lattice::NodeComparison::UNKNOWN, lattice->compare(7,13)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(1,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(5,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order->compare(94,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order->compare(7,13)); } -TEST(LatticeExtenderTest, Brp_without_bisimulation) { +TEST(OrderExtenderTest, Brp_without_bisimulation) { std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; std::string formulaAsString = "P=? [F s=4 & i=N ]"; std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 @@ -84,8 +84,8 @@ TEST(LatticeExtenderTest, Brp_without_bisimulation) { ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); - auto *extender = new storm::analysis::LatticeExtender(dtmc); - auto criticalTuple = extender->toLattice(formulas); + auto *extender = new storm::analysis::OrderExtender(dtmc); + auto criticalTuple = extender->toOrder(formulas); EXPECT_EQ(183, std::get<1>(criticalTuple)); EXPECT_EQ(186, std::get<2>(criticalTuple)); } diff --git a/src/test/storm-pars/analysis/OrderTest.cpp b/src/test/storm-pars/analysis/OrderTest.cpp new file mode 100644 index 000000000..8b712508b --- /dev/null +++ b/src/test/storm-pars/analysis/OrderTest.cpp @@ -0,0 +1,170 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" +#include "storm-pars/analysis/Order.h" +#include "storm/storage/BitVector.h" + +TEST(OrderTest, Simple) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + + auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, nullptr); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,0)); + EXPECT_EQ(nullptr, order.getNode(2)); + + order.add(2); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(2,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(2,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,2)); + + order.add(3); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3,2)); + + order.addToNode(4, order.getNode(2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(4,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(4,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(3,4)); + + order.addBetween(5, order.getNode(0), order.getNode(3)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(5,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(5,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(4,5)); + + order.addBetween(6, order.getNode(5), order.getNode(3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(2,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(5,6)); + + order.addRelationNodes(order.getNode(6), order.getNode(4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(4,6)); + +} + +TEST(OrderTest, copy_order) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + + auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, nullptr); + order.add(2); + order.add(3); + order.addToNode(4, order.getNode(2)); + order.addBetween(5, order.getNode(0), order.getNode(3)); + order.addBetween(6, order.getNode(5), order.getNode(3)); + + + + auto orderCopy = storm::analysis::Order(order); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,0)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(2,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,2)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(2,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3,2)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(2,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, orderCopy.compare(4,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(4,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(4,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(3,4)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(5,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::UNKNOWN, orderCopy.compare(5,4)); + + order.addRelationNodes(order.getNode(6), order.getNode(4)); + orderCopy = storm::analysis::Order(order); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6,0)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(0,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,1)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(1,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(2,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,3)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(3,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(4,6)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, orderCopy.compare(6,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, orderCopy.compare(5,6)); +} + +TEST(OrderTest, merge_nodes) { + auto numberOfStates = 7; + auto above = storm::storage::BitVector(numberOfStates); + above.set(0); + auto below = storm::storage::BitVector(numberOfStates); + below.set(1); + auto initialMiddle = storm::storage::BitVector(numberOfStates); + + auto order = storm::analysis::Order(&above, &below, &initialMiddle, numberOfStates, nullptr); + order.add(2); + order.add(3); + order.addToNode(4, order.getNode(2)); + order.addBetween(5, order.getNode(0), order.getNode(3)); + order.addBetween(6, order.getNode(5), order.getNode(3)); + + order.mergeNodes(order.getNode(4), order.getNode(5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::SAME, order.compare(2,5)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::ABOVE, order.compare(0,4)); + + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(6,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(3,5)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,2)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,4)); + EXPECT_EQ(storm::analysis::Order::NodeComparison::BELOW, order.compare(1,5)); +}