diff --git a/examples/dtmc/nand/nand.pm b/examples/dtmc/nand/nand.pm index 3ae3cc754..9753f1552 100644 --- a/examples/dtmc/nand/nand.pm +++ b/examples/dtmc/nand/nand.pm @@ -68,7 +68,9 @@ endmodule // rewards: final value of gate rewards - [] s=0 & (c=N) & (u=M) : z/N; + // [] s=0 & (c=N) & (u=M) : z/N; + s=0 & (c=N) & (u=M) : z/N; endrewards label "target" = s=4 & z/N<0.1; +label "end" = s=4; diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index d338b7682..1b7935ba8 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -580,41 +580,41 @@ namespace storm { } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions, bool weak, bool buildQuotient) : comparator() { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) : comparator() { STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions); - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient); + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards); + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards, buildQuotient); } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions, bool weak, bool buildQuotient) { - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) { + STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions); - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient); + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards); + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards,buildQuotient); } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) { - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) { + STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded); - partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded); + partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient); } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) { - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) { + STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded); - partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded); + partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient); } template @@ -625,7 +625,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, boost::optional> 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, @@ -643,6 +643,12 @@ namespace storm { newLabeling.addAtomicProposition(ap); } + // If the model had state rewards, we need to build the state rewards for the quotient as well. + boost::optional> stateRewards; + if (keepRewards && model.hasStateRewards()) { + stateRewards = std::vector(this->blocks.size()); + } + // Now build (a) and (b) by traversing all blocks. for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { auto const& block = this->blocks[blockIndex]; @@ -720,6 +726,12 @@ namespace storm { } } } + + // If the model has state rewards, we simply copy the state reward of the representative state, because + // all states in a block are guaranteed to have the same state reward. + if (keepRewards && model.hasStateRewards()) { + stateRewards.get()[blockIndex] = model.getStateRewardVector()[representativeState]; + } } // Now check which of the blocks of the partition contain at least one initial state. @@ -728,16 +740,13 @@ namespace storm { newLabeling.addAtomicPropositionToState("init", initialBlock.getId()); } - // FIXME: - // If reward structures are allowed, the quotient structures need to be built here. - // Finally construct the quotient model. - this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling))); + this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling), std::move(stateRewards))); } template template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, boost::optional> 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. @@ -775,7 +784,7 @@ namespace storm { // If we are required to build the quotient model, do so now. if (buildQuotient) { - this->buildQuotient(model, atomicPropositions, partition, bisimulationType); + this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards); } std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; @@ -1187,13 +1196,13 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool bounded) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool keepRewards, bool bounded) { std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel)); Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc); // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. - if (model.hasStateRewards()) { + if (keepRewards && model.hasStateRewards()) { this->splitRewards(model, partition); } @@ -1277,7 +1286,7 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions, bool keepRewards) { Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc); if (atomicPropositions) { @@ -1298,7 +1307,7 @@ namespace storm { // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. - if (model.hasStateRewards()) { + if (keepRewards && model.hasStateRewards()) { this->splitRewards(model, partition); } @@ -1332,17 +1341,18 @@ namespace storm { template template void DeterministicModelBisimulationDecomposition::splitRewards(ModelType const& model, Partition& partition) { - if (model.hasStateRewards()) { + if (!model.hasStateRewards()) { return; } for (auto& block : partition.getBlocks()) { std::sort(partition.getBegin(block), partition.getEnd(block), [&model] (std::pair const& a, std::pair const& b) { return model.getStateRewardVector()[a.first] < model.getStateRewardVector()[b.first]; } ); - // Update the positions vector. + // Update the positions vector and put the (state) reward values next to the states so we can easily compare them later. storm::storage::sparse::state_type position = block.getBegin(); for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { partition.setPosition(stateIt->first, position); + stateIt->second = model.getStateRewardVector()[stateIt->first]; } // Finally, we need to scan the ranges of states that agree on the probability. @@ -1353,7 +1363,6 @@ namespace storm { // Now we can check whether the block needs to be split, which is the case iff the rewards for the first // and the last state are different. - bool blockSplit = !comparator.isEqual(begin->second, end->second); while (!comparator.isEqual(begin->second, end->second)) { // Now we scan for the first state in the block that disagrees on the reward value. Note that we do // not have to check currentIndex for staying within bounds, because we know the matching state is @@ -1366,6 +1375,9 @@ namespace storm { ++begin; ++currentIndex; } + + // Now we split the block. + partition.splitBlock(block, currentIndex); } } } diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index c71013aa4..3037787aa 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -30,7 +30,7 @@ namespace storm { * @param weak A flag indication whether a weak bisimulation is to be computed. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false); /*! * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation. @@ -41,7 +41,7 @@ namespace storm { * @param weak A flag indication whether a weak bisimulation is to be computed. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false); /*! * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely @@ -54,7 +54,7 @@ namespace storm { * @param bounded If set to true, also bounded until formulas are preserved. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false); /*! * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely @@ -67,7 +67,7 @@ namespace storm { * @param bounded If set to true, also bounded until formulas are preserved. * @param buildQuotient Sets whether or not the quotient model is to be built. */ - DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false); /*! * Retrieves the quotient of the model under the previously computed bisimulation. @@ -404,7 +404,7 @@ namespace storm { * method. */ template - void partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient); + void partitionRefinement(ModelType const& model, boost::optional> 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 @@ -456,7 +456,7 @@ namespace storm { * @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); + void buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards); /*! * Creates the measure-driven initial partition for reaching psi states from phi states. @@ -472,7 +472,7 @@ namespace storm { * @return The resulting partition. */ template - Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool bounded = false); + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false); /*! * Creates the initial partition based on all the labels in the given model. @@ -485,7 +485,7 @@ namespace storm { * @return The resulting partition. */ template - Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>()); + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true); /*! * Splits all blocks of the given partition into a block that contains all divergent states and another block diff --git a/src/utility/cli.h b/src/utility/cli.h index 080322ded..321e60779 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -271,7 +271,7 @@ namespace storm { std::shared_ptr> dtmc = result->template as>(); STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, boost::optional>(), storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, boost::optional>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); result = bisimulationDecomposition.getQuotient(); diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp index b5670064e..ffe337d31 100644 --- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -9,7 +9,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); std::shared_ptr> dtmc = abstractModel->as>(); - storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), true, false, true); std::shared_ptr> result; ASSERT_NO_THROW(result = bisim.getQuotient()); @@ -17,14 +17,14 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { EXPECT_EQ(13, result->getNumberOfStates()); EXPECT_EQ(20, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, std::set({"one"}), false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, std::set({"one"}), true, false, true); ASSERT_NO_THROW(result = bisim2.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); EXPECT_EQ(5, result->getNumberOfStates()); EXPECT_EQ(8, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, std::set({"one"}), true, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, std::set({"one"}), true, true, true); ASSERT_NO_THROW(result = bisim3.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); @@ -38,7 +38,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); std::shared_ptr> dtmc = abstractModel->as>(); - storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), true, false, true); std::shared_ptr> result; ASSERT_NO_THROW(result = bisim.getQuotient()); @@ -46,14 +46,14 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { EXPECT_EQ(334, result->getNumberOfStates()); EXPECT_EQ(546, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, std::set({"observe0Greater1"}), false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, std::set({"observe0Greater1"}), true, false, true); ASSERT_NO_THROW(result = bisim2.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); EXPECT_EQ(65, result->getNumberOfStates()); EXPECT_EQ(105, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, std::set({"observe0Greater1"}), true, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, std::set({"observe0Greater1"}), true, true, true); ASSERT_NO_THROW(result = bisim3.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType());