From 88339f4cffa3bfddba7af34fdeb06a55ab4b45a9 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 22 Sep 2017 16:45:47 +0200
Subject: [PATCH] invoking new functionalities in the cli. Also silenced some
 debug output

---
 src/storm-pomdp-cli/storm-pomdp.cpp           | 39 ++++++++++++++++---
 .../GlobalPOMDPSelfLoopEliminator.cpp         |  6 +--
 2 files changed, 37 insertions(+), 8 deletions(-)

diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index c63f989a4..30ead921e 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -1,6 +1,5 @@
 
 
-#include <storm-pomdp/analysis/UniqueObservationStates.h>
 #include "storm/utility/initialize.h"
 
 #include "storm/settings/modules/GeneralSettings.h"
@@ -36,6 +35,9 @@
 
 #include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h"
 #include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h"
+#include "storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.h"
+#include "storm-pomdp/analysis/UniqueObservationStates.h"
+#include "storm-pomdp/analysis/QualitativeAnalysis.h"
 
 /*!
  * Initialize the settings manager.
@@ -101,14 +103,41 @@ int main(const int argc, const char** argv) {
         // We should not export here if we are going to do some processing first.
         auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(symbolicInput, engine);
         STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP.");
-        // CHECK if prop maximizes, only apply in those situations
         std::shared_ptr<storm::models::sparse::Pomdp<storm::RationalNumber>> pomdp = model->template as<storm::models::sparse::Pomdp<storm::RationalNumber>>();
-        storm::transformer::GlobalPOMDPSelfLoopEliminator<storm::RationalNumber> selfLoopEliminator(*pomdp);
-        pomdp = selfLoopEliminator.transform();
+        
+        std::shared_ptr<storm::logic::Formula const> formula;
+        if (!symbolicInput.properties.empty()) {
+            formula = symbolicInput.properties.front().getRawFormula();
+            STORM_PRINT_AND_LOG("Analyzing property '" << *formula << "'" << std::endl);
+            STORM_LOG_WARN_COND(symbolicInput.properties.size() == 1, "There is currently no support for multiple properties. All other properties will be ignored.");
+        }
+        
+        STORM_PRINT_AND_LOG("Analyzing states with unique observation ..." << std::endl);
         storm::analysis::UniqueObservationStates<storm::RationalNumber> uniqueAnalysis(*pomdp);
         std::cout << uniqueAnalysis.analyse() << std::endl;
 
-
+        // CHECK if prop maximizes, only apply in those situations
+        STORM_PRINT_AND_LOG("Eliminating self-loop choices ...");
+        uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
+        storm::transformer::GlobalPOMDPSelfLoopEliminator<storm::RationalNumber> selfLoopEliminator(*pomdp);
+        pomdp = selfLoopEliminator.transform();
+        STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl);
+
+        if (formula) {
+            if (formula->isProbabilityOperatorFormula()) {
+                storm::analysis::QualitativeAnalysis<storm::RationalNumber> qualitativeAnalysis(*pomdp);
+                STORM_PRINT_AND_LOG("Computing states with probability 0 ...");
+                std::cout << qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()) << std::endl;
+                STORM_PRINT_AND_LOG("Computing states with probability 1 ...");
+                std::cout << qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula()) << std::endl;
+            }
+            STORM_PRINT_AND_LOG("Eliminating mec choices ...");
+            // Todo elimination of mec choices only preserves memoryless schedulers. Selfloop elimination becomes redundant if we do mecChoiceElimination
+            oldChoiceCount = pomdp->getNumberOfChoices();
+            storm::transformer::GlobalPomdpMecChoiceEliminator<storm::RationalNumber> mecChoiceEliminator(*pomdp);
+            pomdp = mecChoiceEliminator.transform(*formula);
+            STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl);
+        }
 
         if (pomdpSettings.isExportToParametricSet()) {
             storm::transformer::ApplyFiniteSchedulerToPomdp<storm::RationalNumber> toPMCTransformer(*pomdp);
diff --git a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp
index dcc98f2d4..76107a7e4 100644
--- a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp
+++ b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp
@@ -57,7 +57,7 @@ namespace storm {
                     vec.set(0, false);
                 }
                 assert(!vec.full());
-                std::cout << "state " << state << " vec " << vec << std::endl;
+               // std::cout << "state " << state << " vec " << vec << std::endl;
                 for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
                     if (vec.get(action)) {
                         filter.set(offset + action);
@@ -65,12 +65,12 @@ namespace storm {
                 }
                 offset += pomdp.getNumberOfChoices(state);
             }
-            std::cout << "filter: " << filter << std::endl;
+           // std::cout << "filter: " << filter << std::endl;
             assert(filter.size() == pomdp.getNumberOfChoices());
             // TODO rewards with state-action rewards
             filter.complement();
 
-            std::cout << "selection: " << filter << std::endl;
+         //   std::cout << "selection: " << filter << std::endl;
 
             ChoiceSelector<ValueType> cs(pomdp);
             return cs.transform(filter)->template as<storm::models::sparse::Pomdp<ValueType>>();