From b6e48b35cc18ab9040e04843dd58c54ffd0d3c8c Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Wed, 29 Aug 2018 12:35:19 +0200 Subject: [PATCH] Implement first version of LatticeExtender --- src/storm-pars-cli/storm-pars.cpp | 5 +- src/storm-pars/analysis/Lattice.cpp | 2 + src/storm-pars/analysis/LatticeExtender.cpp | 218 ++++++++++---------- src/storm-pars/analysis/LatticeExtender.h | 24 +-- 4 files changed, 129 insertions(+), 120 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 96b13e6e0..5700e52e0 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -1,5 +1,6 @@ +#include "storm-pars/analysis/LatticeExtender.h" #include "storm-cli-utilities/cli.h" #include "storm-cli-utilities/model-handling.h" @@ -609,7 +610,9 @@ namespace storm { // Transform to Lattice storm::utility::Stopwatch latticeWatch(true); - storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice(sparseModel, formulas); + + storm::analysis::LatticeExtender> extender = storm::analysis::LatticeExtender>(sparseModel); + storm::analysis::Lattice* lattice = extender.toLattice(formulas); latticeWatch.stop(); STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); ofstream myfile; diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 5adc1cbc3..6e04d82c2 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -25,6 +25,8 @@ namespace storm { } this->numberOfStates = numberOfStates; this->addedStates = storm::storage::BitVector(numberOfStates); + this->addedStates.operator|=(topStates); + this->addedStates.operator|=(bottomStates); } void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 2b1cc1a48..d252149e3 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -9,121 +9,129 @@ #include #include #include "storm/models/sparse/Model.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" #include +#include "storm/storage/BitVector.h" +#include "storm/utility/macros.h" + namespace storm { namespace analysis { - template - LatticeExtender::LatticeExtender(){//std::shared_ptr> model) { - //TODO + template + LatticeExtender::LatticeExtender(std::shared_ptr model) : model(model) { + // intentionally left empty } -// 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; -// } + 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.get()->getNumberOfStates(); + + storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(*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.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 = this->model.get()->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.get()->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; + } + + template class LatticeExtender>; +// template class LatticeExtender>; } } \ No newline at end of file diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 41b5da465..e52a3417d 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -8,31 +8,27 @@ #include #include "storm/models/sparse/Dtmc.h" #include "storm-pars/analysis/Lattice.h" +#include "storm/api/storm.h" + namespace storm { namespace analysis { - template + + 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); + LatticeExtender(std::shared_ptr model); + + storm::analysis::Lattice* toLattice(std::vector> formulas); + + storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::set assumptions); private: - std::shared_ptr> model; + std::shared_ptr model; std::map stateMap; };