32using namespace bisimulation;
34template<
typename ModelType,
typename BlockDataType>
36 this->preserveSingleFormula(
model, formula);
39template<
typename ModelType,
typename BlockDataType>
41 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas)
43 if (formulas.empty()) {
45 this->keepRewards =
true;
47 if (formulas.size() == 1) {
48 this->preserveSingleFormula(
model, *formulas.front());
50 for (
auto const& formula : formulas) {
56template<
typename ModelType,
typename BlockDataType>
58 : measureDrivenInitialPartition(false),
61 respectedAtomicPropositions(),
70template<
typename ModelType,
typename BlockDataType>
73 measureDrivenInitialPartition =
false;
74 phiStates = boost::none;
75 psiStates = boost::none;
93template<
typename ModelType,
typename BlockDataType>
110 this->checkAndSetMeasureDrivenInitialPartition(
model, formula);
113template<
typename ModelType,
typename BlockDataType>
116 std::shared_ptr<storm::logic::Formula const> newFormula = formula.
asSharedPointer();
124 optimalityType = OptimizationDirection::Maximize;
126 optimalityType = OptimizationDirection::Minimize;
136 optimalityType = OptimizationDirection::Maximize;
138 optimalityType = OptimizationDirection::Minimize;
144 std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(
true);
145 std::shared_ptr<storm::logic::Formula const> rightSubformula;
146 if (newFormula->isUntilFormula()) {
147 leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
148 rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
150 measureDrivenInitialPartition =
true;
152 }
else if (newFormula->isEventuallyFormula()) {
153 rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
155 measureDrivenInitialPartition =
true;
159 if (measureDrivenInitialPartition) {
161 std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
162 std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
163 phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
164 psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
166 optimalityType = boost::none;
170template<
typename ModelType,
typename BlockDataType>
171void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespectedAtomicPropositions(
172 std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>>
const& expressions,
173 std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>>
const& labels) {
174 std::set<std::string> labelsToRespect;
175 for (
auto const& labelFormula : labels) {
176 labelsToRespect.insert(labelFormula->getLabel());
178 for (
auto const& expressionFormula : expressions) {
179 labelsToRespect.insert(expressionFormula->toString());
181 if (!respectedAtomicPropositions) {
182 respectedAtomicPropositions = labelsToRespect;
184 respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
188template<
typename ModelType,
typename BlockDataType>
194template<
typename ModelType,
typename BlockDataType>
198 : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) {
200 "Bisimulation currently only supports models with at most one reward model.");
202 storm::exceptions::IllegalFunctionCallException,
203 "Bisimulation is currently supported for models with state or action rewards only. Consider converting the transition rewards to state "
204 "rewards (via suitable function calls).");
206 "Weak bisimulation cannot preserve bounded properties.");
208 "Weak bisimulation cannot preserve discounted properties.");
216template<
typename ModelType,
typename BlockDataType>
218 std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
220 std::chrono::high_resolution_clock::time_point initialPartitionStart = std::chrono::high_resolution_clock::now();
223 STORM_LOG_THROW(options.
phiStates, storm::exceptions::InvalidOptionException,
"Unable to compute measure-driven initial partition without phi states.");
224 STORM_LOG_THROW(options.
psiStates, storm::exceptions::InvalidOptionException,
"Unable to compute measure-driven initial partition without psi states.");
225 this->initializeMeasureDrivenPartition();
227 this->initializeLabelBasedPartition();
229 STORM_LOG_WARN_COND(partition.size() > 1,
"Initial partition consists only of a single block.");
230 std::chrono::high_resolution_clock::duration initialPartitionTime = std::chrono::high_resolution_clock::now() - initialPartitionStart;
234 std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
235 this->performPartitionRefinement();
236 std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
238 std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
239 this->extractDecompositionBlocks();
240 std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
242 std::chrono::high_resolution_clock::time_point quotientBuildStart = std::chrono::high_resolution_clock::now();
244 this->buildQuotient();
246 std::chrono::high_resolution_clock::duration quotientBuildTime = std::chrono::high_resolution_clock::now() - quotientBuildStart;
248 std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
250 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
251 std::chrono::milliseconds initialPartitionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(initialPartitionTime);
252 std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime);
253 std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime);
254 std::chrono::milliseconds quotientBuildTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(quotientBuildTime);
255 std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
256 std::cout <<
"\nTime breakdown:\n";
257 std::cout <<
" * time for initial partition: " << initialPartitionTimeInMilliseconds.count() <<
"ms\n";
258 std::cout <<
" * time for partitioning: " << refinementTimeInMilliseconds.count() <<
"ms\n";
259 std::cout <<
" * time for extraction: " << extractionTimeInMilliseconds.count() <<
"ms\n";
260 std::cout <<
" * time for building quotient: " << quotientBuildTimeInMilliseconds.count() <<
"ms\n";
261 std::cout <<
"------------------------------------------\n";
262 std::cout <<
" * total time: " << totalTimeInMilliseconds.count() <<
"ms\n\n";
266template<
typename ModelType,
typename BlockDataType>
269 std::vector<Block<BlockDataType>*> splitterQueue;
270 std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&](std::unique_ptr<
Block<BlockDataType>>
const& block) {
271 block->data().setSplitter();
272 splitterQueue.push_back(block.get());
276 uint_fast64_t iterations = 0;
277 while (!splitterQueue.empty()) {
283 std::sort(splitterQueue.begin(), splitterQueue.end(),
286 splitterQueue.pop_back();
287 splitter->
data().setSplitter(
false);
290 refinePartitionBasedOnSplitter(*splitter, splitterQueue);
293 std::cout <<
"Performed " << iterations <<
" iterations of partition refinement before abort.\n";
294 STORM_LOG_THROW(
false, storm::exceptions::AbortException,
"Aborted in bisimulation computation.");
300template<
typename ModelType,
typename BlockDataType>
302 STORM_LOG_THROW(this->quotient !=
nullptr, storm::exceptions::IllegalFunctionCallException,
303 "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
304 return this->quotient;
307template<
typename ModelType,
typename BlockDataType>
309 auto const& rewardModel = model.getUniqueRewardModel();
310 if (rewardModel.hasStateRewards()) {
311 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateRewardVector());
313 if (rewardModel.hasStateActionRewards()) {
314 if (model.isNondeterministicModel()) {
315 std::vector<std::set<ValueType>> actionRewards;
316 actionRewards.reserve(model.getNumberOfStates());
318 std::set<ValueType> rewardsAtState;
319 for (
auto choice = model.getTransitionMatrix().getRowGroupIndices()[state];
320 choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
321 rewardsAtState.insert(rewardModel.getStateActionReward(choice));
323 actionRewards.push_back(std::move(rewardsAtState));
325 this->splitInitialPartitionBasedOnActionRewards(actionRewards);
327 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateActionRewardVector());
332template<
typename ModelType,
typename BlockDataType>
335 return rewardVector[a] < rewardVector[b];
339template<
typename ModelType,
typename BlockDataType>
342 return actionRewards[a] < actionRewards[b];
346template<
typename ModelType,
typename BlockDataType>
351 if (label ==
"init") {
354 partition.splitStates(model.getStates(label));
360 this->splitInitialPartitionBasedOnRewards();
364template<
typename ModelType,
typename BlockDataType>
366 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
368 boost::optional<storm::storage::sparse::state_type> representativePsiState;
370 representativePsiState = *options.
psiStates.get().begin();
374 model.getNumberOfStates(), statesWithProbability01.first,
380 this->splitInitialPartitionBasedOnRewards();
384template<
typename ModelType,
typename BlockDataType>
389template<
typename ModelType,
typename BlockDataType>
393 this->blocks.resize(partition.size());
394 for (
auto const& blockPtr : partition.getBlocks()) {
396 partition.sortBlock(*blockPtr);
399 this->blocks[blockPtr->getId()] =
block_type(partition.begin(*blockPtr), partition.end(*blockPtr),
true);
407#ifdef STORM_HAVE_CARL
This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.
virtual void buildQuotient()=0
Builds the quotient model based on the previously computed equivalence classes (stored in the blocks ...
std::shared_ptr< ModelType > getQuotient() const
Retrieves the quotient of the model under the computed bisimulation.
void performPartitionRefinement()
Performs the partition refinement on the model and thereby computes the equivalence classes under str...
virtual void splitInitialPartitionBasedOnRewards()
Splits the initial partition based on the (unique) reward model of the current model.
virtual void splitInitialPartitionBasedOnActionRewards(std::vector< std::set< ValueType > > const &rewardVector)
Splits the initial partition based on the given vector of action rewards.
BisimulationDecomposition(ModelType const &model, Options const &options)
Decomposes the given model into equivalance classes of a bisimulation.
void computeBisimulationDecomposition()
Computes the decomposition of the model into bisimulation equivalence classes.
void extractDecompositionBlocks()
Constructs the blocks of the decomposition object based on the current partition.
virtual void initializeMeasureDrivenPartition()
Creates the measure-driven initial partition for reaching psi states from phi states.
virtual void initializeLabelBasedPartition()
Initializes the initial partition based on all respected labels.
virtual void initialize()
A function that can initialize auxiliary data structures.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
FragmentSpecification propositional()
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
void preserveFormula(storm::logic::Formula const &formula)
Changes the options in a way that the given formula is preserved.
boost::optional< storm::storage::BitVector > psiStates
boost::optional< storm::storage::BitVector > phiStates
bool measureDrivenInitialPartition
boost::optional< std::set< std::string > > respectedAtomicPropositions
An optional set of strings that indicate which of the atomic propositions of the model are to be resp...
bool buildQuotient
A flag that governs whether the quotient model is actually built or only the decomposition is compute...
bool getKeepRewards() const
BisimulationType getType() const
bool getDiscounted() const