From 9bc402a20b46deb48ae5df5d418fc4b08278db1f Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 17 Aug 2018 10:04:37 +0200
Subject: [PATCH] Remove states with transition with probability 1 from model

---
 src/storm-pars-cli/storm-pars.cpp | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 11d6a98bb..f97c67c8b 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -1,4 +1,6 @@
 
+#include <storm-pars/transformer/SparseParametricModelSimplifier.h>
+#include <storm-pars/transformer/SparseParametricDtmcSimplifier.h>
 #include "storm-pars/api/storm-pars.h"
 #include "storm-pars/settings/ParsSettings.h"
 #include "storm-pars/settings/modules/ParametricSettings.h"
@@ -612,6 +614,7 @@ namespace storm {
             
             STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
 
+
             if (model) {
                 auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
                 if (preprocessingResult.second) {
@@ -624,9 +627,21 @@ namespace storm {
             if (parSettings.isMonotonicityAnalysisSet()) {
                 // Do something more fancy.
                 std::cout << "Hello, Jip" << std::endl;
+                auto testModel = (model->as<storm::models::sparse::Dtmc<ValueType>>());
+                // TODO: check if it is a Dtmc
+                auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(*testModel);
+
 
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
                 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 at the time supported");
+
+                if (!simplifier.simplify(*(formulas[0]))) {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
+                }
+
+
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = simplifier.getSimplifiedModel();//->as<storm::models::sparse::Model<ValueType>>();
+//                formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>({simplifier.getSimplifiedFormula()});//storm::api::extractFormulasFromProperties(input.properties);
 
                 STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula(), storm::exceptions::NotSupportedException, "Expecting until formula");
                 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*sparseModel);