diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp index 0117a655f..0fadf2bfc 100644 --- a/src/storm-pars/analysis/AssumptionMaker.cpp +++ b/src/storm-pars/analysis/AssumptionMaker.cpp @@ -28,30 +28,15 @@ namespace storm { if (critical1 == numberOfStates || critical2 == numberOfStates) { result.insert(std::pair>>(lattice, emptySet)); } else { - - //TODO: opruimen storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1)); storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2)); - std::set> assumptions1; - 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); - auto myMap = (runRecursive(lattice1, assumptions1)); - result.insert(myMap.begin(), myMap.end()); + std::set> assumptions; - std::set> assumptions2; - std::shared_ptr assumption2 - = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, var2.getType(), - var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Greater)); - assumptions2.insert(assumption2); + auto myMap = createAssumptions(var1, var2, lattice, assumptions); + result.insert(myMap.begin(), myMap.end()); - auto lattice2 = new Lattice(lattice); - auto myMap2 = (runRecursive(lattice2, assumptions2)); - result.insert(myMap2.begin(), myMap2.end()); + myMap = createAssumptions(var2, var1, lattice, assumptions); + result.insert(myMap.begin(), myMap.end()); } return result; } @@ -67,29 +52,26 @@ 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))); - 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); - auto myMap = (runRecursive(lattice1, assumptions1)); + auto myMap = createAssumptions(var1, var2, lattice, assumptions); result.insert(myMap.begin(), myMap.end()); - - - std::set> assumptions2 = assumptions; - std::shared_ptr assumption2 = std::make_shared(storm::expressions::BinaryRelationExpression(*expressionManager, var1.getType(), - var2.getExpression().getBaseExpressionPointer(), var1.getExpression().getBaseExpressionPointer(), - storm::expressions::BinaryRelationExpression::RelationType::Greater)) ; - assumptions2.insert(assumption2); - auto lattice2 = new Lattice(lattice); - myMap = (runRecursive(lattice2, assumptions2)); + myMap = createAssumptions(var2, var1, lattice, assumptions); result.insert(myMap.begin(), myMap.end()); } return result; } + 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)); + } template class AssumptionMaker; } diff --git a/src/storm-pars/analysis/AssumptionMaker.h b/src/storm-pars/analysis/AssumptionMaker.h index 0472d2fbc..7061a43fb 100644 --- a/src/storm-pars/analysis/AssumptionMaker.h +++ b/src/storm-pars/analysis/AssumptionMaker.h @@ -23,6 +23,8 @@ namespace storm { private: std::map>> runRecursive(storm::analysis::Lattice* lattice, std::set> assumptions); + std::map>> createAssumptions(storm::expressions::Variable var1, storm::expressions::Variable var2, storm::analysis::Lattice* lattice,std::set> assumptions); + storm::analysis::LatticeExtender* latticeExtender; std::shared_ptr expressionManager;