From 2dae5862c882a39e7c49730c9b09edc47c5b57cc Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 30 Jan 2015 23:26:29 +0100 Subject: [PATCH] Small fix to bisimulation options. Former-commit-id: 555c5ef697fb7ae638d472a4787175cbbe17d756 --- .../DeterministicModelBisimulationDecomposition.cpp | 8 ++++---- .../DeterministicModelBisimulationDecomposition.h | 12 +++++------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 6c8641211..08c11a2f2 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -615,7 +615,7 @@ namespace storm { } for (auto const& expressionFormula : atomicExpressionFormulas) { std::stringstream stream; - stream << expressionFormula; + stream << *expressionFormula; labelsToRespect.insert(stream.str()); } respectedAtomicPropositions = labelsToRespect; @@ -722,7 +722,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) { // In order to create the quotient model, we need to construct // (a) the new transition matrix, // (b) the new labeling, @@ -733,7 +733,7 @@ namespace storm { // Prepare the new state labeling for (b). storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); - std::set atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions(); + std::set atomicPropositionsSet = selectedAtomicPropositions; atomicPropositionsSet.insert("init"); std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); for (auto const& ap : atomicPropositions) { @@ -839,7 +839,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 255e2c22a..eae63f442 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -413,8 +413,7 @@ namespace storm { * getQuotient(). * * @param model The model on whose state space to compute the coarses strong bisimulation relation. - * @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given, - * all atomic propositions are considered. + * @param atomicPropositions The set of atomic propositions that the bisimulation considers. * @param backwardTransitions The backward transitions of the model. * @param The initial partition. * @param bisimulationType The kind of bisimulation that is to be computed. @@ -422,7 +421,7 @@ namespace storm { * method. */ template - void partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient); + void partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient); /*! * Refines the partition based on the provided splitter. After calling this method all blocks are stable @@ -466,15 +465,14 @@ namespace storm { * * @param model The model whose state space was used for computing the equivalence classes. This is used for * determining the transitions of each equivalence class. - * @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The - * quotient will only have these atomic propositions. If not given, all atomic propositions will be - * considered. + * @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. + * The quotient will only have these atomic propositions. * @param partition The previously computed partition. This is used for quickly retrieving the block of a * state. * @param bisimulationType The kind of bisimulation that is to be computed. */ template - void buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards); + void buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards); /*! * Creates the measure-driven initial partition for reaching psi states from phi states.