diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index dd0a886b2..fa9c8ebb7 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -138,6 +138,13 @@ namespace storm { storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(program, formulas); STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); + std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl; + std::cout << "INPUTMODEL_INFO;" << + storm::settings::generalSettings().getSymbolicModelFilename() << ";" << + storm::settings::generalSettings().getConstantDefinitionString() << ";" << + model->getNumberOfStates() << ";" << + model->getNumberOfTransitions() << ";" << std::endl; + // Preprocess the model if needed. BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); @@ -181,6 +188,12 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); } } + std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl; + std::cout << "DONE_MODEL_INFO;" << + storm::settings::generalSettings().getSymbolicModelFilename() << ";" << + storm::settings::generalSettings().getConstantDefinitionString() << ";" << + model->getNumberOfStates() << ";" << + model->getNumberOfTransitions() << ";" << std::endl; } template @@ -198,12 +211,7 @@ namespace storm { STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional()); - std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl; - std::cout << "INPUTMODEL_INFO;" << - storm::settings::generalSettings().getSymbolicModelFilename() << ";" << - storm::settings::generalSettings().getConstantDefinitionString() << ";" << - model->getNumberOfStates() << ";" << - model->getNumberOfTransitions() << ";" << std::endl; + // Preprocess the model if needed. BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); @@ -214,14 +222,7 @@ namespace storm { if (!formulas.empty()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); verifySparseModel(model->as>(), formulas); - } - std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl; - std::cout << "DONE_MODEL_INFO;" << - storm::settings::generalSettings().getSymbolicModelFilename() << ";" << - storm::settings::generalSettings().getConstantDefinitionString() << ";" << - model->getNumberOfStates() << ";" << - model->getNumberOfTransitions() << ";" << std::endl; - + } } } }