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

Use parameter lifting for initial ro construction

tempestpy_adaptions
Jip Spel 5 years ago
parent
13f44ab7ea
commit
8214c5758e
7 changed files with 302 additions and 41 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 43
      src/storm-pars/analysis/Lattice.cpp
  2. 34
      src/storm-pars/analysis/Lattice.h
  3. 201
      src/storm-pars/analysis/LatticeExtender.cpp
  4. 33
      src/storm-pars/analysis/LatticeExtender.h
  5. 26
      src/storm-pars/analysis/MonotonicityChecker.cpp
  6. 2
      src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
  7. 4
      src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp

43
src/storm-pars/analysis/Lattice.cpp
View File

@ -38,6 +38,30 @@ namespace storm {
} }
} }
Lattice::Lattice(uint_fast64_t topState, uint_fast64_t bottomState, uint_fast64_t numberOfStates) {
nodes = std::vector<Node *>(numberOfStates);
this->numberOfStates = numberOfStates;
this->addedStates = new storm::storage::BitVector(numberOfStates);
this->doneBuilding = false;
top = new Node();
bottom = new Node();
top->statesAbove = storm::storage::BitVector(numberOfStates);
bottom->statesAbove = storm::storage::BitVector(numberOfStates);
addedStates->set(topState);
bottom->statesAbove.set(topState);
top->states.insert(topState);
nodes[topState] = top;
addedStates->set(bottomState);
bottom->states.insert(bottomState);
nodes[bottomState] = bottom;
assert (addedStates->getNumberOfSetBits() == 2);
}
Lattice::Lattice(Lattice* lattice) { Lattice::Lattice(Lattice* lattice) {
numberOfStates = lattice->getAddedStates()->size(); numberOfStates = lattice->getAddedStates()->size();
nodes = std::vector<Node *>(numberOfStates); nodes = std::vector<Node *>(numberOfStates);
@ -90,6 +114,16 @@ namespace storm {
addedStates->set(state); addedStates->set(state);
} }
void Lattice::addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below) {
assert(!(*addedStates)[state]);
assert(compare(above, below) == ABOVE);
assert (getNode(below)->states.find(below) != getNode(below)->states.end());
assert (getNode(above)->states.find(above) != getNode(above)->states.end());
addBetween(state, getNode(above), getNode(below));
}
void Lattice::addToNode(uint_fast64_t state, Node *node) { void Lattice::addToNode(uint_fast64_t state, Node *node) {
assert(!(*addedStates)[state]); assert(!(*addedStates)[state]);
node->states.insert(state); node->states.insert(state);
@ -111,6 +145,10 @@ namespace storm {
assert (compare(above, below) == ABOVE); assert (compare(above, below) == ABOVE);
} }
void Lattice::addRelation(uint_fast64_t above, uint_fast64_t below) {
addRelationNodes(getNode(above), getNode(below));
}
Lattice::NodeComparison Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { Lattice::NodeComparison Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) {
return compare(getNode(state1), getNode(state2)); return compare(getNode(state1), getNode(state2));
} }
@ -147,6 +185,11 @@ namespace storm {
return UNKNOWN; return UNKNOWN;
} }
bool Lattice::contains(uint_fast64_t state) {
return state >= 0 && state < addedStates->size() && addedStates->get(state);
}
Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) {
return nodes.at(stateNumber); return nodes.at(stateNumber);
} }

34
src/storm-pars/analysis/Lattice.h
View File

@ -40,6 +40,17 @@ namespace storm {
storm::storage::BitVector* initialMiddleStates, storm::storage::BitVector* initialMiddleStates,
uint_fast64_t numberOfStates); uint_fast64_t numberOfStates);
/*!
* Constructs a lattice with the given top state and bottom state.
*
* @param top The top state of the resulting lattice.
* @param bottom The bottom state of the resulting lattice.
* @param numberOfStates Max number of states in endlattice.
*/
Lattice(uint_fast64_t top,
uint_fast64_t bottom,
uint_fast64_t numberOfStates);
/*! /*!
* Constructs a copy of the given lattice. * Constructs a copy of the given lattice.
* *
@ -55,6 +66,15 @@ namespace storm {
*/ */
void addBetween(uint_fast64_t state, Node *node1, Node *node2); void addBetween(uint_fast64_t state, Node *node1, Node *node2);
/*!
* Adds a node with the given state between the nodes of below and above.
* Result: below -> state -> above
* @param state The given state.
* @param above The state number of the state below which a new node (with state) is added
* @param below The state number of the state above which a new node (with state) is added
*/
void addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below);
/*! /*!
* Adds state to the states of the given node. * Adds state to the states of the given node.
* @param state The state which is added. * @param state The state which is added.
@ -75,6 +95,13 @@ namespace storm {
*/ */
void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below); void addRelationNodes(storm::analysis::Lattice::Node *above, storm::analysis::Lattice::Node * below);
/*!
* Adds a new relation between two states to the lattice
* @param above The state closest to the top Node of the Lattice.
* @param below The state closest to the bottom Node of the Lattice.
*/
void addRelation(uint_fast64_t above, uint_fast64_t below);
/*! /*!
* Compares the level of the nodes of the states. * Compares the level of the nodes of the states.
* Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice. * Behaviour unknown when one or more of the states doesnot occur at any Node in the Lattice.
@ -87,6 +114,13 @@ namespace storm {
*/ */
Lattice::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2); Lattice::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2);
/*!
* Check if state is already in lattice
* @param state
* @return
*/
bool contains(uint_fast64_t state);
/*! /*!
* Retrieves the pointer to a Node at which the state occurs. * Retrieves the pointer to a Node at which the state occurs.
* *

201
src/storm-pars/analysis/LatticeExtender.cpp
View File

@ -33,7 +33,33 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
LatticeExtender<ValueType>::LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) { LatticeExtender<ValueType>::LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) {
this->model = model; this->model = model;
assumptionSeen = false;
this->matrix = model->getTransitionMatrix();
this->assumptionSeen = false;
uint_fast64_t numberOfStates = this->model->getNumberOfStates();
// Build stateMap
// TODO: is dit wel nodig
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
stateMap[i] = new storm::storage::BitVector(numberOfStates, false);
auto row = matrix.getRow(i);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions
if (i != rowItr->getColumn() || row.getNumberOfEntries() == 1) {
stateMap[i]->set(rowItr->getColumn(), true);
}
}
}
// Check if MC contains cycles
storm::storage::StronglyConnectedComponentDecompositionOptions const options;
this->sccs = storm::storage::StronglyConnectedComponentDecomposition<ValueType>(matrix, options);
acyclic = true;
for (auto i = 0; acyclic && i < sccs.size(); ++i) {
acyclic &= sccs.getBlock(i).size() <= 1;
}
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
} }
template <typename ValueType> template <typename ValueType>
@ -45,6 +71,7 @@ namespace storm {
uint_fast64_t numberOfStates = this->model->getNumberOfStates(); uint_fast64_t numberOfStates = this->model->getNumberOfStates();
// TODO: dit moet anders kunnen
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model); storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*model);
storm::storage::BitVector phiStates; storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates; storm::storage::BitVector psiStates;
@ -56,6 +83,7 @@ namespace storm {
psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
} }
// Get the maybeStates // Get the maybeStates
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->model->getBackwardTransitions(), phiStates, psiStates); 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 topStates = statesWithProbability01.second;
@ -75,10 +103,13 @@ namespace storm {
for (auto i = 0; acyclic && i < decomposition.size(); ++i) { for (auto i = 0; acyclic && i < decomposition.size(); ++i) {
acyclic &= decomposition.getBlock(i).size() <= 1; acyclic &= decomposition.getBlock(i).size() <= 1;
} }
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
// Create the Lattice
Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates);
if (acyclic) { if (acyclic) {
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
} else { } else {
statesSorted = storm::utility::graph::getTopologicalSort(matrix);
for (uint_fast64_t i = 0; i < numberOfStates; ++i) { for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
stateMap[i] = new storm::storage::BitVector(numberOfStates, false); stateMap[i] = new storm::storage::BitVector(numberOfStates, false);
@ -91,6 +122,7 @@ namespace storm {
} }
} }
for (auto i = 0; i < decomposition.size(); ++i) { for (auto i = 0; i < decomposition.size(); ++i) {
// TODO: alleen als er nog geen van in de lattice zit
auto scc = decomposition.getBlock(i); auto scc = decomposition.getBlock(i);
if (scc.size() > 1) { if (scc.size() > 1) {
auto states = scc.getStates(); auto states = scc.getStates();
@ -103,6 +135,7 @@ namespace storm {
auto intersection = bottomStates | topStates; auto intersection = bottomStates | topStates;
if (intersection[succ1] || intersection[succ2]) { if (intersection[succ1] || intersection[succ2]) {
initialMiddleStates.set(state); initialMiddleStates.set(state);
// ipv daaraan toevoegen, hem toevoegen aan de lattice die we eerder al gecreerd hebben
break; break;
} }
} }
@ -110,15 +143,128 @@ namespace storm {
} }
} }
} }
statesToHandle = &initialMiddleStates; statesToHandle = &initialMiddleStates;
// Create the Lattice
Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates);
return this->extendLattice(lattice);
}
template <typename ValueType>
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(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);
Lattice* lattice = new Lattice(top, bottom, numberOfStates);
for (auto state : statesSorted) {
if (state != bottom && state != top) {
assert (lattice != nullptr);
auto successors = stateMap[state];
if (successors->size() > 1) {
uint_fast64_t min = numberOfStates;
uint_fast64_t max = numberOfStates;
bool allSorted = true;
for (auto succ = successors->getNextSetIndex(0);
succ < numberOfStates; succ = successors->getNextSetIndex(succ + 1)) {
if (min == numberOfStates) {
assert (max == numberOfStates);
min = succ;
max = succ;
} else {
if (minValues[succ] > maxValues[max]) {
max = succ;
} else if (maxValues[succ] < minValues[min]) {
min = succ;
} else {
allSorted = false;
break;
}
}
}
if (allSorted && min != max) {
if (lattice->contains(min) && lattice->contains(max)) {
assert (lattice->compare(min,max) == Lattice::UNKNOWN || lattice->compare(min,max) == Lattice::BELOW);
if (lattice->compare(min, max) == Lattice::UNKNOWN) {
lattice->addRelation(max, min);
}
}
if (!lattice->contains(min)) {
if (lattice->contains(max)) {
lattice->addBetween(min, lattice->getNode(max), lattice->getBottom());
} else {
lattice->add(min);
}
}
if (!lattice->contains(max)) {
// Because of construction min is in the lattice
lattice->addBetween(max, lattice->getNode(min), lattice->getTop());
}
assert (lattice->compare(max, min) == Lattice::ABOVE);
lattice->addBetween(state, max, min);
}
}
}
}
// Handle sccs
auto addedStates = lattice->getAddedStates();
for (auto scc : sccs) {
if (scc.size() > 1) {
auto states = scc.getStates();
auto candidate = -1;
for (auto const& state : states) {
if (addedStates->get(state)) {
candidate = -1;
break;
// if there is a state of the scc already present in the lattice, there is no need to add one.
}
auto successors = stateMap[state];
if (candidate == -1 && successors->getNumberOfSetBits() == 2) {
auto succ1 = successors->getNextSetIndex(0);
auto succ2 = successors->getNextSetIndex(succ1 + 1);
if (addedStates->get(succ1) || addedStates->get(succ2)) {
candidate = state;
}
}
}
if (candidate != -1) {
lattice->add(candidate);
}
}
}
return this->extendLattice(lattice); return this->extendLattice(lattice);
} }
template <typename ValueType> template <typename ValueType>
void LatticeExtender<ValueType>::handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) { void LatticeExtender<ValueType>::handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
assert (assumption != nullptr); assert (assumption != nullptr);
@ -250,15 +396,15 @@ namespace storm {
if (statesSorted.size() > 0) { if (statesSorted.size() > 0) {
auto nextState = *(statesSorted.begin()); auto nextState = *(statesSorted.begin());
while ((*(lattice->getAddedStates()))[nextState] && statesSorted.size() > 1) {
while (lattice->contains(nextState) && statesSorted.size() > 1) {
// states.size()>1 such that there is at least one state left after erase // states.size()>1 such that there is at least one state left after erase
statesSorted.erase(statesSorted.begin()); statesSorted.erase(statesSorted.begin());
nextState = *(statesSorted.begin()); nextState = *(statesSorted.begin());
} }
if (!(*(lattice->getAddedStates()))[nextState]) {
if (!lattice->contains(nextState)) {
auto row = this->model->getTransitionMatrix().getRow(nextState); auto row = this->model->getTransitionMatrix().getRow(nextState);
auto successors = new storm::storage::BitVector(lattice->getAddedStates()->size());
auto successors = new storm::storage::BitVector(numberOfStates);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions // ignore self-loops when there are more transitions
if (nextState != rowItr->getColumn()) { if (nextState != rowItr->getColumn()) {
@ -278,22 +424,22 @@ namespace storm {
} }
auto added = lattice->getAddedStates()->getNumberOfSetBits(); auto added = lattice->getAddedStates()->getNumberOfSetBits();
assert (lattice->getNode(nextState) != nullptr); assert (lattice->getNode(nextState) != nullptr);
assert ((*lattice->getAddedStates())[nextState]);
assert (lattice->contains(nextState));
} }
} else if (assumptionSeen && acyclic) { } else if (assumptionSeen && acyclic) {
auto states = statesSorted; auto states = statesSorted;
if (states.size() > 0) { if (states.size() > 0) {
auto nextState = *(states.begin()); auto nextState = *(states.begin());
while ((*(lattice->getAddedStates()))[nextState] && states.size() > 1) {
while (lattice->contains(nextState) && states.size() > 1) {
// states.size()>1 such that there is at least one state left after erase // states.size()>1 such that there is at least one state left after erase
states.erase(states.begin()); states.erase(states.begin());
nextState = *(states.begin()); nextState = *(states.begin());
} }
if (!(*(lattice->getAddedStates()))[nextState]) {
if (!lattice->contains(nextState)) {
auto row = this->model->getTransitionMatrix().getRow(nextState); auto row = this->model->getTransitionMatrix().getRow(nextState);
auto successors = new storm::storage::BitVector(lattice->getAddedStates()->size());
auto successors = new storm::storage::BitVector(numberOfStates);
for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) { for (auto rowItr = row.begin(); rowItr != row.end(); ++rowItr) {
// ignore self-loops when there are more transitions // ignore self-loops when there are more transitions
if (nextState != rowItr->getColumn()) { if (nextState != rowItr->getColumn()) {
@ -316,25 +462,23 @@ namespace storm {
} }
} }
assert (lattice->getNode(nextState) != nullptr); assert (lattice->getNode(nextState) != nullptr);
assert ((*lattice->getAddedStates())[nextState]);
assert (lattice->contains(nextState));
} }
} else if (!acyclic) { } else if (!acyclic) {
auto addedStates = lattice->getAddedStates();
if (assumptionSeen) { if (assumptionSeen) {
statesToHandle = addedStates;
statesToHandle = lattice->getAddedStates();
} }
auto stateNumber = statesToHandle->getNextSetIndex(0); auto stateNumber = statesToHandle->getNextSetIndex(0);
while (stateNumber != numberOfStates) { while (stateNumber != numberOfStates) {
addedStates = lattice->getAddedStates();
storm::storage::BitVector* successors = stateMap[stateNumber]; storm::storage::BitVector* successors = stateMap[stateNumber];
// Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet
auto succ1 = successors->getNextSetIndex(0); auto succ1 = successors->getNextSetIndex(0);
auto succ2 = successors->getNextSetIndex(succ1 + 1); auto succ2 = successors->getNextSetIndex(succ1 + 1);
assert ((*addedStates)[stateNumber]);
assert (lattice->contains(stateNumber));
if (successors->getNumberOfSetBits() == 1) { if (successors->getNumberOfSetBits() == 1) {
if (!(*addedStates)[succ1]) {
if (!lattice->contains(succ1)) {
lattice->addToNode(succ1, lattice->getNode(stateNumber)); lattice->addToNode(succ1, lattice->getNode(stateNumber));
statesToHandle->set(succ1, true); statesToHandle->set(succ1, true);
auto itr = std::find(statesSorted.begin(), statesSorted.end(), succ1); auto itr = std::find(statesSorted.begin(), statesSorted.end(), succ1);
@ -345,10 +489,10 @@ namespace storm {
statesToHandle->set(stateNumber, false); statesToHandle->set(stateNumber, false);
stateNumber = statesToHandle->getNextSetIndex(0); stateNumber = statesToHandle->getNextSetIndex(0);
} else if (successors->getNumberOfSetBits() == 2 } else if (successors->getNumberOfSetBits() == 2
&& (((*(addedStates))[succ1] && !(*(addedStates))[succ2])
|| (!(*(addedStates))[succ1] && (*(addedStates))[succ2]))) {
&& ((lattice->contains(succ1) && !lattice->contains(succ2))
|| (!lattice->contains(succ1) && lattice->contains(succ2)))) {
if (!(*(addedStates))[succ1]) {
if (!lattice->contains(succ1)) {
std::swap(succ1, succ2); std::swap(succ1, succ2);
} }
@ -377,8 +521,8 @@ namespace storm {
stateNumber = statesToHandle->getNextSetIndex(0); stateNumber = statesToHandle->getNextSetIndex(0);
} }
} else if (!(((*(addedStates))[succ1] && !(*(addedStates))[succ2])
|| (!(*(addedStates))[succ1] && (*(addedStates))[succ2]))) {
} else if (!((lattice->contains(succ1) && !lattice->contains(succ2))
|| (!lattice->contains(succ1) && lattice->contains(succ2)))) {
stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1); stateNumber = statesToHandle->getNextSetIndex(stateNumber + 1);
} else { } else {
statesToHandle->set(stateNumber, false); statesToHandle->set(stateNumber, false);
@ -393,7 +537,7 @@ namespace storm {
stateNumber = numberOfStates; stateNumber = numberOfStates;
} }
while (stateNumber != numberOfStates while (stateNumber != numberOfStates
&& (*(lattice->getAddedStates()))[stateNumber]) {
&& lattice->contains(stateNumber)) {
statesSorted.erase(statesSorted.begin()); statesSorted.erase(statesSorted.begin());
if (statesSorted.size() > 0) { if (statesSorted.size() > 0) {
stateNumber = *(statesSorted.begin()); stateNumber = *(statesSorted.begin());
@ -407,7 +551,7 @@ namespace storm {
// Check if current state has not been added yet, and all successors have, ignore selfloop in this // Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false); successors->set(stateNumber, false);
if ((*successors & *addedStates) == *successors) {
if ((*successors & *(lattice->getAddedStates())) == *successors) {
auto result = extendAllSuccAdded(lattice, stateNumber, successors); auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) { if (std::get<1>(result) != successors->size()) {
return result; return result;
@ -416,15 +560,14 @@ namespace storm {
} }
} }
} else { } else {
addedStates = lattice->getAddedStates();
auto notAddedStates = addedStates->operator~();
auto notAddedStates = lattice->getAddedStates()->operator~();
for (auto stateNumber : notAddedStates) { for (auto stateNumber : notAddedStates) {
// Iterate over all not yet added states // Iterate over all not yet added states
storm::storage::BitVector* successors = stateMap[stateNumber]; storm::storage::BitVector* successors = stateMap[stateNumber];
// Check if current state has not been added yet, and all successors have, ignore selfloop in this // Check if current state has not been added yet, and all successors have, ignore selfloop in this
successors->set(stateNumber, false); successors->set(stateNumber, false);
if ((*successors & *addedStates) == *successors) {
if ((*successors & *(lattice->getAddedStates())) == *successors) {
auto result = extendAllSuccAdded(lattice, stateNumber, successors); auto result = extendAllSuccAdded(lattice, stateNumber, successors);
if (std::get<1>(result) != successors->size()) { if (std::get<1>(result) != successors->size()) {
return result; return result;

33
src/storm-pars/analysis/LatticeExtender.h
View File

@ -5,6 +5,10 @@
#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Dtmc.h"
#include "storm-pars/analysis/Lattice.h" #include "storm-pars/analysis/Lattice.h"
#include "storm/api/storm.h" #include "storm/api/storm.h"
#include "storm-pars/storage/ParameterRegion.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/storage/StronglyConnectedComponent.h"
namespace storm { namespace storm {
@ -23,25 +27,36 @@ namespace storm {
LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model); LatticeExtender(std::shared_ptr<storm::models::sparse::Model<ValueType>> model);
/*! /*!
* Extends the lattice based on the given assumption.
* Creates a lattice based on the given formula.
* *
* @param lattice The lattice.
* @param assumption The assumption on states.
* @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 * @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 * is unknown but needed. When the states have as number the number of states, no states are
* unplaced but needed. * unplaced but needed.
*/ */
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> extendLattice(storm::analysis::Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr);
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas);
/*! /*!
* Creates a lattice based on the given formula.
* Creates a lattice based on the given extremal values.
* *
* @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 * @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 * is unknown but needed. When the states have as number the number of states, no states are
* unplaced but needed. * 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, std::vector<double> minValues, std::vector<double> maxValues);
/*!
* Extends the lattice based on the given assumption.
*
* @param lattice The lattice.
* @param assumption The assumption 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::shared_ptr<storm::expressions::BinaryRelationExpression> assumption = nullptr);
private: private:
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
@ -56,6 +71,10 @@ namespace storm {
storm::storage::BitVector* statesToHandle; storm::storage::BitVector* statesToHandle;
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccs;
storm::storage::SparseMatrix<ValueType> matrix;
void handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption); void handleAssumption(Lattice* lattice, std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors); std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t const & stateNumber, storm::storage::BitVector* successors);

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

@ -175,8 +175,31 @@ namespace storm {
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::createLattice() { std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> MonotonicityChecker<ValueType>::createLattice() {
// Transform to Lattices // Transform to Lattices
storm::utility::Stopwatch latticeWatch(true); storm::utility::Stopwatch latticeWatch(true);
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toLattice(formulas);
// Use parameter lifting modelchecker to get initial min/max values for lattice creation
storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ValueType>, double> plaModelChecker;
std::unique_ptr<storm::modelchecker::CheckResult> checkResult;
auto env = Environment();
auto formula = formulas[0];
const storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> checkTask
= storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula);
STORM_LOG_THROW(plaModelChecker.canHandle(model, checkTask), storm::exceptions::NotSupportedException,
"Cannot handle this formula");
plaModelChecker.specify(env, model, checkTask);
std::unique_ptr<storm::modelchecker::CheckResult> minCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Minimize);
std::unique_ptr<storm::modelchecker::CheckResult> maxCheck = plaModelChecker.check(env, region,storm::solver::OptimizationDirection::Maximize);
auto minRes = minCheck->asExplicitQuantitativeCheckResult<double>();
auto maxRes = maxCheck->asExplicitQuantitativeCheckResult<double>();
std::vector<double> minValues = minRes.getValueVector();
std::vector<double> maxValues = maxRes.getValueVector();
// Create initial lattice
std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTuple = extender->toLattice(formulas, minValues, maxValues);
// Continue based on not (yet) sorted states
std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result; std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> result;
auto val1 = std::get<1>(criticalTuple); auto val1 = std::get<1>(criticalTuple);
@ -515,7 +538,6 @@ namespace storm {
return result; return result;
} }
template <typename ValueType> template <typename ValueType>
std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) { std::map<typename utility::parametric::VariableType<ValueType>::type, std::pair<bool, bool>> MonotonicityChecker<ValueType>::checkOnSamples(std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model, uint_fast64_t numberOfSamples) {
storm::utility::Stopwatch samplesWatch(true); storm::utility::Stopwatch samplesWatch(true);

2
src/test/storm-pars/analysis/AssumptionCheckerTest.cpp
View File

@ -331,7 +331,7 @@ TEST(AssumptionCheckerTest, Simple4) {
below.set(4); below.set(4);
storm::storage::BitVector initialMiddle(5); storm::storage::BitVector initialMiddle(5);
auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5); auto lattice = new storm::analysis::Lattice(&above, &below, &initialMiddle, 5);
auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>( auto assumption = std::make_shared<storm::expressions::BinaryRelationExpression>(
storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(),
expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(), expressionManager->getVariable("1").getExpression().getBaseExpressionPointer(),

4
src/test/storm-pars/analysis/MonotonicityCheckerTest.cpp
View File

@ -110,7 +110,7 @@ TEST(MonotonicityCheckerTest, Derivative_checker) {
TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) { TEST(MonotonicityCheckerTest, Brp_with_bisimulation_no_samples) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [F s=4 & i=N ]";
std::string formulaAsString = "P=? [true U s=4 & i=N ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula // Program and formula
@ -159,7 +159,7 @@ std::vector<storm::storage::ParameterRegion<storm::RationalFunction>> regions =
TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) { TEST(MonotonicityCheckerTest, Brp_with_bisimulation_samples) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
std::string formulaAsString = "P=? [F s=4 & i=N ]";
std::string formulaAsString = "P=? [true U s=4 & i=N ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
// Program and formula // Program and formula

Write Preview
Loading…
Cancel
Save