From f41b61fb7bfee76328c898b4003b727baf37e4b7 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Sat, 2 Feb 2019 14:31:18 +0100
Subject: [PATCH] Make cyclic part faster
---
src/storm-pars-cli/storm-pars.cpp | 12 +--
src/storm-pars/analysis/LatticeExtender.cpp | 93 +++++++++++--------
src/storm-pars/analysis/LatticeExtender.h | 2 +
.../analysis/MonotonicityChecker.cpp | 1 -
src/storm-pars/analysis/MonotonicityChecker.h | 2 -
5 files changed, 60 insertions(+), 50 deletions(-)
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<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()) {
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<storm::expressions::BinaryRelationExpression> assumption);
std::tuple<Lattice*, uint_fast64_t, uint_fast64_t> 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<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>>();
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<carl::Variable, std::pair<bool, bool>> resultCheckOnSamples;
storm::analysis::LatticeExtender<ValueType> *extender;