From 0e88d711e80333b165c3e8b10ece5a0984cb49f2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 11 Jul 2017 10:24:55 +0200 Subject: [PATCH 01/15] Correctly handled reward bounded objectives in multi-objective preprocessing --- .../modelchecker/multiobjective/Objective.h | 4 ++- .../SparseMultiObjectivePreprocessor.cpp | 11 +++++--- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 4 +++ .../pcaa/SparseMdpPcaaWeightVectorChecker.cpp | 28 +++++++++++++++++++ .../pcaa/SparseMdpPcaaWeightVectorChecker.h | 27 ++++++++++++++---- 5 files changed, 64 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h index 09faaf075..d5d269775 100644 --- a/src/storm/modelchecker/multiobjective/Objective.h +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -5,6 +5,7 @@ #include "storm/logic/Formula.h" #include "storm/logic/Bound.h" #include "storm/logic/TimeBound.h" +#include "storm/logic/TimeBoundType.h" #include "storm/solver/OptimizationDirection.h" namespace storm { @@ -28,8 +29,9 @@ namespace storm { // if originalFormula does ot specifies one, the direction is derived from the bound. storm::solver::OptimizationDirection optimizationDirection; - // Lower and upper time/step bouds + // Lower and upper time/step/reward bouds boost::optional lowerTimeBound, upperTimeBound; + boost::optional timeBoundReference; boost::optional lowerResultBound, upperResultBound; diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 485bc41bf..a3c0d9657 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h" #include -#include +#include #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" @@ -12,7 +12,7 @@ #include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/transformer/SubsystemBuilder.h" +#include "storm/transformer/GoalStateMerger.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" @@ -266,8 +266,6 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data) { - STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.getTimeBoundReference().isStepBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); - if (formula.hasLowerBound()) { STORM_LOG_THROW(!formula.getLowerBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The lower time bound for the formula " << formula << " still contains variables"); if (!storm::utility::isZero(formula.getLowerBound()) || formula.isLowerBoundStrict()) { @@ -280,6 +278,8 @@ namespace storm { data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isUpperBoundStrict(), formula.getUpperBound()); } } + + data.objectives.back()->timeBoundReference = formula.getTimeBoundReference(); preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data); } @@ -375,6 +375,9 @@ namespace storm { std::set relevantRewardModels; for (auto const& obj : result.objectives) { relevantRewardModels.insert(*obj.rewardModelName); + if (obj.timeBoundReference->isRewardBound()) { + relevantRewardModels.insert(obj.timeBoundReference->getRewardName()); + } } // Build a subsystem that discards states that yield infinite reward for all schedulers. diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index d3c8e3026..e65aa6325 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -41,6 +41,10 @@ namespace storm { template void SparseMaPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { + for (auto const& obj : this->objectives) { + STORM_LOG_THROW(!obj.timeBoundReference || obj.timeBoundReference->isTimeBound(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking of Markov automata is only supported for time-bounded formulass."); + } + // Split the preprocessed model into transitions from/to probabilistic/Markovian states. SubModel MS = createSubModel(true, weightedRewardVector); SubModel PS = createSubModel(false, weightedRewardVector); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index 40d843f93..0916fd94c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -6,6 +6,9 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/IllegalArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { @@ -28,6 +31,24 @@ namespace storm { template void SparseMdpPcaaWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { + // Check whether reward bounded objectives occur. + bool containsRewardBoundedObjectives = false; + for (auto const& obj : this->objectives) { + if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) { + containsRewardBoundedObjectives = true; + break; + } + } + + if (containsRewardBoundedObjectives) { + boundedPhaseWithRewardBounds(weightVector, weightedRewardVector); + } else { + boundedPhaseOnlyStepBounds(weightVector, weightedRewardVector); + } + } + + template + void SparseMdpPcaaWeightVectorChecker::boundedPhaseOnlyStepBounds(std::vector const& weightVector, std::vector& weightedRewardVector) { // Allocate some memory so this does not need to happen for each time epoch std::vector optimalChoicesInCurrentEpoch(this->model.getNumberOfStates()); std::vector choiceValues(weightedRewardVector.size()); @@ -97,6 +118,13 @@ namespace storm { } } + + template + void SparseMdpPcaaWeightVectorChecker::boundedPhaseWithRewardBounds(std::vector const& weightVector, std::vector& weightedRewardVector) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Multi-objective model checking with reward bounded objectives is not supported."); + } + + template class SparseMdpPcaaWeightVectorChecker>; #ifdef STORM_HAVE_CARL template class SparseMdpPcaaWeightVectorChecker>; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h index 91cb862f1..a04bd9455 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h @@ -19,6 +19,7 @@ namespace storm { class SparseMdpPcaaWeightVectorChecker : public SparsePcaaWeightVectorChecker { public: typedef typename SparseMdpModelType::ValueType ValueType; + typedef typename SparseMdpModelType::RewardModelType RewardModelType; /* * Creates a weight vextor checker. @@ -40,16 +41,32 @@ namespace storm { private: /*! - * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method - * - determines the objectives that are relevant in the current time epoch - * - determines the maximizing scheduler for the weighted reward vector of these objectives - * - computes the values of these objectives w.r.t. this scheduler + * Computes the maximizing scheduler for the weighted sum of the objectives, including also step or reward bounded objectives. + * Moreover, the values of the individual objectives are computed w.r.t. this scheduler. * * @param weightVector the weight vector of the current check * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. */ virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) override; - + + /*! + * Computes the bounded phase for the case that only step bounded objectives are considered. + * + * @param weightVector the weight vector of the current check + * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. + */ + void boundedPhaseOnlyStepBounds(std::vector const& weightVector, std::vector& weightedRewardVector); + + /*! + * Computes the bounded phase for the case that also reward bounded objectives occurr. + * + * @param weightVector the weight vector of the current check + * @param weightedRewardVector the weighted rewards considering the unbounded objectives. Will be invalidated after calling this. + */ + void boundedPhaseWithRewardBounds(std::vector const& weightVector, std::vector& weightedRewardVector); + + + }; } From 275f1ff15eab13ac016a1e9324fb2e74a1a104b5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 11 Jul 2017 10:25:55 +0200 Subject: [PATCH 02/15] only filter the result if there actually is a result and a filter --- src/storm/cli/cli.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index caf3aa0c3..c84fce107 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -683,7 +683,9 @@ namespace storm { } else { filter = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(states, false)); } - result->filter(filter->asQualitativeCheckResult()); + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } return result; }); } @@ -703,8 +705,9 @@ namespace storm { } else { filter = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(states, false)); } - - result->filter(filter->asQualitativeCheckResult()); + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } return result; }); } @@ -724,8 +727,9 @@ namespace storm { } else { filter = storm::api::verifyWithDdEngine(symbolicModel, storm::api::createTask(states, false)); } - - result->filter(filter->asQualitativeCheckResult()); + if (result && filter) { + result->filter(filter->asQualitativeCheckResult()); + } return result; }); } From 9bfb1fedc247618fb1e3b54538dc74b80169dcce Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 11 Jul 2017 14:48:54 +0200 Subject: [PATCH 03/15] requiring that multi objective queries have a multi(..) formula at top level. --- src/storm/logic/FragmentChecker.cpp | 3 +++ src/storm/logic/FragmentSpecification.cpp | 11 +++++++++++ src/storm/logic/FragmentSpecification.h | 4 ++++ .../csl/SparseMarkovAutomatonCslModelChecker.cpp | 4 ++-- .../modelchecker/prctl/SparseMdpPrctlModelChecker.cpp | 4 ++-- 5 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index ee0967d22..6fc458796 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -24,6 +24,9 @@ namespace storm { if (specification.isOperatorAtTopLevelRequired()) { result &= f.isOperatorFormula(); } + if (specification.isMultiObjectiveFormulaAtTopLevelRequired()) { + result &= f.isMultiObjectiveFormula(); + } return result; } diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 19c4116aa..11a3ac2f4 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -88,6 +88,7 @@ namespace storm { FragmentSpecification multiObjective = propositional(); multiObjective.setMultiObjectiveFormulasAllowed(true); + multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true); multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true); multiObjective.setProbabilityOperatorsAllowed(true); multiObjective.setUntilFormulasAllowed(true); @@ -148,6 +149,7 @@ namespace storm { quantitativeOperatorResults = true; operatorAtTopLevelRequired = false; + multiObjectiveFormulaAtTopLevelRequired = false; operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false; } @@ -489,6 +491,15 @@ namespace storm { return *this; } + bool FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired() const { + return multiObjectiveFormulaAtTopLevelRequired; + } + + FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired(bool newValue) { + multiObjectiveFormulaAtTopLevelRequired = newValue; + return *this; + } + bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const { return operatorsAtTopLevelOfMultiObjectiveFormulasRequired; } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 619394189..74d420f5b 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -118,6 +118,9 @@ namespace storm { bool isOperatorAtTopLevelRequired() const; FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue); + bool isMultiObjectiveFormulaAtTopLevelRequired() const; + FragmentSpecification& setMultiObjectiveFormulaAtTopLevelRequired(bool newValue); + bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const; FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue); @@ -170,6 +173,7 @@ namespace storm { bool quantitativeOperatorResults; bool qualitativeOperatorResults; bool operatorAtTopLevelRequired; + bool multiObjectiveFormulaAtTopLevelRequired; bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired; }; diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 2f90c23d5..1bd826c7f 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -39,8 +39,8 @@ namespace storm { } else { // Check whether we consider a multi-objective formula // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude multiple initial states. - if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; return formula.isInFragment(storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true)); } } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 4aaee1400..a40d04f08 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -48,8 +48,8 @@ namespace storm { } else { // Check whether we consider a multi-objective formula // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states. - if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; - if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if (!checkTask.isOnlyInitialStatesRelevantSet()) return false; return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true)); } } From 8aa2b57640f401730000811f8f9bb8d9a11e7ba5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 11 Jul 2017 15:57:48 +0200 Subject: [PATCH 04/15] minor fix for multi-objective preprocessor --- .../multiobjective/SparseMultiObjectivePreprocessor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index a3c0d9657..0596303c8 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -375,7 +375,7 @@ namespace storm { std::set relevantRewardModels; for (auto const& obj : result.objectives) { relevantRewardModels.insert(*obj.rewardModelName); - if (obj.timeBoundReference->isRewardBound()) { + if (obj.timeBoundReference && obj.timeBoundReference->isRewardBound()) { relevantRewardModels.insert(obj.timeBoundReference->getRewardName()); } } From 959115799634005adab834c977a1f2473e0b209a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 11 Jul 2017 19:04:40 +0200 Subject: [PATCH 05/15] new features for storm-pars api: - depth limit for iterative refinement - the regions with inconclusive result are now also part of the result - when analyzing a region, a hypothesis (AllSat or AllViolated) can now be given --- src/storm-pars-cli/storm-pars.cpp | 4 +- src/storm-pars/api/region.h | 27 ++++++-- .../region/RegionModelChecker.cpp | 56 ++++++++++----- .../modelchecker/region/RegionModelChecker.h | 20 ++++-- .../region/RegionResultHypothesis.cpp | 25 +++++++ .../region/RegionResultHypothesis.h | 19 ++++++ .../SparseParameterLiftingModelChecker.cpp | 12 ++-- .../SparseParameterLiftingModelChecker.h | 6 +- ...tingSparseParameterLiftingModelChecker.cpp | 21 +++--- ...datingSparseParameterLiftingModelChecker.h | 2 +- .../results/RegionRefinementCheckResult.cpp | 3 + .../SparseDtmcParameterLiftingTest.cpp | 68 +++++++++---------- .../SparseMdpParameterLiftingTest.cpp | 56 +++++++-------- 13 files changed, 206 insertions(+), 113 deletions(-) create mode 100644 src/storm-pars/modelchecker/region/RegionResultHypothesis.cpp create mode 100644 src/storm-pars/modelchecker/region/RegionResultHypothesis.h diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index bc52f85dc..52d6dff39 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -224,7 +224,7 @@ namespace storm { STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getRefinementThreshold()); - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), refinementThreshold, engine); + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold); return result; }; } else { @@ -237,7 +237,7 @@ namespace storm { postprocessingCallback = [&] (std::unique_ptr const& result) { if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath(), false); } }; diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index a8cc6bbe2..85a481d2d 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -13,6 +13,7 @@ #include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h" #include "storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h" #include "storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/RegionResultHypothesis.h" #include "storm-pars/parser/ParameterRegionParser.h" #include "storm-pars/storage/ParameterRegion.h" #include "storm-pars/utility/parameterlifting.h" @@ -153,21 +154,33 @@ namespace storm { } template - std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine) { + std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine, std::vector const& hypotheses, bool sampleVerticesOfRegions) { auto regionChecker = initializeRegionModelChecker(model, task, engine); - return regionChecker->analyzeRegions(regions, true); + return regionChecker->analyzeRegions(regions, hypotheses, sampleVerticesOfRegions); } - template - std::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, ValueType const& refinementThreshold, storm::modelchecker::RegionCheckEngine engine) { + std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::RegionResultHypothesis const& hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown, bool sampleVerticesOfRegions = false) { + std::vector hypotheses(regions.size(), hypothesis); + return checkRegionsWithSparseEngine(model, task, regions, engine, hypotheses, sampleVerticesOfRegions); + } + + /*! + * Checks and iteratively refines the given region with the sparse engine + * @param engine The considered region checking engine + * @param coverageThreshold if given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold + * @param refinementDepthThreshold if given, the refinement stops at the given depth. depth=0 means no refinement. + * @param hypothesis if not 'unknown', it is only checked whether the hypothesis holds (and NOT the complementary result). + */ + template + std::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, storm::modelchecker::RegionCheckEngine engine, boost::optional const& coverageThreshold, boost::optional const& refinementDepthThreshold = boost::none, storm::modelchecker::RegionResultHypothesis hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown) { auto regionChecker = initializeRegionModelChecker(model, task, engine); - return regionChecker->performRegionRefinement(region, refinementThreshold); + return regionChecker->performRegionRefinement(region, coverageThreshold, refinementDepthThreshold, hypothesis); } template - void exportRegionCheckResultToFile(std::unique_ptr const& checkResult, std::string const& filename) { + void exportRegionCheckResultToFile(std::unique_ptr const& checkResult, std::string const& filename, bool onlyConclusiveResults = false) { auto const* regionCheckResult = dynamic_cast const*>(checkResult.get()); STORM_LOG_THROW(regionCheckResult != nullptr, storm::exceptions::UnexpectedException, "Can not export region check result: The given checkresult does not have the expected type."); @@ -175,7 +188,9 @@ namespace storm { std::ofstream filestream; storm::utility::openFile(filename, filestream); for (auto const& res : regionCheckResult->getRegionResults()) { + if (!onlyConclusiveResults || res.second == storm::modelchecker::RegionResult::AllViolated || res.second == storm::modelchecker::RegionResult::AllSat) { filestream << res.second << ": " << res.first << std::endl; + } } } diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp index a2a19451d..23ba29489 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp @@ -28,31 +28,40 @@ namespace storm { } template - std::unique_ptr> RegionModelChecker::analyzeRegions(std::vector> const& regions, bool sampleVerticesOfRegion) { + std::unique_ptr> RegionModelChecker::analyzeRegions(std::vector> const& regions, std::vector const& hypotheses, bool sampleVerticesOfRegion) { + STORM_LOG_THROW(regions.size() == hypotheses.size(), storm::exceptions::InvalidArgumentException, "The number of regions and the number of hypotheses do not match"); std::vector, storm::modelchecker::RegionResult>> result; + auto hypothesisIt = hypotheses.begin(); for (auto const& region : regions) { - storm::modelchecker::RegionResult regionRes = analyzeRegion(region, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion); + storm::modelchecker::RegionResult regionRes = analyzeRegion(region, *hypothesisIt, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion); result.emplace_back(region, regionRes); + ++hypothesisIt; } return std::make_unique>(std::move(result)); } template - std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, ParametricType const& threshold) { + std::unique_ptr> RegionModelChecker::performRegionRefinement(storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold, RegionResultHypothesis const& hypothesis) { STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " ."); - auto thresholdAsCoefficient = storm::utility::convertNumber(threshold); + auto thresholdAsCoefficient = coverageThreshold ? storm::utility::convertNumber(coverageThreshold.get()) : storm::utility::zero(); auto areaOfParameterSpace = region.area(); auto fractionOfUndiscoveredArea = storm::utility::one(); auto fractionOfAllSatArea = storm::utility::zero(); auto fractionOfAllViolatedArea = storm::utility::zero(); - std::queue, RegionResult>> unprocessedRegions; + // The resulting (sub-)regions std::vector, RegionResult>> result; + + // FIFO queues storing the data for the regions that we still need to process. + std::queue, RegionResult>> unprocessedRegions; + std::queue refinementDepths; unprocessedRegions.emplace(region, RegionResult::Unknown); + refinementDepths.push(0); + uint_fast64_t numOfAnalyzedRegions = 0; CoefficientType displayedProgress = storm::utility::zero(); if (storm::settings::getModule().isShowStatisticsSet()) { @@ -69,12 +78,13 @@ namespace storm { displayedProgress = storm::utility::zero(); } - while (fractionOfUndiscoveredArea > thresholdAsCoefficient) { - STORM_LOG_THROW(!unprocessedRegions.empty(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left."); - STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (" << storm::utility::convertNumber(fractionOfUndiscoveredArea) * 100 << "% still unknown)"); + while (fractionOfUndiscoveredArea > thresholdAsCoefficient && !unprocessedRegions.empty()) { + assert(unprocessedRegions.size() == refinementDepths.size()); + uint64_t currentDepth = refinementDepths.front(); + STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (Refinement depth " << currentDepth << "; " << storm::utility::convertNumber(fractionOfUndiscoveredArea) * 100 << "% still unknown)"); auto& currentRegion = unprocessedRegions.front().first; auto& res = unprocessedRegions.front().second; - res = analyzeRegion(currentRegion, res, false); + res = analyzeRegion(currentRegion, hypothesis, res, false); switch (res) { case RegionResult::AllSat: fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace; @@ -87,18 +97,26 @@ namespace storm { result.push_back(std::move(unprocessedRegions.front())); break; default: - std::vector> newRegions; - currentRegion.split(currentRegion.getCenterPoint(), newRegions); - RegionResult initResForNewRegions = (res == RegionResult::CenterSat) ? RegionResult::ExistsSat : - ((res == RegionResult::CenterViolated) ? RegionResult::ExistsViolated : - RegionResult::Unknown); - for(auto& newRegion : newRegions) { - unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions); + // Split the region as long as the desired refinement depth is not reached. + if (!depthThreshold || currentDepth < depthThreshold.get()) { + std::vector> newRegions; + currentRegion.split(currentRegion.getCenterPoint(), newRegions); + RegionResult initResForNewRegions = (res == RegionResult::CenterSat) ? RegionResult::ExistsSat : + ((res == RegionResult::CenterViolated) ? RegionResult::ExistsViolated : + RegionResult::Unknown); + for (auto& newRegion : newRegions) { + unprocessedRegions.emplace(std::move(newRegion), initResForNewRegions); + refinementDepths.push(currentDepth + 1); + } + } else { + // If the region is not further refined, it is still added to the result + result.push_back(std::move(unprocessedRegions.front())); } break; } ++numOfAnalyzedRegions; unprocessedRegions.pop(); + refinementDepths.pop(); if (storm::settings::getModule().isShowStatisticsSet()) { while (displayedProgress < storm::utility::one() - fractionOfUndiscoveredArea) { STORM_PRINT_AND_LOG("#"); @@ -107,6 +125,12 @@ namespace storm { } } + // Add the still unprocessed regions to the result + while (!unprocessedRegions.empty()) { + result.push_back(std::move(unprocessedRegions.front())); + unprocessedRegions.pop(); + } + if (storm::settings::getModule().isShowStatisticsSet()) { while (displayedProgress < storm::utility::one()) { STORM_PRINT_AND_LOG("-"); diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h index a8f1fdf01..c1a558800 100644 --- a/src/storm-pars/modelchecker/region/RegionModelChecker.h +++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h @@ -5,6 +5,7 @@ #include "storm-pars/modelchecker/results/RegionCheckResult.h" #include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h" #include "storm-pars/modelchecker/region/RegionResult.h" +#include "storm-pars/modelchecker/region/RegionResultHypothesis.h" #include "storm-pars/storage/ParameterRegion.h" #include "storm/models/ModelBase.h" @@ -27,22 +28,29 @@ namespace storm { /*! * Analyzes the given region. - * An initial region result can be given to simplify the analysis (e.g. if the initial result is ExistsSat, we do not check for AllViolated). - * If supported by this model checker, it is possible to sample the vertices of the region whenever AllSat/AllViolated could not be shown. + * @param hypothesis if not 'unknown', the region checker only tries to show the hypothesis + * @param initialResult encodes what is already known about this region + * @param sampleVerticesOfRegion enables sampling of the vertices of the region in cases where AllSat/AllViolated could not be shown. */ - virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0; + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0; /*! * Analyzes the given regions. + * @param hypothesis if not 'unknown', we only try to show the hypothesis for each region + * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown. */ - std::unique_ptr> analyzeRegions(std::vector> const& regions, bool sampleVerticesOfRegion = false) ; + std::unique_ptr> analyzeRegions(std::vector> const& regions, std::vector const& hypotheses, bool sampleVerticesOfRegion = false) ; /*! * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated). - * The refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then the given threshold + * @param region the considered region + * @param coverageThreshold if given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold + * @param depthThreshold if given, the refinement stops at the given depth. depth=0 means no refinement. + * @param hypothesis if not 'unknown', it is only checked whether the hypothesis holds within the given region. + * */ - std::unique_ptr> performRegionRefinement(storm::storage::ParameterRegion const& region, ParametricType const& threshold); + std::unique_ptr> performRegionRefinement(storm::storage::ParameterRegion const& region, boost::optional const& coverageThreshold, boost::optional depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown); }; diff --git a/src/storm-pars/modelchecker/region/RegionResultHypothesis.cpp b/src/storm-pars/modelchecker/region/RegionResultHypothesis.cpp new file mode 100644 index 000000000..3f0968fbc --- /dev/null +++ b/src/storm-pars/modelchecker/region/RegionResultHypothesis.cpp @@ -0,0 +1,25 @@ +#include "storm-pars/modelchecker/region/RegionResultHypothesis.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + std::ostream& operator<<(std::ostream& os, RegionResultHypothesis const& regionResultHypothesis) { + switch (regionResultHypothesis) { + case RegionResultHypothesis::Unknown: + os << "Unknown"; + break; + case RegionResultHypothesis::AllSat: + os << "AllSat?"; + break; + case RegionResultHypothesis::AllViolated: + os << "AllViolated?"; + break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region result hypothesis. The case has not been implemented"); + } + return os; + } + } +} diff --git a/src/storm-pars/modelchecker/region/RegionResultHypothesis.h b/src/storm-pars/modelchecker/region/RegionResultHypothesis.h new file mode 100644 index 000000000..3288fba9c --- /dev/null +++ b/src/storm-pars/modelchecker/region/RegionResultHypothesis.h @@ -0,0 +1,19 @@ +#pragma once + +#include + +namespace storm { + namespace modelchecker { + /*! + * hypothesis for the result for a single Parameter Region + */ + enum class RegionResultHypothesis { + Unknown, + AllSat, + AllViolated + }; + + std::ostream& operator<<(std::ostream& os, RegionResultHypothesis const& regionResultHypothesis); + } +} + diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index 17610df87..d0b2af22b 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -47,8 +47,8 @@ namespace storm { } template - RegionResult SparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { - + RegionResult SparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant."); STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property."); STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state."); @@ -56,12 +56,12 @@ namespace storm { RegionResult result = initialResult; // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated - if (result == RegionResult::Unknown) { + if (hypothesis == RegionResultHypothesis::Unknown && result == RegionResult::Unknown) { result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated; } - // try to prove AllSat or AllViolated, depending on the obtained result - if (result == RegionResult::ExistsSat || result == RegionResult::CenterSat) { + // try to prove AllSat or AllViolated, depending on the hypothesis or the current result + if (hypothesis == RegionResultHypothesis::AllSat || result == RegionResult::ExistsSat || result == RegionResult::CenterSat) { // show AllSat: storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) { @@ -69,7 +69,7 @@ namespace storm { } else if (sampleVerticesOfRegion) { result = sampleVertices(region, result); } - } else if (result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) { + } else if (hypothesis == RegionResultHypothesis::AllViolated || result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) { // show AllViolated: storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize; if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) { diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h index b8abd518c..e0cabd5f0 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h @@ -28,12 +28,8 @@ namespace storm { /*! * Analyzes the given region by means of parameter lifting. - * We first check whether there is one point in the region for which the property is satisfied/violated. - * If the given initialResults already indicates that there is such a point, this step is skipped. - * Then, we check whether ALL points in the region violate/satisfy the property - * */ - virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; /*! * Analyzes the 2^#parameters corner points of the given region. diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp index d3dabab63..8f3ffaad3 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp @@ -28,9 +28,10 @@ namespace storm { }; template - RegionResult ValidatingSparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + RegionResult ValidatingSparseParameterLiftingModelChecker::analyzeRegion(storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) { + - RegionResult currentResult = getImpreciseChecker().analyzeRegion(region, initialResult); + RegionResult currentResult = getImpreciseChecker().analyzeRegion(region, hypothesis, initialResult, false); if (currentResult == RegionResult::AllSat || currentResult == RegionResult::AllViolated) { applyHintsToPreciseChecker(); @@ -48,13 +49,15 @@ namespace storm { currentResult = RegionResult::Unknown; ++numOfWrongRegions; - // Check the other direction - parameterOptDir = storm::solver::invert(parameterOptDir); - preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()]; - if (preciseResult && parameterOptDir == getPreciseChecker().getCurrentCheckTask().getOptimizationDirection()) { - currentResult = RegionResult::AllSat; - } else if (!preciseResult && parameterOptDir == storm::solver::invert(getPreciseChecker().getCurrentCheckTask().getOptimizationDirection())) { - currentResult = RegionResult::AllViolated; + // Check the other direction in case no hypothesis was given + if (hypothesis == RegionResultHypothesis::Unknown) { + parameterOptDir = storm::solver::invert(parameterOptDir); + preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()]; + if (preciseResult && parameterOptDir == getPreciseChecker().getCurrentCheckTask().getOptimizationDirection()) { + currentResult = RegionResult::AllSat; + } else if (!preciseResult && parameterOptDir == storm::solver::invert(getPreciseChecker().getCurrentCheckTask().getOptimizationDirection())) { + currentResult = RegionResult::AllViolated; + } } } } diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h index 7f9789ebf..8fa6a4114 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h @@ -23,7 +23,7 @@ namespace storm { * We first apply unsound solution methods (standard value iteratio with doubles) and then validate the obtained result * by means of exact and soud methods. */ - virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; + virtual RegionResult analyzeRegion(storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override; protected: diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp index 3cf8d1e1d..605865c04 100644 --- a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp +++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp @@ -58,6 +58,9 @@ namespace storm { bool currRegionComplete = false; CoefficientType coveredArea = storm::utility::zero(); for (auto const& r : this->getRegionResults()) { + if (r.second != storm::modelchecker::RegionResult::AllSat && r.second != storm::modelchecker::RegionResult::AllViolated) { + continue; + } CoefficientType interesctionSizeY = std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y)); interesctionSizeY = std::max(interesctionSizeY, storm::utility::zero()); CoefficientType interesctionSizeX = std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x)); diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index 31def397a..f87f4c652 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -31,9 +31,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown,storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -60,9 +60,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -89,9 +89,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -119,9 +119,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -148,9 +148,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -177,9 +177,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -204,7 +204,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { //start testing auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -231,9 +231,9 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { auto exBothRegion=storm::api::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -262,10 +262,10 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { auto allVioRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); auto allVioHardRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -294,10 +294,10 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { auto allVioRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters); auto allVioHardRegion=storm::api::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -326,9 +326,9 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { auto exBothRegion=storm::api::parseRegion("0.8<=PF<=0.9", modelParameters); auto allVioRegion=storm::api::parseRegion("0.01<=PF<=0.8", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -354,7 +354,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { //start testing auto allSatRegion=storm::api::parseRegion("", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp index fd690b876..b5a4138ec 100644 --- a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -30,9 +30,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -59,9 +59,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -88,9 +88,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) { auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -117,9 +117,9 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) { auto allVioRegion = storm::api::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -144,9 +144,9 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) { auto exBothRegion = storm::api::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters); auto allVioRegion = storm::api::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -173,9 +173,9 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) { auto exBothRegion=storm::api::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -203,9 +203,9 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) { auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -232,9 +232,9 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { auto exBothRegion=storm::api::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -260,7 +260,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { //start testing auto allSatRegion=storm::api::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } @@ -287,9 +287,9 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { auto exBothRegion=storm::api::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters); auto allVioRegion=storm::api::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters); - EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true)); - EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); + EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResultHypothesis::Unknown, storm::modelchecker::RegionResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } From 6fd75ac37ec49d157ff4a7d7cfcdc2ac3f81fed3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 11 Jul 2017 22:01:02 +0200 Subject: [PATCH 06/15] fixed issue in cli related to transforming PRISM to JANI --- src/storm/cli/cli.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index c84fce107..343006c6d 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -311,8 +311,6 @@ namespace storm { transformToJani |= transformToJaniForJit; if (transformToJani) { - SymbolicInput output; - storm::prism::Program const& model = output.model.get().asPrismProgram(); auto modelAndRenaming = model.toJaniWithLabelRenaming(true); output.model = modelAndRenaming.first; From 3bcdc1b579719c4e6e0f999bcbfeeaf457dd69be Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 11 Jul 2017 22:01:41 +0200 Subject: [PATCH 07/15] allowing to read transient variables in guards of edges in JIT-based JANI model builder and making the optimization level an option --- .../jit/ExplicitJitJaniModelBuilder.cpp | 36 ++++++++++--------- .../settings/modules/JitBuilderSettings.cpp | 7 ++++ .../settings/modules/JitBuilderSettings.h | 3 ++ 3 files changed, 30 insertions(+), 16 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index f647d86b4..5547a71d4 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -73,12 +73,16 @@ namespace storm { if (settings.isCompilerFlagsSet()) { compilerFlags = settings.getCompilerFlags(); } else { + std::stringstream flagStream; #ifdef LINUX - compilerFlags = "-std=c++14 -fPIC -O3 -march=native -shared"; + flagStream << "-std=c++14 -fPIC -march=native -shared "; #endif #ifdef MACOSX - compilerFlags = "-std=c++14 -stdlib=libc++ -fPIC -march=native -O3 -shared -undefined dynamic_lookup "; + flagStream << "-std=c++14 -stdlib=libc++ -fPIC -march=native -shared -undefined dynamic_lookup "; #endif + + flagStream << "-O" << settings.getOptimizationLevel(); + compilerFlags = flagStream.str(); } if (settings.isBoostIncludeDirectorySet()) { boostIncludeDirectory = settings.getBoostIncludeDirectory(); @@ -1171,7 +1175,7 @@ namespace storm { indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; } - indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector>& edges, uint64_t position) {" << std::endl; + indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, std::vector>& edges, uint64_t position) {" << std::endl; position = 0; uint64_t participatingPosition = 0; for (auto const& inputActionName : synchronizationVector.getInput()) { @@ -1184,7 +1188,7 @@ namespace storm { for (auto const& edge : automaton.getEdges()) { if (edge.getActionIndex() == actionIndex) { std::string edgeName = automaton.getName() + "_" + std::to_string(edgeIndex); - indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName << "(state)) {" << std::endl; + indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName << "(state, transientIn)) {" << std::endl; indent(vectorSource, indentLevel + 3) << "edges.emplace_back(edge_" << edgeName << ");" << std::endl; indent(vectorSource, indentLevel + 2) << "}" << std::endl; } @@ -1198,7 +1202,7 @@ namespace storm { } indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; - indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; + indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; indent(vectorSource, indentLevel + 1) << "#ifndef NDEBUG" << std::endl; indent(vectorSource, indentLevel + 1) << "std::cout << \"exploring synchronization vector " << synchronizationVectorIndex << "\" << std::endl;" << std::endl; indent(vectorSource, indentLevel + 1) << "#endif" << std::endl; @@ -1207,7 +1211,7 @@ namespace storm { participatingPosition = 0; for (auto const& input : synchronizationVector.getInput()) { if (!storm::jani::SynchronizationVector::isNoActionInput(input)) { - indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl; + indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, transientIn, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl; indent(vectorSource, indentLevel + 1) << "if (edges[" << participatingPosition << "].empty()) {" << std::endl; indent(vectorSource, indentLevel + 2) << "return;" << std::endl; indent(vectorSource, indentLevel + 1) << "}" << std::endl; @@ -1902,7 +1906,7 @@ namespace storm { {% endif %} // Non-synchronizing edges. - {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { + {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in, TransientVariables const& transientIn) { if ({$edge.guard}) { return true; } @@ -1979,7 +1983,7 @@ namespace storm { {% endfor %}{% endfor %} // Synchronizing edges. - {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { + {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in, TransientVariables const& transientIn) { if ({$edge.guard}) { return true; } @@ -2109,7 +2113,7 @@ namespace storm { DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction; }; - typedef bool (*EdgeEnabledFunctionPtr)(StateType const&); + typedef bool (*EdgeEnabledFunctionPtr)(StateType const&, TransientVariables const& transientIn); typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}); class Edge { @@ -2124,8 +2128,8 @@ namespace storm { // Intentionally left empty. } - bool isEnabled(StateType const& in) const { - return edgeEnabledFunction(in); + bool isEnabled(StateType const& in, TransientVariables const& transientIn) const { + return edgeEnabledFunction(in, transientIn); } void addDestination(Destination const& destination) { @@ -2281,10 +2285,10 @@ namespace storm { {% endfor %} // Explore all edges that do not take part in synchronization vectors. - exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore); + exploreNonSynchronizingEdges(currentState, transientOut, behaviour, statesToExplore); // Explore all edges that participate in synchronization vectors. - exploreSynchronizingEdges(currentState, behaviour, statesToExplore); + exploreSynchronizingEdges(currentState, transientOut, behaviour, statesToExplore); } {% if dontFixDeadlocks %} @@ -2307,7 +2311,7 @@ namespace storm { return false; } - void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore) { + void exploreNonSynchronizingEdges(StateType const& in, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for edge in nonsynch_edges %}{ if ({$edge.guard}) { Choice& choice = behaviour.addChoice(!model_is_deterministic() && !model_is_discrete_time() && {$edge.markovian}); @@ -2347,9 +2351,9 @@ namespace storm { {% for vector in synch_vectors %}{$vector.functions} {% endfor %} - void exploreSynchronizingEdges(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) { + void exploreSynchronizingEdges(StateType const& state, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for vector in synch_vectors %}{ - exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore); + exploreSynchronizationVector_{$vector.index}(state, transientIn, behaviour, statesToExplore); } {% endfor %} } diff --git a/src/storm/settings/modules/JitBuilderSettings.cpp b/src/storm/settings/modules/JitBuilderSettings.cpp index 127434055..b779f23f5 100644 --- a/src/storm/settings/modules/JitBuilderSettings.cpp +++ b/src/storm/settings/modules/JitBuilderSettings.cpp @@ -20,6 +20,7 @@ namespace storm { const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost"; const std::string JitBuilderSettings::carlIncludeDirectoryOptionName = "carl"; const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags"; + const std::string JitBuilderSettings::optimizationLevelOptionName = "opt"; JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build()); @@ -33,6 +34,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "The optimization level to use.") + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "The compiler flags.").setDefaultValueUnsignedInteger(3).build()).build()); } bool JitBuilderSettings::isCompilerSet() const { @@ -79,6 +82,10 @@ namespace storm { return this->getOption(compilerFlagsOptionName).getArgumentByName("flags").getValueAsString(); } + uint64_t JitBuilderSettings::getOptimizationLevel() const { + return this->getOption(optimizationLevelOptionName).getArgumentByName("level").getValueAsUnsignedInteger(); + } + void JitBuilderSettings::finalize() { // Intentionally left empty. } diff --git a/src/storm/settings/modules/JitBuilderSettings.h b/src/storm/settings/modules/JitBuilderSettings.h index fb169ff20..ad3eb89ac 100644 --- a/src/storm/settings/modules/JitBuilderSettings.h +++ b/src/storm/settings/modules/JitBuilderSettings.h @@ -30,6 +30,8 @@ namespace storm { bool isCompilerFlagsSet() const; std::string getCompilerFlags() const; + uint64_t getOptimizationLevel() const; + bool check() const override; void finalize() override; @@ -42,6 +44,7 @@ namespace storm { static const std::string carlIncludeDirectoryOptionName; static const std::string compilerFlagsOptionName; static const std::string doctorOptionName; + static const std::string optimizationLevelOptionName; }; } From 5a3c67c352293bb5ad4a6093e2a43e6768568973 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 3 Jul 2017 23:36:58 +0200 Subject: [PATCH 08/15] Use result.toString to generate easier-to-parse result files --- src/storm/api/export.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/api/export.h b/src/storm/api/export.h index 79bd63360..b9d781789 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -32,7 +32,7 @@ namespace storm { std::set vars = result.gatherVariables(); std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); filestream << std::endl; - filestream << "!Result: " << result << std::endl; + filestream << "!Result: " << result.toString(false, true) << std::endl; filestream << "!Well-formed Constraints: " << std::endl; std::vector stringConstraints; std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); From 53a2723e0cce7dd4fc9c8cb3e9f4e69956ec7b41 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 11 Jul 2017 22:48:09 +0200 Subject: [PATCH 09/15] storm pars result moved from storm to storm pars --- src/storm-pars/api/export.h | 34 +++++++++++++++++++++++++++++++++ src/storm-pars/api/storm-pars.h | 1 + src/storm/api/export.h | 29 +--------------------------- src/storm/utility/export.h | 31 ++---------------------------- 4 files changed, 38 insertions(+), 57 deletions(-) create mode 100644 src/storm-pars/api/export.h diff --git a/src/storm-pars/api/export.h b/src/storm-pars/api/export.h new file mode 100644 index 000000000..cae413bd8 --- /dev/null +++ b/src/storm-pars/api/export.h @@ -0,0 +1,34 @@ +#include "storm/utility/file.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/analysis/GraphConditions.h" + +namespace storm { + namespace api { + + template + void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result."); + } + + template <> + inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + std::ofstream filestream; + storm::utility::openFile(path, filestream); + filestream << "$Parameters: "; + std::set vars = result.gatherVariables(); + std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); + filestream << std::endl; + filestream << "$Result: " << result.toString(false, true) << std::endl; + filestream << "$Well-formed Constraints: " << std::endl; + std::vector stringConstraints; + std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); + filestream << "$Graph-preserving Constraints: " << std::endl; + stringConstraints.clear(); + std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); + storm::utility::closeFile(filestream); + } + } +} diff --git a/src/storm-pars/api/storm-pars.h b/src/storm-pars/api/storm-pars.h index 42ac7dc79..a1a32ac05 100644 --- a/src/storm-pars/api/storm-pars.h +++ b/src/storm-pars/api/storm-pars.h @@ -1,3 +1,4 @@ #pragma once #include "storm-pars/api/region.h" +#include "storm-pars/api/export.h" \ No newline at end of file diff --git a/src/storm/api/export.h b/src/storm/api/export.h index b9d781789..3ba81525d 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -2,7 +2,6 @@ #include "storm/storage/jani/JSONExporter.h" -#include "storm/analysis/GraphConditions.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/JaniExportSettings.h" @@ -10,7 +9,6 @@ #include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/file.h" #include "storm/utility/macros.h" -#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace api { @@ -18,32 +16,7 @@ namespace storm { void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filename); void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename); - - template - void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result."); - } - - template <> - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { - std::ofstream filestream; - storm::utility::openFile(path, filestream); - filestream << "!Parameters: "; - std::set vars = result.gatherVariables(); - std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); - filestream << std::endl; - filestream << "!Result: " << result.toString(false, true) << std::endl; - filestream << "!Well-formed Constraints: " << std::endl; - std::vector stringConstraints; - std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); - std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); - filestream << "!Graph-preserving Constraints: " << std::endl; - stringConstraints.clear(); - std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); - std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); - storm::utility::closeFile(filestream); - } - + template void exportSparseModelAsDrn(std::shared_ptr> const& model, std::string const& filename, std::vector const& parameterNames) { std::ofstream stream; diff --git a/src/storm/utility/export.h b/src/storm/utility/export.h index b4f5020c0..61fb9e46f 100644 --- a/src/storm/utility/export.h +++ b/src/storm/utility/export.h @@ -1,10 +1,3 @@ -/** - * @file: export.h - * @author: Sebastian Junges - * - * @since October 7, 2014 - */ - #ifndef STORM_UTILITY_EXPORT_H_ #define STORM_UTILITY_EXPORT_H_ @@ -14,32 +7,12 @@ #include "storm/utility/macros.h" #include "storm/utility/file.h" -//#include "storm/storage/parameters.h" -//#include "storm/settings/modules/ParametricSettings.h" -//#include "storm/modelchecker/reachability/CollectConstraints.h" + namespace storm { namespace utility { - /* TODO Fix me - template - void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints const& constraintCollector) { - std::string path = storm::settings::getModule().exportResultPath(); - std::ofstream filestream; - filestream.open(path); - // todo add checks. - filestream << "!Parameters: "; - std::set vars = mcresult.gatherVariables(); - std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, ", ")); - filestream << std::endl; - filestream << "!Result: " << mcresult << std::endl; - filestream << "!Well-formed Constraints: " << std::endl; - std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream << "!Graph-preserving Constraints: " << std::endl; - std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream.close(); - } - */ + template inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& columnHeaders) { From 56616f1e265fb6f7d49a378037309c091a0b3fe7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 11 Jul 2017 22:49:04 +0200 Subject: [PATCH 10/15] trying to clarify sylvan dependency on carl --- resources/3rdparty/CMakeLists.txt | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 3a7a44240..dd0942e92 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -404,6 +404,12 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake) ## ############################################################# +if(STORM_SHIPPED_CARL) + set(sylvan_dep carl) +else() + set(sylvan_dep lib_carl) +endif() + ExternalProject_Add( sylvan DOWNLOAD_COMMAND "" @@ -416,6 +422,7 @@ ExternalProject_Add( INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan LOG_CONFIGURE ON LOG_BUILD ON + DEPENDS ${sylvan_dep} BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} ) @@ -427,9 +434,7 @@ message(STATUS "Storm - Using shipped version of sylvan.") message(STATUS "Storm - Linking with sylvan.") add_imported_library(sylvan STATIC ${Sylvan_LIBRARY} ${Sylvan_INCLUDE_DIR}) add_dependencies(sylvan_STATIC sylvan) -if(STORM_SHIPPED_CARL) - add_dependencies(sylvan carl) -endif() + list(APPEND STORM_DEP_TARGETS sylvan_STATIC) find_package(Hwloc QUIET REQUIRED) From 6621cb814c72e701e08c84ba57de442a207f5101 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 12 Jul 2017 10:42:04 +0200 Subject: [PATCH 11/15] new argument validator: doubleRangeValidatorIncluding --- src/storm/settings/ArgumentValidators.cpp | 9 +++++++++ src/storm/settings/ArgumentValidators.h | 5 +++++ 2 files changed, 14 insertions(+) diff --git a/src/storm/settings/ArgumentValidators.cpp b/src/storm/settings/ArgumentValidators.cpp index b8896590d..8e108b454 100644 --- a/src/storm/settings/ArgumentValidators.cpp +++ b/src/storm/settings/ArgumentValidators.cpp @@ -133,6 +133,10 @@ namespace storm { return createRangeValidatorExcluding(lowerBound, upperBound); } + std::shared_ptr> ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(double lowerBound, double upperBound) { + return createRangeValidatorIncluding(lowerBound, upperBound); + } + std::shared_ptr> ArgumentValidatorFactory::createIntegerGreaterValidator(int_fast64_t lowerBound) { return createGreaterValidator(lowerBound, false); } @@ -174,6 +178,11 @@ namespace storm { return std::make_unique>(lowerBound, upperBound, false, false); } + template + std::shared_ptr> ArgumentValidatorFactory::createRangeValidatorIncluding(ValueType lowerBound, ValueType upperBound) { + return std::make_unique>(lowerBound, upperBound, true, true); + } + template std::shared_ptr> ArgumentValidatorFactory::createGreaterValidator(ValueType lowerBound, bool equalAllowed) { return std::make_unique>(lowerBound, boost::none, equalAllowed, false); diff --git a/src/storm/settings/ArgumentValidators.h b/src/storm/settings/ArgumentValidators.h index bbdb861f5..4b3b0b3d8 100644 --- a/src/storm/settings/ArgumentValidators.h +++ b/src/storm/settings/ArgumentValidators.h @@ -70,6 +70,8 @@ namespace storm { static std::shared_ptr> createUnsignedRangeValidatorExcluding(uint64_t lowerBound, uint64_t upperBound); static std::shared_ptr> createDoubleRangeValidatorExcluding(double lowerBound, double upperBound); + static std::shared_ptr> createDoubleRangeValidatorIncluding(double lowerBound, double upperBound); + static std::shared_ptr> createIntegerGreaterValidator(int_fast64_t lowerBound); static std::shared_ptr> createUnsignedGreaterValidator(uint64_t lowerBound); static std::shared_ptr> createDoubleGreaterValidator(double lowerBound); @@ -87,6 +89,9 @@ namespace storm { template static std::shared_ptr> createRangeValidatorExcluding(ValueType lowerBound, ValueType upperBound); + template + static std::shared_ptr> createRangeValidatorIncluding(ValueType lowerBound, ValueType upperBound); + template static std::shared_ptr> createGreaterValidator(ValueType lowerBound, bool equalAllowed); }; From 48e029dd9d194076597f6ddcee9daaa5b0fe54a9 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 12 Jul 2017 10:42:34 +0200 Subject: [PATCH 12/15] Adapted region settings and CLI to new features. --- src/storm-pars-cli/storm-pars.cpp | 23 ++++++--- .../settings/modules/RegionSettings.cpp | 47 +++++++++++++++++-- .../settings/modules/RegionSettings.h | 25 +++++++++- 3 files changed, 84 insertions(+), 11 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 52d6dff39..32e609bbb 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -209,22 +209,31 @@ namespace storm { std::function(std::shared_ptr const& formula)> verificationCallback; std::function const&)> postprocessingCallback; + STORM_PRINT_AND_LOG(std::endl); + if (regionSettings.isHypothesisSet()) { + STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on "); + } else { + STORM_PRINT_AND_LOG("Analyzing "); + } if (regions.size() == 1) { - STORM_PRINT_AND_LOG(std::endl << "Analyzing parameter region " << regions.front()); + STORM_PRINT_AND_LOG("parameter region " << regions.front()); } else { - STORM_PRINT_AND_LOG(std::endl << "Analyzing " << regions.size() << " parameter regions"); + STORM_PRINT_AND_LOG(regions.size() << " parameter regions"); } - auto engine = regionSettings.getRegionCheckEngine(); STORM_PRINT_AND_LOG(" using " << engine); // Check the given set of regions with or without refinement if (regionSettings.isRefineSet()) { STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); - STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl); + STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getRefinementThreshold()); - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold); + ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); + boost::optional optionalDepthLimit; + if (regionSettings.isDepthLimitSet()) { + optionalDepthLimit = regionSettings.getDepthLimit(); + } + std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); return result; }; } else { @@ -237,7 +246,7 @@ namespace storm { postprocessingCallback = [&] (std::unique_ptr const& result) { if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath(), false); + storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); } }; diff --git a/src/storm-pars/settings/modules/RegionSettings.cpp b/src/storm-pars/settings/modules/RegionSettings.cpp index 2dba3c300..97714b439 100644 --- a/src/storm-pars/settings/modules/RegionSettings.cpp +++ b/src/storm-pars/settings/modules/RegionSettings.cpp @@ -1,3 +1,4 @@ +#include #include "storm-pars/settings/modules/RegionSettings.h" #include "storm/settings/Option.h" @@ -7,6 +8,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/IllegalArgumentValueException.h" +#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace settings { @@ -15,6 +17,8 @@ namespace storm { const std::string RegionSettings::moduleName = "region"; const std::string RegionSettings::regionOptionName = "region"; const std::string RegionSettings::regionShortOptionName = "reg"; + const std::string RegionSettings::hypothesisOptionName = "hypothesis"; + const std::string RegionSettings::hypothesisShortOptionName = "hyp"; const std::string RegionSettings::refineOptionName = "refine"; const std::string RegionSettings::checkEngineOptionName = "engine"; const std::string RegionSettings::printNoIllustrationOptionName = "noillustration"; @@ -24,8 +28,13 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, false, "Sets the region(s) considered for analysis.").setShortName(regionShortOptionName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be a file.").build()).build()); + std::vector hypotheses = {"unknown", "allsat", "allviolated"}; + this->addOption(storm::settings::OptionBuilder(moduleName, hypothesisOptionName, false, "Sets a hypothesis for region analysis. If given, the region(s) are only analyzed w.r.t. that hypothesis.").setShortName(hypothesisShortOptionName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hypothesis", "The hypothesis.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(hypotheses)).setDefaultValueString("unknown").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, false, "Enables region refinement.") - .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("coverage-threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0,1.0)).build()) + .addArgument(storm::settings::ArgumentBuilder::createIntegerArgument("depth-limit", "If given, limits the number of times a region is refined.").setDefaultValueInteger(-1).build()).build()); std::vector engines = {"pl", "exactpl", "validatingpl"}; this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, true, "Sets which engine is used for analyzing regions.") @@ -44,12 +53,44 @@ namespace storm { return this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString(); } + bool RegionSettings::isHypothesisSet() const { + return this->getOption(hypothesisOptionName).getHasOptionBeenSet(); + } + + storm::modelchecker::RegionResultHypothesis RegionSettings::getHypothesis() const { + std::string hypString = this->getOption(hypothesisOptionName).getArgumentByName("hypothesis").getValueAsString(); + + storm::modelchecker::RegionResultHypothesis result; + + if (hypString == "unknown") { + result = storm::modelchecker::RegionResultHypothesis::Unknown; + } else if (hypString == "allsat") { + result = storm::modelchecker::RegionResultHypothesis::AllSat; + } else if (hypString == "allviolated") { + result = storm::modelchecker::RegionResultHypothesis::AllViolated; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Hypothesis " << hypString << " not known."); + } + + return result; + } + bool RegionSettings::isRefineSet() const { return this->getOption(refineOptionName).getHasOptionBeenSet(); } - double RegionSettings::getRefinementThreshold() const { - return this->getOption(refineOptionName).getArgumentByName("threshold").getValueAsDouble(); + double RegionSettings::getCoverageThreshold() const { + return this->getOption(refineOptionName).getArgumentByName("coverage-threshold").getValueAsDouble(); + } + + bool RegionSettings::isDepthLimitSet() const { + return this->getOption(refineOptionName).getArgumentByName("depth-limit").getHasBeenSet() && this->getOption(refineOptionName).getArgumentByName("depth-limit").getValueAsInteger() >= 0; + } + + uint64_t RegionSettings::getDepthLimit() const { + int64_t depth = this->getOption(refineOptionName).getArgumentByName("depth-limit").getValueAsInteger(); + STORM_LOG_THROW(depth >= 0, storm::exceptions::InvalidOperationException, "Tried to retrieve the depth limit but it was not set."); + return (uint64_t) depth; } storm::modelchecker::RegionCheckEngine RegionSettings::getRegionCheckEngine() const { diff --git a/src/storm-pars/settings/modules/RegionSettings.h b/src/storm-pars/settings/modules/RegionSettings.h index e668a3146..0efb45d2f 100644 --- a/src/storm-pars/settings/modules/RegionSettings.h +++ b/src/storm-pars/settings/modules/RegionSettings.h @@ -1,6 +1,7 @@ #pragma once #include "storm-pars/modelchecker/region/RegionCheckEngine.h" +#include "storm-pars/modelchecker/region/RegionResultHypothesis.h" #include "storm/settings/modules/ModuleSettings.h" @@ -29,6 +30,16 @@ namespace storm { */ std::string getRegionString() const; + /*! + * Retrieves whether region(s) were declared + */ + bool isHypothesisSet() const; + + /*! + * Retrieves the region definition string + */ + storm::modelchecker::RegionResultHypothesis getHypothesis() const; + /*! * Retrieves whether region refinement is enabled */ @@ -38,8 +49,18 @@ namespace storm { * Retrieves the threshold considered for iterative region refinement. * The refinement converges as soon as the fraction of unknown area falls below this threshold */ - double getRefinementThreshold() const; + double getCoverageThreshold() const; + /*! + * Retrieves whether a depth threshold has been set for refinement + */ + bool isDepthLimitSet() const; + + /*! + * Returns the depth threshold (if set). It is illegal to call this method if no depth threshold has been set. + */ + uint64_t getDepthLimit() const; + /*! * Retrieves which type of region check should be performed */ @@ -60,6 +81,8 @@ namespace storm { private: const static std::string regionOptionName; const static std::string regionShortOptionName; + const static std::string hypothesisOptionName; + const static std::string hypothesisShortOptionName; const static std::string refineOptionName; const static std::string checkEngineOptionName; const static std::string printNoIllustrationOptionName; From 040c1f0d4c6f64d1e3bfcf7d91da34cbc97e9c0e Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 12 Jul 2017 12:51:27 +0200 Subject: [PATCH 13/15] fixed ignoring the hypothesis when not doing refinement --- src/storm-pars-cli/storm-pars.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 32e609bbb..ce78713ee 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -239,7 +239,7 @@ namespace storm { } else { STORM_PRINT_AND_LOG("." << std::endl); verificationCallback = [&] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine); + std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); return result; }; } From 29855e285388522073a290efa6d644f5c689c129 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Jul 2017 19:52:39 +0200 Subject: [PATCH 14/15] added option to display information about exploration progress to both jit and explicit builder --- src/storm/builder/BuilderOptions.cpp | 12 ++++- src/storm/builder/BuilderOptions.h | 8 ++++ src/storm/builder/ExplicitModelBuilder.cpp | 20 +++++++++ .../jit/ExplicitJitJaniModelBuilder.cpp | 44 +++++++++++++++++-- src/storm/settings/modules/IOSettings.cpp | 12 +++++ src/storm/settings/modules/IOSettings.h | 16 +++++++ 6 files changed, 108 insertions(+), 4 deletions(-) diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 453f2e548..6e42745fd 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -35,7 +35,7 @@ namespace storm { return boost::get(labelOrExpression); } - BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false) { + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), explorationShowProgress(false), explorationShowProgressDelay(0) { // Intentionally left empty. } @@ -55,6 +55,8 @@ namespace storm { } explorationChecks = storm::settings::getModule().isExplorationChecksSet(); + explorationShowProgress = storm::settings::getModule().isExplorationShowProgressSet(); + explorationShowProgressDelay = storm::settings::getModule().getExplorationShowProgressDelay(); } void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) { @@ -163,6 +165,14 @@ namespace storm { bool BuilderOptions::isExplorationChecksSet() const { return explorationChecks; } + + bool BuilderOptions::isExplorationShowProgressSet() const { + return explorationShowProgress; + } + + uint64_t BuilderOptions::getExplorationShowProgressDelay() const { + return explorationShowProgressDelay; + } BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) { explorationChecks = newValue; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index b2923f4f5..a06de50eb 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -94,6 +94,8 @@ namespace storm { bool isBuildAllRewardModelsSet() const; bool isBuildAllLabelsSet() const; bool isExplorationChecksSet() const; + bool isExplorationShowProgressSet() const; + uint64_t getExplorationShowProgressDelay() const; BuilderOptions& setBuildAllRewardModels(); BuilderOptions& addRewardModel(std::string const& rewardModelName); @@ -139,6 +141,12 @@ namespace storm { /// A flag that stores whether exploration checks are to be performed. bool explorationChecks; + + /// A flag that stores whether the progress of exploration is to be printed. + bool explorationShowProgress; + + /// The delay for printing progress information. + uint64_t explorationShowProgressDelay; }; } diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 5add225ce..9de544e7b 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -131,6 +131,11 @@ namespace storm { uint_fast64_t currentRowGroup = 0; uint_fast64_t currentRow = 0; + auto timeOfStart = std::chrono::high_resolution_clock::now(); + auto timeOfLastMessage = std::chrono::high_resolution_clock::now(); + uint64_t numberOfExploredStates = 0; + uint64_t numberOfExploredStatesSinceLastMessage = 0; + // Perform a search through the model. while (!statesToExplore.empty()) { // Get the first state in the queue. @@ -234,6 +239,21 @@ namespace storm { } ++currentRowGroup; } + + if (generator->getOptions().isExplorationShowProgressSet()) { + ++numberOfExploredStatesSinceLastMessage; + ++numberOfExploredStates; + + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= generator->getOptions().getExplorationShowProgressDelay()) { + auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage; + auto durationSinceStart = std::chrono::duration_cast(now - timeOfStart).count(); + std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl; + timeOfLastMessage = std::chrono::high_resolution_clock::now(); + numberOfExploredStatesSinceLastMessage = 0; + } + } } if (markovianStates) { diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 5547a71d4..67ff3be5d 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -527,6 +527,15 @@ namespace storm { } modelData["exploration_checks"] = cpptempl::make_data(list); list = cpptempl::data_list(); + if (options.isExplorationShowProgressSet()) { + list.push_back(cpptempl::data_map()); + } + modelData["expl_progress"] = cpptempl::make_data(list); + + std::stringstream progressDelayStream; + progressDelayStream << options.getExplorationShowProgressDelay(); + modelData["expl_progress_interval"] = cpptempl::make_data(progressDelayStream.str()); + list = cpptempl::data_list(); if (std::is_same::value) { list.push_back(cpptempl::data_map()); } @@ -541,7 +550,7 @@ namespace storm { list.push_back(cpptempl::data_map()); } modelData["double"] = cpptempl::make_data(list); - + list = cpptempl::data_list(); if (storm::settings::getModule().isDontFixDeadlocksSet()) { list.push_back(cpptempl::data_map()); @@ -1646,12 +1655,17 @@ namespace storm { std::string sourceTemplate = R"( #define NDEBUG +{% if expl_progress %} +#define EXPL_PROGRESS +{% endif %} + #include #include #include #include #include #include +#include #include {% if exact %} @@ -2179,7 +2193,7 @@ namespace storm { class JitBuilder : public JitModelBuilderInterface { public: - JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) { + JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder), timeOfStart(std::chrono::high_resolution_clock::now()), timeOfLastMessage(std::chrono::high_resolution_clock::now()), numberOfExploredStates(0), numberOfExploredStatesSinceLastMessage(0) { {% for state in initialStates %}{ StateType state; {% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; @@ -2262,6 +2276,7 @@ namespace storm { getOrAddIndex(initialState, statesToExplore); StateBehaviour behaviour; + while (!statesToExplore.empty()) { StateType currentState = statesToExplore.get(); IndexType currentIndex = getIndex(currentState); @@ -2300,6 +2315,21 @@ namespace storm { this->addStateBehaviour(currentIndex, behaviour); behaviour.clear(); + +#ifdef EXPL_PROGRESS + ++numberOfExploredStatesSinceLastMessage; + ++numberOfExploredStates; + + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= {$expl_progress_interval}) { + auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage; + auto durationSinceStart = std::chrono::duration_cast(now - timeOfStart).count(); + std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl; + timeOfLastMessage = std::chrono::high_resolution_clock::now(); + numberOfExploredStatesSinceLastMessage = 0; + } +#endif } } @@ -2395,14 +2425,22 @@ namespace storm { } private: + // State storage. spp::sparse_hash_map stateIds; std::vector initialStates; std::vector deadlockStates; - + + // Edges. {% for edge in nonsynch_edges %}Edge edge_{$edge.name}; {% endfor %} {% for edge in synch_edges %}Edge edge_{$edge.name}; {% endfor %} + + // Statistics. + std::chrono::high_resolution_clock::time_point timeOfStart; + std::chrono::high_resolution_clock::time_point timeOfLastMessage; + uint64_t numberOfExploredStates; + uint64_t numberOfExploredStatesSinceLastMessage; }; BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder) diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 677b78513..7d26b54ac 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -34,6 +34,8 @@ namespace storm { const std::string IOSettings::explorationOrderOptionShortName = "eo"; const std::string IOSettings::explorationChecksOptionName = "explchecks"; const std::string IOSettings::explorationChecksOptionShortName = "ec"; + const std::string IOSettings::explorationShowProgressOptionName = "explprog"; + const std::string IOSettings::explorationShowProgressOptionShortName = "ep"; const std::string IOSettings::transitionRewardsOptionName = "transrew"; const std::string IOSettings::stateRewardsOptionName = "staterew"; const std::string IOSettings::choiceLabelingOptionName = "choicelab"; @@ -84,6 +86,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explorationShowProgressOptionName, false, "Sets when additional information (if available) about the exploration progress is printed.").setShortName(explorationShowProgressOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait between emitting information.").setDefaultValueUnsignedInteger(0).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); @@ -195,6 +198,14 @@ namespace storm { return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); } + bool IOSettings::isExplorationShowProgressSet() const { + return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger() > 0; + } + + uint64_t IOSettings::getExplorationShowProgressDelay() const { + return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger(); + } + bool IOSettings::isTransitionRewardsSet() const { return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); } @@ -268,6 +279,7 @@ namespace storm { } void IOSettings::finalize() { + // Intentionally left empty. } bool IOSettings::check() const { diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 55f777334..e68c6b515 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -179,6 +179,20 @@ namespace storm { */ bool isExplorationChecksSet() const; + /*! + * Retrieves whether to show information about exploration progress. + * + * @return True if information is to be shown. + */ + bool isExplorationShowProgressSet() const; + + /*! + * Retrieves the delay for printing information about the exploration progress. + * + * @return The desired delay in seconds. If 0, no information about the progress shall be printed. + */ + uint64_t getExplorationShowProgressDelay() const; + /*! * Retrieves the exploration order if it was set. * @@ -334,6 +348,8 @@ namespace storm { static const std::string jitOptionName; static const std::string explorationChecksOptionName; static const std::string explorationChecksOptionShortName; + static const std::string explorationShowProgressOptionName; + static const std::string explorationShowProgressOptionShortName; static const std::string explorationOrderOptionName; static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName; From 11b9c605154e24cb7fd5aed3087a0fe4ffb01d6d Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 12:12:41 +0200 Subject: [PATCH 15/15] Adapted fragment checker test to new multiobjective-fragment specification --- src/test/storm/logic/FragmentCheckerTest.cpp | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 643742bbf..c846f7f68 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -145,26 +145,17 @@ TEST(FragmentCheckerTest, MultiObjective) { std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0.5,1] \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], \"label\", R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));