Allow monotonicity analysis on both Until and Eventually formulas

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);

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;