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

Add TODOs

tempestpy_adaptions
Jip Spel 6 years ago
parent
dc88830acd
commit
2827da84ee
3 changed files with 26 additions and 31 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. 17
      src/storm-pars-cli/storm-pars.cpp
  2. 9
      src/storm-pars/analysis/Lattice.cpp
  3. 29
      src/storm-pars/analysis/Transformer.cpp

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

@ -481,21 +481,26 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula(), storm::exceptions::NotSupportedException, "Expecting until formula");
// Check that formulas[0] is actually a ProbabilityOperator ...
// Check that formulas[0]->asProbabilityOperator().subformula() is an EventuallyFormula..
// Compute phiStates, psiStates via formulas[0]....subformula().as..().subformula
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*sparseModel);
storm::storage::BitVector phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); //right
// get the maybeStates
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates);
model.get()->printModelInformationToStream(std::cout);
storm::storage::BitVector topStates = statesWithProbability01.second;
storm::storage::BitVector bottomStates = statesWithProbability01.first;
storm::analysis::Lattice* lattice = storm::analysis::Transformer::toLattice(matrix, initialStates, topStates, bottomStates, sparseModel.get()->getNumberOfStates());
lattice->toString(std::cout);
// TODO: Analyse lattice with transition matrix
// Where do the parameters occur?
// initially incr.Boolean and decr.Boolean true
// At every occurence as long as either incr.Boolean or decr.Boolean true
// --> check if monotonic
// --> yes --> check position in lattice
// --> if incr. set incr.Boolean = incr.Boolean && true, decr.Boolean = false;
// --> if decr. set incr.Boolean = false, decr.Boolean = decr.Boolean && true;
// --> no --> set both booleans to false
// --> set both incr.bool and decr.bool to false
return;
}

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

@ -58,6 +58,7 @@ namespace storm {
}
Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) {
// TODO: might return nullptr, what to do with it?
Node *node;
for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) {
storm::storage::BitVector states = (*itr)->states;
@ -79,8 +80,8 @@ namespace storm {
out << ", ";
}
}
out << "}" << std::endl;
out << " Address: " << node << std::endl;
out << "}" << "\n";
out << " Address: " << node << "\n";
out << " Above: {";
for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) {
Node *above = *itr2;
@ -99,7 +100,7 @@ namespace storm {
out << ", ";
}
}
out << "}" << std::endl;
out << "}" << "\n";
out << " Below: {";
for (auto itr2 = node->below.begin(); itr2 != node->below.end(); ++itr2) {
@ -119,7 +120,7 @@ namespace storm {
out << ", ";
}
}
out << "}" << std::endl;
out << "}" << "\n";
}
}

29
src/storm-pars/analysis/Transformer.cpp
View File

@ -1,7 +1,7 @@
//
// Created by Jip Spel on 26.07.18.
//
// TODO: Use templates
#include "Transformer.h"
namespace storm {
namespace analysis {
@ -9,10 +9,12 @@ namespace storm {
storm::storage::BitVector const &initialStates,
storm::storage::BitVector topStates,
storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) {
// TODO: take SparseModel as input
// Transform the transition matrix into a vector containing the states with the state to which the transition goes.
std::vector<State*> stateVector = toStateVector(matrix, initialStates);
// Start creating the Lattice.
// TODO: not initializing all fields of Lattice::Node yet, what to do?
// Start creating the Lattice
Lattice::Node top = {topStates};
Lattice::Node bottom = {bottomStates};
Lattice *lattice = new Lattice(&top, &bottom, numberOfStates);
@ -20,8 +22,6 @@ namespace storm {
// Create a copy of the states already present in the lattice.
storm::storage::BitVector seenStates = topStates|=bottomStates;
matrix.printAsMatlabMatrix(std::cout);
while (oldStates != seenStates) {
// As long as new states are discovered, continue.
oldStates = storm::storage::BitVector(seenStates);
@ -46,7 +46,7 @@ namespace storm {
uint_fast64_t successor2 = currentState->successor2;
int compareResult = lattice->compare(successor1, successor2);
if (compareResult == 1) {
//TODO dit in een aparte methode doen
// TODO: create seperate method or change compareResult method?
Lattice::Node *above = lattice->getNode(successor1);
Lattice::Node *below = lattice->getNode(successor2);
std::vector<Lattice::Node *> states1 = above->below;
@ -61,12 +61,6 @@ namespace storm {
&& prob2 != storm::RationalFunction(1)
&& getProbability((*itr1)->states, above->states, matrix) == prob1
&& getProbability((*itr1)->states, below->states, matrix) == prob2) {
std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor1 << std::endl;
std::cout << prob1 << std::endl;
std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor2 << std::endl;
std::cout << prob2 << std::endl;
lattice->addToNode(currentState->stateNumber, (*itr1));
seenStates.set(currentState->stateNumber);
added = true;
@ -101,11 +95,6 @@ namespace storm {
&& getProbability((*itr1)->states, above->states, matrix) == prob1
&& getProbability((*itr1)->states, below->states, matrix) == prob2) {
std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor2 << std::endl;
std::cout << prob1 << std::endl;
std::cout << "Van: " << currentState-> stateNumber << " naar: " << successor1 << std::endl;
std::cout << prob2 << std::endl;
lattice->addToNode(currentState->stateNumber, (*itr1));
seenStates.set(currentState->stateNumber);
added = true;
@ -147,6 +136,7 @@ namespace storm {
std::vector<Transformer::State *>
Transformer::toStateVector(storm::storage::SparseMatrix<storm::RationalFunction> transitionMatrix,
storm::storage::BitVector const &initialStates) {
// TODO: Remove this, unnecessary
std::vector < State *> states = std::vector<State *>({});
std::vector <uint_fast64_t> stack(initialStates.begin(), initialStates.end());
std::vector <uint_fast64_t> seenStates(initialStates.begin(), initialStates.end());
@ -186,6 +176,8 @@ namespace storm {
}
void Transformer::print(storm::storage::BitVector vector, std::string message) {
// TODO: Remove this, unnecessary
uint_fast64_t index = vector.getNextSetIndex(0);
std::cout << message <<": {";
while (index < vector.size()) {
@ -199,6 +191,7 @@ namespace storm {
}
std::vector<uint_fast64_t> Transformer::getNumbers(storm::storage::BitVector vector) {
// TODO: Remove this, unnecessary
std::vector<uint_fast64_t> result = std::vector<uint_fast64_t>({});
uint_fast64_t index = vector.getNextSetIndex(0);
while (index < vector.size()) {
@ -234,11 +227,7 @@ namespace storm {
for (auto itr = row.begin(); itr < row.end() && result == storm::RationalFunction(1); ++itr) {
if ((*itr).getColumn() == successor) {
std::cout << "Tralala" << std::endl;
// TODO: nog checken dat ie wel met state te doen heeft
result = (*itr).getValue();
std::cout << "Van: " << state << " naar: " << successor << std::endl;
std::cout << result << std::endl;
}
}

Write Preview
Loading…
Cancel
Save