sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Renamed Lattice -> Order

main
Jip Spel 6 years ago
parent
1c5d6b7237
commit
08d2893b2c
16 changed files with 577 additions and 577 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 36
      src/storm-pars/analysis/AssumptionChecker.cpp
  2. 16
      src/storm-pars/analysis/AssumptionChecker.h
  3. 8
      src/storm-pars/analysis/AssumptionMaker.cpp
  4. 12
      src/storm-pars/analysis/AssumptionMaker.h
  5. 83
      src/storm-pars/analysis/LatticeExtender.h
  6. 100
      src/storm-pars/analysis/MonotonicityChecker.cpp
  7. 20
      src/storm-pars/analysis/MonotonicityChecker.h
  8. 70
      src/storm-pars/analysis/Order.cpp
  9. 74
      src/storm-pars/analysis/Order.h
  10. 212
      src/storm-pars/analysis/OrderExtender.cpp
  11. 83
      src/storm-pars/analysis/OrderExtender.h
  12. 50
      src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
  13. 20
      src/test/storm-pars/analysis/AssumptionMakerTest.cpp
  14. 170
      src/test/storm-pars/analysis/LatticeTest.cpp
  15. 30
      src/test/storm-pars/analysis/OrderExtenderTest.cpp
  16. 170
      src/test/storm-pars/analysis/OrderTest.cpp

36
src/storm-pars/analysis/AssumptionChecker.cpp
View File

@ -130,7 +130,7 @@ namespace storm {
}
template <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Lattice* lattice) {
AssumptionStatus AssumptionChecker<ValueType>::validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> 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 <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionFunction(Lattice* lattice,
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionFunction(Order* order,
typename storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storage::SparseMatrix<ValueType>::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 <typename ValueType>
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Lattice* lattice) {
AssumptionStatus AssumptionChecker<ValueType>::validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Order* order) {
std::shared_ptr<utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<utility::solver::MathsatSmtSolverFactory>();
std::shared_ptr<expressions::ExpressionManager> 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();

16
src/storm-pars/analysis/AssumptionChecker.h
View File

@ -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<expressions::BinaryRelationExpression> 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<expressions::BinaryRelationExpression> assumption, Lattice* lattice);
AssumptionStatus validateAssumption(std::shared_ptr<expressions::BinaryRelationExpression> 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<expressions::BinaryRelationExpression> assumption, Lattice* lattice);
AssumptionStatus validateAssumptionSMTSolver(std::shared_ptr<expressions::BinaryRelationExpression> assumption, Order* order);
private:
std::shared_ptr<logic::Formula const> formula;
@ -76,7 +76,7 @@ namespace storm {
void createSamples();
AssumptionStatus validateAssumptionFunction(Lattice* lattice,
AssumptionStatus validateAssumptionFunction(Order* order,
typename storage::SparseMatrix<ValueType>::iterator state1succ1,
typename storage::SparseMatrix<ValueType>::iterator state1succ2,
typename storage::SparseMatrix<ValueType>::iterator state2succ1,

8
src/storm-pars/analysis/AssumptionMaker.cpp
View File

@ -16,7 +16,7 @@ namespace storm {
template <typename ValueType>
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice) {
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> AssumptionMaker<ValueType>::createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order) {
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, 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;
}

12
src/storm-pars/analysis/AssumptionMaker.h
View File

@ -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<expressions::BinaryRelationExpression> 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<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Lattice* lattice);
std::map<std::shared_ptr<expressions::BinaryRelationExpression>, AssumptionStatus> createAndCheckAssumption(uint_fast64_t val1, uint_fast64_t val2, Order* order);
private:
AssumptionChecker<ValueType>* assumptionChecker;

83
src/storm-pars/analysis/LatticeExtender.h
View File

@ -1,83 +0,0 @@
#ifndef STORM_LATTICEEXTENDER_H
#define STORM_LATTICEEXTENDER_H
#include <storm/logic/Formula.h>
#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<typename ValueType>
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<storm::models::sparse::Model<ValueType>> 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<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> 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<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr);
private:
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::map<uint_fast64_t, storm::storage::BitVector*> stateMap;
bool acyclic;
bool assumptionSeen;
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccs;
storm::storage::SparseMatrix<ValueType> matrix;
void handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors);
std::tuple<bool, uint_fast64_t, uint_fast64_t> allSuccAdded(Lattice* lattice, uint_fast64_t stateNumber);
};
}
}
#endif //STORM_LATTICEEXTENDER_H

100
src/storm-pars/analysis/MonotonicityChecker.cpp
View File

@ -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<ValueType>(std::move(lowerBoundaries), std::move(upperBoundaries));
}
this->extender = new storm::analysis::LatticeExtender<ValueType>(sparseModel);
this->extender = new storm::analysis::OrderExtender<ValueType>(sparseModel);
}
template <typename ValueType>
std::map<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
auto map = createLattice();
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity() {
auto map = createOrder();
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
auto matrix = sparseModel->getTransitionMatrix();
return checkMonotonicity(map, matrix);
}
template <typename ValueType>
std::map<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
storm::utility::Stopwatch monotonicityCheckWatch(true);
std::map<storm::analysis::Lattice *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> result;
std::map<storm::analysis::Order *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> 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<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, lattice,
auto addedStates = order->getAddedStates()->getNumberOfSetBits();
assert (addedStates == order->getAddedStates()->size());
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> varsMonotone = analyseMonotonicity(i, order,
matrix);
auto assumptions = itr->second;
@ -157,8 +157,8 @@ namespace storm {
}
}
result.insert(
std::pair<storm::analysis::Lattice *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>>(
lattice, varsMonotone));
std::pair<storm::analysis::Order *, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>>(
order, varsMonotone));
}
++i;
outfile << ";";
@ -172,11 +172,11 @@ namespace storm {
}
template <typename ValueType>
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::createLattice() {
// Transform to Lattices
storm::utility::Stopwatch latticeWatch(true);
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::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<storm::models::sparse::Dtmc<ValueType>, double> plaModelChecker;
std::unique_ptr<storm::modelchecker::CheckResult> checkResult;
auto env = Environment();
@ -195,12 +195,12 @@ namespace storm {
std::vector<double> minValues = minRes.getValueVector();
std::vector<double> maxValues = maxRes.getValueVector();
// Create initial lattice
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toLattice(formulas, minValues, maxValues);
// Create initial order
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues);
// Continue based on not (yet) sorted states
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
auto val1 = std::get<1>(criticalTuple);
auto val2 = std::get<2>(criticalTuple);
@ -208,7 +208,7 @@ namespace storm {
std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
if (val1 == numberOfStates && val2 == numberOfStates) {
result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(std::get<0>(criticalTuple), assumptions));
result.insert(std::pair<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(std::get<0>(criticalTuple), assumptions));
} else if (val1 != numberOfStates && val2 != numberOfStates) {
storm::analysis::AssumptionChecker<ValueType> *assumptionChecker;
@ -223,26 +223,26 @@ namespace storm {
"Unable to perform monotonicity analysis on the provided model type.");
}
auto assumptionMaker = new storm::analysis::AssumptionMaker<ValueType>(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 <typename ValueType>
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::extendLatticeWithAssumptions(storm::analysis::Lattice* lattice, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::extendOrderWithAssumptions(storm::analysis::Order* order, storm::analysis::AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions) {
std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
auto numberOfStates = model->getNumberOfStates();
if (val1 == numberOfStates || val2 == numberOfStates) {
assert (val1 == val2);
assert (lattice->getAddedStates()->size() == lattice->getAddedStates()->getNumberOfSetBits());
result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, assumptions));
assert (order->getAddedStates()->size() == order->getAddedStates()->getNumberOfSetBits());
result.insert(std::pair<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(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<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(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<std::shared_ptr<storm::expressions::BinaryRelationExpression>>(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 <typename ValueType>
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) {
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::analyseMonotonicity(uint_fast64_t j, storm::analysis::Order* order, storm::storage::SparseMatrix<ValueType> matrix) {
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> 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<bool, bool> 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<bool, bool> 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 <typename ValueType>
bool MonotonicityChecker<ValueType>::somewhereMonotonicity(Lattice* lattice) {
bool MonotonicityChecker<ValueType>::somewhereMonotonicity(Order* order) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
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<bool, bool> 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<bool, bool> 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

20
src/storm-pars/analysis/MonotonicityChecker.h
View File

@ -2,8 +2,8 @@
#define STORM_MONOTONICITYCHECKER_H
#include <map>
#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<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity();
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> 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<storm::analysis::Lattice*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
std::map<storm::analysis::Order*, std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>>> checkMonotonicity(std::map<storm::analysis::Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix);
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Lattice* lattice, storm::storage::SparseMatrix<ValueType> matrix) ;
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> analyseMonotonicity(uint_fast64_t i, Order* order, storm::storage::SparseMatrix<ValueType> matrix) ;
std::map<Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createLattice();
std::map<Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> createOrder();
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples);
@ -127,7 +127,7 @@ namespace storm {
ValueType getDerivative(ValueType function, typename utility::parametric::VariableType<ValueType>::type var);
std::map<Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendLatticeWithAssumptions(Lattice* lattice, AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
std::map<Order*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> extendOrderWithAssumptions(Order* order, AssumptionMaker<ValueType>* assumptionMaker, uint_fast64_t val1, uint_fast64_t val2, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions);
std::shared_ptr<storm::models::ModelBase> model;
@ -139,7 +139,7 @@ namespace storm {
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> resultCheckOnSamples;
LatticeExtender<ValueType> *extender;
OrderExtender<ValueType> *extender;
std::ofstream outfile;

70
src/storm-pars/analysis/Lattice.cpp → src/storm-pars/analysis/Order.cpp
View File

@ -1,10 +1,10 @@
#include <iostream>
#include <fstream>
#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<uint_fast64_t>* statesSorted) {
Order::Order(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates, std::vector<uint_fast64_t>* statesSorted) {
nodes = std::vector<Node *>(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<Node *>(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::Node*> Lattice::getNodes() {
std::vector<Order::Node*> 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<uint_fast64_t> Lattice::sortStates(storm::storage::BitVector* states) {
std::vector<uint_fast64_t> Order::sortStates(storm::storage::BitVector* states) {
auto numberOfSetBits = states->getNumberOfSetBits();
auto stateSize = states->size();
auto result = std::vector<uint_fast64_t>(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));
}
}

74
src/storm-pars/analysis/Lattice.h → src/storm-pars/analysis/Order.h
View File

@ -1,5 +1,5 @@
#ifndef LATTICE_LATTICE_H
#define LATTICE_LATTICE_H
#ifndef ORDER_ORDER_H
#define ORDER_ORDER_H
#include <iostream>
#include <set>
@ -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<uint_fast64_t>* 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<uint_fast64_t>* 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<Node*> 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<uint_fast64_t> 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

212
src/storm-pars/analysis/LatticeExtender.cpp → src/storm-pars/analysis/OrderExtender.cpp
View File

@ -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<typename ValueType>
LatticeExtender<ValueType>::LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) {
OrderExtender<ValueType>::OrderExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) {
this->model = model;
this->matrix = model->getTransitionMatrix();
this->assumptionSeen = false;
@ -61,7 +61,7 @@ namespace storm {
}
template <typename ValueType>
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> 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<uint_fast64_t> 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 <typename ValueType>
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> maxValues) {
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> 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<uint_fast64_t> 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 <typename ValueType>
void LatticeExtender<ValueType>::handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
void OrderExtender<ValueType>::handleAssumption(Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> 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 <typename ValueType>
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors) {
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::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 <typename ValueType>
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::extendLattice(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
std::tuple<Order*, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::extendOrder(Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> 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 <typename ValueType>
std::tuple<bool, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::allSuccAdded(storm::analysis::Lattice *lattice, uint_fast64_t stateNumber) {
std::tuple<bool, uint_fast64_t, uint_fast64_t> OrderExtender<ValueType>::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<storm::RationalFunction>;
template class OrderExtender<storm::RationalFunction>;
}
}

83
src/storm-pars/analysis/OrderExtender.h
View File

@ -0,0 +1,83 @@
#ifndef STORM_LATTICEEXTENDER_H
#define STORM_LATTICEEXTENDER_H
#include <storm/logic/Formula.h>
#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<typename ValueType>
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<storm::models::sparse::Model<ValueType>> 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<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> toOrder(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas, std::vector<double> minValues, std::vector<double> 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<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> extendOrder(storm::analysis::Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr);
private:
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::map<uint_fast64_t, storm::storage::BitVector*> stateMap;
bool acyclic;
bool assumptionSeen;
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccs;
storm::storage::SparseMatrix<ValueType> matrix;
void handleAssumption(Order* order, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
std::tuple<Order*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Order* order, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors);
std::tuple<bool, uint_fast64_t, uint_fast64_t> allSuccAdded(Order* order, uint_fast64_t stateNumber);
};
}
}
#endif //STORM_ORDEREXTENDER_H

50
src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
View File

@ -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<uint_fast64_t> 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<uint_fast64_t> 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<storm::expressions::BinaryRelationExpression>(
@ -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>(
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<storm::expressions::BinaryRelationExpression>(
@ -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<uint_fast64_t> 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<storm::expressions::BinaryRelationExpression>(
@ -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>(
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>(
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<uint_fast64_t> 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>(
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>(
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>(
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));

20
src/test/storm-pars/analysis/AssumptionMakerTest.cpp
View File

@ -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<storm::RationalFunction>(dtmc);
auto criticalTuple = extender->toLattice(formulas);
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(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<storm::RationalFunction>(dtmc);
auto criticalTuple = extender->toLattice(formulas);
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(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<uint_fast64_t> 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<storm::RationalFunction>(formulas[0], dtmc, region, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&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<uint_fast64_t> 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<storm::RationalFunction>(formulas[0], dtmc, region, 3);
auto assumptionMaker = storm::analysis::AssumptionMaker<storm::RationalFunction>(&assumptionChecker, dtmc->getNumberOfStates(), true);
auto result = assumptionMaker.createAndCheckAssumption(1, 2, lattice);
auto result = assumptionMaker.createAndCheckAssumption(1, 2, order);
auto itr = result.begin();

170
src/test/storm-pars/analysis/LatticeTest.cpp
View File

@ -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));
}

30
src/test/storm-pars/analysis/LatticeExtenderTest.cpp → src/test/storm-pars/analysis/OrderExtenderTest.cpp
View File

@ -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<storm::RationalFunction>(dtmc);
auto criticalTuple = extender->toLattice(formulas);
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(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<storm::RationalFunction>(dtmc);
auto criticalTuple = extender->toLattice(formulas);
auto *extender = new storm::analysis::OrderExtender<storm::RationalFunction>(dtmc);
auto criticalTuple = extender->toOrder(formulas);
EXPECT_EQ(183, std::get<1>(criticalTuple));
EXPECT_EQ(186, std::get<2>(criticalTuple));
}

170
src/test/storm-pars/analysis/OrderTest.cpp
View File

@ -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));
}
Write Preview
Loading…
Cancel
Save