|
@ -21,10 +21,32 @@ namespace storm { |
|
|
class LatticeExtender { |
|
|
class LatticeExtender { |
|
|
|
|
|
|
|
|
public: |
|
|
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); |
|
|
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); |
|
|
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas); |
|
|
|
|
|
|
|
|
|
|
|
/*! |
|
|
|
|
|
* Extends the lattice based on the given assumptions. |
|
|
|
|
|
* |
|
|
|
|
|
* @param lattice The lattice. |
|
|
|
|
|
* @param assumptions The assumptions 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::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions); |
|
|
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions); |
|
|
|
|
|
|
|
|
private: |
|
|
private: |
|
|