runtime statistics output and validation output (temporarily, for testing)

8 years ago · 8043968891
8 changed files with 94 additions and 6 deletions
--- a/src/storm/modelchecker/parametric/ParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@ -19,6 +19,12 @@
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidArgumentException.h"

+#include "storm/utility/Stopwatch.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+
+
 namespace storm {
    namespace modelchecker {
        namespace parametric {
@ -34,7 +40,10 @@ namespace storm {
                STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a property where only the value in the initial states is relevant.");
                STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property.");
                
+                storm::utility::Stopwatch sw(true);
                simplifyParametricModel(checkTask);
+                sw.stop();
+                std::cout << "SIStats: " << sw << std::endl;
                initializeUnderlyingCheckers();
                currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));

@ -83,6 +92,36 @@ namespace storm {
                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
                }
                
+                // TODO remove this:
+                if(storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet() && storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismInputSet() &&  storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {
+                    std::vector<storm::utility::parametric::Valuation<typename SparseModelType::ValueType>> points;
+                    if(result == RegionCheckResult::AllSat || result == RegionCheckResult::AllViolated) {
+                        points = region.getVerticesOfRegion(region.getVariables());
+                        points.push_back(region.getCenterPoint());
+                    } else if (result == RegionCheckResult::CenterSat ||  result == RegionCheckResult::CenterViolated) {
+                        points.push_back(region.getCenterPoint());
+                    }
+                    if(!points.empty()) std::cout << "VALIDATE_REGION:" << region.toString(true) << std::endl;
+                    for (auto const& p : points) {
+                        if((result == RegionCheckResult::AllSat) || (result == RegionCheckResult::CenterSat)) {
+                            std::cout << "EXPECTTRUE:";
+                        } else {
+                            std::cout << "EXPECTFALSE:";
+                        }
+                        std::cout << "STORMEXECUTABLE --prism " << storm::settings::getModule<storm::settings::modules::IOSettings>().getPrismInputFilename()
+                                  <<                 " --prop " <<  storm::settings::getModule<storm::settings::modules::IOSettings>().getProperty();
+                        if( storm::settings::getModule<storm::settings::modules::IOSettings>().isConstantsSet()) {
+                            std::cout <<             " -const " <<  storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
+                        }
+                        for(auto varDef = p.begin(); varDef != p.end(); ++varDef) {
+                            if(varDef!=p.begin())  std::cout << ",";
+                            std::cout << varDef->first << "=" << storm::utility::convertNumber<double>(varDef->second);
+                        }
+                        std::cout << std::endl;
+                    }
+                }
+
+                
                return result;
            }
    
@ -90,6 +129,8 @@ namespace storm {
            std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const {
                STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
                
+                storm::utility::Stopwatch sw(true);
+                
                auto areaOfParameterSpace = region.area();
                auto fractionOfUndiscoveredArea = storm::utility::one<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
                auto fractionOfAllSatArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
@ -131,6 +172,9 @@ namespace storm {
                    ++indexOfCurrentRegion;
                }
                resultRegions.resize(regions.size());
+                
+                sw.stop();
+                std::cout << "REStats: " << sw << std::endl;
                return storm::utility::vector::filterVector(regions, resultRegions);
            }
    
--- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
@ -18,15 +18,25 @@ namespace storm {
            template <typename SparseModelType, typename ConstantType>
            std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
                STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
+                this->swInstantiation.start();
                auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+                this->swInstantiation.stop();
                STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
                storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(instantiatedModel);

                // Check if there are some optimizations implemented for the specified property
+                this->swCheck.start();
                if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
-                    return checkWithHint(modelChecker);
+                    auto result = checkWithHint(modelChecker);
+                    this->swCheck.stop();
+                    return result;
+                    //return checkWithHint(modelChecker);
                } else {
-                    return modelChecker.check(*this->currentCheckTask);
+                    STORM_LOG_WARN("Checking without hint"); // todo:remove this warning
+                    auto result = modelChecker.check(*this->currentCheckTask);
+                    this->swCheck.stop();
+                    return result;
+                    //return modelChecker.check(*this->currentCheckTask);
                }
            }
                
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
@ -166,7 +166,10 @@ namespace storm {
                    return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
                }
                
+                this->swInstantiation.start();
                parameterLifter->specifyRegion(region, dirForParameters);
+                this->swInstantiation.stop();
+                this->swCheck.start();
                
                // Set up the solver
                auto solver = solverFactory->create(parameterLifter->getMatrix());
@ -198,6 +201,7 @@ namespace storm {
                    result[maybeState] = *maybeStateResIt;
                    ++maybeStateResIt;
                }
+                this->swCheck.stop();
                return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
            }
            
--- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
@ -6,6 +6,8 @@
 #include "storm/modelchecker/hints/ModelCheckerHint.h"
 #include "storm/utility/parametric.h"

+#include "storm/utility/Stopwatch.h"
+
 namespace storm {
    namespace modelchecker {
        namespace parametric {
@ -18,6 +20,11 @@ namespace storm {
            public:
                SparseInstantiationModelChecker(SparseModelType const& parametricModel);
                
+                                
+                ~SparseInstantiationModelChecker() {
+                    std::cout << "INStats (instantiation/check): " << swInstantiation << "\t" << swCheck << std::endl;
+                }
+                
                void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
                
                virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
@ -29,6 +36,8 @@ namespace storm {
                
                SparseModelType const& parametricModel;
                std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+                
+                storm::utility::Stopwatch swInstantiation, swCheck;

            private:
                // store the current formula. Note that currentCheckTask only stores a reference to the formula.
--- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
@ -19,19 +19,27 @@ namespace storm {
           template <typename SparseModelType, typename ConstantType>
            std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
                STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
+                this->swInstantiation.start();
                auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+                this->swInstantiation.stop();
                STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
                storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(instantiatedModel);

                // Check if there are some optimizations implemented for the specified property
+                this->swCheck.start();
                if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
-                    return checkWithResultHint(modelChecker);
+                    auto result = checkWithResultHint(modelChecker);
+                    this->swCheck.stop();
+                    return result;
+                    //return checkWithResultHint(modelChecker);
                } else {
-                    return modelChecker.check(*this->currentCheckTask);
+                    auto result = modelChecker.check(*this->currentCheckTask);
+                    this->swCheck.stop();
+                    return result;
+                    //return modelChecker.check(*this->currentCheckTask);
                }
            }
            
-                
            template <typename SparseModelType, typename ConstantType>
            std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelchecker) {
                
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
@ -200,7 +200,10 @@ namespace storm {
                    return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
                }
                
+                this->swInstantiation.start();
                parameterLifter->specifyRegion(region, dirForParameters);
+                this->swInstantiation.stop();
+                this->swCheck.start();
                
                // Set up the solver
                auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix());
@ -238,6 +241,7 @@ namespace storm {
                    result[maybeState] = *maybeStateResIt;
                    ++maybeStateResIt;
                }
+                this->swCheck.stop();
                return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
            }
            
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
@ -22,7 +22,7 @@ namespace storm {
            
            template <typename SparseModelType, typename ConstantType>
            void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                
+                swInit.start();
                reset();
                currentFormula = checkTask.getFormula().asSharedPointer();
                currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
@ -46,6 +46,7 @@ namespace storm {
                        specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
                    }
                }
+                swInit.stop();
            }
            
            template <typename SparseModelType, typename ConstantType>
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
@ -7,6 +7,8 @@
 #include "storm/solver/OptimizationDirection.h"
 #include "storm/utility/parametric.h"

+#include "storm/utility/Stopwatch.h"
+
 namespace storm {
    namespace modelchecker {
        namespace parametric {
@ -22,6 +24,10 @@ namespace storm {
            public:
                SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
                
+                ~SparseParameterLiftingModelChecker() {
+                    std::cout << "PLStats (init/instantiation/check): " << swInit << "\t" << swInstantiation << "\t" << swCheck << std::endl;
+                }
+                
                virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
                
                void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
@ -49,6 +55,8 @@ namespace storm {
                
                SparseModelType const& parametricModel;
                std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+              
+                storm::utility::Stopwatch swInit, swInstantiation, swCheck;

            private:
                // store the current formula. Note that currentCheckTask only stores a reference to the formula.