From dc88830acd9af07d171b5536286445259deb6043 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 3 Aug 2018 12:45:27 +0200 Subject: [PATCH] First try --- src/storm-pars-cli/storm-pars.cpp | 41 ++- src/storm-pars/analysis/Lattice.cpp | 171 ++++++++++++ src/storm-pars/analysis/Lattice.h | 94 +++++++ src/storm-pars/analysis/Transformer.cpp | 249 ++++++++++++++++++ src/storm-pars/analysis/Transformer.h | 55 ++++ .../settings/modules/ParametricSettings.cpp | 6 +- .../settings/modules/ParametricSettings.h | 2 + 7 files changed, 615 insertions(+), 3 deletions(-) create mode 100644 src/storm-pars/analysis/Lattice.cpp create mode 100644 src/storm-pars/analysis/Lattice.h create mode 100644 src/storm-pars/analysis/Transformer.cpp create mode 100644 src/storm-pars/analysis/Transformer.h diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index badcb0212..38d1c6975 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -3,6 +3,8 @@ #include "storm-pars/settings/ParsSettings.h" #include "storm-pars/settings/modules/ParametricSettings.h" #include "storm-pars/settings/modules/RegionSettings.h" +#include "storm-pars/analysis/Lattice.h" +#include "storm-pars/analysis/Transformer.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" @@ -455,7 +457,9 @@ namespace storm { } STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - + + // TODO: Shift this to after preprocessing? + if (model) { auto preprocessingResult = storm::pars::preprocessModel(model, input); if (preprocessingResult.second) { @@ -463,7 +467,40 @@ namespace storm { model->printModelInformationToStream(std::cout); } } - + + + if (parSettings.isMonotonicityAnalysisSet()) { + // Do something more fancy. + std::cout << "Hello, Jip" << std::endl; + std::shared_ptr> sparseModel = model->as>(); + + storm::storage::SparseMatrix matrix = sparseModel.get()->getTransitionMatrix(); + + storm::storage::BitVector initialStates = sparseModel.get()->getInitialStates(); + + 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); + return; + } + + + std::vector> regions = parseRegions(model); std::string samplesAsString = parSettings.getSamples(); SampleInformation samples; diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp new file mode 100644 index 000000000..c5c13f825 --- /dev/null +++ b/src/storm-pars/analysis/Lattice.cpp @@ -0,0 +1,171 @@ +// +// Created by Jip Spel on 24.07.18. +// + +#include +#include "Lattice.h" +namespace storm { + namespace analysis { + Lattice::Lattice(Node *topNode, Node *bottomNode, uint_fast64_t numberOfStates) { + Node *top = new Node(); + top->states = topNode->states; + Node *bottom = new Node(); + bottom->states = bottomNode->states; + top->below.push_back(bottom); + bottom->above.push_back(top); + nodes = std::vector({top, bottom}); +// addedStates.insert(addedStates.end(), top->states.begin(), top->states.end()); +// addedStates.insert(addedStates.end(), bottom->states.begin(), bottom->states.end()); + this->numberOfStates = numberOfStates; + } + + void Lattice::addBetween(uint_fast64_t state, Node *above, Node *below) { + Node *newNode = new Node(); + newNode->states = storm::storage::BitVector(numberOfStates); + newNode->states.set(state); + newNode->above = std::vector({above}); + newNode->below = std::vector({below}); + remove(&(below->above), above); + remove(&(above->below), below); + (below->above).push_back(newNode); + above->below.push_back(newNode); + nodes.push_back(newNode); +// addedStates.push_back(state); + } + + void Lattice::addToNode(uint_fast64_t state, Node *node) { + node->states.set(state); +// addedStates.push_back(state); + } + + int Lattice::compare(uint_fast64_t state1, uint_fast64_t state2) { + Node *node1 = getNode(state1); + Node *node2 = getNode(state2); + + if (node1 == node2) { + return 0; + } + + if (above(node1, node2)) { + return 1; + } + + if (below(node1, node2)) { + return 2; + } + + return -1; + } + + Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { + Node *node; + for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { + storm::storage::BitVector states = (*itr)->states; + + if (states[stateNumber]) return (*itr); + } + return node; + } + + void Lattice::toString(std::ostream &out) { + for (auto itr = nodes.begin(); itr != nodes.end(); ++itr) { + Node *node = *itr; + out << "Node: {"; + uint_fast64_t index = node->states.getNextSetIndex(0); + while (index < numberOfStates) { + out << index; + index = node->states.getNextSetIndex(index+1); + if (index < numberOfStates) { + out << ", "; + } + } + out << "}" << std::endl; + out << " Address: " << node << std::endl; + out << " Above: {"; + for (auto itr2 = node->above.begin(); itr2 != node->above.end(); ++itr2) { + Node *above = *itr2; + out << "{"; + index = above->states.getNextSetIndex(0); + while (index < numberOfStates) { + out << index; + index = above->states.getNextSetIndex(index+1); + if (index < numberOfStates) { + out << ", "; + } + } + + out << "}"; + if (itr2 + 1 != node->above.end()) { + out << ", "; + } + } + out << "}" << std::endl; + + out << " Below: {"; + for (auto itr2 = node->below.begin(); itr2 != node->below.end(); ++itr2) { + Node *below = *itr2; + out << "{"; + index = below->states.getNextSetIndex(0); + while (index < numberOfStates) { + out << index; + index = below->states.getNextSetIndex(index+1); + if (index < numberOfStates) { + out << ", "; + } + } + + out << "}"; + if (itr2 + 1 != node->below.end()) { + out << ", "; + } + } + out << "}" << std::endl; + } + } + + bool Lattice::above(Node *node1, Node *node2) { + if (node1->below.empty()) { + return false; + } + + if (std::find(node1->below.begin(), node1->below.end(), node2) != node1->below.end()) { + return true; + } + + bool result = false; + for (auto itr = node1->below.begin(); node1->below.end() != itr; ++itr) { + result |= above(*itr, node2); + } + return result; + } + + bool Lattice::below(Node *node1, Node *node2) { + if (node1->above.empty()) { + return false; + } + + if (std::find(node1->above.begin(), node1->above.end(), node2) != node1->above.end()) { + return true; + } + + bool result = false; + for (auto itr = node1->above.begin(); node1->above.end() != itr; ++itr) { + result |= below(*itr, node2); + } + return result; + } + + void Lattice::remove(std::vector *nodes, Node *node) { + auto index = std::find(nodes->begin(), nodes->end(), node); + if (index != nodes->end()) { + nodes->erase(index); + } + }; + + void Lattice::setStates(std::vector states, Node *node) { + for (auto itr = states.begin(); itr < states.end(); ++itr) { + node->states.set(*itr); + } + } + } +} diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h new file mode 100644 index 000000000..e80ab7035 --- /dev/null +++ b/src/storm-pars/analysis/Lattice.h @@ -0,0 +1,94 @@ +// +// Created by Jip Spel on 24.07.18. +// + +#ifndef LATTICE_LATTICE_H +#define LATTICE_LATTICE_H + +#include +#include + +#include "storm/storage/BitVector.h" + +namespace storm { + namespace analysis { + class Lattice { + + public: + struct Node { + storm::storage::BitVector states; + std::vector above; + std::vector below; + }; + + /*! + * Constructs a lattice with the given top node and bottom node. + * + * @param topNode The top node of the resulting lattice. + * @param bottomNode The bottom node of the resulting lattice. + */ + Lattice(Node *topNode, Node *bottomNode, uint_fast64_t numberOfStates); + + /*! + * 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. + */ + 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. + */ + void addToNode(uint_fast64_t state, Node *node); + + /*! + * 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. + * @param state1 The first state. + * @param state2 The second state. + * @return 0 if the nodes are on the same level; + * 1 if the node of the first state is closer to top then the node of the second state; + * 2 if the node of the second state is closer to top then the node of the first state; + * -1 if it is unclear from the structure of the lattice how the nodes relate. + */ + int compare(uint_fast64_t state1, uint_fast64_t state2); + + /*! + * Retrieves the pointer to a Node at which the state occurs. + * Behaviour unknown when state does not exists at any Node in the Lattice. + * + * @param state The number of the state. + * + * @return The pointer to the node of the state. + */ + Node *getNode(uint_fast64_t state); + + /*! + * Prints a string representation of the lattice to std::cout. + * + * @param out The stream to output to. + */ + void toString(std::ostream &out); + +// std::vector addedStates; + + private: + std::vector nodes; + + uint_fast64_t numberOfStates; + + bool above(Node *, Node *); + + bool below(Node *, Node *); + + void remove(std::vector *nodes, Node *node); + + void setStates(std::vector states, Node *node); + + }; + } +} +#endif //LATTICE_LATTICE_H diff --git a/src/storm-pars/analysis/Transformer.cpp b/src/storm-pars/analysis/Transformer.cpp new file mode 100644 index 000000000..a87a8d19e --- /dev/null +++ b/src/storm-pars/analysis/Transformer.cpp @@ -0,0 +1,249 @@ +// +// Created by Jip Spel on 26.07.18. +// + +#include "Transformer.h" +namespace storm { + namespace analysis { + Lattice *Transformer::toLattice(storm::storage::SparseMatrix matrix, + storm::storage::BitVector const &initialStates, + storm::storage::BitVector topStates, + storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates) { + // 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. + 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); + + 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]) { + + // Check if the current state number has not been added, but its successors have been added. + if (currentState->successor1 == currentState->successor2) { + // If there is only one successor, the state should be added to the same Node as its successor + lattice->addToNode(currentState->stateNumber, lattice->getNode(currentState->successor1)); + // Add stateNumber to the set with seen states. + seenStates.set(currentState->stateNumber); + } else { + // 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) { + //TODO dit in een aparte methode doen + Lattice::Node *above = lattice->getNode(successor1); + Lattice::Node *below = lattice->getNode(successor2); + std::vector states1 = above->below; + std::vector states2 = below->above; + bool added = false; + for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) { + for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) { + if ((*itr1)->states == (*itr2)->states) { + storm::RationalFunction prob1 = getProbability(currentState->stateNumber, successor1, matrix); + storm::RationalFunction prob2 = getProbability(currentState->stateNumber, successor2, matrix); + if (prob1 != storm::RationalFunction(1) + && 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; + } + } + + } + } + + if (!added) { + // 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) { + //TODO dit in een aparte methode doen + // als er in de below van successor 2 en de above van succesor 1 een overlap is met een state, dan moet je kijken naar de kans + Lattice::Node *above = lattice->getNode(successor2); + Lattice::Node *below = lattice->getNode(successor1); + std::vector states1 = above->below; + std::vector states2 = below->above; + bool added = false; + for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) { + for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) { + if ((*itr1)->states == (*itr2)->states) { + storm::RationalFunction prob1 = getProbability(currentState->stateNumber, successor2, matrix); + storm::RationalFunction prob2 = getProbability(currentState->stateNumber, successor1, matrix); + if (prob1 != storm::RationalFunction(1) + && prob2 != storm::RationalFunction(1) + && 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; + } + } + } + } + + if (!added) { + // 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: what to do? + STORM_LOG_DEBUG("Failed to add" << currentState->stateNumber << "\n"); + } + + } + } + } + + } + + return lattice; + } + + std::vector + Transformer::toStateVector(storm::storage::SparseMatrix transitionMatrix, + storm::storage::BitVector const &initialStates) { + std::vector < State *> states = std::vector({}); + std::vector stack(initialStates.begin(), initialStates.end()); + std::vector seenStates(initialStates.begin(), initialStates.end()); + uint_fast64_t currentState; + + while (!stack.empty()) { + currentState = stack.back(); + stack.pop_back(); + std::vector successorStates(0, 2); + + // Assume there are at most 2 successors + for (auto const &successor : transitionMatrix.getRowGroup(currentState)) { + if (!storm::utility::isZero(successor.getValue())) { + // Only explore the state if the transition was actually there. + uint_fast64_t successorNumber = successor.getColumn(); + if (std::find(seenStates.begin(), seenStates.end(), successorNumber) == seenStates.end()) { + stack.push_back(successorNumber); + seenStates.push_back(successorNumber); + } + successorStates.push_back(successorNumber); + } + } + + State *state = new State(); + state->stateNumber = currentState; + state->successor1 = successorStates.back(); + successorStates.pop_back(); + if (!successorStates.empty()) { + state->successor2 = successorStates.back(); + successorStates.pop_back(); + } else { + state->successor2 = state->successor1; + } + states.push_back(state); + } + return states; + } + + void Transformer::print(storm::storage::BitVector vector, std::string message) { + uint_fast64_t index = vector.getNextSetIndex(0); + std::cout << message <<": {"; + while (index < vector.size()) { + std::cout << index; + index = vector.getNextSetIndex(index+1); + if (index < vector.size()) { + std::cout << ", "; + } + } + std::cout << "}" << std::endl; + } + + std::vector Transformer::getNumbers(storm::storage::BitVector vector) { + std::vector result = std::vector({}); + uint_fast64_t index = vector.getNextSetIndex(0); + while (index < vector.size()) { + result.push_back(index); + index = vector.getNextSetIndex(index+1); + + } + return result; + } + + storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix) { + std::vector successorNumbers = getNumbers(successor); + storm::RationalFunction result = storm::RationalFunction(1); + for (auto itr = successorNumbers.begin(); itr < successorNumbers.end() && result == storm::RationalFunction(1); ++itr) { + result = getProbability(state, (*itr), matrix); + } + return result; + } + + storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix matrix) { + std::vector stateNumbers = getNumbers(state); + storm::RationalFunction result = storm::RationalFunction(1); + for (auto itr = stateNumbers.begin(); itr < stateNumbers.end() && result == storm::RationalFunction(1); ++itr) { + result = getProbability((*itr), successor, matrix); + } + return result; + } + + storm::RationalFunction Transformer::getProbability(uint_fast64_t state, uint_fast64_t successor, storm::storage::SparseMatrix matrix) { + storm::RationalFunction result = storm::RationalFunction(1); + // Iterate over all row groups. + auto row = matrix.getRow(state); + + 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; + } + + } + + return result; + } + } +} diff --git a/src/storm-pars/analysis/Transformer.h b/src/storm-pars/analysis/Transformer.h new file mode 100644 index 000000000..d584227f2 --- /dev/null +++ b/src/storm-pars/analysis/Transformer.h @@ -0,0 +1,55 @@ +// +// Created by Jip Spel on 26.07.18. +// + +#ifndef LATTICE_BUILDER_H +#define LATTICE_BUILDER_H + +#include "storm/storage/BitVector.h" +#include "storm/storage/SparseMatrix.h" +#include "Lattice.h" +namespace storm { + namespace analysis { + class Transformer { + public: + struct State { + uint_fast64_t stateNumber; + uint_fast64_t successor1; + uint_fast64_t successor2; + }; + + /*! + * Returns the pointer to the Lattice constructed from the given transitionMatrix, + * BitVector of initialStates, vector with the top states and vector with the bottom states. + * Assumes that every state has at least one and at most two outgoing transitions. + * + * @param matrix The transition matrix. + * @param initialStates The BitVector containing the initialStates. + * @param topStates Vector containing the numbers of the top states. + * @param bottomStates Vector containing the numbers of the bottom states. + * + * @return The lattice ordering of the states. + */ + static Lattice *toLattice(storm::storage::SparseMatrix matrix, + storm::storage::BitVector const &initialStates, + storm::storage::BitVector topStates, + storm::storage::BitVector bottomStates, uint_fast64_t numberOfStates); + + private: + static std::vector + toStateVector(storm::storage::SparseMatrix transitionMatrix, + storm::storage::BitVector const &initialStates); + + static void print(storm::storage::BitVector vector, std::string message); + + static std::vector getNumbers(storm::storage::BitVector vector); + + static storm::RationalFunction getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix); + + static storm::RationalFunction getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix matrix); + + static storm::RationalFunction getProbability(uint_fast64_t state, uint_fast64_t successor, storm::storage::SparseMatrix matrix); + }; + } +} +#endif //LATTICE_BUILDER_H diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index 7ecbd6166..ef64acb94 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -65,7 +65,11 @@ namespace storm { bool ParametricSettings::isSampleExactSet() const { return this->getOption(sampleExactOptionName).getHasOptionBeenSet(); } - + + bool ParametricSettings::isMonotonicityAnalysisSet() const { + // TODO: Make this dependent on the input. + return true; + } } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 1f10a4b35..0fa167409 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -63,6 +63,8 @@ namespace storm { * Retrieves whether samples are to be computed exactly. */ bool isSampleExactSet() const; + + bool isMonotonicityAnalysisSet() const; const static std::string moduleName;