Make cyclic part faster

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<storm::models::sparse::Model<ValueType>>();
@@ -617,16 +618,11 @@ namespace storm {
                 auto keptRows = matrix.getRowFilter(selectedStates);
                 storm::storage::SparseMatrix<ValueType> newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates);
                 // TODO: rewards get lost
-                // obtain the reward model for the resulting system
-//                std::unordered_map<std::string, RewardModelType> 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<storm::models::sparse::Dtmc<ValueType>>(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()) {

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,37 +327,22 @@ 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;
-                        storm::storage::BitVector successors = stateMap[stateNumber];
-
-                        // 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];
-                            }
+                    if (assumptionSeen) {
+                        statesToHandle = addedStates;
                     }
-
-                        if (check) {
-                            auto result = extendAllSuccAdded(lattice, stateNumber, successors);
-                            if (std::get<1>(result) != successors.size()) {
-                                return result;
-                            }
-                        } else {
+                    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);
 
-                            if (addedStates[stateNumber] && successors.getNumberOfSetBits() == 2
+                        assert (addedStates[stateNumber]);
+                        if (successors.getNumberOfSetBits() == 2
                             && ((addedStates[succ1] && !addedStates[succ2])
-                                        ||(!addedStates[succ1] && addedStates[succ2]))) {
+                                || (!addedStates[succ1] && addedStates[succ2]))) {
 
                             if (!addedStates[succ1]) {
                                 std::swap(succ1, succ2);
@@ -369,13 +356,41 @@ namespace storm {
                             } 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 {
+                            assert (successors.getNumberOfSetBits() == 2);
+                            statesToHandle.set(stateNumber, false);
+                            stateNumber = statesToHandle.getNextSetIndex(0);
                         }
                     }
 
+                    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];
+
+                        // 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);
                     }
                 }
             }

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<storm::expressions::BinaryRelationExpression> assumption);
 
             std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> extendAllSuccAdded(Lattice* lattice, uint_fast64_t stateNumber, storm::storage::BitVector successors);

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<carl::Variable, std::pair<bool, bool>>();
             if (model != nullptr) {
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();

src/storm-pars/analysis/MonotonicityChecker.h

@@ -72,8 +72,6 @@ namespace storm {
 
             bool validate;
 
-            bool sccElimination;
-
             std::map<carl::Variable, std::pair<bool, bool>> resultCheckOnSamples;
 
             storm::analysis::LatticeExtender<ValueType> *extender;