From 12e0ef537c218946d305450dbf49b750a248aaf7 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 26 Jul 2019 11:12:00 +0200 Subject: [PATCH] Small fixes --- .../analysis/MonotonicityChecker.cpp | 2 + src/storm-pars/analysis/Order.cpp | 40 ++++- src/storm-pars/analysis/Order.h | 13 +- src/storm-pars/analysis/OrderExtender.cpp | 163 ++++++++++-------- 4 files changed, 137 insertions(+), 81 deletions(-) diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index e4d18e9f6..47bc27b69 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -195,6 +195,8 @@ namespace storm { std::vector minValues = minRes.getValueVector(); std::vector maxValues = maxRes.getValueVector(); + // TODO: zijn de value vectors nu precies omgedraaid? + // Create initial order std::tuple criticalTuple = extender->toOrder(formulas, minValues, maxValues); // std::tuple criticalTuple = extender->toOrder(formulas); diff --git a/src/storm-pars/analysis/Order.cpp b/src/storm-pars/analysis/Order.cpp index fe8b94233..476a9e058 100644 --- a/src/storm-pars/analysis/Order.cpp +++ b/src/storm-pars/analysis/Order.cpp @@ -14,7 +14,7 @@ namespace storm { this->numberOfStates = numberOfStates; this->addedStates = new storm::storage::BitVector(numberOfStates); this->doneBuilding = false; - this->statesSorted = statesSorted; + this->statesSorted = *statesSorted; this->statesToHandle = initialMiddleStates; top = new Node(); @@ -47,7 +47,7 @@ namespace storm { this->numberOfStates = numberOfStates; this->addedStates = new storm::storage::BitVector(numberOfStates); this->doneBuilding = false; - this->statesSorted = statesSorted; + this->statesSorted = *statesSorted; this->statesToHandle = new storm::storage::BitVector(numberOfStates); top = new Node(); @@ -102,14 +102,16 @@ namespace storm { } } - this->statesSorted = order->statesSorted; - this->statesToHandle = order->statesToHandle; + auto statesSortedOrder = order->getStatesSorted(); + for (auto itr = statesSortedOrder.begin(); itr != statesSortedOrder.end(); ++itr) { + this->statesSorted.push_back(*itr); + } + this->statesToHandle = new storm::storage::BitVector(*(order->statesToHandle)); } void Order::addBetween(uint_fast64_t state, Node *above, Node *below) { assert(!(*addedStates)[state]); assert(compare(above, below) == ABOVE); - Node *newNode = new Node(); nodes[state] = newNode; @@ -195,10 +197,11 @@ namespace storm { bool Order::contains(uint_fast64_t state) { - return state >= 0 && state < addedStates->size() && addedStates->get(state); + return state < addedStates->size() && addedStates->get(state); } Order::Node *Order::getNode(uint_fast64_t stateNumber) { + assert (stateNumber < numberOfStates); return nodes.at(stateNumber); } @@ -350,5 +353,30 @@ namespace storm { void Order::merge(uint_fast64_t var1, uint_fast64_t var2) { mergeNodes(getNode(var1), getNode(var2)); } + + std::vector Order::getStatesSorted() { + return statesSorted; + } + + uint_fast64_t Order::getNextSortedState() { + if (statesSorted.begin() != statesSorted.end()) { + return *(statesSorted.begin()); + } else { + return numberOfStates; + } + } + + void Order::removeFirstStatesSorted() { + statesSorted.erase(statesSorted.begin()); + } + + void Order::removeStatesSorted(uint_fast64_t state) { + assert(containsStatesSorted(state)); + statesSorted.erase(std::find(statesSorted.begin(), statesSorted.end(), state)); + } + + bool Order::containsStatesSorted(uint_fast64_t state) { + return std::find(statesSorted.begin(), statesSorted.end(), state) != statesSorted.end(); + } } } diff --git a/src/storm-pars/analysis/Order.h b/src/storm-pars/analysis/Order.h index bd5270e30..fa4397498 100644 --- a/src/storm-pars/analysis/Order.h +++ b/src/storm-pars/analysis/Order.h @@ -212,11 +212,22 @@ namespace storm { storm::storage::BitVector* statesToHandle; - std::vector* statesSorted; + uint_fast64_t getNextSortedState(); + + bool containsStatesSorted(uint_fast64_t state); + + void removeFirstStatesSorted(); + + void removeStatesSorted(uint_fast64_t state); + + protected: + std::vector getStatesSorted(); private: std::vector nodes; + std::vector statesSorted; + storm::storage::BitVector* addedStates; Node* top; diff --git a/src/storm-pars/analysis/OrderExtender.cpp b/src/storm-pars/analysis/OrderExtender.cpp index 4b32d63eb..991f88f35 100644 --- a/src/storm-pars/analysis/OrderExtender.cpp +++ b/src/storm-pars/analysis/OrderExtender.cpp @@ -69,7 +69,6 @@ namespace storm { uint_fast64_t numberOfStates = this->model->getNumberOfStates(); - // TODO: dit moet anders kunnen storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*model); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; @@ -130,43 +129,65 @@ namespace storm { template std::tuple OrderExtender::toOrder(std::vector> formulas, std::vector minValues, std::vector maxValues) { uint_fast64_t numberOfStates = this->model->getNumberOfStates(); - - // Compare min/max for all states - 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 or eventually formula"); - - 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->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"); - - uint_fast64_t bottom = bottomStates.getNextSetIndex(0); - uint_fast64_t top = topStates.getNextSetIndex(0); +// +// // Compare min/max for all states +// 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 or eventually formula"); +// +// // TODO: dit moet anders kunnen +// 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->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"); +// + uint_fast64_t bottom = numberOfStates; + uint_fast64_t top = numberOfStates; std::vector statesSorted = storm::utility::graph::getTopologicalSort(matrix); - Order *order = new Order(top, bottom, numberOfStates, &statesSorted); - + Order *order = nullptr; + + for (auto state : statesSorted) { + if ((minValues[numberOfStates - 1 - state] == 1 || maxValues[numberOfStates - 1 - state] == 0) + && minValues[numberOfStates - 1 - state] == maxValues[numberOfStates - 1 - state]) { + if (maxValues[numberOfStates - 1 - state] == 0) { + assert (bottom == numberOfStates); + bottom = state; + } + if (minValues[numberOfStates - 1 - state] == 1) { + assert (top == numberOfStates); + top = state; + } + if (bottom != numberOfStates && top != numberOfStates) { + order = new Order(top, bottom, numberOfStates, &statesSorted); + } - for (auto state : *(order->statesSorted)) { - if (state != bottom && state != top) { + } else { assert (order != nullptr); auto successors = stateMap[state]; - if (successors->size() > 1) { + if (successors->getNumberOfSetBits() == 1) { + auto succ = successors->getNextSetIndex(0); + if (succ != state) { + if (!order->contains(succ)) { + order->add(succ); + } + order->addToNode(state, order->getNode(succ)); + } + } else if (successors->getNumberOfSetBits() > 1) { uint_fast64_t min = numberOfStates; uint_fast64_t max = numberOfStates; bool allSorted = true; @@ -178,9 +199,9 @@ namespace storm { min = succ; max = succ; } else { - if (minValues[succ] > maxValues[max]) { + if (minValues[numberOfStates - 1 - succ] > maxValues[numberOfStates - 1 - max]) { max = succ; - } else if (maxValues[succ] < minValues[min]) { + } else if (maxValues[numberOfStates - 1 - succ] < minValues[numberOfStates - 1 - min]) { min = succ; } else { allSorted = false; @@ -214,6 +235,8 @@ namespace storm { } } + assert (order != nullptr); + // Handle sccs auto addedStates = order->getAddedStates(); for (auto scc : sccs) { @@ -368,8 +391,6 @@ namespace storm { handleAssumption(order, assumption); } - auto statesSorted = order->statesSorted; - auto oldNumberSet = numberOfStates; while (oldNumberSet != order->getAddedStates()->getNumberOfSetBits()) { oldNumberSet = order->getAddedStates()->getNumberOfSetBits(); @@ -390,9 +411,8 @@ namespace storm { 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()) { - statesSorted->erase(itr); + if (order->containsStatesSorted(succ1)) { + order->removeStatesSorted(succ1); } } statesToHandle->set(stateNumber, false); @@ -407,18 +427,16 @@ namespace storm { 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); + if (order->containsStatesSorted(succ2)) { + order->removeStatesSorted(succ2); } order->addBetween(succ2, order->getTop(), order->getNode(stateNumber)); statesToHandle->set(succ2); statesToHandle->set(stateNumber, false); stateNumber = statesToHandle->getNextSetIndex(0); } else if (compare == Order::BELOW) { - auto itr = std::find(statesSorted->begin(), statesSorted->end(), succ2); - if (itr != statesSorted->end()) { - statesSorted->erase(itr); + if (order->containsStatesSorted(succ2)) { + order->removeStatesSorted(succ2); } order->addBetween(succ2, order->getNode(stateNumber), order->getBottom()); statesToHandle->set(succ2); @@ -442,39 +460,36 @@ namespace storm { } // Normal backwardreasoning - if (statesSorted->size() > 0) { - auto stateNumber = *(statesSorted->begin()); - 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 (order->contains(stateNumber)) { - auto resAllAdded = allSuccAdded(order, stateNumber); - if (!std::get<0>(resAllAdded)) { - return std::make_tuple(order, std::get<1>(resAllAdded), std::get<2>(resAllAdded)); - } + auto stateNumber = order->getNextSortedState(); + while (stateNumber != numberOfStates && order->contains(stateNumber)) { + order->removeFirstStatesSorted(); + stateNumber = order->getNextSortedState(); + + if (stateNumber != numberOfStates && order->contains(stateNumber)) { + auto resAllAdded = allSuccAdded(order, stateNumber); + if (!std::get<0>(resAllAdded)) { + return std::make_tuple(order, std::get<1>(resAllAdded), std::get<2>(resAllAdded)); } } + } - if (!order->contains(stateNumber)) { - auto successors = stateMap[stateNumber]; - - 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 (order->getNode(stateNumber) != nullptr); - if (!acyclic) { - order->statesToHandle->set(stateNumber); - } - statesSorted->erase(statesSorted->begin()); + if (stateNumber != numberOfStates && !order->contains(stateNumber)) { + auto successors = stateMap[stateNumber]; + + 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 (order->getNode(stateNumber) != nullptr); + if (!acyclic) { + order->statesToHandle->set(stateNumber); } + order->removeFirstStatesSorted(); } - assert (order->getNode(stateNumber) != nullptr); - assert (order->contains(stateNumber)); } + assert (stateNumber == numberOfStates || order->getNode(stateNumber) != nullptr); + assert (stateNumber == numberOfStates || order->contains(stateNumber)); } assert (order->getAddedStates()->getNumberOfSetBits() == numberOfStates);