From dc52e9b056eac7656468ab620091963f78023118 Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Fri, 7 Sep 2018 12:57:56 +0200 Subject: [PATCH] Create copy of lattice and assumptionslist at earlier point --- src/storm-pars/analysis/AssumptionMaker.cpp | 20 ++++++++------------ src/storm-pars/analysis/AssumptionMaker.h | 1 - src/storm-pars/analysis/Lattice.cpp | 1 - 3 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 0fadf2bfc..134e52097 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -13,15 +13,12 @@ namespace storm { this->expressionManager = std::make_shared(storm::expressions::ExpressionManager()); for (uint_fast64_t i = 0; i < this->numberOfStates; ++i) { expressionManager->declareIntegerVariable(std::to_string(i)); - expressionManager->declareFreshIntegerVariable(); } } - template std::map>> AssumptionMaker::startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2) { - std::map>> result; std::set> emptySet; @@ -32,7 +29,9 @@ namespace storm { storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); std::set> assumptions; - auto myMap = createAssumptions(var1, var2, lattice, assumptions); + auto latticeCopy = new Lattice(lattice); + std::set> assumptionsCopy = std::set>(assumptions); + auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); result.insert(myMap.begin(), myMap.end()); myMap = createAssumptions(var2, var1, lattice, assumptions); @@ -52,7 +51,9 @@ namespace storm { storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(std::get<1>(criticalPair))); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(std::get<2>(criticalPair))); - auto myMap = createAssumptions(var1, var2, lattice, assumptions); + auto latticeCopy = new Lattice(lattice); + std::set> assumptionsCopy = std::set>(assumptions); + auto myMap = createAssumptions(var1, var2, latticeCopy, assumptionsCopy); result.insert(myMap.begin(), myMap.end()); myMap = createAssumptions(var2, var1, lattice, assumptions); result.insert(myMap.begin(), myMap.end()); @@ -63,19 +64,14 @@ namespace storm { template std::map>> AssumptionMaker::createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice, std::set> assumptions) { - std::set> assumptions1 = std::set>(assumptions); std::shared_ptr assumption1 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(), var1.getExpression().getBaseExpressionPointer(), var2.getExpression().getBaseExpressionPointer(), storm::expressions::BinaryRelationExpression::RelationType::Greater)); - assumptions1.insert(assumption1); - auto lattice1 = new Lattice(lattice); - return (runRecursive(lattice1, assumptions1)); + assumptions.insert(assumption1); + return (runRecursive(lattice, assumptions)); } template class AssumptionMaker; } } - - -// Een map met daarin een pointer naar de lattic en een set met de geldende assumptions voor die lattice \ No newline at end of file diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 7061a43fb..2fa0a890c 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -19,7 +19,6 @@ namespace storm { std::map>> startMakingAssumptions(storm::analysis::Lattice* lattice, uint_fast64_t critical1, uint_fast64_t critical2); - private: std::map>> runRecursive(storm::analysis::Lattice* lattice, std::set> assumptions); diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp index 1846b816e..a7e5acfe5 100644 --- a/src/storm-pars/analysis/Lattice.cpp +++ b/src/storm-pars/analysis/Lattice.cpp @@ -139,7 +139,6 @@ namespace storm { return UNKNOWN; } - Lattice::Node *Lattice::getNode(uint_fast64_t stateNumber) { return nodes.at(stateNumber); }