From 9e8d910a49a2d40106166306cb0d4084770c72c9 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 28 Aug 2018 16:25:03 +0200 Subject: [PATCH] WIP Add LatticeExtender --- src/storm-pars/analysis/Lattice.cpp | 8 +- src/storm-pars/analysis/Lattice.h | 120 ++---------------- src/storm-pars/analysis/LatticeExtender.cpp | 129 ++++++++++++++++++++ src/storm-pars/analysis/LatticeExtender.h | 42 +++++++ 4 files changed, 185 insertions(+), 114 deletions(-) create mode 100644 src/storm-pars/analysis/LatticeExtender.cpp create mode 100644 src/storm-pars/analysis/LatticeExtender.h diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index b2fa043e7..5adc1cbc3 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -24,7 +24,7 @@ namespace storm { nodes.at(i) = bottom; } this->numberOfStates = numberOfStates; - + this->addedStates = storm::storage::BitVector(numberOfStates); } void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { @@ -38,11 +38,13 @@ namespace storm { (below->above).insert(newNode); above->below.insert(newNode); nodes.at(state) = newNode; + addedStates.set(state); } void Lattice::addToNode(uint_fast64_t state, Node *node) { node->states.set(state); nodes.at(state) = node; + addedStates.set(state); } void Lattice::add(uint_fast64_t state) { @@ -83,6 +85,10 @@ namespace storm { return nodes.at(stateNumber); } + storm::storage::BitVector Lattice::getAddedStates() { + return addedStates; + } + void Lattice::toString(std::ostream &out) { std::vector printedNodes = std::vector({}); for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 03147431e..a5644db48 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -6,17 +6,12 @@ #define LATTICE_LATTICE_H #include +#include #include -#include -#include -#include "storm/models/sparse/Model.h" #include "storm/storage/BitVector.h" -#include "storm/storage/SparseMatrix.h" -#include "storm/utility/macros.h" -#include "storm/utility/graph.h" -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/NotSupportedException.h" + + namespace storm { @@ -90,6 +85,8 @@ namespace storm { */ Node *getNode(uint_fast64_t state); + storm::storage::BitVector getAddedStates(); + /*! * Prints a string representation of the lattice to the output stream. * @@ -104,115 +101,12 @@ namespace storm { */ void toDotFile(std::ostream &out); - /*! - * Creates a Lattice based on the transition matrix, topStates of the Lattice and bottomStates of the Lattice - * @tparam ValueType Type of the probabilities - * @param model The pointer to the model - * @param formulas Vector with pointer to formula - * @return pointer to the created Lattice. - */ - template - static Lattice* toLattice(std::shared_ptr> sparseModel, std::vector> formulas) { - STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); - STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() - && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() - || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula"); - - uint_fast64_t numberOfStates = sparseModel.get()->getNumberOfStates(); - - storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*sparseModel); - storm::storage::BitVector phiStates; - storm::storage::BitVector psiStates; - if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { - phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - } else { - phiStates = storm::storage::BitVector(numberOfStates, true); - psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - } - - // Get the maybeStates - std::pair statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates); - storm::storage::BitVector topStates = statesWithProbability01.second; - storm::storage::BitVector bottomStates = statesWithProbability01.first; - - 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 - auto matrix = sparseModel.get()->getTransitionMatrix(); - - std::map stateMap; - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - stateMap[i] = storm::storage::BitVector(numberOfStates, false); - - auto row = matrix.getRow(i); - for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { - stateMap[i].set(rowItr->getColumn(), true); - } - // TODO: allow more than 2 transitions? or fix this in preprocessing? - STORM_LOG_THROW(stateMap[i].getNumberOfSetBits() <= 2, storm::exceptions::NotSupportedException, "Only two outgoing transitions per state allowed"); - } - - // Start creating the Lattice - storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); - storm::storage::BitVector oldStates(numberOfStates); - - // Create a copy of the states already present in the lattice. - storm::storage::BitVector seenStates = topStates|= bottomStates; - - while (oldStates != seenStates) { - // As long as new states are added to the lattice, continue. - oldStates = storm::storage::BitVector(seenStates); - - for (auto stateItr = stateMap.begin(); stateItr != stateMap.end(); ++stateItr) { - // Iterate over all states - auto stateNumber = stateItr->first; - storm::storage::BitVector successors = stateItr->second; - - // Check if current state has not been added yet, and all successors have - bool check = !seenStates[stateNumber]; - for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) { - check &= seenStates[succIndex]; - } - - if (check && 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))); - seenStates.set(stateNumber); - } else if (check && successors.getNumberOfSetBits() > 1) { - // TODO: allow more than 2 transitions? - - // 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 == 1) { - // successor 1 is closer to top than successor 2 - lattice->addBetween(stateNumber, lattice->getNode(successor1), - lattice->getNode(successor2)); - } else if (compareResult == 2) { - // successor 2 is closer to top than successor 1 - lattice->addBetween(stateNumber, lattice->getNode(successor2), - lattice->getNode(successor1)); - } else if (compareResult == 0) { - // the successors are at the same level - lattice->addToNode(stateNumber, lattice->getNode(successor1)); - } else { - // TODO: is this what we want? - lattice->add(stateNumber); - } - seenStates.set(stateNumber); - } - } - } - - return lattice; - } private: std::vector nodes; + storm::storage::BitVector addedStates; + Node* top; Node* bottom; diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp new file mode 100644 index 000000000..2b1cc1a48 --- /dev/null +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -0,0 +1,129 @@ +// +// Created by Jip Spel on 28.08.18. +// + +#include "LatticeExtender.h" +#include "storm/utility/macros.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" +#include +#include +#include "storm/models/sparse/Model.h" + +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/NotSupportedException.h" + +#include + +namespace storm { + namespace analysis { + + template + LatticeExtender::LatticeExtender(){//std::shared_ptr> model) { + //TODO + } + +// template +// storm::analysis::Lattice* LatticeExtender::toLattice(std::vector> formulas) { +// STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); +// STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() +// && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() +// || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula"); +// +// uint_fast64_t numberOfStates = this->model.getNumberOfStates(); +// +// storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(this->model); +// storm::storage::BitVector phiStates; +// storm::storage::BitVector psiStates; +// if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { +// phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); +// psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); +// } else { +// phiStates = storm::storage::BitVector(numberOfStates, true); +// psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); +// } +// +// // Get the maybeStates +// std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->model.getBackwardTransitions(), phiStates, psiStates); +// storm::storage::BitVector topStates = statesWithProbability01.second; +// storm::storage::BitVector bottomStates = statesWithProbability01.first; +// +// 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 +// auto matrix = this->model.getTransitionMatrix(); +// +// for (uint_fast64_t i = 0; i < numberOfStates; ++i) { +// stateMap[i] = storm::storage::BitVector(numberOfStates, false); +// +// auto row = matrix.getRow(i); +// for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { +// stateMap[i].set(rowItr->getColumn(), true); +// } +// // TODO: allow more than 2 transitions? or fix this in preprocessing? +// STORM_LOG_THROW(stateMap[i].getNumberOfSetBits() <= 2, storm::exceptions::NotSupportedException, "Only two outgoing transitions per state allowed"); +// } +// +// // Create the Lattice +// storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); +// return this->extendLattice(lattice, std::set({})); +// } +// +// template +// storm::analysis::Lattice* LatticeExtender::extendLattice(storm::analysis::Lattice* lattice, std::set assumptions) { +// uint_fast64_t numberOfStates = this->model.getNumberOfStates(); +// +// storm::storage::BitVector oldStates(numberOfStates); +// +// // Create a copy of the states already present in the lattice. +// storm::storage::BitVector seenStates = lattice->getAddedStates(); +// +// while (oldStates != seenStates) { +// // As long as new states are added to the lattice, continue. +// oldStates = storm::storage::BitVector(seenStates); +// +// for (auto stateItr = stateMap.begin(); stateItr != stateMap.end(); ++stateItr) { +// // Iterate over all states +// auto stateNumber = stateItr->first; +// storm::storage::BitVector successors = stateItr->second; +// +// // Check if current state has not been added yet, and all successors have +// bool check = !seenStates[stateNumber]; +// for (auto succIndex = successors.getNextSetIndex(0); check && succIndex != numberOfStates; succIndex = successors.getNextSetIndex(++succIndex)) { +// check &= seenStates[succIndex]; +// } +// +// if (check && 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))); +// seenStates.set(stateNumber); +// } else if (check && successors.getNumberOfSetBits() > 1) { +// // TODO: allow more than 2 transitions? +// +// // 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 == 1) { +// // successor 1 is closer to top than successor 2 +// lattice->addBetween(stateNumber, lattice->getNode(successor1), +// lattice->getNode(successor2)); +// } else if (compareResult == 2) { +// // successor 2 is closer to top than successor 1 +// lattice->addBetween(stateNumber, lattice->getNode(successor2), +// lattice->getNode(successor1)); +// } else if (compareResult == 0) { +// // the successors are at the same level +// lattice->addToNode(stateNumber, lattice->getNode(successor1)); +// } else { +// // TODO: create critical pair +// } +// seenStates.set(stateNumber); +// } +// } +// } +// return lattice; +// } + } +} \ No newline at end of file diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h new file mode 100644 index 000000000..41b5da465 --- /dev/null +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -0,0 +1,42 @@ +// +// Created by Jip Spel on 28.08.18. +// + +#ifndef STORM_LATTICEEXTENDER_H +#define STORM_LATTICEEXTENDER_H + +#include +#include "storm/models/sparse/Dtmc.h" +#include "storm-pars/analysis/Lattice.h" + + + +namespace storm { + namespace analysis { + + template + class LatticeExtender { + + public: + LatticeExtender(); + +// /*! +// * Creates a Lattice based on the transition matrix, topStates of the Lattice and bottomStates of the Lattice +// * @tparam ValueType Type of the probabilities +// * @param model The pointer to the model +// * @param formulas Vector with pointer to formula +// * @return pointer to the created Lattice. +// */ +// storm::analysis::Lattice* toLattice(std::vector> formulas); +// +// storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::set assumptions); + + private: + std::shared_ptr> model; + + std::map stateMap; + }; + } +} + +#endif //STORM_LATTICEEXTENDER_H