diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 38d1c6975..9a73ee0d5 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -481,21 +481,26 @@ namespace storm { std::vector> 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> 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 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; } diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index c5c13f825..77f4e83f8 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -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"; } } diff --git a/src/storm-pars/analysis/Transformer.cpp b/src/storm-pars/analysis/Transformer.cpp index a87a8d19e..9a2baba53 100644 --- a/src/storm-pars/analysis/Transformer.cpp +++ b/src/storm-pars/analysis/Transformer.cpp @@ -1,7 +1,7 @@ // // Created by Jip Spel on 26.07.18. // - +// TODO: Use templates #include "Transformer.h" namespace storm { namespace analysis { @@ -9,19 +9,19 @@ 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 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); storm::storage::BitVector oldStates(numberOfStates); // 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 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::toStateVector(storm::storage::SparseMatrix transitionMatrix, storm::storage::BitVector const &initialStates) { + // TODO: Remove this, unnecessary std::vector < State *> states = std::vector({}); std::vector stack(initialStates.begin(), initialStates.end()); std::vector 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 Transformer::getNumbers(storm::storage::BitVector vector) { + // TODO: Remove this, unnecessary std::vector result = std::vector({}); 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; } }