From 92bd07c9c5c9fc3b2d7d618bbfe2ba30ec566461 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Tue, 21 Aug 2018 13:21:21 +0200
Subject: [PATCH] Allow monotonicity analysis on both Until and Eventually
 formulas

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

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 8ac1cac18..7437f10ea 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -510,13 +510,22 @@ namespace storm {
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
 
                 STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
-                STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula(), storm::exceptions::NotSupportedException, "Expecting until formula");
+                STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
+                                && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
+                                        || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula");
 
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
                 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*sparseModel);
 
-                storm::storage::BitVector phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
-                storm::storage::BitVector psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); //right
+                storm::storage::BitVector phiStates;
+                storm::storage::BitVector psiStates;
+                if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
+                    phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
+                    psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
+                } else {
+                    phiStates = storm::storage::BitVector(sparseModel.get()->getNumberOfStates(), true);
+                    psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
+                }
 
                 // Get the maybeStates
                 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates);
diff --git a/src/storm-pars/analysis/Lattice.cpp b/src/storm-pars/analysis/Lattice.cpp
index 038b18e4f..3f0f8da3f 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;