From 11b9c605154e24cb7fd5aed3087a0fe4ffb01d6d Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 12:12:41 +0200 Subject: [PATCH 01/19] Adapted fragment checker test to new multiobjective-fragment specification --- src/test/storm/logic/FragmentCheckerTest.cpp | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 643742bbf..c846f7f68 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -145,26 +145,17 @@ TEST(FragmentCheckerTest, MultiObjective) { std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0.5,1] \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], \"label\", R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); From 9bccae9c5c6e8e548903997d167fa6346e51d6d5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 15:59:31 +0200 Subject: [PATCH 02/19] uint_fast64_t -> uint64_t --- .../SparseModelMemoryProduct.cpp | 150 +++++++++--------- .../SparseModelMemoryProduct.h | 14 +- 2 files changed, 82 insertions(+), 82 deletions(-) diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 56b3a6aa0..2ad64c746 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -24,10 +24,10 @@ namespace storm { template std::shared_ptr> SparseModelMemoryProduct::build() { - uint_fast64_t modelStateCount = model.getNumberOfStates(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t modelStateCount = model.getNumberOfStates(); + uint64_t memoryStateCount = memory.getNumberOfStates(); - std::vector memorySuccessors = computeMemorySuccessors(); + std::vector memorySuccessors = computeMemorySuccessors(); // Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false); @@ -41,8 +41,8 @@ namespace storm { storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates); // Compute the mapping to the states of the result - uint_fast64_t reachableStateCount = 0; - toResultStateMapping = std::vector (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits::max()); + uint64_t reachableStateCount = 0; + toResultStateMapping = std::vector (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits::max()); for (auto const& reachableState : reachableStates) { toResultStateMapping[reachableState] = reachableStateCount; ++reachableStateCount; @@ -64,18 +64,18 @@ namespace storm { } template - uint_fast64_t const& SparseModelMemoryProduct::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const { + uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } template - std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { - uint_fast64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); + std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { + uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); + uint64_t memoryStateCount = memory.getNumberOfStates(); + std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { + for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + for (uint64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal]; if (memoryTransition) { for (auto const& modelTransitionIndex : memoryTransition.get()) { @@ -88,25 +88,25 @@ namespace storm { } template - storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); // Explore the reachable states via DFS. // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) storm::storage::BitVector reachableStates = initialStates; - std::vector stack(reachableStates.begin(), reachableStates.end()); + std::vector stack(reachableStates.begin(), reachableStates.end()); while (!stack.empty()) { - uint_fast64_t stateIndex = stack.back(); + uint64_t stateIndex = stack.back(); stack.pop_back(); - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { if (!storm::utility::isZero(modelTransitionIt->getValue())) { - uint_fast64_t successorModelState = modelTransitionIt->getColumn(); - uint_fast64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); - uint_fast64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; - uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + uint64_t successorModelState = modelTransitionIt->getColumn(); + uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); + uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; + uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; if (!reachableStates.get(successorStateIndex)) { reachableStates.set(successorStateIndex, true); stack.push_back(successorStateIndex); @@ -118,23 +118,23 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); - uint_fast64_t numResTransitions = 0; + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = reachableStates.getNumberOfSetBits(); + uint64_t numResTransitions = 0; for (auto const& stateIndex : reachableStates) { numResTransitions += model.getTransitionMatrix().getRow(stateIndex / memoryStateCount).getNumberOfEntries(); } storm::storage::SparseMatrixBuilder builder(numResStates, numResStates, numResTransitions, true); - uint_fast64_t currentRow = 0; + uint64_t currentRow = 0; for (auto const& stateIndex : reachableStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; auto const& modelRow = model.getTransitionMatrix().getRow(modelState); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { - uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -144,30 +144,30 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); - uint_fast64_t numResChoices = 0; - uint_fast64_t numResTransitions = 0; + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = reachableStates.getNumberOfSetBits(); + uint64_t numResChoices = 0; + uint64_t numResTransitions = 0; for (auto const& stateIndex : reachableStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { + uint64_t modelState = stateIndex / memoryStateCount; + for (uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { ++numResChoices; numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); } } storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, true, numResStates); - uint_fast64_t currentRow = 0; + uint64_t currentRow = 0; for (auto const& stateIndex : reachableStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; builder.newRowGroup(currentRow); - for (uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { + for (uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { - uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -179,18 +179,18 @@ namespace storm { template storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { - uint_fast64_t modelStateCount = model.getNumberOfStates(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t modelStateCount = model.getNumberOfStates(); + uint64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); + uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); storm::models::sparse::StateLabeling resultLabeling(numResStates); for (std::string modelLabel : model.getStateLabeling().getLabels()) { if (modelLabel != "init") { storm::storage::BitVector resLabeledStates(numResStates, false); for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) { - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = getResultState(modelState, memoryState); + for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { resLabeledStates.set(resState, true); @@ -204,8 +204,8 @@ namespace storm { STORM_LOG_THROW(!resultLabeling.containsLabel(memoryLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " << memoryLabel << "."); storm::storage::BitVector resLabeledStates(numResStates, false); for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { - for (uint_fast64_t modelState = 0; modelState < modelStateCount; ++modelState) { - uint_fast64_t const& resState = getResultState(modelState, memoryState); + for (uint64_t modelState = 0; modelState < modelStateCount; ++modelState) { + uint64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { resLabeledStates.set(resState, true); @@ -218,20 +218,20 @@ namespace storm { } template - std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { + std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { std::unordered_map> result; - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); for (auto const& rewardModel : model.getRewardModels()) { boost::optional> stateRewards; if (rewardModel.second.hasStateRewards()) { stateRewards = std::vector(numResStates, storm::utility::zero()); - uint_fast64_t modelState = 0; + uint64_t modelState = 0; for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { if (!storm::utility::isZero(modelStateReward)) { - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = getResultState(modelState, memoryState); + for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { stateRewards.get()[resState] = modelStateReward; @@ -244,16 +244,16 @@ namespace storm { boost::optional> stateActionRewards; if (rewardModel.second.hasStateActionRewards()) { stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); - uint_fast64_t modelState = 0; - uint_fast64_t modelRow = 0; + uint64_t modelState = 0; + uint64_t modelRow = 0; for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { if (!storm::utility::isZero(modelStateActionReward)) { while (modelRow >= model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]) { ++modelState; } - uint_fast64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = getResultState(modelState, memoryState); + uint64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; + for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; @@ -266,19 +266,19 @@ namespace storm { boost::optional> transitionRewards; if (rewardModel.second.hasTransitionRewards()) { storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); - uint_fast64_t stateIndex = 0; + uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { if (resState < numResStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; - uint_fast64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); - for (uint_fast64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { - uint_fast64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; - uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); + for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex); for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) { - uint_fast64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); - uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } } @@ -300,19 +300,19 @@ namespace storm { components.rateTransitions = true; } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { // We also need to translate the exit rates and the Markovian states - uint_fast64_t numResStates = components.transitionMatrix.getRowGroupCount(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = components.transitionMatrix.getRowGroupCount(); + uint64_t memoryStateCount = memory.getNumberOfStates(); std::vector resultExitRates; resultExitRates.reserve(components.transitionMatrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); - uint_fast64_t stateIndex = 0; + uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { if (resState < numResStates) { assert(resState == resultExitRates.size()); - uint_fast64_t modelState = stateIndex / memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; resultExitRates.push_back(modelExitRates[modelState]); if (modelMarkovianStates.get(modelState)) { resultMarkovianStates.set(resState, true); diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 0c60923e7..b5faf2ab4 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -33,33 +33,33 @@ namespace storm { // Retrieves the state of the resulting model that represents the given memory and model state. // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable). - uint_fast64_t const& getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const; + uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const; private: // Computes for each pair of memory state and model transition index the successor memory state // The resulting vector maps (modelTransition * memoryStateCount) + memoryState to the corresponding successor state of the memory structure - std::vector computeMemorySuccessors() const; + std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model - storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const; + storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const; // Methods that build the model components // Matrix for deterministic models - storm::storage::SparseMatrix buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; // Matrix for nondeterministic models - storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; // Reward models - std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; + std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; // Builds the resulting model std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) - std::vector toResultStateMapping; + std::vector toResultStateMapping; storm::models::sparse::Model const& model; From 43642fef847959dbdb7cb293aa5f468508be4116 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 16:41:28 +0200 Subject: [PATCH 03/19] Improved product of model and memory structure: We can now enforce that certain states are considered reachable. --- .../SparseModelMemoryProduct.cpp | 69 +++++++++++-------- .../SparseModelMemoryProduct.h | 23 ++++--- 2 files changed, 56 insertions(+), 36 deletions(-) diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 2ad64c746..7e7c4af5b 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -19,9 +19,21 @@ namespace storm { template SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { - // intentionally left empty + reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memory.getNumberOfStates(), false); } - + + template + void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { + reachableStates.set(modelState * memory.getNumberOfStates() + memoryState, true); + } + + template + void SparseModelMemoryProduct::setBuildFullProduct() { + reachableStates.clear(); + reachableStates.complement(); + } + + template std::shared_ptr> SparseModelMemoryProduct::build() { uint64_t modelStateCount = model.getNumberOfStates(); @@ -38,7 +50,7 @@ namespace storm { } STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); - storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates); + computeReachableStates(memorySuccessors, initialStates); // Compute the mapping to the states of the result uint64_t reachableStateCount = 0; @@ -50,8 +62,8 @@ namespace storm { // Build the model components storm::storage::SparseMatrix transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ? - buildDeterministicTransitionMatrix(reachableStates, memorySuccessors) : - buildNondeterministicTransitionMatrix(reachableStates, memorySuccessors); + buildDeterministicTransitionMatrix(memorySuccessors) : + buildNondeterministicTransitionMatrix(memorySuccessors); storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); @@ -88,37 +100,38 @@ namespace storm { } template - storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { + void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) { uint64_t memoryStateCount = memory.getNumberOfStates(); // Explore the reachable states via DFS. // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) - storm::storage::BitVector reachableStates = initialStates; - std::vector stack(reachableStates.begin(), reachableStates.end()); - while (!stack.empty()) { - uint64_t stateIndex = stack.back(); - stack.pop_back(); - uint64_t modelState = stateIndex / memoryStateCount; - uint64_t memoryState = stateIndex % memoryStateCount; - - auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); - for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { - if (!storm::utility::isZero(modelTransitionIt->getValue())) { - uint64_t successorModelState = modelTransitionIt->getColumn(); - uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); - uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; - uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; - if (!reachableStates.get(successorStateIndex)) { - reachableStates.set(successorStateIndex, true); - stack.push_back(successorStateIndex); + reachableStates |= initialStates; + if (!reachableStates.full()) { + std::vector stack(reachableStates.begin(), reachableStates.end()); + while (!stack.empty()) { + uint64_t stateIndex = stack.back(); + stack.pop_back(); + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + + auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); + for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { + if (!storm::utility::isZero(modelTransitionIt->getValue())) { + uint64_t successorModelState = modelTransitionIt->getColumn(); + uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); + uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; + uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + if (!reachableStates.get(successorStateIndex)) { + reachableStates.set(successorStateIndex, true); + stack.push_back(successorStateIndex); + } } } } } - return reachableStates; } - + template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResTransitions = 0; @@ -144,7 +157,7 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index b5faf2ab4..55a72172d 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -14,9 +14,7 @@ namespace storm { /*! * This class builds the product of the given sparse model and the given memory structure. * This is similar to the well-known product of a model with a deterministic rabin automaton. - * Note: we already do one memory-structure-step for the initial state, i.e., if s is an initial state of - * the given model and s satisfies memoryStructure.getTransitionMatrix[0][n], then (s,n) will be the corresponding - * initial state of the resulting model. + * The product contains only the reachable states of the product * * The states of the resulting sparse model will have the original state labels plus the labels of this * memory structure. @@ -28,11 +26,18 @@ namespace storm { SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + // Enforces that the given model and memory state as well as the successor(s) are considered reachable -- even if they are not reachable from an initial state. + void addReachableState(uint64_t const& modelState, uint64_t const& memoryState); + + // Enforces that every state is considered reachable. If this is set, the result has size #modelStates * #memoryStates + void setBuildFullProduct(); + // Invokes the building of the product std::shared_ptr> build(); // Retrieves the state of the resulting model that represents the given memory and model state. - // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable). + // Should only be called AFTER calling build(); + // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not part of product). uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const; private: @@ -42,13 +47,13 @@ namespace storm { std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model - storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const; + void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates); // Methods that build the model components // Matrix for deterministic models - storm::storage::SparseMatrix buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const; // Matrix for nondeterministic models - storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const; // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; // Reward models @@ -61,7 +66,9 @@ namespace storm { // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) std::vector toResultStateMapping; - + // Indicates which states are considered reachable. (s, m) is reachable if this BitVector is true at (s * memoryStateCount) + m + storm::storage::BitVector reachableStates; + storm::models::sparse::Model const& model; storm::storage::MemoryStructure const& memory; From 5bdbc00bcd39327ae1452bf2005277f1cfde0f70 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 14 Jul 2017 13:35:48 +0200 Subject: [PATCH 04/19] Changed carlConfig path for shipped carl --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index dd0942e92..b8b9ba12a 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -271,7 +271,7 @@ if(USE_CARL) LOG_INSTALL ON BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT} ) - include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlExport/carlConfig.cmake) + include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlConfig.cmake) set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) From 4351be551210a03147e4f60fd511a2b50d79b23e Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 10:43:34 +0200 Subject: [PATCH 05/19] Allowed building memory product with respect to a scheduler --- src/storm/storage/Distribution.cpp | 12 + src/storm/storage/Distribution.h | 10 +- .../SparseModelMemoryProduct.cpp | 224 +++++++++++++++--- .../SparseModelMemoryProduct.h | 13 +- 4 files changed, 222 insertions(+), 37 deletions(-) diff --git a/src/storm/storage/Distribution.cpp b/src/storm/storage/Distribution.cpp index 0c2ac73db..9d0d89d19 100644 --- a/src/storm/storage/Distribution.cpp +++ b/src/storm/storage/Distribution.cpp @@ -156,6 +156,18 @@ namespace storm { return false; } + template + ValueType Distribution::getProbability(StateType const& state) const { + auto it = this->distribution.find(state); + if (it == this->distribution.end()) { + return storm::utility::zero(); + } else { + return it->second; + } + } + + + template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); template class Distribution; diff --git a/src/storm/storage/Distribution.h b/src/storm/storage/Distribution.h index ff4b0689b..328e87f98 100644 --- a/src/storm/storage/Distribution.h +++ b/src/storm/storage/Distribution.h @@ -73,7 +73,7 @@ namespace storm { * entry is removed. */ void shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); - + /*! * Retrieves an iterator to the elements in this distribution. * @@ -132,6 +132,14 @@ namespace storm { bool less(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const; + + /*! + * Returns the probability of the given state + * @param state The state for which the probability is returned. + * @return The probability of the given state. + */ + ValueType getProbability(StateType const& state) const; + private: // A list of states and the probabilities that are assigned to them. container_type distribution; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 7e7c4af5b..97e601f52 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -32,10 +32,10 @@ namespace storm { reachableStates.clear(); reachableStates.complement(); } - template - std::shared_ptr> SparseModelMemoryProduct::build() { + std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { + uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -50,7 +50,7 @@ namespace storm { } STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); - computeReachableStates(memorySuccessors, initialStates); + computeReachableStates(memorySuccessors, initialStates, scheduler); // Compute the mapping to the states of the result uint64_t reachableStateCount = 0; @@ -61,17 +61,22 @@ namespace storm { } // Build the model components - storm::storage::SparseMatrix transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ? - buildDeterministicTransitionMatrix(memorySuccessors) : - buildNondeterministicTransitionMatrix(memorySuccessors); + storm::storage::SparseMatrix transitionMatrix; + if (scheduler) { + transitionMatrix = buildTransitionMatrixForScheduler(memorySuccessors, scheduler.get()); + } else if (model.getTransitionMatrix().hasTrivialRowGrouping()) { + transitionMatrix = buildDeterministicTransitionMatrix(memorySuccessors); + } else { + transitionMatrix = buildNondeterministicTransitionMatrix(memorySuccessors); + } storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); - std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); + std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); // Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states. labeling.addLabel("init", initialStates % reachableStates); - return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels), scheduler); } @@ -100,7 +105,7 @@ namespace storm { } template - void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) { + void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { uint64_t memoryStateCount = memory.getNumberOfStates(); // Explore the reachable states via DFS. // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) @@ -113,16 +118,37 @@ namespace storm { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; - auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); - for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { - if (!storm::utility::isZero(modelTransitionIt->getValue())) { - uint64_t successorModelState = modelTransitionIt->getColumn(); - uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); - uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; - uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; - if (!reachableStates.get(successorStateIndex)) { - reachableStates.set(successorStateIndex, true); - stack.push_back(successorStateIndex); + if (scheduler) { + auto choices = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution(); + uint64_t groupStart = model.getTransitionMatrix().getRowGroupIndices()[modelState]; + for (auto const& choice : choices) { + STORM_LOG_ASSERT(groupStart + choice.first < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1], "Invalid choice " << choice.first << " at model state " << modelState << "."); + auto const& row = model.getTransitionMatrix().getRow(groupStart + choice.first); + for (auto modelTransitionIt = row.begin(); modelTransitionIt != row.end(); ++modelTransitionIt) { + if (!storm::utility::isZero(modelTransitionIt->getValue())) { + uint64_t successorModelState = modelTransitionIt->getColumn(); + uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); + uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; + uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + if (!reachableStates.get(successorStateIndex)) { + reachableStates.set(successorStateIndex, true); + stack.push_back(successorStateIndex); + } + } + } + } + } else { + auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); + for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { + if (!storm::utility::isZero(modelTransitionIt->getValue())) { + uint64_t successorModelState = modelTransitionIt->getColumn(); + uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); + uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; + uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + if (!reachableStates.get(successorStateIndex)) { + reachableStates.set(successorStateIndex, true); + stack.push_back(successorStateIndex); + } } } } @@ -190,6 +216,101 @@ namespace storm { return builder.build(); } + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = reachableStates.getNumberOfSetBits(); + uint64_t numResChoices = 0; + uint64_t numResTransitions = 0; + bool hasTrivialNondeterminism = true; + for (auto const& stateIndex : reachableStates) { + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + storm::storage::SchedulerChoice choice = scheduler.getChoice(modelState, memoryState); + if (choice.isDefined()) { + ++numResChoices; + if (choice.isDeterministic()) { + uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choice.getDeterministicChoice(); + numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); + } else { + std::set successors; + for (auto const& choiceIndex : choice.getChoiceAsDistribution()) { + if (!storm::utility::isZero(choiceIndex.second)) { + uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choiceIndex.first; + for (auto const& entry : model.getTransitionMatrix().getRow(modelRow)) { + successors.insert(entry.getColumn()); + } + } + } + numResTransitions += successors.size(); + } + } else { + uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; + uint64_t groupEnd = model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; + hasTrivialNondeterminism = hasTrivialNondeterminism && (groupEnd == modelRow + 1); + for (; groupEnd; ++modelRow) { + ++numResChoices; + numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); + } + } + } + + storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, !hasTrivialNondeterminism, hasTrivialNondeterminism ? 0 : numResStates); + uint64_t currentRow = 0; + for (auto const& stateIndex : reachableStates) { + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + if (!hasTrivialNondeterminism) { + builder.newRowGroup(currentRow); + } + storm::storage::SchedulerChoice choice = scheduler.getChoice(modelState, memoryState); + if (choice.isDefined()) { + if (choice.isDeterministic()) { + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choice.getDeterministicChoice(); + auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); + for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); + } + } else { + std::map transitions; + for (auto const& choiceIndex : choice.getChoiceAsDistribution()) { + if (!storm::utility::isZero(choiceIndex.second)) { + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choiceIndex.first; + auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); + for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + ValueType transitionValue = choiceIndex.second * entryIt->getValue(); + auto insertionRes = transitions.insert(std::make_pair(getResultState(entryIt->getColumn(), successorMemoryState), transitionValue)); + if (!insertionRes.second) { + insertionRes.first->second += transitionValue; + } + } + } + } + for (auto const& transition : transitions) { + builder.addNextValue(currentRow, transition.first, transition.second); + } + } + ++currentRow; + } else { + for (uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { + auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); + for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); + } + ++currentRow; + } + } + } + + return builder.build(); + } + template storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { uint64_t modelStateCount = model.getNumberOfStates(); @@ -231,7 +352,7 @@ namespace storm { } template - std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { + std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const { std::unordered_map> result; uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); @@ -269,7 +390,12 @@ namespace storm { uint64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { - stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; + if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { + ValueType factor = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution().getProbability(rowOffset); + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState]] = factor * modelStateActionReward; + } else { + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; + } } } } @@ -285,14 +411,42 @@ namespace storm { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); - for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { - uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; - uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; - auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex); - for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) { - uint64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; - builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); + if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { + std::map rewards; + for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + auto transitionEntryIt = model.getTransitionMatrix().getRow(modelRowIndex).begin(); + for (auto const& rewardEntry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { + while (transitionEntryIt->getColumn() != rewardEntry.getColumn()) { + STORM_LOG_ASSERT(transitionEntryIt != model.getTransitionMatrix().getRow(modelRowIndex).end(), "The reward transition matrix is not a submatrix of the model transition matrix."); + ++transitionEntryIt; + } + uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + auto insertionRes = rewards.insert(std::make_pair(getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue())); + if (!insertionRes.second) { + insertionRes.first->second += rewardEntry.getValue(); + } + } + } + uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState]; + for (auto& reward : rewards) { + builder.addNextValue(resRowIndex, reward.first, reward.second); + } + } else { + for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + auto transitionEntryIt = model.getTransitionMatrix().getRow(modelRowIndex).begin(); + for (auto const& rewardEntry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { + while (transitionEntryIt->getColumn() != rewardEntry.getColumn()) { + STORM_LOG_ASSERT(transitionEntryIt != model.getTransitionMatrix().getRow(modelRowIndex).end(), "The reward transition matrix is not a submatrix of the model transition matrix."); + ++transitionEntryIt; + } + uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(resRowIndex, getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue()); + } } } } @@ -306,7 +460,7 @@ namespace storm { } template - std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const { + std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const { storm::storage::sparse::ModelComponents> components (std::move(matrix), std::move(labeling), std::move(rewardModels)); if (model.isOfType(storm::models::ModelType::Ctmc)) { @@ -337,7 +491,15 @@ namespace storm { components.exitRates = std::move(resultExitRates); } - return storm::utility::builder::buildModelFromComponents(model.getType(), std::move(components)); + storm::models::ModelType resultType = model.getType(); + if (scheduler && !scheduler->isPartialScheduler()) { + if (model.isOfType(storm::models::ModelType::Mdp)) { + resultType = storm::models::ModelType::Dtmc; + } + // Note that converting deterministic MAs to CTMCs via state elimination does not preserve all properties (e.g. step bounded) + } + + return storm::utility::builder::buildModelFromComponents(resultType, std::move(components)); } template class SparseModelMemoryProduct; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 55a72172d..b37527542 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -8,6 +8,7 @@ #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/Scheduler.h" namespace storm { namespace storage { @@ -32,8 +33,8 @@ namespace storm { // Enforces that every state is considered reachable. If this is set, the result has size #modelStates * #memoryStates void setBuildFullProduct(); - // Invokes the building of the product - std::shared_ptr> build(); + // Invokes the building of the product under the specified scheduler (if given). + std::shared_ptr> build(boost::optional> const& scheduler = boost::none); // Retrieves the state of the resulting model that represents the given memory and model state. // Should only be called AFTER calling build(); @@ -47,20 +48,22 @@ namespace storm { std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model - void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates); + void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler); // Methods that build the model components // Matrix for deterministic models storm::storage::SparseMatrix buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const; // Matrix for nondeterministic models storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const; + // Matrix for models that consider a scheduler + storm::storage::SparseMatrix buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const; // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; // Reward models - std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; + std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const; // Builds the resulting model - std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const; + std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) From 4251c9f5252508e9ed8fa4a4907ff263dcad74e4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 10:56:28 +0200 Subject: [PATCH 06/19] added function to build a trivial memory structure --- .../multiobjective/SparseMultiObjectivePreprocessor.cpp | 4 +--- .../storage/memorystructure/MemoryStructureBuilder.cpp | 7 +++++++ src/storm/storage/memorystructure/MemoryStructureBuilder.h | 5 +++++ 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 0596303c8..09f0fdc6a 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -69,9 +69,7 @@ namespace storm { template SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { - storm::storage::MemoryStructureBuilder memoryBuilder(1, model); - memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); - memory = std::make_shared(memoryBuilder.build()); + memory = std::make_shared(storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model)); // The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names memoryLabelPrefix = "mem"; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 9ee23eaa6..696e9662a 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -83,6 +83,13 @@ namespace storm { return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates)); } + template + MemoryStructure MemoryStructureBuilder::buildTrivialMemoryStructure(storm::models::sparse::Model const& model) { + MemoryStructureBuilder memoryBuilder(1, model); + memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); + return memoryBuilder.build(); + } + template class MemoryStructureBuilder; template class MemoryStructureBuilder; template class MemoryStructureBuilder; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index 9fbe65c78..1cb51f384 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -57,6 +57,11 @@ namespace storm { */ MemoryStructure build(); + /*! + * Builds a trivial memory structure for the given model (consisting of a single memory state) + */ + static MemoryStructure buildTrivialMemoryStructure(storm::models::sparse::Model const& model); + private: storm::models::sparse::Model const& model; From 7bd9ef798f827e2f0c48305295b0dd6189d87cc9 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 10:57:07 +0200 Subject: [PATCH 07/19] returning the memory structure of a scheduler --- src/storm/storage/Scheduler.cpp | 5 +++++ src/storm/storage/Scheduler.h | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index a1dc1ecbd..7ddc7e457 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -86,6 +86,11 @@ namespace storm { return memoryStructure ? memoryStructure->getNumberOfStates() : 1; } + template + boost::optional const& Scheduler::getMemoryStructure() const { + return memoryStructure; + } + template void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index c1c3a5f88..b51e308b9 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -70,6 +70,11 @@ namespace storm { * Retrieves the number of memory states this scheduler considers. */ uint_fast64_t getNumberOfMemoryStates() const; + + /*! + * Retrieves the memory structure associated with this scheduler + */ + boost::optional const& getMemoryStructure() const; /*! * Returns a copy of this scheduler with the new value type From a348f6ea8e828aa7de690250c157d45b9bc6caed Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 11:24:24 +0200 Subject: [PATCH 08/19] function to apply a given scheduler to a nondeterministic model --- .../models/sparse/NondeterministicModel.cpp | 20 +++++++++++++++++++ .../models/sparse/NondeterministicModel.h | 14 +++++++++++++ 2 files changed, 34 insertions(+) diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index e823d455a..5b5aebe89 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -2,6 +2,9 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/storage/Scheduler.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -46,6 +49,23 @@ namespace storm { } } + template + std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { + boost::optional> memoryProduct; + if (scheduler.isMemorylessScheduler()) { + storm::storage::MemoryStructure memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); + memoryProduct = memStruct.product(*this); + } else { + boost::optional const& memStruct = scheduler.getMemoryStructure(); + STORM_LOG_ASSERT(memStruct, "Memoryless scheduler without memory structure."); + memoryProduct = memStruct->product(*this); + } + if (!dropUnreachableStates) { + memoryProduct->setBuildFullProduct(); + } + return memoryProduct->build(scheduler); + } + template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 1f2bd157a..ab0a21a04 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -5,6 +5,13 @@ #include "storm/utility/OsDetection.h" namespace storm { + + // Forward declare Scheduler class. + namespace storage { + template + class Scheduler; + } + namespace models { namespace sparse { @@ -48,6 +55,13 @@ namespace storm { virtual void reduceToStateBasedRewards() override; + /*! + * Applies the given scheduler to this model. + * @param scheduler the considered scheduler. + * @param dropUnreachableStates if set, the resulting model only considers the states that are reachable from an initial state + */ + std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates = true); + virtual void printModelInformationToStream(std::ostream& out) const override; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; From 6af15f3a0d32f17dd624a7486989e52d9557a98a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 11:29:34 +0200 Subject: [PATCH 09/19] Memory Structure Product with custom reward model type --- .../memorystructure/MemoryStructure.cpp | 8 +- .../storage/memorystructure/MemoryStructure.h | 7 +- .../MemoryStructureBuilder.cpp | 1 + .../SparseModelMemoryProduct.cpp | 88 ++++++++++--------- .../SparseModelMemoryProduct.h | 12 +-- 5 files changed, 62 insertions(+), 54 deletions(-) diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index 3d9348c44..499bc4db6 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -106,9 +106,9 @@ namespace storm { return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling), std::move(resultInitialMemoryStates)); } - template - SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const { - return SparseModelMemoryProduct(sparseModel, *this); + template + SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const { + return SparseModelMemoryProduct(sparseModel, *this); } std::string MemoryStructure::toString() const { @@ -143,7 +143,9 @@ namespace storm { } template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; + template SparseModelMemoryProduct> MemoryStructure::product(storm::models::sparse::Model> const& sparseModel) const; template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; + template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; } } diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index 9df320fd3..64bd7aaa9 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -6,11 +6,12 @@ #include "storm/logic/Formula.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/Model.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace storage { - template + template class SparseModelMemoryProduct; /*! @@ -53,8 +54,8 @@ namespace storm { * Builds the product of this memory structure and the given sparse model. * An exception is thrown if the state labelings of this memory structure and the given model are not disjoint. */ - template - SparseModelMemoryProduct product(storm::models::sparse::Model const& sparseModel) const; + template > + SparseModelMemoryProduct product(storm::models::sparse::Model const& sparseModel) const; std::string toString() const; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 696e9662a..148cbf2ca 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -91,6 +91,7 @@ namespace storm { } template class MemoryStructureBuilder; + template class MemoryStructureBuilder>; template class MemoryStructureBuilder; template class MemoryStructureBuilder; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 97e601f52..58f773cfe 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -17,24 +17,24 @@ namespace storm { namespace storage { - template - SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { + template + SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memory.getNumberOfStates(), false); } - template - void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { + template + void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { reachableStates.set(modelState * memory.getNumberOfStates() + memoryState, true); } - template - void SparseModelMemoryProduct::setBuildFullProduct() { + template + void SparseModelMemoryProduct::setBuildFullProduct() { reachableStates.clear(); reachableStates.complement(); } - template - std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { + template + std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -70,7 +70,7 @@ namespace storm { transitionMatrix = buildNondeterministicTransitionMatrix(memorySuccessors); } storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); - std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); + std::unordered_map rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); // Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states. labeling.addLabel("init", initialStates % reachableStates); @@ -80,13 +80,13 @@ namespace storm { } - template - uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { + template + uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } - template - std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { + template + std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); uint64_t memoryStateCount = memory.getNumberOfStates(); std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); @@ -104,8 +104,8 @@ namespace storm { return result; } - template - void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { + template + void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { uint64_t memoryStateCount = memory.getNumberOfStates(); // Explore the reachable states via DFS. // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) @@ -156,8 +156,8 @@ namespace storm { } } - template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResTransitions = 0; @@ -182,8 +182,8 @@ namespace storm { return builder.build(); } - template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; @@ -216,8 +216,8 @@ namespace storm { return builder.build(); } - template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; @@ -311,8 +311,8 @@ namespace storm { return builder.build(); } - template - storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { + template + storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -351,16 +351,19 @@ namespace storm { return resultLabeling; } - template - std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const { - std::unordered_map> result; + template + std::unordered_map SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const { + + typedef typename RewardModelType::ValueType RewardValueType; + + std::unordered_map result; uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); for (auto const& rewardModel : model.getRewardModels()) { - boost::optional> stateRewards; + boost::optional> stateRewards; if (rewardModel.second.hasStateRewards()) { - stateRewards = std::vector(numResStates, storm::utility::zero()); + stateRewards = std::vector(numResStates, storm::utility::zero()); uint64_t modelState = 0; for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { if (!storm::utility::isZero(modelStateReward)) { @@ -375,9 +378,9 @@ namespace storm { ++modelState; } } - boost::optional> stateActionRewards; + boost::optional> stateActionRewards; if (rewardModel.second.hasStateActionRewards()) { - stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); + stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); uint64_t modelState = 0; uint64_t modelRow = 0; for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { @@ -402,9 +405,9 @@ namespace storm { ++modelRow; } } - boost::optional> transitionRewards; + boost::optional> transitionRewards; if (rewardModel.second.hasTransitionRewards()) { - storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); + storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { if (resState < numResStates) { @@ -412,7 +415,7 @@ namespace storm { uint64_t memoryState = stateIndex % memoryStateCount; uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { - std::map rewards; + std::map rewards; for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; auto transitionEntryIt = model.getTransitionMatrix().getRow(modelRowIndex).begin(); @@ -454,14 +457,14 @@ namespace storm { } transitionRewards = builder.build(); } - result.insert(std::make_pair(rewardModel.first, storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); + result.insert(std::make_pair(rewardModel.first, RewardModelType(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); } return result; } - template - std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const { - storm::storage::sparse::ModelComponents> components (std::move(matrix), std::move(labeling), std::move(rewardModels)); + template + std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels, boost::optional> const& scheduler) const { + storm::storage::sparse::ModelComponents components (std::move(matrix), std::move(labeling), std::move(rewardModels)); if (model.isOfType(storm::models::ModelType::Ctmc)) { components.rateTransitions = true; @@ -472,8 +475,8 @@ namespace storm { std::vector resultExitRates; resultExitRates.reserve(components.transitionMatrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); - auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); - auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); + auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); + auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { @@ -502,9 +505,10 @@ namespace storm { return storm::utility::builder::buildModelFromComponents(resultType, std::move(components)); } - template class SparseModelMemoryProduct; - template class SparseModelMemoryProduct; - template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct>; + template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct; } } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index b37527542..fb959daa5 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -21,11 +21,11 @@ namespace storm { * memory structure. * An exception is thrown if the state labelings are not disjoint. */ - template + template > class SparseModelMemoryProduct { public: - SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); // Enforces that the given model and memory state as well as the successor(s) are considered reachable -- even if they are not reachable from an initial state. void addReachableState(uint64_t const& modelState, uint64_t const& memoryState); @@ -34,7 +34,7 @@ namespace storm { void setBuildFullProduct(); // Invokes the building of the product under the specified scheduler (if given). - std::shared_ptr> build(boost::optional> const& scheduler = boost::none); + std::shared_ptr> build(boost::optional> const& scheduler = boost::none); // Retrieves the state of the resulting model that represents the given memory and model state. // Should only be called AFTER calling build(); @@ -60,10 +60,10 @@ namespace storm { // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; // Reward models - std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const; + std::unordered_map buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const; // Builds the resulting model - std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const; + std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels, boost::optional> const& scheduler) const; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) @@ -72,7 +72,7 @@ namespace storm { // Indicates which states are considered reachable. (s, m) is reachable if this BitVector is true at (s * memoryStateCount) + m storm::storage::BitVector reachableStates; - storm::models::sparse::Model const& model; + storm::models::sparse::Model const& model; storm::storage::MemoryStructure const& memory; }; From 5651b237714e705aee4912a216be53d398cdb227 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 11:58:07 +0200 Subject: [PATCH 10/19] fixing minor compiling issue --- .../models/sparse/NondeterministicModel.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 5b5aebe89..32839a630 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -51,19 +51,21 @@ namespace storm { template std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { - boost::optional> memoryProduct; if (scheduler.isMemorylessScheduler()) { - storm::storage::MemoryStructure memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); - memoryProduct = memStruct.product(*this); + auto memoryProduct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this).product(*this); + if (!dropUnreachableStates) { + memoryProduct.setBuildFullProduct(); + } + return memoryProduct.build(scheduler); } else { boost::optional const& memStruct = scheduler.getMemoryStructure(); STORM_LOG_ASSERT(memStruct, "Memoryless scheduler without memory structure."); - memoryProduct = memStruct->product(*this); - } - if (!dropUnreachableStates) { - memoryProduct->setBuildFullProduct(); + auto memoryProduct = memStruct->product(*this); + if (!dropUnreachableStates) { + memoryProduct.setBuildFullProduct(); + } + return memoryProduct.build(scheduler); } - return memoryProduct->build(scheduler); } template From e8e189723fe6c6e1e7db182ad83f21065981fdc2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 13:06:05 +0200 Subject: [PATCH 11/19] fixed applying memoryless schedulers --- src/storm/models/sparse/NondeterministicModel.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 32839a630..3382bfd95 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -52,7 +52,8 @@ namespace storm { template std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { if (scheduler.isMemorylessScheduler()) { - auto memoryProduct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this).product(*this); + auto memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); + auto memoryProduct = memStruct.product(*this); if (!dropUnreachableStates) { memoryProduct.setBuildFullProduct(); } From d35a5e4bdd5cf2fef83341728ff00a18068ab482 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Jul 2017 11:39:37 +0200 Subject: [PATCH 12/19] returning the time bound type from a timeBoundReference --- src/storm/logic/TimeBoundType.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index 7200cc89d..0bd6aba0c 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -24,7 +24,10 @@ namespace storm { assert(rewardName != ""); // Empty reward name is reserved. } - + TimeBoundType getType() const { + return type; + } + bool isStepBound() const { return type == TimeBoundType::Steps; } From defcd7d5d72a6649ecbf786a5ae1569bfbd384c6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Jul 2017 11:42:06 +0200 Subject: [PATCH 13/19] Multi-objective model checking: adapted data structures to allow more general objectives --- .../modelchecker/multiobjective/Objective.h | 48 +---- .../SparseMultiObjectivePreprocessor.cpp | 196 +++++++++--------- .../SparseMultiObjectivePreprocessor.h | 19 +- .../SparseMultiObjectivePreprocessorTask.h | 16 +- .../SparseCbAchievabilityQuery.cpp | 56 +++-- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 96 ++++----- .../pcaa/SparseMdpPcaaWeightVectorChecker.cpp | 31 ++- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 15 +- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 22 +- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 6 +- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 39 ++-- 11 files changed, 260 insertions(+), 284 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h index d5d269775..6b1f44f1f 100644 --- a/src/storm/modelchecker/multiobjective/Objective.h +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -13,57 +13,27 @@ namespace storm { namespace multiobjective { template struct Objective { + // the original input formula std::shared_ptr originalFormula; - // the name of the considered reward model in the preprocessedModel - boost::optional rewardModelName; + // The preprocessed (simplified) formula + std::shared_ptr formula; // True iff the complementary event is considered. // E.g. if we consider P<1-t [F !"safe"] instead of P>=t [ G "safe"] bool considersComplementaryEvent; - // The probability/reward threshold for the preprocessed model (if originalFormula specifies one). - boost::optional bound; - // The optimization direction for the preprocessed model - // if originalFormula does ot specifies one, the direction is derived from the bound. - storm::solver::OptimizationDirection optimizationDirection; - - // Lower and upper time/step/reward bouds - boost::optional lowerTimeBound, upperTimeBound; - boost::optional timeBoundReference; - + // Limitations for the quantitative objective value (e.g. 0 <= value <= 1 for probabilities). + // Can be used to guide the underlying solver boost::optional lowerResultBound, upperResultBound; void printToStream(std::ostream& out) const { - out << originalFormula->toString(); - out << " \t"; - out << "direction: "; - out << optimizationDirection; - out << " \t"; - out << "intern bound: "; - if (bound){ - out << *bound; - } else { - out << " -none- "; - } + out << "Original: " << *originalFormula; out << " \t"; - out << "time bounds: "; - if (lowerTimeBound && upperTimeBound) { - out << (lowerTimeBound->isStrict() ? "(" : "[") << lowerTimeBound->getBound() << "," << upperTimeBound->getBound() << (upperTimeBound->isStrict() ? ")" : "]"); - } else if (lowerTimeBound) { - out << (lowerTimeBound->isStrict() ? ">" : ">=") << lowerTimeBound->getBound(); - } else if (upperTimeBound) { - out << (upperTimeBound->isStrict() ? "<" : "<=") << upperTimeBound->getBound(); - } else { - out << " -none- "; - } - out << " \t"; - out << "intern reward model: "; - if (rewardModelName) { - out << *rewardModelName; - } else { - out << " -none- "; + out << "Preprocessed: " << *formula; + if (considersComplementaryEvent) { + out << " (Complementary event)"; } out << " \t"; out << "result bounds: "; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 09f0fdc6a..7d359a5ab 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -113,80 +113,81 @@ namespace storm { Objective& objective = *data.objectives.back(); - objective.considersComplementaryEvent = false; + // Check whether the complementary event is considered + objective.considersComplementaryEvent = formula.isProbabilityOperatorFormula() && formula.getSubformula().isGloballyFormula(); + storm::logic::OperatorInformation opInfo; if (formula.hasBound()) { - STORM_LOG_THROW(!formula.getBound().threshold.containsVariables(), storm::exceptions::InvalidPropertyException, "The formula " << formula << "considers a non-constant threshold"); - objective.bound = formula.getBound(); - if (storm::logic::isLowerBound(formula.getBound().comparisonType)) { - objective.optimizationDirection = storm::solver::OptimizationDirection::Maximize; - } else { - objective.optimizationDirection = storm::solver::OptimizationDirection::Minimize; - } - STORM_LOG_WARN_COND(!formula.hasOptimalityType() || formula.getOptimalityType() == objective.optimizationDirection, "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold."); - } else if (formula.hasOptimalityType()){ - objective.optimizationDirection = formula.getOptimalityType(); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); - } - - if (formula.isProbabilityOperatorFormula()){ - preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), data); - } else if (formula.isRewardOperatorFormula()){ - preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), data); - } else if (formula.isTimeOperatorFormula()){ - preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), data); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); - } - - // Invert the bound and optimization direction (if necessary) - if (objective.considersComplementaryEvent) { - if (objective.bound) { - objective.bound->threshold = objective.bound->threshold.getManager().rational(storm::utility::one()) - objective.bound->threshold; - switch (objective.bound->comparisonType) { + opInfo.bound = formula.getBound(); + // Invert the bound (if necessary) + if (objective.considersComplementaryEvent) { + opInfo.bound->threshold = opInfo.bound->threshold.getManager().rational(storm::utility::one()) - opInfo.bound->threshold; + switch (opInfo.bound->comparisonType) { case storm::logic::ComparisonType::Greater: - objective.bound->comparisonType = storm::logic::ComparisonType::Less; + opInfo.bound->comparisonType = storm::logic::ComparisonType::Less; break; case storm::logic::ComparisonType::GreaterEqual: - objective.bound->comparisonType = storm::logic::ComparisonType::LessEqual; + opInfo.bound->comparisonType = storm::logic::ComparisonType::LessEqual; break; case storm::logic::ComparisonType::Less: - objective.bound->comparisonType = storm::logic::ComparisonType::Greater; + opInfo.bound->comparisonType = storm::logic::ComparisonType::Greater; break; case storm::logic::ComparisonType::LessEqual: - objective.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; + opInfo.bound->comparisonType = storm::logic::ComparisonType::GreaterEqual; break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " has unexpected comparison type"); } } - objective.optimizationDirection = storm::solver::invert(objective.optimizationDirection); + if (storm::logic::isLowerBound(opInfo.bound->comparisonType)) { + opInfo.optimalityType = storm::solver::OptimizationDirection::Maximize; + } else { + opInfo.optimalityType = storm::solver::OptimizationDirection::Minimize; + } + STORM_LOG_WARN_COND(!formula.hasOptimalityType(), "Optimization direction of formula " << formula << " ignored as the formula also specifies a threshold."); + } else if (formula.hasOptimalityType()){ + opInfo.optimalityType = formula.getOptimalityType(); + // Invert the optimality type (if necessary) + if (objective.considersComplementaryEvent) { + opInfo.optimalityType = storm::solver::invert(opInfo.optimalityType.get()); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Objective " << formula << " does not specify whether to minimize or maximize"); + } + + if (formula.isProbabilityOperatorFormula()){ + preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), opInfo, data); + } else if (formula.isRewardOperatorFormula()){ + preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), opInfo, data); + } else if (formula.isTimeOperatorFormula()){ + preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), opInfo, data); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); } } template - void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { // Probabilities are between zero and one data.objectives.back()->lowerResultBound = storm::utility::zero(); data.objectives.back()->upperResultBound = storm::utility::one(); if (formula.getSubformula().isUntilFormula()){ - preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data); + preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data); } else if (formula.getSubformula().isBoundedUntilFormula()){ - preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), data); + preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data); } else if (formula.getSubformula().isGloballyFormula()){ - preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), data); + preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data); } else if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparseMultiObjectivePreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { STORM_LOG_THROW((formula.hasRewardModelName() && data.originalModel.hasRewardModel(formula.getRewardModelName())) || (!formula.hasRewardModelName() && data.originalModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model is not unique or the formula " << formula << " does not specify an existing reward model."); @@ -203,43 +204,39 @@ namespace storm { data.objectives.back()->lowerResultBound = storm::utility::zero(); if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data, rewardModelName); } else if (formula.getSubformula().isCumulativeRewardFormula()) { - preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), data, rewardModelName); + preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), opInfo, data, rewardModelName); } else if (formula.getSubformula().isTotalRewardFormula()) { - preprocessTotalRewardFormula(data, rewardModelName); + preprocessTotalRewardFormula(opInfo, data, rewardModelName); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparseMultiObjectivePreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { // Time formulas are only supported for Markov automata STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); data.objectives.back()->lowerResultBound = storm::utility::zero(); if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), opInfo, data); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data) { + void SparseMultiObjectivePreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr subformula) { storm::modelchecker::SparsePropositionalModelChecker mc(data.originalModel); storm::storage::BitVector rightSubformulaResult = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector leftSubformulaResult = mc.check(formula.getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Check if the formula is already satisfied in the initial state because then the transformation to expected rewards will fail. - if (!data.objectives.back()->lowerTimeBound) { - if (!(data.originalModel.getInitialStates() & rightSubformulaResult).empty()) { - // TODO: Handle this case more properly - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented."); - } - } + // TODO: Handle this case more properly + STORM_LOG_THROW((data.originalModel.getInitialStates() & rightSubformulaResult).empty(), storm::exceptions::NotImplementedException, "The Probability for the objective " << *data.objectives.back()->originalFormula << " is always one as the rhs of the until formula is true in the initial state. This (trivial) case is currently not implemented."); // Create a memory structure that stores whether a non-PhiState or a PsiState has already been reached storm::storage::MemoryStructureBuilder builder(2, data.originalModel); @@ -255,7 +252,11 @@ namespace storm { storm::storage::MemoryStructure objectiveMemory = builder.build(); data.memory = std::make_shared(data.memory->product(objectiveMemory)); - data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + if (subformula == nullptr) { + subformula = std::make_shared(); + } + data.objectives.back()->formula = std::make_shared(subformula, rewardModelName, opInfo); auto relevantStatesFormula = std::make_shared(relevantStatesLabel); data.tasks.push_back(std::make_shared>(data.objectives.back(), relevantStatesFormula, formula.getRightSubformula().asSharedPointer())); @@ -263,38 +264,37 @@ namespace storm { } template - void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { - if (formula.hasLowerBound()) { - STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); - if (!storm::utility::isZero(formula.getLowerBound()) || formula.isLowerBoundStrict()) { - data.objectives.back()->lowerTimeBound = storm::logic::TimeBound(formula.isLowerBoundStrict(), formula.getLowerBound()); - } - } - if (formula.hasUpperBound()) { - STORM_LOG_THROW(!formula.getUpperBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The Upper time bound for the formula " << formula << " still contains variables"); - if (!storm::utility::isInfinity(formula.getUpperBound())) { - data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound()); + void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { + + // Check how to handle this query + if (!formula.getTimeBoundReference().isRewardBound() && (!formula.hasLowerBound() || (!formula.isLowerBoundStrict() && storm::utility::isZero(formula.template getLowerBound())))) { + std::shared_ptr subformula; + if (!formula.hasUpperBound()) { + // The formula is actually unbounded + subformula = std::make_shared(); + } else { + STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || formula.getTimeBoundReference().isTimeBound(), storm::exceptions::InvalidPropertyException, "Bounded until formulas for Markov Automata are only allowed when time bounds are considered."); + storm::logic::TimeBound bound(formula.isUpperBoundStrict(), formula.getUpperBound()); + subformula = std::make_shared(bound, formula.getTimeBoundReference().getType()); } + preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), opInfo, data, subformula); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property " << formula << "is not supported"); } - - data.objectives.back()->timeBoundReference = formula.getTimeBoundReference(); - preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data); } template - void SparseMultiObjectivePreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data) { - // The formula will be transformed to an until formula for the complementary event. - data.objectives.back()->considersComplementaryEvent = true; - + void SparseMultiObjectivePreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { + // The formula is transformed to an until formula for the complementary event. auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data); + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), opInfo, data); } template - void SparseMultiObjectivePreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + void SparseMultiObjectivePreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { if (formula.isReachabilityProbabilityFormula()){ - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data); + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), opInfo, data); return; } @@ -318,7 +318,9 @@ namespace storm { auto relevantStatesFormula = std::make_shared(relevantStatesLabel); - data.objectives.back()->rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + std::string auxRewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + auto totalRewardFormula = std::make_shared(); + data.objectives.back()->formula = std::make_shared(totalRewardFormula, auxRewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); if (formula.isReachabilityRewardFormula()) { @@ -334,23 +336,19 @@ namespace storm { } template - void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - STORM_LOG_THROW(!formula.getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The time bound for the formula " << formula << " still contains variables"); - if (!storm::utility::isInfinity(formula.getBound())) { - data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isBoundStrict(), formula.getBound()); - } - - assert(optionalRewardModelName.is_initialized()); - data.objectives.back()->rewardModelName = *optionalRewardModelName; - + storm::logic::TimeBound bound(formula.isBoundStrict(), formula.getBound()); + auto cumulativeRewardFormula = std::make_shared(bound, storm::logic::TimeBoundType::Steps); + data.objectives.back()->formula = std::make_shared(cumulativeRewardFormula, *optionalRewardModelName, opInfo); } template - void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName) { - assert(optionalRewardModelName.is_initialized()); - data.objectives.back()->rewardModelName = *optionalRewardModelName; + void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + + auto totalRewardFormula = std::make_shared(); + data.objectives.back()->formula = std::make_shared(totalRewardFormula, *optionalRewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); } @@ -372,9 +370,10 @@ namespace storm { std::set relevantRewardModels; for (auto const& obj : result.objectives) { - relevantRewardModels.insert(*obj.rewardModelName); - if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) { - relevantRewardModels.insert(obj.timeBoundReference->getRewardName()); + if (obj.formula->isRewardOperatorFormula()) { + relevantRewardModels.insert(obj.formula->asRewardOperatorFormula().getRewardModelName()); + } else { + STORM_LOG_ASSERT(false, "Unknown formula type."); } } @@ -407,7 +406,7 @@ namespace storm { typename SparseMultiObjectivePreprocessor::ReturnType::QueryType SparseMultiObjectivePreprocessor::getQueryType(std::vector> const& objectives) { uint_fast64_t numOfObjectivesWithThreshold = 0; for (auto& obj : objectives) { - if (obj.bound) { + if (obj.formula->hasBound()) { ++numOfObjectivesWithThreshold; } } @@ -434,8 +433,12 @@ namespace storm { // Get the choices that yield non-zero reward storm::storage::BitVector zeroRewardChoices(result.preprocessedModel->getNumberOfChoices(), true); for (auto const& obj : result.objectives) { - auto const& rewModel = result.preprocessedModel->getRewardModel(*obj.rewardModelName); - zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + if (obj.formula->isRewardOperatorFormula()) { + auto const& rewModel = result.preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName()); + zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions); + } else { + STORM_LOG_ASSERT(false, "Unknown formula type."); + } } // Get the states that have reward for at least one (or for all) choices assigned to it. @@ -476,8 +479,9 @@ namespace storm { storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true); bool hasMinRewardToCheck = false; for (auto const& objIndex : finiteRewardCheckObjectives) { - auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].rewardModelName.get()); - if (storm::solver::minimize(result.objectives[objIndex].optimizationDirection)) { + STORM_LOG_ASSERT(result.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator."); + auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); + if (storm::solver::minimize(result.objectives[objIndex].formula->getOptimalityType())) { hasMinRewardToCheck = true; } else { maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions); diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 318433575..505431e62 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -50,19 +50,20 @@ namespace storm { /*! * Apply the neccessary preprocessing for the given formula. * @param formula the current (sub)formula + * @param opInfo the information of the resulting operator formula * @param data the current data. The currently processed objective is located at data.objectives.back() * @param optionalRewardModelName the reward model name that is considered for the formula (if available) */ static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data); - static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data); - static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data); - static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, PreprocessorData& data); - static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data); - static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data); - static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data); - static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. + static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr subformula = nullptr); + static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. /*! diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h index e34e37584..f84b935b6 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h @@ -58,8 +58,9 @@ namespace storm { objectiveRewards[row] = preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, goalStates); } } - STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); - preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards))); + STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula."); + STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), typename SparseModelType::RewardModelType(boost::none, std::move(objectiveRewards))); } private: @@ -91,8 +92,9 @@ namespace storm { std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero()); } } - STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); - preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), std::move(objectiveRewards)); + STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula."); + STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), std::move(objectiveRewards)); } private: @@ -117,8 +119,10 @@ namespace storm { std::vector timeRewards(preprocessedModel.getNumberOfStates(), storm::utility::zero()); storm::utility::vector::setVectorValues(timeRewards, dynamic_cast const&>(preprocessedModel).getMarkovianStates() & relevantStates, storm::utility::one()); - STORM_LOG_ASSERT(this->objective->rewardModelName.is_initialized(), "No reward model name has been specified"); - preprocessedModel.addRewardModel(this->objective->rewardModelName.get(), typename SparseModelType::RewardModelType(std::move(timeRewards))); + + STORM_LOG_ASSERT(this->objective->formula->isRewardOperatorFormula(), "No reward operator formula."); + STORM_LOG_ASSERT(this->objective->formula->asRewardOperatorFormula().hasRewardModelName(), "No reward model name has been specified"); + preprocessedModel.addRewardModel(this->objective->formula->asRewardOperatorFormula().getRewardModelName(), typename SparseModelType::RewardModelType(std::move(timeRewards))); } private: diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 86faf88a7..628fbb687 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -26,7 +26,7 @@ namespace storm { template SparseCbAchievabilityQuery::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparseCbQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); + STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager); } @@ -134,36 +134,34 @@ namespace storm { void SparseCbAchievabilityQuery::addObjectiveConstraints() { storm::expressions::Expression zero = this->expressionManager->rational(storm::utility::zero()); for (Objective const& obj : this->objectives) { - if (obj.rewardModelName) { - STORM_LOG_THROW(obj.bound, storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); - STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotSupportedException, "Constraint based method currently does not support step bounds"); - std::vector rewards = getActionBasedExpectedRewards(*obj.rewardModelName); - storm::expressions::Expression objValue = zero; - for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { - if (!storm::utility::isZero(rewards[choice])) { - objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); - } - } - // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division - STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "The threshold for one objective still contains undefined variables"); - storm::expressions::Expression threshold = this->expressionManager->rational(obj.bound->threshold.evaluateAsRational()); - switch (obj.bound->comparisonType) { - case storm::logic::ComparisonType::Greater: - solver->add( objValue > threshold); - break; - case storm::logic::ComparisonType::GreaterEqual: - solver->add( objValue >= threshold); - break; - case storm::logic::ComparisonType::Less: - solver->add( objValue < threshold); - break; - case storm::logic::ComparisonType::LessEqual: - solver->add( objValue <= threshold); - break; - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); + STORM_LOG_THROW(obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::InvalidOperationException, "Constraint-based solver only supports total-reward objectives. Got " << *obj.formula << " instead."); + STORM_LOG_THROW(obj.formula->hasBound(), storm::exceptions::InvalidOperationException, "Invoked achievability query but no bound was specified for at least one objective."); + STORM_LOG_THROW(obj.formula->asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::InvalidOperationException, "Expected reward operator with a reward model name. Got " << *obj.formula << " instead."); + std::vector rewards = getActionBasedExpectedRewards(obj.formula->asRewardOperatorFormula().getRewardModelName()); + storm::expressions::Expression objValue = zero; + for (uint_fast64_t choice = 0; choice < rewards.size(); ++choice) { + if (!storm::utility::isZero(rewards[choice])) { + objValue = objValue + (this->expressionManager->rational(rewards[choice]) * expectedChoiceVariables[choice].getExpression()); } } + // We need to actually evaluate the threshold as rational number. Otherwise a threshold like '<=16/9' might be considered as 1 due to integer division + storm::expressions::Expression threshold = this->expressionManager->rational(obj.formula->getThreshold().evaluateAsRational()); + switch (obj.formula->getBound().comparisonType) { + case storm::logic::ComparisonType::Greater: + solver->add( objValue > threshold); + break; + case storm::logic::ComparisonType::GreaterEqual: + solver->add( objValue >= threshold); + break; + case storm::logic::ComparisonType::Less: + solver->add( objValue < threshold); + break; + case storm::logic::ComparisonType::LessEqual: + solver->add( objValue <= threshold); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "One or more objectives have an invalid comparison type"); + } } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index e65aa6325..e695fa8db 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -8,9 +8,11 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/solver/GmmxxLinearEquationSolver.h" +#include "storm/logic/Formulas.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace modelchecker { @@ -25,13 +27,17 @@ namespace storm { SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { // Set the (discretized) state action rewards. this->discreteActionRewards.resize(objectives.size()); - for(auto objIndex : this->objectivesWithNoUpperTimeBound) { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); + for (auto objIndex : this->objectivesWithNoUpperTimeBound) { + auto const& formula = *objectives[objIndex].formula; + STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula); + STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula() || (formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().isTimeBounded()), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + STORM_LOG_WARN_COND(!formula.getSubformula().isCumulativeRewardFormula() || (objectives[objIndex].originalFormula->isProbabilityOperatorFormula() && objectives[objIndex].originalFormula->asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula()), "Objective " << objectives[objIndex].originalFormula << " was simplified to a cumulative reward formula. Correctness of the algorithm is unknown for this type of property."); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero()); - if(rewModel.hasStateRewards()) { + if (rewModel.hasStateRewards()) { // Note that state rewards are earned over time and thus play no role for probabilistic states - for(auto markovianState : this->model.getMarkovianStates()) { + for (auto markovianState : this->model.getMarkovianStates()) { this->discreteActionRewards[objIndex][this->model.getTransitionMatrix().getRowGroupIndices()[markovianState]] += rewModel.getStateReward(markovianState) / this->model.getExitRate(markovianState); } } @@ -41,10 +47,6 @@ namespace storm { template void SparseMaPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - for (auto const& obj : this->objectives) { - STORM_LOG_THROW(!obj.timeBoundReference || obj.timeBoundReference->isTimeBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking of Markov automata is only supported for time-bounded formulass."); - } - // Split the preprocessed model into transitions from/to probabilistic/Markovian states. SubModel MS = createSubModel(true, weightedRewardVector); SubModel PS = createSubModel(false, weightedRewardVector); @@ -82,7 +84,7 @@ namespace storm { // Compute values that can be obtained at Markovian states after letting one (digitized) time unit pass. // Only perform such a step if there is time left. - if(currentEpoch>0) { + if (currentEpoch>0) { performMSStep(MS, PS, consideredObjectives, weightVector); --currentEpoch; } else { @@ -93,7 +95,7 @@ namespace storm { // compose the results from MS and PS storm::utility::vector::setVectorValues(this->weightedResult, MS.states, MS.weightedSolutionVector); storm::utility::vector::setVectorValues(this->weightedResult, PS.states, PS.weightedSolutionVector); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], MS.states, MS.objectiveSolutionVectors[objIndex]); storm::utility::vector::setVectorValues(this->objectiveResults[objIndex], PS.states, PS.objectiveSolutionVectors[objIndex]); } @@ -118,16 +120,16 @@ namespace storm { result.weightedRewardVector.resize(result.getNumberOfChoices()); storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector); result.objectiveRewardVectors.resize(this->objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { std::vector& objVector = result.objectiveRewardVectors[objIndex]; objVector = std::vector(result.weightedRewardVector.size(), storm::utility::zero()); - if(this->objectivesWithNoUpperTimeBound.get(objIndex)) { + if (this->objectivesWithNoUpperTimeBound.get(objIndex)) { storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]); } else { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName()); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported)."); - if(rewModel.hasStateActionRewards()) { + if (rewModel.hasStateActionRewards()) { storm::utility::vector::selectVectorValues(objVector, result.choices, rewModel.getStateActionRewardVector()); } } @@ -136,7 +138,7 @@ namespace storm { result.weightedSolutionVector.resize(result.getNumberOfStates()); storm::utility::vector::selectVectorValues(result.weightedSolutionVector, result.states, this->weightedResult); result.objectiveSolutionVectors.resize(this->objectives.size()); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { result.objectiveSolutionVectors[objIndex].resize(result.weightedSolutionVector.size()); storm::utility::vector::selectVectorValues(result.objectiveSolutionVectors[objIndex], result.states, this->objectiveResults[objIndex]); } @@ -163,11 +165,10 @@ namespace storm { std::vector timeBounds; std::vector eToPowerOfMinusMaxRateTimesBound; VT smallestNonZeroBound = storm::utility::zero(); - for(auto const& obj : this->objectives) { - if(obj.upperTimeBound){ - STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); - timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational())); - STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound."); + for (auto const& obj : this->objectives) { + if (obj.formula->getSubformula().isCumulativeRewardFormula()) { + timeBounds.push_back(obj.formula->getSubformula().asCumulativeRewardFormula().template getBound()); + STORM_LOG_THROW(!storm::utility::isZero(timeBounds.back()), storm::exceptions::InvalidPropertyException, "Got zero-valued upper time bound. This is not suppoted."); eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back())); smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back()); } else { @@ -175,7 +176,7 @@ namespace storm { eToPowerOfMinusMaxRateTimesBound.push_back(storm::utility::zero()); } } - if(storm::utility::isZero(smallestNonZeroBound)) { + if (storm::utility::isZero(smallestNonZeroBound)) { // There are no time bounds. In this case, one is a valid digitization constant. return storm::utility::one(); } @@ -189,16 +190,16 @@ namespace storm { VT delta = smallestNonZeroBound / smallestStepBound; while(true) { bool deltaValid = true; - for(auto const& objIndex : objectivesWithTimeBound) { + for (auto const& objIndex : objectivesWithTimeBound) { auto const& timeBound = timeBounds[objIndex]; - if(timeBound/delta != std::floor(timeBound/delta)) { + if (timeBound/delta != std::floor(timeBound/delta)) { deltaValid = false; break; } } - if(deltaValid) { + if (deltaValid) { VT weightedPrecisionForCurrentDelta = storm::utility::zero(); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { VT precisionOfObj = storm::utility::zero(); if (objectivesWithTimeBound.get(objIndex)) { precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[objIndex] * storm::utility::pow(storm::utility::one() + maxRate * delta, timeBounds[objIndex] / delta) ); @@ -207,7 +208,7 @@ namespace storm { } deltaValid &= weightedPrecisionForCurrentDelta <= goalPrecisionTimesNorm; } - if(deltaValid) { + if (deltaValid) { break; } ++smallestStepBound; @@ -229,19 +230,19 @@ namespace storm { void SparseMaPcaaWeightVectorChecker::digitize(SubModel& MS, VT const& digitizationConstant) const { std::vector rateVector(MS.getNumberOfChoices()); storm::utility::vector::selectVectorValues(rateVector, MS.states, this->model.getExitRates()); - for(uint_fast64_t row = 0; row < rateVector.size(); ++row) { + for (uint_fast64_t row = 0; row < rateVector.size(); ++row) { VT const eToMinusRateTimesDelta = std::exp(-rateVector[row] * digitizationConstant); - for(auto& entry : MS.toMS.getRow(row)) { + for (auto& entry : MS.toMS.getRow(row)) { entry.setValue((storm::utility::one() - eToMinusRateTimesDelta) * entry.getValue()); - if(entry.getColumn() == row) { + if (entry.getColumn() == row) { entry.setValue(entry.getValue() + eToMinusRateTimesDelta); } } - for(auto& entry : MS.toPS.getRow(row)) { + for (auto& entry : MS.toPS.getRow(row)) { entry.setValue((storm::utility::one() - eToMinusRateTimesDelta) * entry.getValue()); } MS.weightedRewardVector[row] *= storm::utility::one() - eToMinusRateTimesDelta; - for(auto& objVector : MS.objectiveRewardVectors) { + for (auto& objVector : MS.objectiveRewardVectors) { objVector[row] *= storm::utility::one() - eToMinusRateTimesDelta; } } @@ -258,13 +259,12 @@ namespace storm { void SparseMaPcaaWeightVectorChecker::digitizeTimeBounds(TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { VT const maxRate = this->model.getMaximalExitRate(); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower time bounds are not supported by this model checker"); VT errorTowardsZero = storm::utility::zero(); VT errorAwayFromZero = storm::utility::zero(); - if(obj.upperTimeBound) { - VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational()); + if (obj.formula->getSubformula().isCumulativeRewardFormula()) { + VT timeBound = obj.formula->getSubformula().asCumulativeRewardFormula().template getBound(); uint_fast64_t digitizedBound = storm::utility::convertNumber(timeBound/digitizationConstant); auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; timeBoundIt->second.set(objIndex); @@ -272,7 +272,7 @@ namespace storm { digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { this->offsetsToUnderApproximation[objIndex] = -errorTowardsZero; this->offsetsToOverApproximation[objIndex] = errorAwayFromZero; } else { @@ -324,11 +324,11 @@ namespace storm { template void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { - if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { + if (upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) { consideredObjectives |= upperTimeBoundIt->second; - for(auto objIndex : upperTimeBoundIt->second) { + for (auto objIndex : upperTimeBoundIt->second) { // This objective now plays a role in the weighted sum - ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + ValueType factor = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], factor); storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], factor); } @@ -345,16 +345,16 @@ namespace storm { // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b); auto const& newChoices = minMax.solver->getSchedulerChoices(); - if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { + if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives optimalChoicesAtCurrentEpoch = newChoices; PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector; - if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); } } else { // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed - if(linEq.solver == nullptr || newChoices != optimalChoicesAtCurrentEpoch) { + if (linEq.solver == nullptr || newChoices != optimalChoicesAtCurrentEpoch) { optimalChoicesAtCurrentEpoch = newChoices; linEq.solver = nullptr; storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); @@ -365,17 +365,17 @@ namespace storm { // Get the results for the individual objectives. // Note that we do not consider an estimate for each objective (as done in the unbounded phase) since the results from the previous epoch are already pretty close - for(auto objIndex : consideredObjectives) { + for (auto objIndex : consideredObjectives) { auto const& objectiveRewardVectorPS = PS.objectiveRewardVectors[objIndex]; auto const& objectiveSolutionVectorMS = MS.objectiveSolutionVectors[objIndex]; // compute rhs of equation system, i.e., PS.toMS * x + Rewards // To safe some time, only do this for the obtained optimal choices auto itGroupIndex = PS.toPS.getRowGroupIndices().begin(); auto itChoiceOffset = optimalChoicesAtCurrentEpoch.begin(); - for(auto& bValue : linEq.b) { + for (auto& bValue : linEq.b) { uint_fast64_t row = (*itGroupIndex) + (*itChoiceOffset); bValue = objectiveRewardVectorPS[row]; - for(auto const& entry : PS.toMS.getRow(row)){ + for (auto const& entry : PS.toMS.getRow(row)){ bValue += entry.getValue() * objectiveSolutionVectorMS[entry.getColumn()]; } ++itGroupIndex; @@ -393,14 +393,14 @@ namespace storm { storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector); MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues); storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector); - if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { + if (consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector; - if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); } } else { - for(auto objIndex : consideredObjectives) { + for (auto objIndex : consideredObjectives) { MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); storm::utility::vector::addVectors(MS.objectiveRewardVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]); MS.toPS.multiplyWithVector(PS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index 0916fd94c..0744f1d7d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -5,6 +5,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" +#include "storm/logic/Formulas.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/NotSupportedException.h" @@ -21,24 +22,22 @@ namespace storm { storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) : SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { - // set the state action rewards + // set the state action rewards. Also do some sanity checks on the objectives. for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); - STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected."); + auto const& formula = *objectives[objIndex].formula; + STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula); + STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() || formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); + typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); + STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix()); } } template void SparseMdpPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - // Check whether reward bounded objectives occur. + // Currently, only step bounds are considered. + // TODO: Check whether reward bounded objectives occur. bool containsRewardBoundedObjectives = false; - for (auto const& obj : this->objectives) { - if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) { - containsRewardBoundedObjectives = true; - break; - } - } if (containsRewardBoundedObjectives) { boundedPhaseWithRewardBounds(weightVector, weightedRewardVector); @@ -56,12 +55,10 @@ namespace storm { // Get for each occurring timeBound the indices of the objectives with that bound. std::map> stepBounds; for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower step bounds are not supported by this model checker"); - if (obj.upperTimeBound) { - STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); - uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->getBound().evaluateAsInt(); - if (obj.upperTimeBound->isStrict()) { + if (this->objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) { + auto const& subformula = this->objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula(); + uint_fast64_t stepBound = subformula.template getBound(); + if (subformula.isBoundStrict()) { --stepBound; } auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first; @@ -85,7 +82,7 @@ namespace storm { consideredObjectives |= stepBoundIt->second; for(auto objIndex : stepBoundIt->second) { // This objective now plays a role in the weighted sum - ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + ValueType factor = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex]; storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], factor); } ++stepBoundIt; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index 74e646103..a1d457c11 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -31,18 +31,17 @@ namespace storm { void SparsePcaaAchievabilityQuery::initializeThresholdData() { thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - STORM_LOG_ASSERT(obj.bound.is_initialized(), "Achievability query invoked but there is an objective without bound."); - STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); - thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); - if (storm::solver::minimize(obj.optimizationDirection)) { - STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + auto const& formula = *this->objectives[objIndex].formula; + STORM_LOG_ASSERT(formula.hasBound(), "Achievability query invoked but there is an objective without bound."); + thresholds.push_back(formula.template getThresholdAs()); + if (storm::solver::minimize(formula.getOptimalityType())) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound."); // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. // Hence, we also negate the threshold thresholds.back() *= -storm::utility::one(); } - strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); + strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType)); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index c459ce7df..0405a6022 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -24,7 +24,7 @@ namespace storm { STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType::QueryType::Quantitative, "Invalid query Type"); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if (!this->objectives[objIndex].bound.is_initialized()) { + if (!this->objectives[objIndex].formula->hasBound()) { indexOfOptimizingObjective = objIndex; break; } @@ -41,19 +41,19 @@ namespace storm { thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); std::vector> thresholdConstraints; - thresholdConstraints.reserve(this->objectives.size()-1); + thresholdConstraints.reserve(this->objectives.size() - 1); for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - auto const& obj = this->objectives[objIndex]; - if (obj.bound) { - STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); - thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); - if (storm::solver::minimize(obj.optimizationDirection)) { - STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + auto const& formula = *this->objectives[objIndex].formula; + + if (formula.hasBound()) { + thresholds.push_back(formula.template getThresholdAs()); + if (storm::solver::minimize(formula.getOptimalityType())) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(formula.getBound().comparisonType), "Minimizing objective should not specify an upper bound."); // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. // Hence, we also negate the threshold thresholds.back() *= -storm::utility::one(); } - strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); + strictThresholds.set(objIndex, storm::logic::isStrict(formula.getBound().comparisonType)); WeightVector normalVector(this->objectives.size(), storm::utility::zero()); normalVector[objIndex] = -storm::utility::one(); thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back()); @@ -74,7 +74,7 @@ namespace storm { // transform the obtained result for the preprocessed model to a result w.r.t. the original model and return the checkresult auto const& obj = this->objectives[indexOfOptimizingObjective]; - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { if (obj.considersComplementaryEvent) { result = storm::utility::one() - result; } @@ -95,7 +95,7 @@ namespace storm { template bool SparsePcaaQuantitativeQuery::checkAchievability() { - if (this->objectives.size()>1) { + if (this->objectives.size() > 1) { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 9276613b1..a978dc53c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -107,7 +107,7 @@ namespace storm { step.upperBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getOverApproximationOfInitialStateResults()); // For the minimizing objectives, we need to scale the corresponding entries with -1 as we want to consider the downward closure for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if (storm::solver::minimize(this->objectives[objIndex].optimizationDirection)) { + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { step.lowerBoundPoint[objIndex] *= -storm::utility::one(); step.upperBoundPoint[objIndex] *= -storm::utility::one(); } @@ -161,7 +161,7 @@ namespace storm { result.reserve(point.size()); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { if (obj.considersComplementaryEvent) { result.push_back(storm::utility::one() - point[objIndex]); } else { @@ -192,7 +192,7 @@ namespace storm { transformationVector.reserve(numObjectives); for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { auto const& obj = this->objectives[objIndex]; - if (storm::solver::maximize(obj.optimizationDirection)) { + if (storm::solver::maximize(obj.formula->getOptimalityType())) { if (obj.considersComplementaryEvent) { transformationMatrix[objIndex][objIndex] = -storm::utility::one(); transformationVector.push_back(storm::utility::one()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index be8727462..452254107 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -12,6 +12,7 @@ #include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" +#include "storm/logic/Formulas.h" #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/exceptions/UnexpectedException.h" @@ -42,10 +43,11 @@ namespace storm { // set data for unbounded objectives for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - auto const& obj = objectives[objIndex]; - if (!obj.upperTimeBound) { + auto const& formula = *objectives[objIndex].formula; + if (formula.getSubformula().isTotalRewardFormula()) { objectivesWithNoUpperTimeBound.set(objIndex, true); - actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(*obj.rewardModelName).getChoicesWithZeroReward(model.getTransitionMatrix()); + STORM_LOG_ASSERT(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), "Unexpected type of operator formula."); + actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(model.getTransitionMatrix()); } } } @@ -59,26 +61,27 @@ namespace storm { boost::optional weightedLowerResultBound = storm::utility::zero(); boost::optional weightedUpperResultBound = storm::utility::zero(); for (auto objIndex : objectivesWithNoUpperTimeBound) { - if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { - if (objectives[objIndex].lowerResultBound && weightedUpperResultBound) { - weightedUpperResultBound.get() -= weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + auto const& obj = objectives[objIndex]; + if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { + if (obj.lowerResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get(); } else { weightedUpperResultBound = boost::none; } - if (objectives[objIndex].upperResultBound && weightedLowerResultBound) { - weightedLowerResultBound.get() -= weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + if (obj.upperResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() -= weightVector[objIndex] * obj.upperResultBound.get(); } else { weightedLowerResultBound = boost::none; } storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], -weightVector[objIndex]); } else { - if (objectives[objIndex].lowerResultBound && weightedLowerResultBound) { - weightedLowerResultBound.get() += weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + if (obj.lowerResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() += weightVector[objIndex] * obj.lowerResultBound.get(); } else { weightedLowerResultBound = boost::none; } - if (objectives[objIndex].upperResultBound && weightedUpperResultBound) { - weightedUpperResultBound.get() += weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + if (obj.upperResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() += weightVector[objIndex] * obj.upperResultBound.get(); } else { weightedUpperResultBound = boost::none; } @@ -90,8 +93,8 @@ namespace storm { unboundedIndividualPhase(weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound - for(auto const& obj : this->objectives) { - if(obj.lowerTimeBound || obj.upperTimeBound) { + for (auto const& obj : this->objectives) { + if (!obj.formula->getSubformula().isTotalRewardFormula()) { boundedPhase(weightVector, weightedRewardVector); break; } @@ -140,8 +143,8 @@ namespace storm { template storm::storage::Scheduler::ValueType> SparsePcaaWeightVectorChecker::computeScheduler() const { STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - for(auto const& obj : this->objectives) { - STORM_LOG_THROW(!obj.lowerTimeBound && !obj.upperTimeBound, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives."); + for (auto const& obj : this->objectives) { + STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula(), storm::exceptions::NotImplementedException, "Scheduler retrival is only implemented for objectives without time-bound."); } storm::storage::Scheduler result(this->optimalChoices.size()); @@ -202,7 +205,7 @@ namespace storm { if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin(); objectiveResults[objIndex] = weightedResult; - if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { + if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one()); } for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { @@ -235,7 +238,7 @@ namespace storm { if (!storm::utility::isZero(weightVector[objIndex])) { objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; ValueType scalingFactor = storm::utility::one() / sumOfWeightsOfUncheckedObjectives; - if (storm::solver::minimize(obj.optimizationDirection)) { + if (storm::solver::minimize(obj.formula->getOptimalityType())) { scalingFactor *= -storm::utility::one(); } storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor); From 241fc880770351b0a650f3af12498ff21c3f6911 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 19 Jul 2017 20:23:52 +0200 Subject: [PATCH 14/19] multi-dimensional time bounds --- src/storm/logic/BoundedUntilFormula.cpp | 190 +++++++++++------- src/storm/logic/BoundedUntilFormula.h | 38 ++-- .../logic/VariableSubstitutionVisitor.cpp | 30 ++- src/storm/parser/JaniParser.cpp | 56 ++++-- 4 files changed, 199 insertions(+), 115 deletions(-) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index ff5df2d2a..fecbf2673 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -11,10 +11,20 @@ namespace storm { namespace logic { - BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReference), lowerBound(lowerBound), upperBound(upperBound) { + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference({timeBoundReference}), lowerBound({lowerBound}), upperBound({upperBound}) { STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound."); } - + + BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula,std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) { + assert(timeBoundReferences.size() == upperBound.size()); + assert(timeBoundReferences.size() == lowerBound.size()); + STORM_LOG_THROW(this->getDimension() != 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one dimension."); + for(unsigned i = 0; i < timeBoundReferences.size(); ++i) { + STORM_LOG_THROW(hasLowerBound(i) || hasUpperBound(i), storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound in each dimension."); + } + } + + bool BoundedUntilFormula::isBoundedUntilFormula() const { return true; } @@ -28,111 +38,141 @@ namespace storm { } void BoundedUntilFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { - if (this->getTimeBoundReference().isRewardBound()) { - referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + for (unsigned i = 0; i < this->getDimension(); ++i) { + if (this->getTimeBoundReference(i).isRewardBound()) { + referencedRewardModels.insert(this->getTimeBoundReference().getRewardName()); + } } + this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels); this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels); } - TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const { - return timeBoundReference; + TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference(unsigned i) const { + assert(i < timeBoundReference.size()); + return timeBoundReference.at(i); } + bool BoundedUntilFormula::isMultiDimensional() const { + assert(timeBoundReference.size() != 0); + return timeBoundReference.size() > 1; + } + unsigned BoundedUntilFormula::getDimension() const { + return timeBoundReference.size(); + } - bool BoundedUntilFormula::isLowerBoundStrict() const { - return lowerBound.get().isStrict(); + bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const { + assert(i < lowerBound.size()); + return lowerBound.at(i).get().isStrict(); } bool BoundedUntilFormula::hasLowerBound() const { - return static_cast(lowerBound); + for(auto const& lb : lowerBound) { + if (static_cast(lb)) { + return true; + } + } + return false; + } + + bool BoundedUntilFormula::hasLowerBound(unsigned i) const { + return static_cast(lowerBound.at(i)); } - bool BoundedUntilFormula::hasIntegerLowerBound() const { - return lowerBound.get().getBound().hasIntegerType(); + bool BoundedUntilFormula::hasIntegerLowerBound(unsigned i) const { + return lowerBound.at(i).get().getBound().hasIntegerType(); } - bool BoundedUntilFormula::isUpperBoundStrict() const { - return upperBound.get().isStrict(); + bool BoundedUntilFormula::isUpperBoundStrict(unsigned i) const { + return upperBound.at(i).get().isStrict(); } bool BoundedUntilFormula::hasUpperBound() const { - return static_cast(upperBound); + for(auto const& ub : upperBound) { + if (static_cast(ub)) { + return true; + } + } + return false; } - bool BoundedUntilFormula::hasIntegerUpperBound() const { - return upperBound.get().getBound().hasIntegerType(); + bool BoundedUntilFormula::hasUpperBound(unsigned i) const { + return static_cast(upperBound.at(i)); } - storm::expressions::Expression const& BoundedUntilFormula::getLowerBound() const { - return lowerBound.get().getBound(); + bool BoundedUntilFormula::hasIntegerUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound().hasIntegerType(); + } + + storm::expressions::Expression const& BoundedUntilFormula::getLowerBound(unsigned i) const { + return lowerBound.at(i).get().getBound(); } - storm::expressions::Expression const& BoundedUntilFormula::getUpperBound() const { - return upperBound.get().getBound(); + storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigned i) const { + return upperBound.at(i).get().getBound(); } template <> - double BoundedUntilFormula::getLowerBound() const { + double BoundedUntilFormula::getLowerBound(unsigned i) const { checkNoVariablesInBound(this->getLowerBound()); - double bound = this->getLowerBound().evaluateAsDouble(); + double bound = this->getLowerBound(i).evaluateAsDouble(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - double BoundedUntilFormula::getUpperBound() const { + double BoundedUntilFormula::getUpperBound(unsigned i) const { checkNoVariablesInBound(this->getUpperBound()); - double bound = this->getUpperBound().evaluateAsDouble(); + double bound = this->getUpperBound(i).evaluateAsDouble(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - storm::RationalNumber BoundedUntilFormula::getLowerBound() const { - checkNoVariablesInBound(this->getLowerBound()); - storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + storm::RationalNumber BoundedUntilFormula::getLowerBound(unsigned i) const { + checkNoVariablesInBound(this->getLowerBound(i)); + storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational(); STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - storm::RationalNumber BoundedUntilFormula::getUpperBound() const { - checkNoVariablesInBound(this->getUpperBound()); - storm::RationalNumber bound = this->getUpperBound().evaluateAsRational(); + storm::RationalNumber BoundedUntilFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound(i)); + storm::RationalNumber bound = this->getUpperBound(i).evaluateAsRational(); STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return bound; } template <> - uint64_t BoundedUntilFormula::getLowerBound() const { - checkNoVariablesInBound(this->getLowerBound()); - int_fast64_t bound = this->getLowerBound().evaluateAsInt(); + uint64_t BoundedUntilFormula::getLowerBound(unsigned i) const { + checkNoVariablesInBound(this->getLowerBound(i)); + int_fast64_t bound = this->getLowerBound(i).evaluateAsInt(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return static_cast(bound); } template <> - uint64_t BoundedUntilFormula::getUpperBound() const { - checkNoVariablesInBound(this->getUpperBound()); - int_fast64_t bound = this->getUpperBound().evaluateAsInt(); + uint64_t BoundedUntilFormula::getUpperBound(unsigned i) const { + checkNoVariablesInBound(this->getUpperBound(i)); + int_fast64_t bound = this->getUpperBound(i).evaluateAsInt(); STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return static_cast(bound); } template <> - double BoundedUntilFormula::getNonStrictUpperBound() const { - double bound = getUpperBound(); - STORM_LOG_THROW(!isUpperBoundStrict() || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + double BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const { + double bound = getUpperBound(i); + STORM_LOG_THROW(!isUpperBoundStrict(i) || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); return bound; } template <> - uint64_t BoundedUntilFormula::getNonStrictUpperBound() const { - int_fast64_t bound = getUpperBound(); - if (isUpperBoundStrict()) { + uint64_t BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const { + int_fast64_t bound = getUpperBound(i); + if (isUpperBoundStrict(i)) { STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); return bound - 1; } else { @@ -148,41 +188,53 @@ namespace storm { this->getLeftSubformula().writeToStream(out); out << " U"; - if (this->getTimeBoundReference().isRewardBound()) { - out << "{\"" << this->getTimeBoundReference().getRewardName() << "\"}"; + if (this->isMultiDimensional()) { + out << "["; } - if (this->hasLowerBound()) { - if (this->hasUpperBound()) { - if (this->isLowerBoundStrict()) { - out << "("; - } else { - out << "["; - } - out << this->getLowerBound(); - out << ", "; - out << this->getUpperBound(); - if (this->isUpperBoundStrict()) { - out << ")"; + for(unsigned i = 0; i < this->getDimension(); ++i) { + if (i > 0) { + out << ","; + } + if (this->getTimeBoundReference(i).isRewardBound()) { + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + } + if (this->hasLowerBound(i)) { + if (this->hasUpperBound(i)) { + if (this->isLowerBoundStrict(i)) { + out << "("; + } else { + out << "["; + } + out << this->getLowerBound(i); + out << ", "; + out << this->getUpperBound(i); + if (this->isUpperBoundStrict(i)) { + out << ")"; + } else { + out << "]"; + } } else { - out << "]"; + if (this->isLowerBoundStrict(i)) { + out << ">"; + } else { + out << ">="; + } + out << getLowerBound(i); } } else { - if (this->isLowerBoundStrict()) { - out << ">"; + if (this->isUpperBoundStrict(i)) { + out << "<"; } else { - out << ">="; + out << "<="; } - out << getLowerBound(); + out << this->getUpperBound(i); } - } else { - if (this->isUpperBoundStrict()) { - out << "<"; - } else { - out << "<="; - } - out << this->getUpperBound(); + out << " "; + } + if (this->isMultiDimensional()) { + out << "]"; } - out << " "; + this->getRightSubformula().writeToStream(out); return out; diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 5ff571d84..2b2e33945 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -1,5 +1,4 @@ -#ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ -#define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ +#pragma once #include @@ -13,7 +12,8 @@ namespace storm { class BoundedUntilFormula : public BinaryPathFormula { public: BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, boost::optional const& lowerBound, boost::optional const& upperBound, TimeBoundReference const& timeBoundReference); - + BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); + virtual bool isBoundedUntilFormula() const override; virtual bool isProbabilityPathFormula() const override; @@ -22,39 +22,43 @@ namespace storm { virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; - TimeBoundReference const& getTimeBoundReference() const; + TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const; - bool isLowerBoundStrict() const; + bool isLowerBoundStrict(unsigned i = 0) const; bool hasLowerBound() const; - bool hasIntegerLowerBound() const; + bool hasLowerBound(unsigned i) const; + bool hasIntegerLowerBound(unsigned i = 0) const; - bool isUpperBoundStrict() const; + bool isUpperBoundStrict(unsigned i = 0) const; bool hasUpperBound() const; - bool hasIntegerUpperBound() const; + bool hasUpperBound(unsigned i) const; + bool hasIntegerUpperBound(unsigned i = 0) const; + + bool isMultiDimensional() const; + unsigned getDimension() const; - storm::expressions::Expression const& getLowerBound() const; - storm::expressions::Expression const& getUpperBound() const; + storm::expressions::Expression const& getLowerBound(unsigned i = 0) const; + storm::expressions::Expression const& getUpperBound(unsigned i = 0) const; template - ValueType getLowerBound() const; + ValueType getLowerBound(unsigned i = 0) const; template - ValueType getUpperBound() const; + ValueType getUpperBound(unsigned i = 0) const; template - ValueType getNonStrictUpperBound() const; + ValueType getNonStrictUpperBound(unsigned i = 0) const; virtual std::ostream& writeToStream(std::ostream& out) const override; private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); - TimeBoundReference timeBoundReference; - boost::optional lowerBound; - boost::optional upperBound; + std::vector timeBoundReference; + std::vector> lowerBound; + std::vector> upperBound; }; } } -#endif /* STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ */ diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 8c0945adb..00eee1e01 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -37,17 +37,29 @@ namespace storm { boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { auto left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); auto right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); - - boost::optional lowerBound; - if (f.hasLowerBound()) { - lowerBound = TimeBound(f.isLowerBoundStrict(), f.getLowerBound().substitute(substitution)); - } - boost::optional upperBound; - if (f.hasUpperBound()) { - upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution)); + + std::vector> lowerBounds; + std::vector> upperBounds; + std::vector tbReferences; + + for (unsigned i = 0; i < f.getDimension(); ++i) { + std::cout << f.hasLowerBound(i) << std::endl; + if (f.hasLowerBound(i)) { + lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution))); + } else { + lowerBounds.push_back(boost::none); + } + + if (f.hasUpperBound(i)) { + upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution))); + } else { + lowerBounds.push_back(boost::none); + } + tbReferences.push_back(f.getTimeBoundReference(i)); } - return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundReference())); + + return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, tbReferences)); } boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 28ac7ae7c..f92acab7a 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -165,9 +165,8 @@ namespace storm { if (piStructure.count("lower") > 0) { pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval", {}, {}); // TODO substitute constants. + std::cout << "have lower bound" << std::endl; STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds"); - - } if (piStructure.count("lower-exclusive") > 0) { STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); @@ -175,16 +174,17 @@ namespace storm { } if (piStructure.count("upper") > 0) { + std::cout << "have upper bound" << std::endl; pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval", {}, {}); // TODO substitute constants. STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds"); } if (piStructure.count("upper-exclusive") > 0) { - STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); - pi.lowerBoundStrict = piStructure.at("upper-exclusive"); + STORM_LOG_THROW(pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.upperBoundStrict = piStructure.at("upper-exclusive"); } - STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded"); + STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operator must have a bounded interval, but no bounds found in '" << piStructure << "'"); return pi; @@ -367,22 +367,38 @@ namespace storm { return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)); } else if (propertyStructure.count("reward-bounds") > 0 ) { - storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("reward-bounds")); - STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); - STORM_LOG_THROW(propertyStructure.at("reward-bounds").count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); - storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("reward-bounds").at("exp"), "Reward expression in " + context, globalVars, constants); - STORM_LOG_THROW(!rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); - std::string rewardName = rewExpr.getVariables().begin()->getName(); - STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); - double lowerBound = 0.0; - if(pi.hasLowerBound()) { - lowerBound = pi.lowerBound.evaluateAsDouble(); + std::vector> lowerBounds; + std::vector> upperBounds; + std::vector tbReferences; + for (auto const& rbStructure : propertyStructure.at("reward-bounds")) { + storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), "Reward expression in " + context, globalVars, constants); + STORM_LOG_THROW(rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); + std::string rewardName = rewExpr.getVariables().begin()->getName(); + STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + double upperBound = pi.upperBound.evaluateAsDouble(); + STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); + if (pi.hasLowerBound()) { + lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); + } else { + lowerBounds.push_back(boost::none); + } + if (pi.hasUpperBound()) { + upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); + } else { + upperBounds.push_back(boost::none); + } + tbReferences.push_back(storm::logic::TimeBoundReference(rewardName)); } - double upperBound = pi.upperBound.evaluateAsDouble(); - STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); - STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm"); - return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(rewardName)); + auto res = std::make_shared(args[0], args[1], lowerBounds, upperBounds, tbReferences); + return res; } if (args[0]->isTrueFormula()) { From c0d364cf1b7fe0536f2069430c11351c56a8d8b1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Jul 2017 19:15:41 +0200 Subject: [PATCH 15/19] fixed a warning --- src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 58f773cfe..1d1d7f77c 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -248,7 +248,7 @@ namespace storm { uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; uint64_t groupEnd = model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; hasTrivialNondeterminism = hasTrivialNondeterminism && (groupEnd == modelRow + 1); - for (; groupEnd; ++modelRow) { + for (; modelRow < groupEnd; ++modelRow) { ++numResChoices; numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); } From 5b35927ecb40540178fa63fc70b7b25d2d605866 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 19 Jul 2017 20:20:28 +0200 Subject: [PATCH 16/19] fix for some multi-objective queries --- .../multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 452254107..7333f6db6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -270,8 +270,8 @@ namespace storm { // Set the result for this objective accordingly storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); - storm::utility::vector::setVectorValues(objectiveResults[objIndex], ~maybeStates, storm::utility::zero()); } + storm::utility::vector::setVectorValues(objectiveResults[objIndex], ~maybeStates, storm::utility::zero()); // Update the estimate for the next objectives. if (!storm::utility::isZero(weightVector[objIndex])) { From 234b590bdf93ce122831e38d409d2f83998fa08b Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 20 Jul 2017 15:51:36 +0200 Subject: [PATCH 17/19] Fixed #include --- src/storm/modelchecker/multiobjective/Objective.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h index 6b1f44f1f..b58cfd589 100644 --- a/src/storm/modelchecker/multiobjective/Objective.h +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -2,7 +2,7 @@ #include -#include "storm/logic/Formula.h" +#include "storm/logic/Formulas.h" #include "storm/logic/Bound.h" #include "storm/logic/TimeBound.h" #include "storm/logic/TimeBoundType.h" From c03c5fceb7764d503c7ba94fa56e9a12b7d6c861 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 22 Jul 2017 19:48:51 +0200 Subject: [PATCH 18/19] fixed warnings related to the mixed use of struct/class --- src/storm/builder/ExplicitModelBuilder.h | 2 +- src/storm/generator/Choice.cpp | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 501111673..ef5da691b 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -43,7 +43,7 @@ namespace storm { using namespace storm::generator; // Forward-declare classes. - template struct RewardModelBuilder; + template class RewardModelBuilder; class ChoiceInformationBuilder; template, typename StateType = uint32_t> diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index cfa9cec9d..be5f597da 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -174,11 +174,11 @@ namespace storm { return out; } - template class Choice; + template struct Choice; #ifdef STORM_HAVE_CARL - template class Choice; - template class Choice; + template struct Choice; + template struct Choice; #endif } } From ad9008e0c1af058c0e4ed5f3b03c8f6e8924c2f1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 22 Jul 2017 21:22:01 +0200 Subject: [PATCH 19/19] fixing more warnings related to struct vs. class forward declarations --- src/storm/abstraction/BottomStateResult.cpp | 4 ++-- src/storm/abstraction/GameBddResult.cpp | 4 ++-- src/storm/abstraction/jani/EdgeAbstractor.h | 2 +- src/storm/abstraction/prism/CommandAbstractor.h | 2 +- .../modelchecker/exploration/SparseExplorationModelChecker.h | 2 +- src/storm/modelchecker/exploration/Statistics.cpp | 2 +- src/storm/parser/JaniParser.h | 2 +- 7 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/storm/abstraction/BottomStateResult.cpp b/src/storm/abstraction/BottomStateResult.cpp index a5f9576af..a2f60083e 100644 --- a/src/storm/abstraction/BottomStateResult.cpp +++ b/src/storm/abstraction/BottomStateResult.cpp @@ -8,7 +8,7 @@ namespace storm { // Intentionally left empty. } - template class BottomStateResult; - template class BottomStateResult; + template struct BottomStateResult; + template struct BottomStateResult; } } diff --git a/src/storm/abstraction/GameBddResult.cpp b/src/storm/abstraction/GameBddResult.cpp index 87aaeaee8..c1fbe457a 100644 --- a/src/storm/abstraction/GameBddResult.cpp +++ b/src/storm/abstraction/GameBddResult.cpp @@ -13,8 +13,8 @@ namespace storm { // Intentionally left empty. } - template class GameBddResult; - template class GameBddResult; + template struct GameBddResult; + template struct GameBddResult; } } diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index 674805666..ac88b6b04 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -43,7 +43,7 @@ namespace storm { class AbstractionInformation; template - class BottomStateResult; + struct BottomStateResult; namespace jani { template diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index e673de271..b26492125 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -42,7 +42,7 @@ namespace storm { class AbstractionInformation; template - class BottomStateResult; + struct BottomStateResult; namespace prism { template diff --git a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.h b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.h index 98a6f5854..95d55a539 100644 --- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.h +++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.h @@ -25,7 +25,7 @@ namespace storm { template class StateGeneration; template class ExplorationInformation; template class Bounds; - template class Statistics; + template struct Statistics; } using namespace exploration_detail; diff --git a/src/storm/modelchecker/exploration/Statistics.cpp b/src/storm/modelchecker/exploration/Statistics.cpp index 977747067..5284948b4 100644 --- a/src/storm/modelchecker/exploration/Statistics.cpp +++ b/src/storm/modelchecker/exploration/Statistics.cpp @@ -39,7 +39,7 @@ namespace storm { out << "EC detections: " << ecDetections << " (" << failedEcDetections << " failed, " << totalNumberOfEcDetected << " EC(s) detected)" << std::endl; } - template class Statistics; + template struct Statistics; } } diff --git a/src/storm/parser/JaniParser.h b/src/storm/parser/JaniParser.h index ff6429df4..9a6bdace6 100644 --- a/src/storm/parser/JaniParser.h +++ b/src/storm/parser/JaniParser.h @@ -18,7 +18,7 @@ namespace storm { class Variable; class Composition; class Property; - class PropertyInterval; + struct PropertyInterval; } namespace logic {