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

Small fixes

tempestpy_adaptions
Jip Spel 5 years ago
parent
e0b2869bd5
commit
12e0ef537c
4 changed files with 137 additions and 81 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. 2
      src/storm-pars/analysis/MonotonicityChecker.cpp
  2. 40
      src/storm-pars/analysis/Order.cpp
  3. 13
      src/storm-pars/analysis/Order.h
  4. 163
      src/storm-pars/analysis/OrderExtender.cpp

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

@ -195,6 +195,8 @@ namespace storm {
std::vector<double> minValues = minRes.getValueVector();
std::vector<double> maxValues = maxRes.getValueVector();
// TODO: zijn de value vectors nu precies omgedraaid?
// Create initial order
std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas, minValues, maxValues);
// std::tuple<storm::analysis::Order*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toOrder(formulas);

40
src/storm-pars/analysis/Order.cpp
View File

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

13
src/storm-pars/analysis/Order.h
View File

@ -212,11 +212,22 @@ namespace storm {
storm::storage::BitVector* statesToHandle;
std::vector<uint_fast64_t>* statesSorted;
uint_fast64_t getNextSortedState();
bool containsStatesSorted(uint_fast64_t state);
void removeFirstStatesSorted();
void removeStatesSorted(uint_fast64_t state);
protected:
std::vector<uint_fast64_t> getStatesSorted();
private:
std::vector<Node*> nodes;
std::vector<uint_fast64_t> statesSorted;
storm::storage::BitVector* addedStates;
Node* top;

163
src/storm-pars/analysis/OrderExtender.cpp
View File

@ -69,7 +69,6 @@ namespace storm {
uint_fast64_t numberOfStates = this->model->getNumberOfStates();
// TODO: dit moet anders kunnen
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model);
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
@ -130,43 +129,65 @@ namespace storm {
template <typename ValueType>
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
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<storm::models::sparse::Model<ValueType>> 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<storm::storage::BitVector, storm::storage::BitVector> 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<storm::models::sparse::Model<ValueType>> 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<storm::storage::BitVector, storm::storage::BitVector> 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<uint_fast64_t> 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);

Write Preview
Loading…
Cancel
Save