From 5a793839e97af2c4599694029e994de548cb249d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 9 Nov 2016 21:57:06 +0100
Subject: [PATCH] add some trace messages

Former-commit-id: 345e378eaf869cb36b5706e12bc614d5bd10501a [formerly 46bc4549956396a406f531ca2c90bd3a04a66bdf]
Former-commit-id: d7ebfccc6d12b5d18469879f79ef1d9b9ca5d951
---
 src/cli/cli.cpp       |  9 +++++++--
 src/cli/entrypoints.h | 16 ++++++++--------
 2 files changed, 15 insertions(+), 10 deletions(-)

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<storm::settings::modules::DebugSettings>().isLogfileSet()) {
                 storm::utility::initializeFileLogging();
             }
@@ -216,6 +217,7 @@ namespace storm {
                 storm::storage::SymbolicModelDescription model;
                 std::vector<storm::jani::Property> 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<storm::settings::modules::GeneralSettings>().isPropertySet()) {
                     if (model.isJaniModel()) {
@@ -249,7 +252,8 @@ namespace storm {
                     }
                 }
                 
-                if(model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
+                if (model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
+                    STORM_LOG_TRACE("Exporting JANI model.");
                     if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().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<storm::settings::modules::GeneralSettings>().isParametricSet()) {
 #ifdef STORM_HAVE_CARL
                     buildAndCheckSymbolicModel<storm::RationalFunction>(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<storm::modelchecker::CheckResult> result;
 
-                if(program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+                if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
                     storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(program);
                     storm::modelchecker::CheckTask<storm::logic::Formula> 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<storm::models::sparse::Mdp<ValueType>> checker(program);
                     storm::modelchecker::CheckTask<storm::logic::Formula> 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;
                 }