From fda8a8f2ab74386c720bb93b25ae2f755849bae7 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 9 Nov 2016 20:34:11 +0100
Subject: [PATCH] jit model builder tests passing
Former-commit-id: f4223ba69f434727b84028ef0a7837900fcecc3b [formerly 0cd02249bc83dfd1e40ca44106e8876cf30072c6]
Former-commit-id: d14358914e0b446d97e8836e7c5565bcfaa33b63
---
src/builder/jit/ExplicitJitJaniModelBuilder.cpp | 4 ++--
src/builder/jit/ModelComponentsBuilder.cpp | 12 +++++++++++-
src/storage/prism/ToJaniConverter.cpp | 2 +-
3 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 7dd4d78d6..353879fdb 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -85,11 +85,11 @@ namespace storm {
if (topLevelComposition.isAutomatonComposition()) {
parallelAutomata.push_back(this->model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName()));
} else {
- STORM_LOG_ASSERT(topLevelComposition.isParallelComposition(), "Expected parallel composition.");
+ STORM_LOG_THROW(topLevelComposition.isParallelComposition(), storm::exceptions::WrongFormatException, "Expected parallel composition.");
storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition();
for (auto const& composition : parallelComposition.getSubcompositions()) {
- STORM_LOG_ASSERT(composition->isAutomatonComposition(), "Expected flat parallel composition.");
+ STORM_LOG_THROW(composition->isAutomatonComposition(), storm::exceptions::WrongFormatException, "Expected flat parallel composition.");
parallelAutomata.push_back(this->model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()));
}
}
diff --git a/src/builder/jit/ModelComponentsBuilder.cpp b/src/builder/jit/ModelComponentsBuilder.cpp
index 21af3915b..8135e4666 100644
--- a/src/builder/jit/ModelComponentsBuilder.cpp
+++ b/src/builder/jit/ModelComponentsBuilder.cpp
@@ -132,7 +132,17 @@ namespace storm {
} else if (modelType == storm::jani::ModelType::MDP) {
return new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
} else {
- return nullptr;
+ std::vector<ValueType> exitRates(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ for (auto state : *markovianStates) {
+ for (auto const& element : transitionMatrix.getRow(transitionMatrix.getRowGroupIndices()[state])) {
+ exitRates[state] += element.getValue();
+ }
+ for (auto& element : transitionMatrix.getRow(transitionMatrix.getRowGroupIndices()[state])) {
+ element.setValue(element.getValue() / exitRates[state]);
+ }
+ }
+
+ return new storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(*markovianStates), std::move(exitRates), std::move(rewardModels));
}
}
diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp
index acebc5ff3..776d144c2 100644
--- a/src/storage/prism/ToJaniConverter.cpp
+++ b/src/storage/prism/ToJaniConverter.cpp
@@ -226,8 +226,8 @@ namespace storm {
for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
newEdge.addTransientAssignment(assignment);
}
+ transientEdgeAssignments.erase(transientEdgeAssignmentsToAdd);
}
- transientEdgeAssignments.erase(transientEdgeAssignmentsToAdd);
// Finally add the constructed edge.
automaton.addEdge(newEdge);