73 phiStates = boost::none;
74 psiStates = boost::none;
89template<
typename ModelType,
typename BlockDataType>
103 this->checkAndSetMeasureDrivenInitialPartition(
model, formula);
106template<
typename ModelType,
typename BlockDataType>
109 std::shared_ptr<storm::logic::Formula const> newFormula = formula.
asSharedPointer();
117 optimalityType = OptimizationDirection::Maximize;
119 optimalityType = OptimizationDirection::Minimize;
129 optimalityType = OptimizationDirection::Maximize;
131 optimalityType = OptimizationDirection::Minimize;
137 std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(
true);
138 std::shared_ptr<storm::logic::Formula const> rightSubformula;
139 if (newFormula->isUntilFormula()) {
140 leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
141 rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
143 measureDrivenInitialPartition =
true;
145 }
else if (newFormula->isEventuallyFormula()) {
146 rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
148 measureDrivenInitialPartition =
true;
152 if (measureDrivenInitialPartition) {
154 std::unique_ptr<storm::modelchecker::CheckResult> phiStatesCheckResult = checker.check(*leftSubformula);
155 std::unique_ptr<storm::modelchecker::CheckResult> psiStatesCheckResult = checker.check(*rightSubformula);
156 phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
157 psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
159 optimalityType = boost::none;
163template<
typename ModelType,
typename BlockDataType>
164void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespectedAtomicPropositions(
165 std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>>
const& expressions,
166 std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>>
const& labels) {
167 std::set<std::string> labelsToRespect;
168 for (
auto const& labelFormula : labels) {
169 labelsToRespect.insert(labelFormula->getLabel());
171 for (
auto const& expressionFormula : expressions) {
172 labelsToRespect.insert(expressionFormula->toString());
174 if (!respectedAtomicPropositions) {
175 respectedAtomicPropositions = labelsToRespect;
177 respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
181template<
typename ModelType,
typename BlockDataType>
187template<
typename ModelType,
typename BlockDataType>
190 Options
const& options)
191 : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) {
192 STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException,
193 "Bisimulation currently only supports models with at most one reward model.");
194 STORM_LOG_THROW(!options.getKeepRewards() || !model.hasRewardModel() || !model.getUniqueRewardModel().hasTransitionRewards(),
195 storm::exceptions::IllegalFunctionCallException,
196 "Bisimulation is currently supported for models with state or action rewards only. Consider converting the transition rewards to state "
197 "rewards (via suitable function calls).");
198 STORM_LOG_THROW(options.getType() != BisimulationType::Weak || !options.getBounded(), storm::exceptions::IllegalFunctionCallException,
199 "Weak bisimulation cannot preserve bounded properties.");
202 if (!this->options.respectedAtomicPropositions) {
203 this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels();
207template<
typename ModelType,
typename BlockDataType>
209 std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
211 std::chrono::high_resolution_clock::time_point initialPartitionStart = std::chrono::high_resolution_clock::now();
213 if (options.measureDrivenInitialPartition) {
214 STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException,
"Unable to compute measure-driven initial partition without phi states.");
215 STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException,
"Unable to compute measure-driven initial partition without psi states.");
216 this->initializeMeasureDrivenPartition();
218 this->initializeLabelBasedPartition();
220 STORM_LOG_WARN_COND(partition.size() > 1,
"Initial partition consists only of a single block.");
221 std::chrono::high_resolution_clock::duration initialPartitionTime = std::chrono::high_resolution_clock::now() - initialPartitionStart;
225 std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
226 this->performPartitionRefinement();
227 std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
229 std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
230 this->extractDecompositionBlocks();
231 std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
233 std::chrono::high_resolution_clock::time_point quotientBuildStart = std::chrono::high_resolution_clock::now();
234 if (options.buildQuotient) {
235 this->buildQuotient();
237 std::chrono::high_resolution_clock::duration quotientBuildTime = std::chrono::high_resolution_clock::now() - quotientBuildStart;
239 std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
242 std::chrono::milliseconds initialPartitionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(initialPartitionTime);
243 std::chrono::milliseconds refinementTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(refinementTime);
244 std::chrono::milliseconds extractionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime);
245 std::chrono::milliseconds quotientBuildTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(quotientBuildTime);
246 std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
247 std::cout <<
"\nTime breakdown:\n";
248 std::cout <<
" * time for initial partition: " << initialPartitionTimeInMilliseconds.count() <<
"ms\n";
249 std::cout <<
" * time for partitioning: " << refinementTimeInMilliseconds.count() <<
"ms\n";
250 std::cout <<
" * time for extraction: " << extractionTimeInMilliseconds.count() <<
"ms\n";
251 std::cout <<
" * time for building quotient: " << quotientBuildTimeInMilliseconds.count() <<
"ms\n";
252 std::cout <<
"------------------------------------------\n";
253 std::cout <<
" * total time: " << totalTimeInMilliseconds.count() <<
"ms\n\n";
257template<
typename ModelType,
typename BlockDataType>
260 std::vector<Block<BlockDataType>*> splitterQueue;
261 std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&](std::unique_ptr<
Block<BlockDataType>>
const& block) {
262 block->data().setSplitter();
263 splitterQueue.push_back(block.get());
267 uint_fast64_t iterations = 0;
268 while (!splitterQueue.empty()) {
274 std::sort(splitterQueue.begin(), splitterQueue.end(),
277 splitterQueue.pop_back();
278 splitter->
data().setSplitter(
false);
281 refinePartitionBasedOnSplitter(*splitter, splitterQueue);
284 std::cout <<
"Performed " << iterations <<
" iterations of partition refinement before abort.\n";
285 STORM_LOG_THROW(
false, storm::exceptions::AbortException,
"Aborted in bisimulation computation.");
291template<
typename ModelType,
typename BlockDataType>
293 STORM_LOG_THROW(this->quotient !=
nullptr, storm::exceptions::IllegalFunctionCallException,
294 "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
295 return this->quotient;
298template<
typename ModelType,
typename BlockDataType>
300 auto const& rewardModel = model.getUniqueRewardModel();
301 if (rewardModel.hasStateRewards()) {
302 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateRewardVector());
304 if (rewardModel.hasStateActionRewards()) {
305 if (model.isNondeterministicModel()) {
306 std::vector<std::set<ValueType>> actionRewards;
307 actionRewards.reserve(model.getNumberOfStates());
309 std::set<ValueType> rewardsAtState;
310 for (
auto choice = model.getTransitionMatrix().getRowGroupIndices()[state];
311 choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
312 rewardsAtState.insert(rewardModel.getStateActionReward(choice));
314 actionRewards.push_back(std::move(rewardsAtState));
316 this->splitInitialPartitionBasedOnActionRewards(actionRewards);
318 this->splitInitialPartitionBasedOnRewards(rewardModel.getStateActionRewardVector());
323template<
typename ModelType,
typename BlockDataType>
326 return rewardVector[a] < rewardVector[b];
330template<
typename ModelType,
typename BlockDataType>
333 return actionRewards[a] < actionRewards[b];
337template<
typename ModelType,
typename BlockDataType>
341 for (
auto const& label : options.respectedAtomicPropositions.get()) {
342 if (label ==
"init") {
345 partition.splitStates(model.getStates(label));
350 if (options.getKeepRewards() && model.hasRewardModel()) {
351 this->splitInitialPartitionBasedOnRewards();
355template<
typename ModelType,
typename BlockDataType>
357 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
359 boost::optional<storm::storage::sparse::state_type> representativePsiState;
360 if (!options.psiStates.get().empty()) {
361 representativePsiState = *options.psiStates.get().begin();
365 model.getNumberOfStates(), statesWithProbability01.first,
366 options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
370 if (options.getKeepRewards() && model.hasRewardModel()) {
371 this->splitInitialPartitionBasedOnRewards();
375template<
typename ModelType,
typename BlockDataType>
380template<
typename ModelType,
typename BlockDataType>
384 this->blocks.resize(partition.size());
385 for (
auto const& blockPtr : partition.getBlocks()) {
387 partition.sortBlock(*blockPtr);
390 this->blocks[blockPtr->getId()] =
block_type(partition.begin(*blockPtr), partition.end(*blockPtr),
true);
398#ifdef STORM_HAVE_CARL