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

WIP Add LatticeExtender

tempestpy_adaptions
Jip Spel 6 years ago
parent
b0b0623fcf
commit
9e8d910a49
4 changed files with 185 additions and 114 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. 8
      src/storm-pars/analysis/Lattice.cpp
  2. 120
      src/storm-pars/analysis/Lattice.h
  3. 129
      src/storm-pars/analysis/LatticeExtender.cpp
  4. 42
      src/storm-pars/analysis/LatticeExtender.h

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

@ -24,7 +24,7 @@ namespace storm {
nodes.at(i) = bottom;
}
this->numberOfStates = numberOfStates;
this->addedStates = storm::storage::BitVector(numberOfStates);
}
void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) {
@ -38,11 +38,13 @@ namespace storm {
(below->above).insert(newNode);
above->below.insert(newNode);
nodes.at(state) = newNode;
addedStates.set(state);
}
void Lattice::addToNode(uint_fast64_t state, Node *node) {
node->states.set(state);
nodes.at(state) = node;
addedStates.set(state);
}
void Lattice::add(uint_fast64_t state) {
@ -83,6 +85,10 @@ namespace storm {
return nodes.at(stateNumber);
}
storm::storage::BitVector Lattice::getAddedStates() {
return addedStates;
}
void Lattice::toString(std::ostream &out) {
std::vector<Node*> printedNodes = std::vector<Node*>({});
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {

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

@ -6,17 +6,12 @@
#define LATTICE_LATTICE_H
#include <iostream>
#include <set>
#include <vector>
#include <storm/logic/Formula.h>
#include <storm/modelchecker/propositional/SparsePropositionalModelChecker.h>
#include "storm/models/sparse/Model.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/utility/macros.h"
#include "storm/utility/graph.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
@ -90,6 +85,8 @@ namespace storm {
*/
Node *getNode(uint_fast64_t state);
storm::storage::BitVector getAddedStates();
/*!
* Prints a string representation of the lattice to the output stream.
*
@ -104,115 +101,12 @@ namespace storm {
*/
void toDotFile(std::ostream &out);
/*!
* 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.
*/
template <typename ValueType>
static Lattice* toLattice(std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::shared_ptr<storm::logic::Formula const>> 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 = sparseModel.get()->getNumberOfStates();
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*sparseModel);
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(sparseModel.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 = sparseModel.get()->getTransitionMatrix();
std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
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");
}
// 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 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: is this what we want?
lattice->add(stateNumber);
}
seenStates.set(stateNumber);
}
}
}
return lattice;
}
private:
std::vector<Node*> nodes;
storm::storage::BitVector addedStates;
Node* top;
Node* bottom;

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

@ -0,0 +1,129 @@
//
// Created by Jip Spel on 28.08.18.
//
#include "LatticeExtender.h"
#include "storm/utility/macros.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/utility/graph.h"
#include <storm/logic/Formula.h>
#include <storm/modelchecker/propositional/SparsePropositionalModelChecker.h>
#include "storm/models/sparse/Model.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include <set>
namespace storm {
namespace analysis {
template <typename ValueType>
LatticeExtender<ValueType>::LatticeExtender(){//std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model) {
//TODO
}
// template <typename ValueType>
// storm::analysis::Lattice* LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::models::sparse::Model<ValueType>> 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<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");
//
// // 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<storm::expressions::Expression>({}));
// }
//
// template <typename ValueType>
// storm::analysis::Lattice* LatticeExtender<ValueType>::extendLattice(storm::analysis::Lattice* lattice, std::set<storm::expressions::Expression> 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;
// }
}
}

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

@ -0,0 +1,42 @@
//
// Created by Jip Spel on 28.08.18.
//
#ifndef STORM_LATTICEEXTENDER_H
#define STORM_LATTICEEXTENDER_H
#include <storm/logic/Formula.h>
#include "storm/models/sparse/Dtmc.h"
#include "storm-pars/analysis/Lattice.h"
namespace storm {
namespace analysis {
template <typename ValueType>
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<std::shared_ptr<storm::logic::Formula const>> formulas);
//
// storm::analysis::Lattice* extendLattice(storm::analysis::Lattice* lattice, std::set<storm::expressions::Expression> assumptions);
private:
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> model;
std::map<uint_fast64_t, storm::storage::BitVector> stateMap;
};
}
}
#endif //STORM_LATTICEEXTENDER_H
Write Preview
Loading…
Cancel
Save