From aa6e44a1e22a594d2ab92805c7078b2c30dab4e8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 14 Oct 2014 18:07:52 +0200
Subject: [PATCH] Some fixes after merge.

Former-commit-id: 5df69ca65586b07f993849a73ccd7ee5ef47850c
---
 src/models/AtomicPropositionsLabeling.h       | 13 -------
 ...icModelStrongBisimulationDecomposition.cpp |  1 +
 src/stormParametric.cpp                       | 10 ++++--
 src/utility/ConstantsComparator.h             | 34 +++++++++++++++++++
 4 files changed, 43 insertions(+), 15 deletions(-)

diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h
index 8959756a4..dfcc1db04 100644
--- a/src/models/AtomicPropositionsLabeling.h
+++ b/src/models/AtomicPropositionsLabeling.h
@@ -249,19 +249,6 @@ public:
         auto apIndexPair = nameToLabelingMap.find(ap);
 		return this->singleLabelings[apIndexPair->second].get(state);
 	}
-
-    /*!
-     * Retrieves the set of atomic propositions of the model.
-     *
-     * @return The set of atomic propositions of the model.
-     */
-    std::set<std::string> getAtomicPropositions() const {
-        std::set<std::string> result;
-        for (auto const& labeling : this->nameToLabelingMap) {
-            result.insert(labeling.first);
-        }
-        return result;
-    }
     
 	/*!
 	 * Returns the number of atomic propositions managed by this object (set in the initialization).
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index 93433d19f..92fb2a142 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -900,5 +900,6 @@ namespace storm {
         }
         
         template class DeterministicModelStrongBisimulationDecomposition<double>;
+//        template class DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction>;
     }
 }
\ No newline at end of file
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index d22c210bb..936a931fa 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -10,6 +10,7 @@
 #include "src/modelchecker/reachability/CollectConstraints.h"
 
 //#include "src/modelchecker/reachability/DirectEncoding.h"
+//#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
 #include "src/modelchecker/reachability/SparseSccModelChecker.h"
 #include "src/storage/parameters.h"
 /*!
@@ -34,8 +35,6 @@ int main(const int argc, const char** argv) {
         storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
         std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, constants);
         
-        
-        
         model->printModelInformationToStream(std::cout);
 
         // Program Translation Time Measurement, End
@@ -43,6 +42,13 @@ int main(const int argc, const char** argv) {
         std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
 
         std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::Dtmc<storm::RationalFunction>>();
+        
+        // Perform bisimulation minimization if requested.
+//        if (storm::settings::generalSettings().isBisimulationSet()) {
+//            storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true);
+//            dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
+//        }
+        
         assert(dtmc);
         storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> constraintCollector;
         constraintCollector(*dtmc);
diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h
index fc46b251f..4936216ca 100644
--- a/src/utility/ConstantsComparator.h
+++ b/src/utility/ConstantsComparator.h
@@ -78,6 +78,40 @@ namespace storm {
             double precision;
         };
         
+#ifdef PARAMETRIC_SYSTEMS
+        template<>
+        class ConstantsComparator<storm::RationalFunction> {
+        public:
+            bool isOne(storm::RationalFunction const& value) {
+                return value.isOne();
+            }
+            
+            bool isZero(storm::RationalFunction const& value) {
+                return value.isZero();
+            }
+            
+            bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) {
+                return value1 == value2;
+            }
+        };
+        
+        template<>
+        class ConstantsComparator<storm::Polynomial> {
+        public:
+            bool isOne(storm::Polynomial const& value) {
+                return value.isOne();
+            }
+            
+            bool isZero(storm::Polynomial const& value) {
+                return value.isZero();
+            }
+            
+            bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) {
+                return value1 == value2;
+            }
+        };
+#endif
+        
     }
 }