diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 75ac5421d..c534039fb 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -198,7 +198,12 @@ 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); @@ -210,6 +215,13 @@ namespace storm { 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; + } } }