SplitterBasedRefinement.cpp File Reference

#include "storm/transformer/bisimulation/SplitterBasedRefinement.h"
#include <algorithm>
#include <cstdint>
#include <deque>
#include <limits>
#include <ranges>
#include <type_traits>
#include <vector>
#include "storm/adapters/IntervalForward.h"
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/models/sparse/Model.h"
#include "storm/transformer/bisimulation/Partition.h"
#include "storm/transformer/bisimulation/SparseAccumulator.h"
#include "storm/transformer/bisimulation/WeakBisimulationData.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"

Include dependency graph for SplitterBasedRefinement.cpp:

Go to the source code of this file.

Classes
struct	storm::bisimulation::detail::SplitterRefinementContext< ValueType, Mode >
struct	storm::bisimulation::detail::SplitterRefinementContext< ValueType, Mode >::DefaultCache
	The scratch space every mode needs. More...
struct	storm::bisimulation::detail::SplitterRefinementContext< ValueType, Mode >::WeakDiscreteTimeCache
	The additional scratch space that refining a block with respect to weak bisimulation on a discrete-time model needs, cf. refineBlockWeak. More...

Namespaces
namespace	storm
namespace	storm::bisimulation
namespace	storm::bisimulation::detail

Functions
template<typename ValueType, SplitterRefinementMode Mode> requires (Mode != SplitterRefinementMode::Strong)
void	storm::bisimulation::detail::recomputeSilentStates (SplitterRefinementContext< ValueType, Mode > &context, auto const &candidates)
	Recomputes whether the given candidate states are silent.
template<typename ValueType, SplitterRefinementMode Mode> requires (Mode != SplitterRefinementMode::Strong)
bool	storm::bisimulation::detail::checkSilentStates (SplitterRefinementContext< ValueType, Mode > const &context)
	Checks that the recorded silent states match the current partition.
template<typename ValueType, SplitterRefinementMode Mode>
void	storm::bisimulation::detail::enqueueSubBlocks (SplitterRefinementContext< ValueType, Mode > &context, storm::bisimulation::Partition::Block const splitBlock)
	Replaces the given block, which has just been split, by its sub-blocks in the queue of splitters.
template<typename ValueType, SplitterRefinementMode Mode>
void	storm::bisimulation::detail::refineBlockStrong (SplitterRefinementContext< ValueType, Mode > &context, storm::bisimulation::Partition::Block const predecessorBlockToSplit)
	Refines the given predecessor block of the current splitter with respect to the probability of moving to the splitter.
template<typename ValueType>
void	storm::bisimulation::detail::refineBlockWeak (SplitterRefinementContext< ValueType, SplitterRefinementMode::WeakDiscreteTime > &context, storm::bisimulation::Partition::Block const block, storm::bisimulation::Partition::Block const splitterBlock)
	Refines the given predecessor block of the current splitter with respect to the probability of moving to the splitter, conditioned on leaving the own block.
template<typename ValueType, SplitterRefinementMode Mode>
void	storm::bisimulation::detail::refinePartitionBasedOnSplitter (SplitterRefinementContext< ValueType, Mode > &context, storm::bisimulation::Partition::Block const splitterBlock)
template<typename ValueType, SplitterRefinementMode Mode>
void	storm::bisimulation::performSplitterBasedRefinement (storm::models::sparse::Model< ValueType > const &model, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::bisimulation::Partition &partition, ValueType const tolerance, storm::OptionalRef< WeakBisimulationData > weakData=storm::NullRef)
	Performs splitter-based partition refinement.
template void	storm::bisimulation::performSplitterBasedRefinement< double, SplitterRefinementMode::Strong > (storm::models::sparse::Model< double > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::bisimulation::Partition &partition, double const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< double, SplitterRefinementMode::WeakDiscreteTime > (storm::models::sparse::Model< double > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::bisimulation::Partition &partition, double const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< double, SplitterRefinementMode::WeakContinuousTime > (storm::models::sparse::Model< double > const &model, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::bisimulation::Partition &partition, double const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::Strong > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalNumber const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakDiscreteTime > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalNumber const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< storm::RationalNumber, SplitterRefinementMode::WeakContinuousTime > (storm::models::sparse::Model< storm::RationalNumber > const &model, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalNumber const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::Strong > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::storage::SparseMatrix< storm::RationalFunction > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalFunction const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakDiscreteTime > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::storage::SparseMatrix< storm::RationalFunction > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalFunction const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)
template void	storm::bisimulation::performSplitterBasedRefinement< storm::RationalFunction, SplitterRefinementMode::WeakContinuousTime > (storm::models::sparse::Model< storm::RationalFunction > const &model, storm::storage::SparseMatrix< storm::RationalFunction > const &backwardTransitions, storm::bisimulation::Partition &partition, storm::RationalFunction const tolerance, storm::OptionalRef< WeakBisimulationData > weakData)