diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 9a73ee0d5..470699988 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -4,7 +4,6 @@ #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" @@ -47,6 +46,12 @@ namespace storm { bool graphPreserving; bool exact; }; + + struct State { + uint_fast64_t stateNumber; + uint_fast64_t successor1; + uint_fast64_t successor2; + }; template std::vector> parseRegions(std::shared_ptr const& model) { @@ -429,13 +434,168 @@ namespace storm { storm::pars::verifyRegionsWithSparseEngine(model, input, regions); } } - + template void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); } - + + + template + ValueType getProbability(uint_fast64_t state, uint_fast64_t successor, storm::storage::SparseMatrix matrix) { + ValueType result = ValueType(1); + // Iterate over all row groups. + auto row = matrix.getRow(state); + + for (auto itr = row.begin(); itr < row.end() && result == ValueType(1); ++itr) { + if ((*itr).getColumn() == successor) { + result = (*itr).getValue(); + } + + } + + return result; + } + + template + ValueType getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix matrix) { + ValueType result = ValueType(1); + uint_fast64_t index = state.getNextSetIndex(0); + while (index < state.size() && result == ValueType(1)) { + result = getProbability(index, successor, matrix); + index = state.getNextSetIndex(index+1); + } + return result; + } + + template + ValueType getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix) { + ValueType result = ValueType(1); + uint_fast64_t index = successor.getNextSetIndex(0); + while (index < successor.size() && result == ValueType(1)) { + result = getProbability(state, index, matrix); + index = successor.getNextSetIndex(index+1); + } + return result; + } + + template + storm::analysis::Lattice* toLattice(std::shared_ptr> model, + storm::storage::BitVector topStates, + storm::storage::BitVector bottomStates) { + storm::storage::SparseMatrix 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 stateVector = std::vector({}); + 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); + for (auto itr = row.begin(); itr < row.end() && state->successor2 == numberOfStates; ++itr) { + if ((*itr).getValue() != ValueType(1)) { + if (state->successor1 == numberOfStates) { + state->successor1 = (*itr).getColumn(); + } else { + state->successor2 = (*itr).getColumn(); + } + } else { + state-> successor1 = (*itr).getColumn(); + state-> successor2 = (*itr).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]) { + + // 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 || compareResult == 2) { + + if (compareResult == 2) { + // swap + auto temp = successor1; + successor1 = successor2; + successor2 = temp; + } + // Additional check, if states have the same probability of reaching a given next state, + // then they should be at the same node + // TODO: can this be removed, e.g. adding a step to preprocessing, making this superfluous + storm::analysis::Lattice::Node *above = lattice->getNode(successor1); + storm::analysis::Lattice::Node *below = lattice->getNode(successor2); + std::vector states1 = above->below; + std::vector states2 = below->above; + for (auto itr1 = states1.begin(); itr1 < states1.end(); ++itr1) { + for (auto itr2 = states2.begin(); itr2 < states2.end(); ++itr2) { + if ((*itr1)->states == (*itr2)->states) { + ValueType prob1 = getProbability(currentState->stateNumber, successor1, matrix); + ValueType prob2 = getProbability(currentState->stateNumber, successor2, matrix); + if (prob1 != ValueType(1) + && prob2 != ValueType(1) + && getProbability((*itr1)->states, above->states, matrix) == prob1 + && getProbability((*itr1)->states, below->states, matrix) == prob2) { + lattice->addToNode(currentState->stateNumber, (*itr1)); + seenStates.set(currentState->stateNumber); + } + } + } + } + + if (!seenStates.get(currentState->stateNumber)) { + // 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 void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule(); @@ -458,8 +618,6 @@ 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) { @@ -472,24 +630,24 @@ namespace storm { 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::shared_ptr> sparseModel = model->as>(); 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"); 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); + // Get the maybeStates + std::pair statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates); 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()); + + // Transform to LatticeLattice + storm::analysis::Lattice* lattice = toLattice(sparseModel, topStates, bottomStates); + lattice->toString(std::cout); + std::cout << "Bye, Jip" << std::endl; // TODO: Analyse lattice with transition matrix // Where do the parameters occur? @@ -528,6 +686,8 @@ namespace storm { verifyParametricModel(model, input, regions, samples); } } + + void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) diff --git a/src/storm-pars/analysis/Transformer.cpp b/src/storm-pars/analysis/Transformer.cpp deleted file mode 100644 index 6bcae81a9..000000000 --- a/src/storm-pars/analysis/Transformer.cpp +++ /dev/null @@ -1,155 +0,0 @@ -// -// Created by Jip Spel on 26.07.18. -// -// TODO: Use templates -#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) { - // 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 = std::vector({}); - - 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); - for (auto itr = row.begin(); itr < row.end() && state->successor2 == numberOfStates; ++itr) { - if ((*itr).getValue() != storm::RationalFunction(1)) { - if (state->successor1 == numberOfStates) { - state->successor1 = (*itr).getColumn(); - } else { - state->successor2 = (*itr).getColumn(); - } - } else { - state-> successor1 = (*itr).getColumn(); - state-> successor2 = (*itr).getColumn(); - } - } - stateVector.push_back(state); - } - - // Start creating the Lattice - Lattice *lattice = new 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]) { - - // 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 || compareResult == 2) { - - if (compareResult == 2) { - // swap - auto temp = successor1; - successor1 = successor2; - successor2 = temp; - } - // Additional check, if states have the same probability of reaching a given next state, - // then they should be at the same node - Lattice::Node *above = lattice->getNode(successor1); - Lattice::Node *below = lattice->getNode(successor2); - std::vector states1 = above->below; - std::vector states2 = below->above; - 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) { - lattice->addToNode(currentState->stateNumber, (*itr1)); - seenStates.set(currentState->stateNumber); - } - } - } - } - - if (!seenStates.get(currentState->stateNumber)) { - // 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; - } - - storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, storm::storage::BitVector successor, storm::storage::SparseMatrix matrix) { - storm::RationalFunction result = storm::RationalFunction(1); - uint_fast64_t index = successor.getNextSetIndex(0); - while (index < successor.size() && result == storm::RationalFunction(1)) { - result = getProbability(state, index, matrix); - index = successor.getNextSetIndex(index+1); - } - return result; - } - - storm::RationalFunction Transformer::getProbability(storm::storage::BitVector state, uint_fast64_t successor, storm::storage::SparseMatrix matrix) { - storm::RationalFunction result = storm::RationalFunction(1); - uint_fast64_t index = state.getNextSetIndex(0); - while (index < state.size() && result == storm::RationalFunction(1)) { - result = getProbability(index, successor, matrix); - index = state.getNextSetIndex(index+1); - } - 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) { - result = (*itr).getValue(); - } - - } - - return result; - } - } -} diff --git a/src/storm-pars/analysis/Transformer.h b/src/storm-pars/analysis/Transformer.h deleted file mode 100644 index 1d3bf64a1..000000000 --- a/src/storm-pars/analysis/Transformer.h +++ /dev/null @@ -1,49 +0,0 @@ -// -// Created by Jip Spel on 26.07.18. -// - -#ifndef LATTICE_BUILDER_H -#define LATTICE_BUILDER_H - -#include -#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 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