From 67862b0a8d6633837602d22276b437edb4562417 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Mon, 1 Oct 2018 14:05:56 +0200 Subject: [PATCH] First implementation for cyclic parts in model --- src/storm-pars-cli/storm-pars.cpp | 8 ---- src/storm-pars/analysis/AssumptionMaker.cpp | 2 + src/storm-pars/analysis/LatticeExtender.cpp | 47 ++++++++++++++++----- src/storm-pars/analysis/LatticeExtender.h | 2 + 4 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index c44989300..ed4e645d3 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -531,14 +531,6 @@ namespace storm { std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); std::shared_ptr> sparseModel = model->as>(); - // Check if MC is acyclic - auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(sparseModel->getTransitionMatrix(), false, false); - for (auto i = 0; i < decomposition.size(); ++i) { - auto scc = decomposition.getBlock(i); - STORM_LOG_THROW(scc.size() <= 1, storm::exceptions::NotSupportedException, "Cycle found, not supporting cyclic MCs"); - } - - // Transform to Lattices storm::utility::Stopwatch latticeWatch(true); storm::analysis::LatticeExtender *extender = new storm::analysis::LatticeExtender(sparseModel); diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 9cef9ab3c..280183184 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -65,7 +65,9 @@ namespace storm { auto val2 = std::get<2>(criticalTriple); storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(val1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(val2)); + // TODO: check of in lattice de relatie niet al andersom bestaat + assert(lattice->compare(val1, val2) == storm::analysis::Lattice::UNKNOWN); auto latticeCopy = new Lattice(lattice); std::vector> assumptionsCopy = std::vector>( assumptions); diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index b4be618ed..a26713fa7 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -17,6 +17,8 @@ #include "storm/exceptions/NotSupportedException.h" #include +#include +#include #include "storm/storage/BitVector.h" #include "storm/utility/macros.h" @@ -25,8 +27,35 @@ namespace storm { namespace analysis { template - LatticeExtender::LatticeExtender(std::shared_ptr> model) : model(model) { - // intentionally left empty + LatticeExtender::LatticeExtender(std::shared_ptr> model) { + this->model = model; + + initialMiddleStates = storm::storage::BitVector(model->getNumberOfStates()); + // Check if MC is acyclic + auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), false, false); + for (auto i = 0; i < decomposition.size(); ++i) { + auto scc = decomposition.getBlock(i); + if (scc.size() > 1) { + auto states = scc.getStates(); + bool added = false; + for (auto itr = states.begin(); !added && itr != states.end(); ++itr) { + auto state = *itr; + storm::storage::BitVector subSystem = storm::storage::BitVector(model->getNumberOfStates()); + subSystem.set(states.begin(), states.end(), true); + subSystem.set(state, false); + auto subDecomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), subSystem, false, false); + bool acyclic = true; + for (auto i = 0; acyclic && i < subDecomposition.size(); ++i) { + auto subScc = subDecomposition.getBlock(i); + acyclic = subScc.size() <= 1; + } + if (acyclic) { + initialMiddleStates.set(state); + added = true; + } + } + } + } } template @@ -71,6 +100,9 @@ namespace storm { // Create the Lattice storm::analysis::Lattice *lattice = new storm::analysis::Lattice(topStates, bottomStates, numberOfStates); + for (auto state = initialMiddleStates.getNextSetIndex(0); state != numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) { + lattice->add(state); + } return this->extendLattice(lattice); } @@ -110,8 +142,9 @@ namespace storm { } } - auto oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); - while (lattice->getAddedStates().getNumberOfSetBits() != numberOfStates) { + auto oldNumberSet = numberOfStates; + while (oldNumberSet != lattice->getAddedStates().getNumberOfSetBits()) { + oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); for (auto stateItr = stateMap.begin(); stateItr != stateMap.end(); ++stateItr) { storm::storage::BitVector seenStates = (lattice->getAddedStates()); // Iterate over all states @@ -169,12 +202,6 @@ namespace storm { lattice->addBetween(stateNumber, lattice->getNode(highest), lattice->getNode(lowest)); } } - // Nothing changed and not done yet - if (oldNumberSet == lattice->getAddedStates().getNumberOfSetBits()) { - // add the first unset state to the lattice between top and bottom - lattice->add(lattice->getAddedStates().getNextUnsetIndex(0)); - } - oldNumberSet = lattice->getAddedStates().getNumberOfSetBits(); } return std::make_tuple(lattice, numberOfStates, numberOfStates); } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 48bb7123a..8737c8f9e 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -53,6 +53,8 @@ namespace storm { std::shared_ptr> model; std::map stateMap; + + storm::storage::BitVector initialMiddleStates; }; } }