diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 957f48c7e..4c33bde22 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -563,6 +563,7 @@ namespace storm { } if (parSettings.isSccEliminationSet()) { + storm::utility::Stopwatch eliminationWatch(true); // TODO: check for correct Model type STORM_PRINT("Applying scc elimination" << std::endl); auto sparseModel = model->as>(); @@ -617,16 +618,11 @@ namespace storm { auto keptRows = matrix.getRowFilter(selectedStates); storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); // TODO: rewards get lost - // obtain the reward model for the resulting system -// std::unordered_map rewardModels; -// if(rewardModelName) { -// storm::utility::vector::filterVectorInPlace(actionRewards, keptRows); -// rewardModels.insert(std::make_pair(*rewardModelName, RewardModelType(boost::none, std::move(actionRewards)))); -// } model = std::make_shared>(std::move(newTransitionMatrix), sparseModel->getStateLabeling().getSubLabeling(selectedStates)); - - STORM_PRINT("SCC Elimination applied" << std::endl); + eliminationWatch.stop(); + STORM_PRINT(std::endl << "Time for scc elimination: " << eliminationWatch << "." << std::endl << std::endl); + model->printModelInformationToStream(std::cout); } if (parSettings.isMonotonicityAnalysisSet()) { diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp index f046c3d0a..4d3d8df7f 100644 --- a/src/storm-pars/analysis/LatticeExtender.cpp +++ b/src/storm-pars/analysis/LatticeExtender.cpp @@ -112,6 +112,8 @@ namespace storm { } } + statesToHandle = initialMiddleStates; + // Create the Lattice Lattice *lattice = new Lattice(topStates, bottomStates, initialMiddleStates, numberOfStates); @@ -325,57 +327,70 @@ namespace storm { } else if (!acyclic) { // TODO: kan dit niet efficienter - for (auto stateNumber = 0; stateNumber < numberOfStates; stateNumber++) { - auto addedStates = lattice->getAddedStates(); - - // Iterate over all states -// auto stateNumber = i; + auto addedStates = lattice->getAddedStates(); + if (assumptionSeen) { + statesToHandle = addedStates; + } + auto stateNumber = statesToHandle.getNextSetIndex(0); + while (stateNumber != numberOfStates) { + addedStates = lattice->getAddedStates(); storm::storage::BitVector successors = stateMap[stateNumber]; + // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet + auto succ1 = successors.getNextSetIndex(0); + auto succ2 = successors.getNextSetIndex(succ1 + 1); - // Check if current state has not been added yet, and all successors have - bool check = !addedStates[stateNumber]; - for (auto succIndex = successors.getNextSetIndex(0); - check && succIndex != successors.size(); succIndex = successors.getNextSetIndex( - ++succIndex)) { - // if the stateNumber equals succIndex we have a self-loop, ignoring selfloop as seenStates[stateNumber] = false - if (succIndex != stateNumber) { - check &= addedStates[succIndex]; + assert (addedStates[stateNumber]); + if (successors.getNumberOfSetBits() == 2 + && ((addedStates[succ1] && !addedStates[succ2]) + || (!addedStates[succ1] && addedStates[succ2]))) { + + if (!addedStates[succ1]) { + std::swap(succ1, succ2); } - } - if (check) { - auto result = extendAllSuccAdded(lattice, stateNumber, successors); - if (std::get<1>(result) != successors.size()) { - return result; + auto compare = lattice->compare(stateNumber, succ1); + if (compare == Lattice::ABOVE) { + lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); + } else if (compare == Lattice::BELOW) { + lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); + } else { + assert(false); } + statesToHandle.set(succ2); + statesToHandle.set(stateNumber, false); + stateNumber = statesToHandle.getNextSetIndex(0); + } else if (!((addedStates[succ1] && !addedStates[succ2]) + || (!addedStates[succ1] && addedStates[succ2]))) { + stateNumber = statesToHandle.getNextSetIndex(stateNumber + 1); } else { - // Checking for states which are already added to the lattice, and only have one successor left which haven't been added yet - auto succ1 = successors.getNextSetIndex(0); - auto succ2 = successors.getNextSetIndex(succ1 + 1); - - if (addedStates[stateNumber] && successors.getNumberOfSetBits() == 2 - && ((addedStates[succ1] && !addedStates[succ2]) - ||(!addedStates[succ1] && addedStates[succ2]))) { + assert (successors.getNumberOfSetBits() == 2); + statesToHandle.set(stateNumber, false); + stateNumber = statesToHandle.getNextSetIndex(0); + } + } - if (!addedStates[succ1]) { - std::swap(succ1, succ2); - } + addedStates = lattice->getAddedStates(); + for (auto stateNumber = addedStates.getNextUnsetIndex(0); stateNumber < numberOfStates; stateNumber = addedStates.getNextUnsetIndex(stateNumber + 1)) { + // Iterate over all not yet added states + storm::storage::BitVector successors = stateMap[stateNumber]; - auto compare = lattice->compare(stateNumber, succ1); - if (compare == Lattice::ABOVE) { - lattice->addBetween(succ2, lattice->getTop(), lattice->getNode(stateNumber)); - } else if (compare == Lattice::BELOW) { - lattice->addBetween(succ2, lattice->getNode(stateNumber), lattice->getBottom()); - } else { - assert(false); - } + // 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); } - } - // if nothing changed, then add a state between top and bottom + + + // if nothing changed and there are states left, then add a state between top and bottom if (oldNumberSet == lattice->getAddedStates().getNumberOfSetBits() && oldNumberSet != numberOfStates) { - lattice->add(lattice->getAddedStates().getNextUnsetIndex(0)); + auto stateNumber = lattice->getAddedStates().getNextUnsetIndex(0); + lattice->add(stateNumber); + statesToHandle.set(stateNumber); } } } diff --git a/src/storm-pars/analysis/LatticeExtender.h b/src/storm-pars/analysis/LatticeExtender.h index af848b094..0d4787f00 100644 --- a/src/storm-pars/analysis/LatticeExtender.h +++ b/src/storm-pars/analysis/LatticeExtender.h @@ -60,6 +60,8 @@ namespace storm { bool assumptionSeen; + storm::storage::BitVector statesToHandle; + void handleAssumption(Lattice* lattice, std::shared_ptr assumption); std::tuple extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors); diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp index 5018fb9e8..26b23673e 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.cpp +++ b/src/storm-pars/analysis/MonotonicityChecker.cpp @@ -35,7 +35,6 @@ namespace storm { this->model = model; this->formulas = formulas; this->validate = validate; - this->sccElimination = sccElimination; this->resultCheckOnSamples = std::map>(); if (model != nullptr) { std::shared_ptr> sparseModel = model->as>(); diff --git a/src/storm-pars/analysis/MonotonicityChecker.h b/src/storm-pars/analysis/MonotonicityChecker.h index d8f6a94d0..b4b6db84c 100644 --- a/src/storm-pars/analysis/MonotonicityChecker.h +++ b/src/storm-pars/analysis/MonotonicityChecker.h @@ -72,8 +72,6 @@ namespace storm { bool validate; - bool sccElimination; - std::map> resultCheckOnSamples; storm::analysis::LatticeExtender *extender;