diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index 4135e4ded..f2f6c4fa8 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -38,8 +38,6 @@ namespace storm { template std::tuple LatticeExtender::toLattice(std::vector> formulas) { -// storm::utility::Stopwatch latticeWatch(true); - STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis"); STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula() @@ -71,7 +69,6 @@ namespace storm { auto initialMiddleStates = storm::storage::BitVector(numberOfStates); // Check if MC contains cycles - // TODO maybe move to other place? storm::storage::StronglyConnectedComponentDecompositionOptions const options; auto decomposition = storm::storage::StronglyConnectedComponentDecomposition(model->getTransitionMatrix(), options); acyclic = true; @@ -119,8 +116,6 @@ namespace storm { // Create the Lattice Lattice *lattice = new Lattice(&topStates, &bottomStates, &initialMiddleStates, numberOfStates); -// latticeWatch.stop(); -// STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl); return this->extendLattice(lattice); } @@ -325,11 +320,9 @@ namespace storm { } } else if (!acyclic) { - // TODO: kan dit niet efficienter auto addedStates = lattice->getAddedStates(); if (assumptionSeen) { statesToHandle = addedStates; - // TODO: statesSorted = } auto stateNumber = statesToHandle->getNextSetIndex(0); while (stateNumber != numberOfStates) { @@ -384,8 +377,6 @@ namespace storm { } } -// addedStates = lattice->getAddedStates(); -// auto notAddedStates = addedStates->operator~(); if (!assumptionSeen) { stateNumber = *(statesSorted.begin()); while (stateNumber != numberOfStates && (*(lattice->getAddedStates()))[stateNumber]) { @@ -393,20 +384,17 @@ namespace storm { stateNumber = *(statesSorted.begin()); } - if (stateNumber == numberOfStates) { - assert(false); - } - storm::storage::BitVector* successors = stateMap[stateNumber]; - - // Check if current state has not been added yet, and all successors have, ignore selfloop in this - successors->set(stateNumber, false); - if ((*successors & *addedStates) == *successors) { - auto result = extendAllSuccAdded(lattice, stateNumber, successors); - if (std::get<1>(result) != successors->size()) { - return result; - } - statesToHandle->set(stateNumber); + storm::storage::BitVector* successors = stateMap[stateNumber]; + + // Check if current state has not been added yet, and all successors have, ignore selfloop in this + successors->set(stateNumber, false); + if ((*successors & *addedStates) == *successors) { + auto result = extendAllSuccAdded(lattice, stateNumber, successors); + if (std::get<1>(result) != successors->size()) { + return result; } + statesToHandle->set(stateNumber); + } } else { addedStates = lattice->getAddedStates(); auto notAddedStates = addedStates->operator~(); @@ -445,6 +433,7 @@ namespace storm { lattice->setDoneBuilding(true); return std::make_tuple(lattice, numberOfStates, numberOfStates); } + template class LatticeExtender; } } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index 63f224792..7497aa594 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -1,7 +1,3 @@ -// -// Created by Jip Spel on 28.08.18. -// - #ifndef STORM_LATTICEEXTENDER_H #define STORM_LATTICEEXTENDER_H @@ -10,9 +6,6 @@ #include "storm-pars/analysis/Lattice.h" #include "storm/api/storm.h" - - - namespace storm { namespace analysis {