Some fixes after merge.

Former-commit-id: 5df69ca655

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

src/storage/DeterministicModelStrongBisimulationDecomposition.cpp

@@ -900,5 +900,6 @@ namespace storm {
         }
         
         template class DeterministicModelStrongBisimulationDecomposition<double>;
+//        template class DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction>;
     }
 }

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

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
+        
     }
 }