removed 'size-in-memory' output as it was outdated and unreliable. added timing measurements for model construction and model checking

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -1546,7 +1546,7 @@ namespace storm {
                         STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << ".");
                         STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << ".");
                         auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata);
-                        if (terminalEntry.second) {
+                        if (!terminalEntry.second) {
                             labelExpression = !labelExpression;
                         }
                         terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)));

src/storm/cli/cli.cpp

@@ -227,16 +227,29 @@ namespace storm {
                 propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter());
             }
             
+            auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             if (ioSettings.isPrismOrJaniInputSet()) {
                 storm::storage::SymbolicModelDescription model;
                 std::vector<storm::jani::Property> properties;
                 
                 STORM_LOG_TRACE("Parsing symbolic input.");
+                boost::optional<std::map<std::string, std::string>> labelRenaming;
                 if (ioSettings.isPrismInputSet()) {
                     model = storm::parseProgram(ioSettings.getPrismInputFilename());
-                    if (ioSettings.isPrismToJaniSet()) {
+                    bool transformToJani = ioSettings.isPrismToJaniSet();
-                        model = model.toJani(true);
+                    bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet();
+                    STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model.");
+                    transformToJani |= transformToJaniForJit;
+                    
+                    if (transformToJani) {
+                        auto modelAndRenaming = model.toJaniWithLabelRenaming(true);
+                        if (!modelAndRenaming.second.empty()) {
+                            labelRenaming = modelAndRenaming.second;
+                        }
+                        model = modelAndRenaming.first;
                     }
                 } else if (ioSettings.isJaniInputSet()) {
                     auto input = storm::parseJaniModel(ioSettings.getJaniInputFilename());
@@ -256,11 +269,19 @@ 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.");
-                if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
+                if (generalSettings.isPropertySet()) {
                     if (model.isJaniModel()) {
-                        properties = storm::parsePropertiesForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel(), propertyFilter);
+                        properties = storm::parsePropertiesForJaniModel(generalSettings.getProperty(), model.asJaniModel(), propertyFilter);
+                        
+                        if (labelRenaming) {
+                            std::vector<storm::jani::Property> amendedProperties;
+                            for (auto const& property : properties) {
+                                amendedProperties.emplace_back(property.substituteLabels(labelRenaming.get()));
+                            }
+                            properties = std::move(amendedProperties);
+                        }
                     } else {
-                        properties = storm::parsePropertiesForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram(), propertyFilter);
+                        properties = storm::parsePropertiesForPrismProgram(generalSettings.getProperty(), model.asPrismProgram(), propertyFilter);
                     }
                     
                     constantDefinitions = model.parseConstantDefinitions(constantDefinitionString);
@@ -279,13 +300,13 @@ namespace storm {
                 }
                 
                 STORM_LOG_TRACE("Building and checking symbolic model.");
-                if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
+                if (generalSettings.isParametricSet()) {
 #ifdef STORM_HAVE_CARL
                     buildAndCheckSymbolicModel<storm::RationalFunction>(model, properties, true);
 #else
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
 #endif
-                } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+                } else if (generalSettings.isExactSet()) {
 #ifdef STORM_HAVE_CARL
                     buildAndCheckSymbolicModel<storm::RationalNumber>(model, properties, true);
 #else
@@ -294,14 +315,14 @@ namespace storm {
                 } else {
                     buildAndCheckSymbolicModel<double>(model, properties, true);
                 }
-            } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
+            } else if (ioSettings.isExplicitSet()) {
-                STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
+                STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
 
                 // If the model is given in an explicit format, we parse the properties without allowing expressions
                 // in formulas.
                 std::vector<storm::jani::Property> properties;
-                if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
+                if (generalSettings.isPropertySet()) {
-                    properties = storm::parsePropertiesForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), propertyFilter);
+                    properties = storm::parsePropertiesForExplicit(generalSettings.getProperty(), propertyFilter);
                 }
 
                 buildAndCheckExplicitModel<double>(properties, true);

src/storm/cli/entrypoints.h

@@ -7,6 +7,7 @@
 
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/utility/ExplicitExporter.h"
+#include "storm/utility/Stopwatch.h"
 
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/exceptions/InvalidSettingsException.h"
@@ -18,23 +19,22 @@ namespace storm {
 
         template<typename ValueType>
         void applyFilterFunctionAndOutput(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) {
-            
             if (result->isQuantitative()) {
                 switch (ft) {
                     case storm::modelchecker::FilterType::VALUES:
-                        std::cout << *result << std::endl;
+                        STORM_PRINT_AND_LOG(*result << std::endl);
                         return;
                     case storm::modelchecker::FilterType::SUM:
-                        std::cout << result->asQuantitativeCheckResult<ValueType>().sum();
+                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().sum());
                         return;
                     case storm::modelchecker::FilterType::AVG:
-                        std::cout << result->asQuantitativeCheckResult<ValueType>().average();
+                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().average());
                         return;
                     case storm::modelchecker::FilterType::MIN:
-                        std::cout << result->asQuantitativeCheckResult<ValueType>().getMin();
+                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMin());
                         return;
                     case storm::modelchecker::FilterType::MAX:
-                        std::cout << result->asQuantitativeCheckResult<ValueType>().getMax();
+                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMax());
                         return;
                     case storm::modelchecker::FilterType::ARGMIN:
                     case storm::modelchecker::FilterType::ARGMAX:
@@ -47,16 +47,16 @@ namespace storm {
             } else {
                 switch (ft) {
                     case storm::modelchecker::FilterType::VALUES:
-                        std::cout << *result << std::endl;
+                        STORM_PRINT_AND_LOG(*result << std::endl);
                         return;
                     case storm::modelchecker::FilterType::EXISTS:
-                        std::cout << result->asQualitativeCheckResult().existsTrue();
+                        STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue());
                         return;
                     case storm::modelchecker::FilterType::FORALL:
-                        std::cout << result->asQualitativeCheckResult().forallTrue();
+                        STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue());
                         return;
                     case storm::modelchecker::FilterType::COUNT:
-                        std::cout << result->asQualitativeCheckResult().count();
+                        STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count());
                         return;
                         
                     case storm::modelchecker::FilterType::ARGMIN:
@@ -75,17 +75,19 @@ namespace storm {
         template<typename ValueType>
         void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             for (auto const& property : properties) {
-                std::cout << std::endl << "Model checking property: " << property << " ...";
+                STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
                 std::cout.flush();
+                storm::utility::Stopwatch modelCheckingWatch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+                modelCheckingWatch.stop();
                 if (result) {
-                    std::cout << " done." << std::endl;
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
-                    std::cout << "Result (initial states): ";
+                    STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                     applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
-                    std::cout << std::endl;
+                    STORM_PRINT_AND_LOG(std::endl);
                 } else {
-                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
             }
         }
@@ -96,17 +98,19 @@ namespace storm {
 
             for (auto const& property : properties) {
                 STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs.");
-                std::cout << std::endl << "Model checking property: " << property << " ...";
+                STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
                 std::cout.flush();
+                storm::utility::Stopwatch modelCheckingWatch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+                modelCheckingWatch.stop();
                 if (result) {
-                    std::cout << " done." << std::endl;
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
-                    std::cout << "Result (initial states): ";
+                    STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                     applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType());
-                    std::cout << std::endl;
+                    STORM_PRINT_AND_LOG(std::endl);
                 } else {
-                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
 
                 if (storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultToFile()) {
@@ -120,15 +124,17 @@ namespace storm {
         void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             typedef double ValueType;
             for (auto const& property : properties) {
-                std::cout << std::endl << "Model checking property: " << property << " ...";
+                STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
                 std::cout.flush();
+                storm::utility::Stopwatch modelCheckingWatch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+                modelCheckingWatch.stop();
                 if (result) {
-                    std::cout << " done." << std::endl;
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
-                    std::cout << "Result (initial states): ";
+                    STORM_PRINT_AND_LOG("Result (initial states): ");
-                    std::cout << *result << std::endl;
+                    STORM_PRINT_AND_LOG(*result << std::endl);
                 } else {
-                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
             }
         }
@@ -140,18 +146,22 @@ namespace storm {
             STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
 
             for (auto const& property : formulas) {
-                std::cout << std::endl << "Model checking property: " << property << " ...";
+                STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
                 std::cout.flush();
                 bool formulaSupported = false;
                 std::unique_ptr<storm::modelchecker::CheckResult> result;
 
+                storm::utility::Stopwatch modelCheckingWatch(false);
+                
                 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);
 
                     formulaSupported = checker.canHandle(task);
                     if (formulaSupported) {
+                        modelCheckingWatch.start();
                         result = checker.check(task);
+                        modelCheckingWatch.stop();
                     }
                 } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
                     storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<ValueType>> checker(program);
@@ -159,23 +169,25 @@ namespace storm {
 
                     formulaSupported = checker.canHandle(task);
                     if (formulaSupported) {
+                        modelCheckingWatch.start();
                         result = checker.check(task);
+                        modelCheckingWatch.stop();
                     }
                 } else {
                     // Should be catched before.
                     assert(false);
                 }
                 if (!formulaSupported) {
-                    std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the formula cannot be handled by the selected engine/method." << std::endl);
                 }
 
                 if (result) {
-                    std::cout << " done." << std::endl;
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
-                    std::cout << "Result (initial states): ";
+                    STORM_PRINT_AND_LOG("Result (initial states): ");
                     applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
-                    std::cout << std::endl;
+                    STORM_PRINT_AND_LOG(std::endl);
                 } else {
-                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
             }
         }
@@ -190,18 +202,21 @@ namespace storm {
         template<storm::dd::DdType DdType>
         void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& property : formulas) {
-                std::cout << std::endl << "Model checking property: " << property << " ...";
+                STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
                 std::cout.flush();
+                
+                storm::utility::Stopwatch modelCheckingWatch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+                modelCheckingWatch.stop();
 
                 if (result) {
-                    std::cout << " done." << std::endl;
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
-                    std::cout << "Result (initial states): ";
+                    STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
                     applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
-                    std::cout << std::endl;
+                    STORM_PRINT_AND_LOG(std::endl);
                 } else {
-                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
             }
         }
@@ -209,17 +224,20 @@ namespace storm {
         template<storm::dd::DdType DdType>
         void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& property : formulas) {
-                std::cout << std::endl << "Model checking property: " << property << " ...";
+                STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
                 std::cout.flush();
+                
+                storm::utility::Stopwatch modelCheckingWatch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+                modelCheckingWatch.stop();
                 if (result) {
-                    std::cout << " done." << std::endl;
+                    STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
-                    std::cout << "Result (initial states): ";
+                    STORM_PRINT_AND_LOG("Result (initial states): ");
                     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
                     applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
-                    std::cout << std::endl;
+                    STORM_PRINT_AND_LOG(std::endl);
                 } else {
-                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
                 }
             }
         }
@@ -267,7 +285,10 @@ namespace storm {
         template<storm::dd::DdType LibraryType>
         void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             // Start by building the model.
+            storm::utility::Stopwatch modelBuildingWatch(true);
             auto markovModel = buildSymbolicModel<double, LibraryType>(model, extractFormulasFromProperties(properties));
+            modelBuildingWatch.stop();
+            STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
             
             // Print some information about the model.
             markovModel->printModelInformationToStream(std::cout);
@@ -284,7 +305,10 @@ namespace storm {
         void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             auto formulas = extractFormulasFromProperties(properties);
             // Start by building the model.
+            storm::utility::Stopwatch modelBuildingWatch(true);
             std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas);
+            modelBuildingWatch.stop();
+            STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
 
             STORM_LOG_THROW(markovModel, storm::exceptions::UnexpectedException, "The model was not successfully built.");
             
@@ -359,7 +383,11 @@ namespace storm {
             storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>();
 
             STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
+
+            storm::utility::Stopwatch modelBuildingWatch(true);
             std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none);
+            modelBuildingWatch.stop();
+            STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl);
             
             // Preprocess the model if needed.
             BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties));

src/storm/logic/Formula.cpp

@@ -443,6 +443,11 @@ namespace storm {
             return visitor.substitute(*this);
         }
         
+        std::shared_ptr<Formula> Formula::substitute(std::map<std::string, std::string> const& labelSubstitution) const {
+            LabelSubstitutionVisitor visitor(labelSubstitution);
+            return visitor.substitute(*this);
+        }
+        
         storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) const {
             ToExpressionVisitor visitor;
             if (labelToExpressionMapping.empty()) {

src/storm/logic/Formula.h

@@ -197,6 +197,7 @@ namespace storm {
             
             std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             std::shared_ptr<Formula> substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const;
+            std::shared_ptr<Formula> substitute(std::map<std::string, std::string> const& labelSubstitution) const;
 
             /*!
              * Takes the formula and converts it to an equivalent expression. The formula may contain atomic labels, but

src/storm/logic/LabelSubstitutionVisitor.cpp

@@ -5,7 +5,11 @@
 namespace storm {
     namespace logic {
         
-        LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) : labelToExpressionMapping(labelToExpressionMapping) {
+        LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) : labelToExpressionMapping(&labelToExpressionMapping), labelToLabelMapping(nullptr) {
+            // Intentionally left empty.
+        }
+
+        LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, std::string> const& labelToLabelMapping) : labelToExpressionMapping(nullptr), labelToLabelMapping(&labelToLabelMapping) {
             // Intentionally left empty.
         }
         
@@ -15,11 +19,20 @@ namespace storm {
         }
         
         boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
-            auto it = labelToExpressionMapping.find(f.getLabel());
+            if (labelToExpressionMapping) {
-            if (it != labelToExpressionMapping.end()) {
+                auto it = labelToExpressionMapping->find(f.getLabel());
+                if (it != labelToExpressionMapping->end()) {
                     return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(it->second));
                 } else {
-                return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f));
+                    return f.asSharedPointer();
+                }
+            } else {
+                auto it = labelToLabelMapping->find(f.getLabel());
+                if (it != labelToLabelMapping->end()) {
+                    return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(it->second));
+                } else {
+                    return f.asSharedPointer();
+                }
             }
         }
     }

src/storm/logic/LabelSubstitutionVisitor.h

@@ -13,13 +13,15 @@ namespace storm {
         class LabelSubstitutionVisitor : public CloneVisitor {
         public:
             LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping);
+            LabelSubstitutionVisitor(std::map<std::string, std::string> const& labelToLabelMapping);
             
             std::shared_ptr<Formula> substitute(Formula const& f) const;
             
             virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
             
         private:
-            std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping;
+            std::map<std::string, storm::expressions::Expression> const* labelToExpressionMapping;
+            std::map<std::string, std::string> const* labelToLabelMapping;
         };
         
     }

src/storm/modelchecker/results/CheckResult.cpp

@@ -39,7 +39,7 @@ namespace storm {
             return false;
         }
         
-        std::ostream& operator<<(std::ostream& out, CheckResult& checkResult) {
+        std::ostream& operator<<(std::ostream& out, CheckResult const& checkResult) {
             checkResult.writeToStream(out);
             return out;
         }

src/storm/modelchecker/results/CheckResult.h

@@ -106,7 +106,7 @@ namespace storm {
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
         };
         
-        std::ostream& operator<<(std::ostream& out, CheckResult& checkResult);
+        std::ostream& operator<<(std::ostream& out, CheckResult const& checkResult);
     }
 }
 

src/storm/models/ModelBase.h

@@ -61,13 +61,6 @@ namespace storm {
              */
             virtual uint_fast64_t getNumberOfTransitions() const = 0;
                         
-            /*!
-             * Retrieves (an approximation of) the size of the model in bytes.
-             *
-             * @return The size of th model in bytes.
-             */
-            virtual std::size_t getSizeInBytes() const = 0;
-            
             /*!
              * Prints information about the model to the specified stream.
              *

src/storm/models/sparse/MarkovAutomaton.cpp

@@ -236,11 +236,6 @@ namespace storm {
                 }
             }
             
-            template <typename ValueType, typename RewardModelType>
-            std::size_t MarkovAutomaton<ValueType, RewardModelType>::getSizeInBytes() const {
-                return NondeterministicModel<ValueType, RewardModelType>::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType);
-            }
-            
             template <typename ValueType, typename RewardModelType>
             void MarkovAutomaton<ValueType, RewardModelType>::turnRatesToProbabilities() {
                 this->exitRates.resize(this->getNumberOfStates());

src/storm/models/sparse/MarkovAutomaton.h

@@ -195,8 +195,6 @@ namespace storm {
                 
                 virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;
                                 
-                std::size_t getSizeInBytes() const override;
-                
                 virtual void printModelInformationToStream(std::ostream& out) const override;
                 
             private:

src/storm/models/sparse/Model.cpp

@@ -188,18 +188,6 @@ namespace storm {
                 return static_cast<bool>(choiceLabeling);
             }
             
-            template<typename ValueType, typename RewardModelType>
-            std::size_t Model<ValueType, RewardModelType>::getSizeInBytes() const {
-                std::size_t result = transitionMatrix.getSizeInBytes() + stateLabeling.getSizeInBytes();
-                for (auto const& rewardModel : this->rewardModels) {
-                    result += rewardModel.second.getSizeInBytes();
-                }
-                if (hasChoiceLabeling()) {
-                    result += getChoiceLabeling().size() * sizeof(LabelSet);
-                }
-                return result;
-            }
-            
             template<typename ValueType, typename RewardModelType>
             void Model<ValueType, RewardModelType>::printModelInformationToStream(std::ostream& out) const {
                 this->printModelInformationHeaderToStream(out);
@@ -219,7 +207,6 @@ namespace storm {
                 this->printRewardModelsInformationToStream(out);
                 this->getStateLabeling().printLabelingInformationToStream(out);
                 out << "choice labels: \t" << (this->hasChoiceLabeling() ? "yes" : "no")  << std::noboolalpha << std::endl;
-                out << "Size in memory: " << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
                 out << "-------------------------------------------------------------- " << std::endl;
             }
             

src/storm/models/sparse/Model.h

@@ -276,13 +276,6 @@ namespace storm {
                  */
                 virtual void reduceToStateBasedRewards() = 0;
                                 
-                /*!
-                 * Retrieves (an approximation of) the size of the model in bytes.
-                 *
-                 * @return The size of the internal representation of the model measured in bytes.
-                 */
-                virtual std::size_t getSizeInBytes() const override;
-                
                 /*!
                  * Prints information about the model to the specified stream.
                  *

src/storm/models/sparse/StandardRewardModel.cpp

@@ -270,22 +270,6 @@ namespace storm {
                 return true;
             }
 
-
-            template<typename ValueType>
-            std::size_t StandardRewardModel<ValueType>::getSizeInBytes() const {
-                std::size_t result = 0;
-                if (this->hasStateRewards()) {
-                    result += this->getStateRewardVector().size() * sizeof(ValueType);
-                }
-                if (this->hasStateActionRewards()) {
-                    result += this->getStateActionRewardVector().size() * sizeof(ValueType);
-                }
-                if (this->hasTransitionRewards()) {
-                    result += this->getTransitionRewardMatrix().getSizeInBytes();
-                }
-                return result;
-            }
-            
             template <typename ValueType>
             std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel) {
                 out << std::boolalpha << "reward model [state reward: "

src/storm/models/sparse/StandardRewardModel.h

@@ -275,13 +275,6 @@ namespace storm {
                  */
                 bool isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const;
                 
-                /*!
-                 * Retrieves (an approximation of) the size of the model in bytes.
-                 *
-                 * @return The size of the internal representation of the model measured in bytes.
-                 */
-                std::size_t getSizeInBytes() const;
-                
                 template <typename ValueTypePrime>
                 friend std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueTypePrime> const& rewardModel);
                 

src/storm/models/sparse/StateLabeling.cpp

@@ -109,14 +109,6 @@ namespace storm {
                 this->labelings[nameToLabelingIndexMap.at(label)] = labeling;
             }
             
-            std::size_t StateLabeling::getSizeInBytes() const {
-                std::size_t result = sizeof(*this);
-                if (!labelings.empty()) {
-                    result += labelings.size() * labelings.front().getSizeInBytes();
-                }
-                return result;
-            }
-            
             void StateLabeling::printLabelingInformationToStream(std::ostream& out) const {
                 out << "Labels: \t" << this->getNumberOfLabels() << std::endl;
                 for (auto const& labelIndexPair : this->nameToLabelingIndexMap) {

src/storm/models/sparse/StateLabeling.h

@@ -146,13 +146,6 @@ namespace storm {
                  */
                 void setStates(std::string const& label, storage::BitVector&& labeling);
                                 
-                /*!
-                 * Returns (an approximation of) the size of the labeling measured in bytes.
-                 *
-                 * @return The size of the labeling measured in bytes.
-                 */
-                std::size_t getSizeInBytes() const;
-                
                 /*!
                  * Prints information about the labeling to the specified stream.
                  *

src/storm/models/symbolic/Model.cpp

@@ -114,12 +114,6 @@ namespace storm {
                 return this->getTransitionMatrix().notZero();
             }
             
-            template<storm::dd::DdType Type, typename ValueType>
-            std::size_t Model<Type, ValueType>::getSizeInBytes() const {
-                // FIXME: This assumes a fixed value of 16 bytes per node, which isn't necessarily true.
-                return sizeof(*this) + 16 * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount());
-            }
-            
             template<storm::dd::DdType Type, typename ValueType>
             std::set<storm::expressions::Variable> const& Model<Type, ValueType>::getRowVariables() const {
                 return rowVariables;
@@ -222,7 +216,6 @@ namespace storm {
                 for (auto const& label : labelToExpressionMap) {
                     out << "   * " << label.first << std::endl;
                 }
-                out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
                 out << "-------------------------------------------------------------- " << std::endl;
             }
             

src/storm/models/symbolic/Model.h

@@ -254,8 +254,6 @@ namespace storm {
                  */
                 uint_fast64_t getNumberOfRewardModels() const;
                 
-                virtual std::size_t getSizeInBytes() const override;
-                
                 virtual void printModelInformationToStream(std::ostream& out) const override;
                 
                 virtual bool isSymbolicModel() const override;

src/storm/parser/DeterministicSparseTransitionParser.cpp

@@ -54,7 +54,7 @@ namespace storm {
             bool insertDiagonalEntriesIfMissing = !isRewardFile;
             DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData(), insertDiagonalEntriesIfMissing);
 
-            STORM_LOG_INFO("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
+            STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros.");
 
             // If first pass returned zero, the file format was wrong.
             if (firstPass.numberOfNonzeroEntries == 0) {

src/storm/settings/modules/IOSettings.cpp

@@ -195,7 +195,6 @@ namespace storm {
                 return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString());
             }
 
-            
             bool IOSettings::isPrismCompatibilityEnabled() const {
                 return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
             }

src/storm/solver/GmmxxLinearEquationSolver.cpp

@@ -138,7 +138,7 @@ namespace storm {
         bool GmmxxLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             auto method = this->getSettings().getSolutionMethod();
             auto preconditioner = this->getSettings().getPreconditioner();
-            STORM_LOG_INFO("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations).");
+            STORM_LOG_DEBUG("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations).");
             if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi && preconditioner != GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) {
                 STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored.");
             }
@@ -193,7 +193,7 @@ namespace storm {
                 
                 // Check if the solver converged and issue a warning otherwise.
                 if (iter.converged()) {
-                    STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations.");
+                    STORM_LOG_DEBUG("Iterative solver converged after " << iter.get_iteration() << " iterations.");
                     return true;
                 } else {
                     STORM_LOG_WARN("Iterative solver did not converge.");
@@ -204,7 +204,7 @@ namespace storm {
                 
                 // Check if the solver converged and issue a warning otherwise.
                 if (iterations < this->getSettings().getMaximalNumberOfIterations()) {
-                    STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
+                    STORM_LOG_DEBUG("Iterative solver converged after " << iterations << " iterations.");
                     return true;
                 } else {
                     STORM_LOG_WARN("Iterative solver did not converge.");

src/storm/storage/SparseMatrix.cpp

@@ -1295,19 +1295,6 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        std::size_t SparseMatrix<ValueType>::getSizeInBytes() const {
-            uint_fast64_t size = sizeof(*this);
-            
-            // Add size of columns and values.
-            size += sizeof(MatrixEntry<index_type, ValueType>) * columnsAndValues.capacity();
-            
-            // Add row_indications size.
-            size += sizeof(uint_fast64_t) * rowIndications.capacity();
-            
-            return size;
-        }
-        
         template<typename ValueType>
         typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRows(index_type startRow, index_type endRow) const {
             return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);

src/storm/storage/SparseMatrix.h

@@ -847,13 +847,6 @@ namespace storm {
              */
             void printAsMatlabMatrix(std::ostream& out) const;
             
-            /*!
-             * Returns the size of the matrix in memory measured in bytes.
-             *
-             * @return The size of the matrix in memory measured in bytes.
-             */
-            std::size_t getSizeInBytes() const;
-            
             /*!
              * Calculates a hash value over all values contained in the matrix.
              *

src/storm/storage/SymbolicModelDescription.cpp

@@ -126,6 +126,18 @@ namespace storm {
             }
         }
         
+        std::pair<SymbolicModelDescription, std::map<std::string, std::string>> SymbolicModelDescription::toJaniWithLabelRenaming(bool makeVariablesGlobal) const {
+            if (this->isJaniModel()) {
+                return std::make_pair(*this, std::map<std::string, std::string>());
+            }
+            if (this->isPrismProgram()) {
+                auto modelAndRenaming = this->asPrismProgram().toJaniWithLabelRenaming(makeVariablesGlobal);
+                return std::make_pair(SymbolicModelDescription(modelAndRenaming.first), modelAndRenaming.second);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
+            }
+        }
+        
         SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
             std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = parseConstantDefinitions(constantDefinitionString);
             if (this->isJaniModel()) {

src/storm/storage/SymbolicModelDescription.h

@@ -39,6 +39,7 @@ namespace storm {
             std::vector<std::string> getParameterNames() const;
             
             SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
+            std::pair<SymbolicModelDescription, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool makeVariablesGlobal = true) const;
             
             SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
             SymbolicModelDescription preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;

src/storm/storage/jani/Property.cpp

@@ -32,6 +32,10 @@ namespace storm {
             return Property(name, filterExpression.substitute(substitution), comment);
         }
         
+        Property Property::substituteLabels(std::map<std::string, std::string> const& substitution) const {
+            return Property(name, filterExpression.substituteLabels(substitution), comment);
+        }
+        
         FilterExpression const& Property::getFilter() const {
             return this->filterExpression;
         }

src/storm/storage/jani/Property.h

@@ -42,6 +42,11 @@ namespace storm {
             FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
                 return FilterExpression(formula->substitute(substitution), ft);
             }
+            
+            FilterExpression substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const {
+                return FilterExpression(formula->substitute(labelSubstitution), ft);
+            }
+
         private:
             // For now, we assume that the states are always the initial states.
             std::shared_ptr<storm::logic::Formula const> formula;
@@ -84,6 +89,7 @@ namespace storm {
             std::string const& getComment() const;
             
             Property substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+            Property substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const;
             
             FilterExpression const& getFilter() const;
             

src/storm/storage/prism/Program.cpp

@@ -5,6 +5,7 @@
 #include <boost/algorithm/string/join.hpp>
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
 
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/settings/SettingsManager.h"
@@ -1009,7 +1010,6 @@ namespace storm {
             std::set<storm::expressions::Variable> variablesAndConstants;
             std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
             
-            
             // Check the commands of the modules.
             bool hasProbabilisticCommand = false;
             bool hasMarkovianCommand = false;
@@ -1627,7 +1627,15 @@ namespace storm {
         
         storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
             ToJaniConverter converter;
-            return converter.convert(*this, allVariablesGlobal);
+            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal);
+            STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
+            return resultingModel;
+        }
+
+        std::pair<storm::jani::Model, std::map<std::string, std::string>> Program::toJaniWithLabelRenaming(bool allVariablesGlobal) const {
+            ToJaniConverter converter;
+            storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal);
+            return std::make_pair(resultingModel, converter.getLabelRenaming());
         }
 
         storm::expressions::ExpressionManager& Program::getManager() const {

src/storm/storage/prism/Program.h

@@ -22,6 +22,7 @@
 namespace storm {
     namespace jani {
         class Model;
+        class Property;
     }
     
     namespace prism {
@@ -587,6 +588,12 @@ namespace storm {
              */
             storm::jani::Model toJani(bool allVariablesGlobal = false) const;
             
+            /*!
+             * Converts the PRISM model into an equivalent JANI model and retrieves possible label renamings that had
+             * to be performed in the process.
+             */
+            std::pair<storm::jani::Model, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool allVariablesGlobal = false) const;
+            
         private:
             /*!
              * This function builds a command that corresponds to the synchronization of the given list of commands.

src/storm/storage/prism/ToJaniConverter.cpp

@@ -12,7 +12,7 @@
 namespace storm {
     namespace prism {
         
-        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal) const {
+        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal) {
             std::shared_ptr<storm::expressions::ExpressionManager> manager = program.getManager().getSharedPointer();
                         
             // Start by creating an empty JANI model.
@@ -97,9 +97,14 @@ namespace storm {
             // Go through the labels and construct assignments to transient variables that are added to the loctions.
             std::vector<storm::jani::Assignment> transientLocationAssignments;
             for (auto const& label : program.getLabels()) {
-                auto newExpressionVariable = manager->declareBooleanVariable("label_" + label.getName());
+                bool renameLabel = manager->hasVariable(label.getName()) || program.hasRewardModel(label.getName());
+                std::string finalLabelName = renameLabel ? "label_" + label.getName() : label.getName();
+                if (renameLabel) {
+                    STORM_LOG_WARN_COND(!renameLabel, "Label '" << label.getName() << "' was renamed to '" << finalLabelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists.");
+                    labelRenaming[label.getName()] = finalLabelName;
+                }
+                auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName);
                 storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true));
-
                 transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression());
             }
             
@@ -284,5 +289,13 @@ namespace storm {
             return janiModel;
         }
         
+        bool ToJaniConverter::labelsWereRenamed() const {
+            return !labelRenaming.empty();
+        }
+        
+        std::map<std::string, std::string> const& ToJaniConverter::getLabelRenaming() const {
+            return labelRenaming;
+        }
+        
     }
 }

src/storm/storage/prism/ToJaniConverter.h

@@ -1,5 +1,8 @@
 #pragma once
 
+#include <map>
+#include <string>
+
 namespace storm {
     namespace jani {
         class Model;
@@ -11,7 +14,13 @@ namespace storm {
         
         class ToJaniConverter {
         public:
-            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false) const;
+            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false);
+            
+            bool labelsWereRenamed() const;
+            std::map<std::string, std::string> const& getLabelRenaming() const;
+            
+        private:
+            std::map<std::string, std::string> labelRenaming;
         };
         
     }

src/storm/storm.cpp

@@ -32,7 +32,7 @@ int main(const int argc, const char** argv) {
         totalTimer.stop();
 
         if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
-            storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeMilliseconds());
+            storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds());
         }
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {

src/storm/utility/Stopwatch.cpp

@@ -0,0 +1,51 @@
+#include "storm/utility/Stopwatch.h"
+
+namespace storm {
+    namespace utility {
+        
+        Stopwatch::Stopwatch(bool startNow) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
+            if (startNow) {
+                start();
+            }
+        }
+        
+        Stopwatch::SecondType Stopwatch::getTimeInSeconds() const {
+            return std::chrono::duration_cast<std::chrono::seconds>(accumulatedTime).count();
+        }
+        
+        Stopwatch::MilisecondType Stopwatch::getTimeInMilliseconds() const {
+            return std::chrono::duration_cast<std::chrono::milliseconds>(accumulatedTime).count();
+        }
+        
+        Stopwatch::NanosecondType Stopwatch::getTimeInNanoseconds() const {
+            return accumulatedTime.count();
+        }
+        
+        void Stopwatch::addToTime(std::chrono::nanoseconds timeNanoseconds) {
+            accumulatedTime += timeNanoseconds;
+        }
+        
+        void Stopwatch::stop() {
+            STORM_LOG_WARN_COND(!stopped, "Stopwatch is already paused.");
+            stopped = true;
+            accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement;
+        }
+        
+        void Stopwatch::start() {
+            STORM_LOG_WARN_COND(stopped, "Stopwatch is already running.");
+            stopped = false;
+            startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
+        }
+        
+        void Stopwatch::reset() {
+            accumulatedTime = std::chrono::nanoseconds::zero();
+            stopped = true;
+        }
+        
+        std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {
+            out << stopwatch.getTimeInSeconds() << "." << (stopwatch.getTimeInMilliseconds() % 1000) << "s";
+            return out;
+        }
+        
+    }
+}

src/storm/utility/Stopwatch.h

@@ -13,106 +13,68 @@ namespace storm {
          */
         class Stopwatch {
         public:
+            typedef decltype(std::chrono::duration_cast<std::chrono::seconds>(std::chrono::seconds::zero()).count()) SecondType;
+            typedef decltype(std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::milliseconds::zero()).count()) MilisecondType;
+            typedef decltype(std::chrono::duration_cast<std::chrono::nanoseconds>(std::chrono::nanoseconds::zero()).count()) NanosecondType;
             
             /*!
              * Constructor.
              *
              * @param startNow If true, the stopwatch starts right away.
              */
-            Stopwatch(bool startNow = false) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
+            Stopwatch(bool startNow = false);
-                if (startNow) {
-                    start();
-                }
-            }
-
-            /*!
-             * Destructor.
-             */
-            ~Stopwatch() = default;
 
             /*!
-             * Get measured time in seconds.
+             * Gets the measured time in seconds.
-             *
-             * @return seconds as floating point number.
              */
-            double getTimeSeconds() const {
+            SecondType getTimeInSeconds() const;
-                return std::chrono::duration<float>(accumulatedTime).count();
-            }
 
             /*!
-             * Get measured time in milliseconds.
+             * Gets the measured time in milliseconds.
-             *
-             * @return Milliseconds.
              */
-            unsigned long long int getTimeMilliseconds() const {
+            MilisecondType getTimeInMilliseconds() const;
-                return std::chrono::duration_cast<std::chrono::milliseconds>(accumulatedTime).count();
-            }
 
             /*!
-             * Get measured time in nanoseconds.
+             * Gets the measured time in nanoseconds.
-             *
-             * @return Nanoseconds.
              */
-            unsigned long long int getTimeNanoseconds() const {
+            NanosecondType getTimeInNanoseconds() const;
-                return accumulatedTime.count();
-            }
 
             /*!
              * Add given time to measured time.
              *
              * @param timeNanoseconds Additional time in nanoseconds.
              */
-            void addToTime(std::chrono::nanoseconds timeNanoseconds) {
+            void addToTime(std::chrono::nanoseconds timeNanoseconds);
-                accumulatedTime += timeNanoseconds;
-            }
 
             /*!
              * Stop stopwatch and add measured time to total time.
              */
-            void stop() {
+            void stop();
-                if (stopped) {
-                    // Assertions are only available in DEBUG build and therefore not used here.
-                    STORM_LOG_WARN("Stopwatch is already paused.");
-                }
-                stopped = true;
-                accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement;
-            }
 
             /*!
              * Start stopwatch (again) and start measuring time.
              */
-            void start() {
+            void start();
-                if (!stopped) {
-                    // Assertions are only available in DEBUG build and therefore not used here.
-                    STORM_LOG_WARN("Stopwatch is already running.");
-                }
-                stopped = false;
-                startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
-            }
             
             /*!
-             * Reset the stopwatch. Reset the measured time to zero and stop the stopwatch.
+             * Reset the stopwatch.
              */
-            void reset() {
+            void reset();
-                accumulatedTime = std::chrono::nanoseconds::zero();
-                stopped = true;
-            }
-
-            friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {
-                out << stopwatch.getTimeSeconds();
-                return out;
-            }
 
+            friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch);
             
         private:
-            // Total measured time
+            // The time accumulated so far.
             std::chrono::nanoseconds accumulatedTime;
-            // Flag indicating if the stopwatch is stopped right now.
+            // A flag indicating if the stopwatch is stopped right now.
             bool stopped;
-            // Timepoint when the stopwatch was started the last time.
-            std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;
             
+            // The timepoint when the stopwatch was started the last time (if it's not stopped).
+            std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;
         };
+        
+        std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch);
     }
 }
 

src/storm/utility/storm.h

@@ -96,7 +96,7 @@
 #include "storm/exceptions/NotImplementedException.h"
 #include "storm/exceptions/NotSupportedException.h"
 
-#include "storm/storage/jani/JSONExporter.h"
+#include "storm/utility/Stopwatch.h"
 
 namespace storm {
 
@@ -231,7 +231,11 @@ namespace storm {
     
     template<typename ModelType>
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        storm::utility::Stopwatch preprocessingWatch(true);
+        
+        bool operationPerformed = false;
         if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
+            operationPerformed = true;
             std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
             ma->close();
             if (ma->hasOnlyTrivialNondeterminism()) {
@@ -241,6 +245,7 @@ namespace storm {
         }
 
         if (model->isSparseModel() && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
+            operationPerformed = true;
             storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
             if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
                 bisimType = storm::storage::BisimulationType::Weak;
@@ -250,6 +255,11 @@ namespace storm {
             return performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
         }
 
+        preprocessingWatch.stop();
+        if (operationPerformed) {
+            STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
+        }
+        
         return model;
     }
 
@@ -300,17 +310,17 @@ namespace storm {
         switch(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine()) {
             case storm::settings::modules::CoreSettings::Engine::Sparse: {
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
-                STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
+                STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model.");
                 return (sparseModel, formula, onlyInitialStatesRelevant);
             }
             case storm::settings::modules::CoreSettings::Engine::Hybrid: {
                 std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
-                STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model");
+                STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a DD-based input model.");
                 return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant);
             }
             case storm::settings::modules::CoreSettings::Engine::Dd: {
                 std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
-                STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
+                STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a DD-based input model.");
                 return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
             }
             default: {