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

Move creation of Lattice to Lattice class

tempestpy_adaptions
Jip Spel 6 years ago
parent
5f6a894a32
commit
c6e6331db2
3 changed files with 114 additions and 93 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. 89
      src/storm-pars-cli/storm-pars.cpp
  2. 9
      src/storm-pars/analysis/Lattice.cpp
  3. 109
      src/storm-pars/analysis/Lattice.h

89
src/storm-pars-cli/storm-pars.cpp
View File

@ -49,11 +49,7 @@ namespace storm {
bool exact;
};
struct State {
uint_fast64_t stateNumber;
uint_fast64_t successor1;
uint_fast64_t successor2;
};
template <typename ValueType>
std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) {
@ -443,86 +439,7 @@ namespace storm {
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
}
template <typename ValueType>
storm::analysis::Lattice* toLattice(std::shared_ptr<storm::models::sparse::Model<ValueType>> model,
storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates) {
storm::storage::SparseMatrix<ValueType> matrix = model.get()->getTransitionMatrix();
storm::storage::BitVector initialStates = model.get()->getInitialStates();
uint_fast64_t numberOfStates = model.get()->getNumberOfStates();
// Transform the transition matrix into a vector containing the states with the state to which the transition goes.
std::vector <State*> stateVector = std::vector<State *>({});
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
State* state = new State();
state->stateNumber = i;
state->successor1 = numberOfStates;
state->successor2 = numberOfStates;
auto row = matrix.getRow(i);
//TODO assert that there are at most two successors
if ((*(row.begin())).getValue() != ValueType(1)) {
state->successor1 = (*(row.begin())).getColumn();
state->successor2 = (*(++row.begin())).getColumn();
} else {
state-> successor1 = (*(row.begin())).getColumn();
state-> successor2 = (*(row.begin())).getColumn();
}
stateVector.push_back(state);
}
// 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 itr = stateVector.begin(); itr != stateVector.end(); ++itr) {
// Iterate over all states
State *currentState = *itr;
if (!seenStates[currentState->stateNumber]
&& seenStates[currentState->successor1]
&& seenStates[currentState->successor2]) {
// Otherwise, check how the two states compare, and add if the comparison is possible.
uint_fast64_t successor1 = currentState->successor1;
uint_fast64_t successor2 = currentState->successor2;
int compareResult = lattice->compare(successor1, successor2);
if (compareResult == 1 || compareResult == 2) {
// getNode will not return nullptr, as compare already checked this
if (compareResult == 2) {
// swap
auto temp = successor1;
successor1 = successor2;
successor2 = temp;
}
// successor 1 is closer to top than successor 2
lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1),
lattice->getNode(successor2));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else if (compareResult == 0) {
// the successors are at the same level
lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else {
// TODO: what to do?
STORM_LOG_DEBUG("Failed to add" << currentState->stateNumber << "\n");
}
}
}
}
return lattice;
}
template <storm::dd::DdType DdType, typename ValueType>
@ -589,12 +506,12 @@ namespace storm {
storm::storage::BitVector bottomStates = statesWithProbability01.first;
// Transform to LatticeLattice
storm::analysis::Lattice* lattice = toLattice(sparseModel, topStates, bottomStates);
storm::storage::SparseMatrix<ValueType> matrix = sparseModel.get()->getTransitionMatrix();
storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice<ValueType>(matrix, topStates, bottomStates);
lattice->toString(std::cout);
// Monotonicity?
bool monotoneInAll = true;
storm::storage::SparseMatrix<ValueType> matrix = sparseModel.get()->getTransitionMatrix();
for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) {
// go over all rows
auto row = matrix.getRow(i);

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

@ -9,9 +9,9 @@ namespace storm {
Lattice::Lattice(storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) {
Node *top = new Node();
top = new Node();
top->states = topStates;
Node *bottom = new Node();
bottom = new Node();
bottom->states = bottomStates;
top->below.push_back(bottom);
bottom->above.push_back(top);
@ -29,7 +29,6 @@ namespace storm {
}
void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) {
std::cout << "Adding: " << state << std::endl;
Node *newNode = new Node();
newNode->states = storm::storage::BitVector(numberOfStates);
newNode->states.set(state);
@ -47,6 +46,10 @@ namespace storm {
nodes.at(state) = node;
}
void Lattice::add(uint_fast64_t state) {
addBetween(state, top, bottom);
}
int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) {
Node *node1 = getNode(state1);
Node *node2 = getNode(state2);

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

@ -8,7 +8,10 @@
#include <iostream>
#include <vector>
#include "storm/models/sparse/Model.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
namespace storm {
namespace analysis {
@ -33,18 +36,24 @@ namespace storm {
/*!
* Adds a node with the given state below node1 and above node2.
* @param state The given state.
* @param node1 The pointer to the node below which a new node is added.
* @param node2 The pointer to the node above which a new node is added.
* @param node1 The pointer to the node below which a new node (with state) is added
* @param node2 The pointer to the node above which a new node (with state) is added
*/
void addBetween(uint_fast64_t state, Node *node1, Node *node2);
/*!
* Adds state to the states of the given node.
* @param state The state which is added.
* @param node The pointer to the node to which state is added.
* @param node The pointer to the node to which state is added, should not be nullptr.
*/
void addToNode(uint_fast64_t state, Node *node);
/*!
* Adds state between the top and bottom node of the lattice
* @param state The given state
*/
void add(uint_fast64_t state);
/*!
* 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.
@ -74,11 +83,103 @@ namespace storm {
*/
void toString(std::ostream &out);
// std::vector<uint_fast64_t> addedStates;
/*!
* Creates a Lattice based on the transition matrix, topStates of the Lattice and bottomStates of the Lattice
* @tparam ValueType Type of the probabilities
* @param matrix The transition matrix.
* @param topStates Set of topStates of the Lattice.
* @param bottomStates Set of bottomStates of the Lattice.
* @return pointer to the created Lattice.
*/
template <typename ValueType>
static Lattice* toLattice(storm::storage::SparseMatrix<ValueType> matrix,
storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates) {
uint_fast64_t numberOfStates = matrix.getColumnCount();
// Transform the transition matrix into a vector containing the states with the state to which the transition goes.
std::vector <State*> stateVector = std::vector<State *>({});
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
State* state = new State();
state->stateNumber = i;
auto row = matrix.getRow(i);
//TODO assert that there are at most two successors
if ((*(row.begin())).getValue() != ValueType(1)) {
state->successor1 = (*(row.begin())).getColumn();
state->successor2 = (*(++row.begin())).getColumn();
} else {
state-> successor1 = (*(row.begin())).getColumn();
state-> successor2 = (*(row.begin())).getColumn();
}
stateVector.push_back(state);
}
// 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 itr = stateVector.begin(); itr != stateVector.end(); ++itr) {
// Iterate over all states
State *currentState = *itr;
if (!seenStates[currentState->stateNumber]
&& seenStates[currentState->successor1]
&& seenStates[currentState->successor2]) {
// Otherwise, check how the two states compare, and add if the comparison is possible.
uint_fast64_t successor1 = currentState->successor1;
uint_fast64_t successor2 = currentState->successor2;
int compareResult = lattice->compare(successor1, successor2);
if (compareResult == 1) {
// successor 1 is closer to top than successor 2
lattice->addBetween(currentState->stateNumber, lattice->getNode(successor1),
lattice->getNode(successor2));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else if (compareResult == 2) {
// successor 2 is closer to top than successor 1
lattice->addBetween(currentState->stateNumber, lattice->getNode(successor2),
lattice->getNode(successor1));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else if (compareResult == 0) {
// the successors are at the same level
lattice->addToNode(currentState->stateNumber, lattice->getNode(successor1));
// Add stateNumber to the set with seen states.
seenStates.set(currentState->stateNumber);
} else {
// TODO: is this what we want?
lattice->add(currentState->stateNumber);
}
}
}
}
return lattice;
}
private:
struct State {
uint_fast64_t stateNumber;
uint_fast64_t successor1;
uint_fast64_t successor2;
};
std::vector<Node *> nodes;
Node * top;
Node * bottom;
uint_fast64_t numberOfStates;
bool above(Node *, Node *);

Write Preview
Loading…
Cancel
Save