diff --git a/.gitignore b/.gitignore index aa15c7b9a..03286848f 100644 --- a/.gitignore +++ b/.gitignore @@ -43,3 +43,5 @@ build//CMakeLists.txt #Temp texteditor files *.orig *.*~ +# CMake generated/configured files +src/utility/storm-version.cpp diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 89dce2caf..ba3d5b7fa 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -97,13 +97,11 @@ namespace storm { * @param program The program to translate. * @param constantDefinitionString A string that contains a comma-separated definition of all undefined * constants in the model. - * @param rewardModelName The name of reward model to be added to the model. This must be either a reward - * model of the program or the empty string. In the latter case, the constructed model will contain no - * rewards. + * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - static std::unique_ptr> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { - // Start by defining the undefined constants in the model. + static std::unique_ptr> translateProgram(storm::prism::Program program, storm::prism::RewardModel const& rewardModel = storm::prism::RewardModel(), std::string const& constantDefinitionString = "") { + // Start by defining the undefined constants in the model. // First, we need to parse the constant definition string. std::map constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -118,21 +116,21 @@ namespace storm { // all expressions in the program so we can then evaluate them without having to store the values of the // constants in the state (i.e., valuation). preparedProgram = preparedProgram.substituteConstants(); - ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModelName); + ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel); std::unique_ptr> result; switch (program.getModelType()) { case storm::prism::Program::ModelType::DTMC: - result = std::unique_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMC: - result = std::unique_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::MDP: - result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::prism::Program::ModelType::CTMDP: - result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModel.hasStateRewards() ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModel.hasTransitionRewards() ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; default: LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -636,11 +634,10 @@ namespace storm { * Explores the state space of the given program and returns the components of the model as a result. * * @param program The program whose state space to explore. - * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model - * is considered. + * @param rewardModel The reward model that is to be considered. * @return A structure containing the components of the resulting model. */ - static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) { + static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel) { ModelComponents modelComponents; expressions::ExpressionEvaluation eval; @@ -657,9 +654,6 @@ namespace storm { // Create the structure for storing the reachable state space. StateInformation stateInformation; - // Get the selected reward model or create an empty one if none is selected. - storm::prism::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::prism::RewardModel(); - // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC; diff --git a/src/exceptions/BaseException.cpp b/src/exceptions/BaseException.cpp index 0acae02ac..ed28a918c 100644 --- a/src/exceptions/BaseException.cpp +++ b/src/exceptions/BaseException.cpp @@ -13,8 +13,12 @@ namespace storm { BaseException::BaseException(char const* cstr) { stream << cstr; } + + BaseException::~BaseException() { + // Intentionally left empty. + } - const char* BaseException::what() const throw() { + const char* BaseException::what() const noexcept { std::string errorString = this->stream.str(); char* result = new char[errorString.size() + 1]; result[errorString.size()] = '\0'; diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index 8bf12ea23..aae0b208a 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -29,12 +29,17 @@ namespace storm { */ BaseException(char const* cstr); + /*! + * Declare a destructor to counter the "looser throw specificator" error + */ + virtual ~BaseException(); + /*! * Retrieves the message associated with this exception. * * @return The message associated with this exception. */ - virtual const char* what() const throw(); + virtual const char* what() const noexcept; protected: // This stream stores the message of this exception. diff --git a/src/exceptions/ExceptionMacros.h b/src/exceptions/ExceptionMacros.h index a638d62ba..5d1090a06 100644 --- a/src/exceptions/ExceptionMacros.h +++ b/src/exceptions/ExceptionMacros.h @@ -14,6 +14,8 @@ exception_name(char const* cstr) : BaseException(cstr) { \ } \ exception_name(exception_name const& cp) : BaseException(cp) { \ } \ +~exception_name() throw() { \ +} \ template \ exception_name& operator<<(T const& var) { \ this->stream << var; \ diff --git a/src/settings/OptionBuilder.h b/src/settings/OptionBuilder.h index 2d7ad9a19..abcd35862 100644 --- a/src/settings/OptionBuilder.h +++ b/src/settings/OptionBuilder.h @@ -68,7 +68,7 @@ namespace storm { */ OptionBuilder& addArgument(std::shared_ptr argument) { STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option."); - STORM_LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional."); + STORM_LOG_THROW(this->arguments.empty() || argument->getIsOptional() || !this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional."); std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName()); STORM_LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name."); diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index d04ec0d25..ece0d9a00 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -61,7 +61,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("rewardmodel", "The name of the reward model to use.").setDefaultValueString("").setIsOptional(true).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pctlOptionName, false, "Specifies a PCTL formula that is to be checked on the model.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("formula", "The formula to check.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pctlFileOptionName, false, "Specifies the PCTL formulas that are to be checked on the model.") @@ -154,6 +155,14 @@ namespace storm { return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); } + bool GeneralSettings::isSymbolicRewardModelNameSet() const { + return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getHasBeenSet(); + } + + std::string GeneralSettings::getSymbolicRewardModelName() const { + return this->getOption(symbolicOptionName).getArgumentByName("rewardmodel").getValueAsString(); + } + bool GeneralSettings::isPctlPropertySet() const { return this->getOption(pctlOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index c65ab57a2..22f8fe58f 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -39,7 +39,6 @@ namespace storm { */ bool isVersionSet() const; - /*! * Retrieves the name of the module for which to show the help or "all" to indicate that the full help * needs to be shown. @@ -127,6 +126,20 @@ namespace storm { * @return The name of the file that contains the symbolic model specification. */ std::string getSymbolicModelFilename() const; + + /*! + * Retrieves whether the name of a reward model was passed to the symbolic option. + * + * @return True iff the name of a reward model was passed to the symbolic option. + */ + bool isSymbolicRewardModelNameSet() const; + + /*! + * Retrieves the name of the reward model if one was set using the symbolic option. + * + * @return The name of the selected reward model. + */ + std::string getSymbolicRewardModelName() const; /*! * Retrieves whether the pctl option was set. diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index cf06b674e..d433a1d5b 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -13,10 +13,7 @@ namespace storm { namespace storage { template - std::size_t DeterministicModelBisimulationDecomposition::Block::blockId = 0; - - template - DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) { + DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id), label(label) { if (next != nullptr) { next->prev = this; } @@ -247,7 +244,7 @@ namespace storm { template DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { // Create the block and give it an iterator to itself. - typename std::list::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr); + typename std::list::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr, this->blocks.size()); it->setIterator(it); // Set up the different parts of the internal structure. @@ -265,7 +262,7 @@ namespace storm { template DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { - typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr); + typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, this->blocks.size()); Block& firstBlock = *firstIt; firstBlock.setIterator(firstIt); @@ -278,7 +275,7 @@ namespace storm { } firstBlock.setAbsorbing(true); - typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr(new std::string(prob1Label))); + typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, this->blocks.size(), std::shared_ptr(new std::string(prob1Label))); Block& secondBlock = *secondIt; secondBlock.setIterator(secondIt); @@ -290,7 +287,7 @@ namespace storm { } secondBlock.setAbsorbing(true); - typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); + typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, this->blocks.size(), otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); Block& thirdBlock = *thirdIt; thirdBlock.setIterator(thirdIt); @@ -411,7 +408,7 @@ namespace storm { } // Actually create the new block and insert it at the correct position. - typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); + typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, this->blocks.size(), block.getLabelPtr()); selfIt->setIterator(selfIt); Block& newBlock = *selfIt; @@ -435,7 +432,7 @@ namespace storm { } // Actually insert the new block. - typename std::list::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block); + typename std::list::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block, this->blocks.size()); Block& newBlock = *it; newBlock.setIterator(it); @@ -563,9 +560,16 @@ namespace storm { } std::cout << std::endl << "state to block mapping: " << std::endl; for (auto const& block : stateToBlockMapping) { - std::cout << block << " "; + std::cout << block << "[" << block->getId() <<"] "; } std::cout << std::endl; + if (this->keepSilentProbabilities) { + std::cout << "silent probabilities" << std::endl; + for (auto const& prob : silentProbabilities) { + std::cout << prob << " "; + } + std::cout << std::endl; + } std::cout << "size: " << this->blocks.size() << std::endl; assert(this->check()); } @@ -576,41 +580,41 @@ namespace storm { } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) : comparator() { - STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions, 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); - partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient); + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions); + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient); } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { - STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + 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."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType); - partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient); + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions); + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, 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.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + STORM_LOG_THROW(!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, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); + partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, 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.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); + STORM_LOG_THROW(!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, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); + partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); } template @@ -621,7 +625,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType) { // In order to create the quotient model, we need to construct // (a) the new transition matrix, // (b) the new labeling, @@ -632,7 +636,8 @@ namespace storm { // Prepare the new state labeling for (b). storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); - std::set atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions(); + std::set atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions(); + atomicPropositionsSet.insert("init"); std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); for (auto const& ap : atomicPropositions) { newLabeling.addAtomicProposition(ap); @@ -646,7 +651,8 @@ namespace storm { // they all behave equally. storm::storage::sparse::state_type representativeState = *block.begin(); - // However, for weak bisimulation, we need to make sure the representative state is a non-silent one. + // However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if + // there is any such state). if (bisimulationType == BisimulationType::WeakDtmc) { for (auto const& state : block) { if (!partition.isSilent(state, comparator)) { @@ -731,7 +737,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, 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 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. @@ -763,13 +769,13 @@ namespace storm { std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; }); // Convert the state-value-pairs to states only. - std::function const&)> projection = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; - this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true); + std::function const&)> projection = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; + this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true); } // If we are required to build the quotient model, do so now. if (buildQuotient) { - this->buildQuotient(model, partition, bisimulationType); + this->buildQuotient(model, atomicPropositions, partition, bisimulationType); } std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; @@ -1188,6 +1194,12 @@ namespace storm { 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()) { + this->splitRewards(model, partition); + } + // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. if (bisimulationType == BisimulationType::WeakDtmc) { @@ -1268,13 +1280,29 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions) { Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc); - for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { - if (label == "init") { - continue; + + if (atomicPropositions) { + for (auto const& label : atomicPropositions.get()) { + if (label == "init") { + continue; + } + partition.splitLabel(model.getLabeledStates(label)); } - partition.splitLabel(model.getLabeledStates(label)); + } else { + for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { + if (label == "init") { + continue; + } + partition.splitLabel(model.getLabeledStates(label)); + } + } + + // If the model has state rewards, we need to consider them, because otherwise reward properties are not + // preserved. + if (model.hasStateRewards()) { + this->splitRewards(model, partition); } // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent @@ -1304,6 +1332,47 @@ namespace storm { } } + template + template + void DeterministicModelBisimulationDecomposition::splitRewards(ModelType const& model, Partition& partition) { + 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. + 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); + } + + // Finally, we need to scan the ranges of states that agree on the probability. + typename std::vector>::const_iterator begin = partition.getBegin(block); + typename std::vector>::const_iterator current = begin; + typename std::vector>::const_iterator end = partition.getEnd(block) - 1; + storm::storage::sparse::state_type currentIndex = block.getBegin(); + + // 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 + // within bounds. + ValueType const& currentValue = begin->second; + + ++begin; + ++currentIndex; + while (begin != end && comparator.isEqual(begin->second, currentValue)) { + ++begin; + ++currentIndex; + } + } + } + } + template class DeterministicModelBisimulationDecomposition; #ifdef PARAMETRIC_SYSTEMS diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 47d605b99..c71013aa4 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -25,19 +25,23 @@ namespace storm { * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. * * @param model The model to decompose. + * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the + * model will be respected. If built, the quotient model will only contain the respected atomic propositions. * @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, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool weak = false, bool buildQuotient = false); /*! * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation. * * @param model The model to decompose. + * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the + * model will be respected. If built, the quotient model will only contain the respected atomic propositions. * @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, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool weak = false, bool buildQuotient = false); /*! * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely @@ -83,7 +87,7 @@ namespace storm { typedef typename std::list::const_iterator const_iterator; // Creates a new block with the given begin and end. - Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label = nullptr); + Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr const& label = nullptr); // Prints the block. void print(Partition const& partition) const; @@ -226,9 +230,6 @@ namespace storm { // The label of the block or nullptr if it has none. std::shared_ptr label; - - // A counter for the IDs of the blocks. - static std::size_t blockId; }; class Partition { @@ -394,6 +395,8 @@ 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 backwardTransitions The backward transitions of the model. * @param The initial partition. * @param bisimulationType The kind of bisimulation that is to be computed. @@ -401,7 +404,7 @@ namespace storm { * method. */ template - void partitionRefinement(ModelType const& model, 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 buildQuotient); /*! * Refines the partition based on the provided splitter. After calling this method all blocks are stable @@ -445,12 +448,15 @@ 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 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, Partition const& partition, BisimulationType bisimulationType); + void buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType); /*! * Creates the measure-driven initial partition for reaching psi states from phi states. @@ -474,10 +480,12 @@ namespace storm { * @param model The model whose state space is partitioned based on its labels. * @param backwardTransitions The backward transitions of the model. * @param bisimulationType The kind of bisimulation that is to be computed. + * @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic + * propositions of the model are respected. * @return The resulting partition. */ template - Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType); + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType, boost::optional> const& atomicPropositions = boost::optional>()); /*! * Splits all blocks of the given partition into a block that contains all divergent states and another block @@ -500,6 +508,15 @@ namespace storm { template void initializeSilentProbabilities(ModelType const& model, Partition& partition); + /*! + * Splits all blocks of the partition in a way such that the states of each block agree on the rewards. + * + * @param model The model from which to look-up the rewards. + * @param partition The partition that is to be split. + */ + template + void splitRewards(ModelType const& model, Partition& partition); + // If required, a quotient model is built and stored in this member. std::shared_ptr> quotient; diff --git a/src/storage/StateBlock.h b/src/storage/StateBlock.h index e9a8d5ebe..32d21c98c 100644 --- a/src/storage/StateBlock.h +++ b/src/storage/StateBlock.h @@ -10,7 +10,7 @@ namespace storm { namespace storage { - // Typedef the most common state container + // Typedef the most common state container. typedef boost::container::flat_set FlatSetStateContainer; std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index b988f012e..58d749ad8 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -145,6 +145,10 @@ namespace storm { return variableNameToModuleIndexPair->second; } + bool Program::hasRewardModel() const { + return !this->rewardModels.empty(); + } + std::vector const& Program::getRewardModels() const { return this->rewardModels; } @@ -159,6 +163,11 @@ namespace storm { return this->getRewardModels()[nameIndexPair->second]; } + RewardModel const& Program::getRewardModel(uint_fast64_t index) const { + STORM_LOG_THROW(this->getNumberOfRewardModels() > index, storm::exceptions::OutOfRangeException, "Reward model with index " << index << " does not exist."); + return this->rewardModels[index]; + } + std::vector