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 getAtomicPropositions() const { - std::set 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; +// template class DeterministicModelStrongBisimulationDecomposition; } } \ 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> model = storm::adapters::ExplicitModelAdapter::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(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; std::shared_ptr> dtmc = model->as>(); + + // Perform bisimulation minimization if requested. +// if (storm::settings::generalSettings().isBisimulationSet()) { +// storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); +// dtmc = bisimulationDecomposition.getQuotient()->as>(); +// } + assert(dtmc); storm::modelchecker::reachability::CollectConstraints 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 { + 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 { + 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 + } }