diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 3c4cbf535..78914aac3 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -207,6 +207,7 @@ namespace storm { } void processOptions() { + STORM_LOG_TRACE("Processing options."); if (storm::settings::getModule().isLogfileSet()) { storm::utility::initializeFileLogging(); } @@ -216,6 +217,7 @@ namespace storm { storm::storage::SymbolicModelDescription model; std::vector properties; + STORM_LOG_TRACE("Parsing symbolic input."); if (ioSettings.isPrismInputSet()) { model = storm::parseProgram(ioSettings.getPrismInputFilename()); if (ioSettings.isPrismToJaniSet()) { @@ -226,7 +228,7 @@ namespace storm { model = input.first; if (ioSettings.isJaniPropertiesSet()) { for (auto const& propName : ioSettings.getJaniProperties()) { - STORM_LOG_THROW( input.second.count(propName) == 1, storm::exceptions::InvalidArgumentException, "No property with name " << propName << " known."); + STORM_LOG_THROW(input.second.count(propName) == 1, storm::exceptions::InvalidArgumentException, "No property with name " << propName << " known."); properties.push_back(input.second.at(propName)); } } @@ -234,6 +236,7 @@ namespace storm { } // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. + STORM_LOG_TRACE("Parsing properties."); uint64_t i = 0; if (storm::settings::getModule().isPropertySet()) { if (model.isJaniModel()) { @@ -249,7 +252,8 @@ namespace storm { } } - if(model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { + if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { + STORM_LOG_TRACE("Exporting JANI model."); if (storm::settings::getModule().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); @@ -267,6 +271,7 @@ namespace storm { std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); + STORM_LOG_TRACE("Building and checking symbolic model."); if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL buildAndCheckSymbolicModel(model, properties, true); diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f5e1bd77c..c32458e9c 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -124,30 +124,30 @@ namespace storm { for (auto const& property : formulas) { std::cout << std::endl << "Model checking property: " << property << " ..."; - bool supportFormula; + bool formulaSupported = false; std::unique_ptr result; - if(program.getModelType() == storm::prism::Program::ModelType::DTMC) { + if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { storm::modelchecker::SparseExplorationModelChecker> checker(program); storm::modelchecker::CheckTask task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); - supportFormula = checker.canHandle(task); - if (supportFormula) { + formulaSupported = checker.canHandle(task); + if (formulaSupported) { result = checker.check(task); } - } else if(program.getModelType() == storm::prism::Program::ModelType::MDP) { + } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { storm::modelchecker::SparseExplorationModelChecker> checker(program); storm::modelchecker::CheckTask task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); - supportFormula = checker.canHandle(task); - if (supportFormula) { + formulaSupported = checker.canHandle(task); + if (formulaSupported) { result = checker.check(task); } } else { // Should be catched before. assert(false); } - if(!supportFormula) { + if (!formulaSupported) { std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl; }