From 285cde32aeabef3e8a90711b07409f9c4687dfe7 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Tue, 18 Sep 2018 14:40:18 +0200
Subject: [PATCH] Also give result when lattice does not contain all states

---
 src/storm-pars/analysis/AssumptionMaker.cpp | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/storm-pars/analysis/AssumptionMaker.cpp b/src/storm-pars/analysis/AssumptionMaker.cpp
index bc918b48c..9cef9ab3c 100644
--- a/src/storm-pars/analysis/AssumptionMaker.cpp
+++ b/src/storm-pars/analysis/AssumptionMaker.cpp
@@ -31,14 +31,19 @@ namespace storm {
                 storm::expressions::Variable var1 = expressionManager->getVariable(std::to_string(critical1));
                 storm::expressions::Variable var2 = expressionManager->getVariable(std::to_string(critical2));
 
-                auto latticeCopy = new Lattice(lattice);
                 std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions;
-                auto myMap = createAssumptions(var1, var2, latticeCopy, assumptions);
+                auto myMap = createAssumptions(var1, var2, new Lattice(lattice), assumptions);
                 result.insert(myMap.begin(), myMap.end());
 
                 std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>> assumptions2;
-                myMap = createAssumptions(var2, var1, lattice, assumptions2);
+                myMap = createAssumptions(var2, var1, new Lattice(lattice), assumptions2);
                 result.insert(myMap.begin(), myMap.end());
+                if (result.size() == 0) {
+                    // No assumptions could be made, all not valid based on sampling, therefore returning original lattice
+                    result.insert(std::pair<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>>(lattice, emptySet));
+                } else {
+                    delete lattice;
+                }
             }
             return result;
         }