diff --git a/examples/multiobjective/ma/simple/simple.csl b/examples/multiobjective/ma/simple/simple.csl new file mode 100644 index 000000000..75452f1a2 --- /dev/null +++ b/examples/multiobjective/ma/simple/simple.csl @@ -0,0 +1 @@ +multi(Pmax=? [ F s=3 ], Pmax=? [ F s=4 ]) diff --git a/examples/multiobjective/ma/simple/simple.ma b/examples/multiobjective/ma/simple/simple.ma new file mode 100644 index 000000000..92a003555 --- /dev/null +++ b/examples/multiobjective/ma/simple/simple.ma @@ -0,0 +1,15 @@ + +ma + +module simple + + s : [0..4]; + + + [alpha] (s=0) -> 1 : (s' = 1); + [beta] (s=0) -> 0.8 : (s'=0) + 0.2 : (s'=2); + <> (s=1) -> 9 : (s'=0) + 1 : (s'=3); + <> (s=2) -> 12 : (s'=4); + <> (s>2) -> 1 : true; + +endmodule \ No newline at end of file diff --git a/examples/multiobjective/ma/stream/stream2.ma b/examples/multiobjective/ma/stream/stream2.ma new file mode 100644 index 000000000..3b49c808b --- /dev/null +++ b/examples/multiobjective/ma/stream/stream2.ma @@ -0,0 +1,49 @@ + +ma + +const int N = 2; // num packages + +const double inRate = 4; +const double processingRate = 5; + +module streamingclient + + s : [0..2]; // current state: + // 0: decide whether to start + // 1: buffering + // 2: running + + n : [0..N]; // number of received packages + k : [0..N]; // number of processed packages + + [buffer] s=0 & n 1 : (s'=1); + [start] s=0 & k 1 : (s'=2) & (k'=k+1); + + <> s=1 -> inRate : (n'=n+1) & (s'=0); + + <> s=2 & n inRate : (n'=n+1) + processingRate : (k'=k+1); + <> s=2 & n inRate : (n'=n+1) + processingRate : (s'=0); + <> s=2 & n=N & k processingRate : (k'=k+1); + <> s=2 & n=N & k=N -> processingRate : (s'=3); + + <> s=3 -> 1 : true; +endmodule + +// All packages received and buffer empty +label "done" = (s=3); + +rewards "buffering" + s=1 : 1; +endrewards + +rewards "initialbuffering" + s=1 & k = 0: 1; +endrewards + +rewards "intermediatebuffering" + s=1 & k > 0: 1; +endrewards + +rewards "numRestarts" + [start] k > 0 : 1; +endrewards diff --git a/examples/multiobjective/ma/stream/stream2_pareto.csl b/examples/multiobjective/ma/stream/stream2_pareto.csl new file mode 100644 index 000000000..443415858 --- /dev/null +++ b/examples/multiobjective/ma/stream/stream2_pareto.csl @@ -0,0 +1 @@ +multi(R{"initialbuffering"}min=? [ F "done" ], R{numRestarts}min=? [ F "done" ]) diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp new file mode 100644 index 000000000..edfafdcab --- /dev/null +++ b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp @@ -0,0 +1,66 @@ +#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h" + +#include "src/utility/macros.h" +#include "src/logic/Formulas.h" +#include "src/logic/FragmentSpecification.h" + +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h" + +#include "src/utility/Stopwatch.h" + +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + template + SparseMaMultiObjectiveModelChecker::SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model) : SparseMarkovAutomatonCslModelChecker(model) { + // Intentionally left empty. + } + + template + bool SparseMaMultiObjectiveModelChecker::canHandle(CheckTask const& checkTask) const { + // A formula without multi objective (sub)formulas can be handled by the base class + if(SparseMarkovAutomatonCslModelChecker::canHandle(checkTask)) return true; + //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this. + if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setStepBoundedUntilFormulasAllowed(true)); + } + + template + std::unique_ptr SparseMaMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported."); + std::unique_ptr result; + +#ifdef STORM_HAVE_CARL + storm::utility::Stopwatch swPreprocessing; + auto preprocessorData = helper::SparseMultiObjectivePreprocessor::preprocess(checkTask.getFormula(), this->getModel()); + swPreprocessing.pause(); + STORM_LOG_DEBUG("Preprocessing done. Data: " << preprocessorData); + + storm::utility::Stopwatch swHelper; + auto resultData = helper::SparseMultiObjectiveHelper::check(preprocessorData); + swHelper.pause(); + STORM_LOG_DEBUG("Modelchecking done."); + + storm::utility::Stopwatch swPostprocessing; + result = helper::SparseMultiObjectivePostprocessor::postprocess(preprocessorData, resultData, swPreprocessing, swHelper, swPostprocessing); + STORM_LOG_DEBUG("Postprocessing done."); +#else + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); +#endif + return result; + } + + + + template class SparseMaMultiObjectiveModelChecker>; + } +} diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h new file mode 100644 index 000000000..94b4926d8 --- /dev/null +++ b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h @@ -0,0 +1,27 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ + +#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" + +namespace storm { + namespace modelchecker { + template + class SparseMaMultiObjectiveModelChecker : public SparseMarkovAutomatonCslModelChecker { + public: + typedef typename SparseMaModelType::ValueType ValueType; + typedef typename SparseMaModelType::RewardModelType RewardModelType; + + explicit SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model); + + virtual bool canHandle(CheckTask const& checkTask) const override; + + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; + + private: + + + }; + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 1b3f71146..661d3a0c3 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -54,7 +54,7 @@ namespace storm { result = helper::SparseMultiObjectivePostprocessor::postprocess(preprocessorData, resultData, swPreprocessing, swHelper, swPostprocessing); STORM_LOG_DEBUG("Postprocessing done."); #else - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi objective model checking requires carl."); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); #endif return result; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp index 75b2c5839..59a8327d0 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp @@ -2,6 +2,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/Mdp.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h" #include "src/utility/constants.h" @@ -306,6 +307,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class SparseMultiObjectiveHelper, storm::RationalNumber>; + template class SparseMultiObjectiveHelper, storm::RationalNumber>; #endif } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp index 696e8883f..3c67a63b7 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp @@ -4,6 +4,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/Mdp.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -323,6 +324,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; + template class SparseMultiObjectivePostprocessor, storm::RationalNumber>; #endif } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 8d950c4ef..978af4461 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h" #include "src/models/sparse/Mdp.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -441,8 +442,8 @@ namespace storm { data.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); } - template class SparseMultiObjectivePreprocessor>; + template class SparseMultiObjectivePreprocessor>; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index 54bcdcc23..785ba8c0c 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -4,6 +4,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/Mdp.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "src/solver/MinMaxLinearEquationSolver.h" @@ -218,8 +219,11 @@ namespace storm { template class SparseMultiObjectiveWeightVectorChecker>; template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; + template class SparseMultiObjectiveWeightVectorChecker>; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; #ifdef STORM_HAVE_CARL template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; + template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() const; #endif } diff --git a/src/settings/modules/MultiObjectiveSettings.cpp b/src/settings/modules/MultiObjectiveSettings.cpp index 1cd1f51b1..bf3f48219 100644 --- a/src/settings/modules/MultiObjectiveSettings.cpp +++ b/src/settings/modules/MultiObjectiveSettings.cpp @@ -63,10 +63,11 @@ namespace storm { } bool MultiObjectiveSettings::check() const { - return ArgumentValidators::writableFileValidator()(getExportPlotUnderApproximationFileName()) - && ArgumentValidators::writableFileValidator()(getExportPlotOverApproximationFileName()) - && ArgumentValidators::writableFileValidator()(getExportPlotParetoPointsFileName()) - && ArgumentValidators::writableFileValidator()(getExportPlotBoundariesFileName()); + return !isExportPlotSet() + || (ArgumentValidators::writableFileValidator()(getExportPlotUnderApproximationFileName()) + && ArgumentValidators::writableFileValidator()(getExportPlotOverApproximationFileName()) + && ArgumentValidators::writableFileValidator()(getExportPlotParetoPointsFileName()) + && ArgumentValidators::writableFileValidator()(getExportPlotBoundariesFileName())); } } // namespace modules diff --git a/src/utility/storm.h b/src/utility/storm.h index a11fe2191..927d37cbf 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -67,6 +67,7 @@ #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" +#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -328,7 +329,14 @@ namespace storm { ma->close(); } storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); - result = modelchecker.check(task); + if(modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } else { + storm::modelchecker::SparseMaMultiObjectiveModelChecker> modelchecker2(*ma); + if(modelchecker2.canHandle(task)){ + result = modelchecker2.check(task); + } + } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported."); }