From 5dcebdef935da06dcfd43a259be55c989a869a88 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 11 Mar 2020 10:14:06 +0100 Subject: [PATCH] Fixed invocation of storm without a model. --- src/storm-cli-utilities/model-handling.h | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index b3b6de3ff..4f026d8db 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -289,12 +289,14 @@ namespace storm { // Set whether a transformation to jani is required or necessary mpi.transformToJani = ioSettings.isPrismToJaniSet(); - auto builderType = storm::utility::getBuilderType(mpi.engine); - bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit; - STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); - bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA); - STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model."); - mpi.transformToJani |= (transformToJaniForJit || transformToJaniForDdMA); + if (input.model) { + auto builderType = storm::utility::getBuilderType(mpi.engine); + bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit; + STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); + bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA); + STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model."); + mpi.transformToJani |= (transformToJaniForJit || transformToJaniForDdMA); + } // Set the Valuetype used during model building mpi.buildValueType = mpi.verificationValueType;