From 6540b486e732a7921d08852ce9f7c3450e944729 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 6 Apr 2020 14:31:47 +0200 Subject: [PATCH 1/2] NotSupportedException when using drn export for symbolic models --- src/storm-cli-utilities/model-handling.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 6dad6fbb0..e6508c190 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -566,6 +566,10 @@ namespace storm { if (ioSettings.isExportExplicitSet()) { storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector()); } + + if (ioSettings.isExportDdSet()) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drdd format is only supported for DDs."); + } if (ioSettings.isExportDotSet()) { storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth()); @@ -576,6 +580,10 @@ namespace storm { void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); + if (ioSettings.isExportExplicitSet()) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exporting in drn format is only supported for sparse models."); + } + if (ioSettings.isExportDdSet()) { storm::api::exportSparseModelAsDrdd(model, ioSettings.getExportDdFilename()); } From 7ffe322e06e46595cb337a47d5b8b6dd2a4c9434 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 8 Apr 2020 12:31:45 +0200 Subject: [PATCH 2/2] SparseModelMemoryProduct: Fixed incorrect computation of state-action rewards under a randomized policy. --- 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 3907f0625..1f30f23fb 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -410,7 +410,7 @@ namespace storm { if (isStateReachable(modelState, memoryState)) { if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { ValueType factor = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution().getProbability(rowOffset); - stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)]] = factor * modelStateActionReward; + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)]] += factor * modelStateActionReward; } else { stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)] + rowOffset] = modelStateActionReward; }