Browse Source

jit model builder tests passing

Former-commit-id: f4223ba69f [formerly 0cd02249bc]
Former-commit-id: d14358914e
tempestpy_adaptions
dehnert 8 years ago
parent
commit
fda8a8f2ab
  1. 4
      src/builder/jit/ExplicitJitJaniModelBuilder.cpp
  2. 12
      src/builder/jit/ModelComponentsBuilder.cpp
  3. 2
      src/storage/prism/ToJaniConverter.cpp

4
src/builder/jit/ExplicitJitJaniModelBuilder.cpp

@ -85,11 +85,11 @@ namespace storm {
if (topLevelComposition.isAutomatonComposition()) { if (topLevelComposition.isAutomatonComposition()) {
parallelAutomata.push_back(this->model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName())); parallelAutomata.push_back(this->model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName()));
} else { } 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(); storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition();
for (auto const& composition : parallelComposition.getSubcompositions()) { 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())); parallelAutomata.push_back(this->model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()));
} }
} }

12
src/builder/jit/ModelComponentsBuilder.cpp

@ -132,7 +132,17 @@ namespace storm {
} else if (modelType == storm::jani::ModelType::MDP) { } 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)); return new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels));
} else { } 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));
} }
} }

2
src/storage/prism/ToJaniConverter.cpp

@ -226,8 +226,8 @@ namespace storm {
for (auto const& assignment : transientEdgeAssignmentsToAdd->second) { for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
newEdge.addTransientAssignment(assignment); newEdge.addTransientAssignment(assignment);
} }
transientEdgeAssignments.erase(transientEdgeAssignmentsToAdd);
} }
transientEdgeAssignments.erase(transientEdgeAssignmentsToAdd);
// Finally add the constructed edge. // Finally add the constructed edge.
automaton.addEdge(newEdge); automaton.addEdge(newEdge);

Loading…
Cancel
Save