From 1aa8f409cba718b0d71aa3f77f7938c4b93d2f40 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Tue, 21 Aug 2018 11:32:08 +0200
Subject: [PATCH] Change error messages + add new ones

---
 src/storm-pars-cli/storm-pars.cpp   | 7 ++++---
 src/storm-pars/analysis/Lattice.cpp | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 7dbeb0e6c..8ac1cac18 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -523,6 +523,8 @@ namespace storm {
                 storm::storage::BitVector topStates = statesWithProbability01.second;
                 storm::storage::BitVector bottomStates = statesWithProbability01.first;
 
+                STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states");
+                STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states");
                 // Transform to Lattice
                 storm::storage::SparseMatrix<ValueType> matrix = sparseModel.get()->getTransitionMatrix();
                 storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice<ValueType>(matrix, topStates, bottomStates);
@@ -540,16 +542,15 @@ namespace storm {
                     // go over all rows
                     auto row = matrix.getRow(i);
 
-
                     auto first = (*row.begin());
                     if (first.getValue() != ValueType(1)) {
-                        auto second = (* (row.begin() + 1));
+                        auto second = (*(++row.begin()));
 
                         auto val = first.getValue();
                         auto vars = val.gatherVariables();
                         for (auto itr = vars.begin(); itr != vars.end(); ++itr) {
                             auto derivative = val.derivative(*itr);
-                            STORM_LOG_THROW(derivative.isConstant(), storm::exceptions::NotSupportedException, "Expecting probability to have at most degree 1");
+                            STORM_LOG_THROW(derivative.isConstant(), storm::exceptions::NotSupportedException, "Expecting derivative to be constant");
 
                             if (varsMonotone.find(*itr) == varsMonotone.end()) {
                                 varsMonotone[*itr].first = true;
diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp
index 3f0f8da3f..038b18e4f 100644
--- a/src/storm-pars/analysis/Lattice.cpp
+++ b/src/storm-pars/analysis/Lattice.cpp
@@ -34,8 +34,8 @@ namespace storm {
             newNode->states.set(state);
             newNode->above = std::vector<Node *>({above});
             newNode->below = std::vector<Node *>({below});
-            remove(&(below->above), above);
-            remove(&(above->below), below);
+//            remove(&(below->above), above);
+//            remove(&(above->below), below);
             (below->above).push_back(newNode);
             above->below.push_back(newNode);
             nodes.at(state) = newNode;