first steps towards MAs

Former-commit-id: f217884d13

examples/multiobjective/ma/simple/simple.csl

@@ -0,0 +1 @@
+multi(Pmax=? [ F s=3 ], Pmax=? [ F s=4 ]) 

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

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<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> 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

examples/multiobjective/ma/stream/stream2_pareto.csl

@@ -0,0 +1 @@
+multi(R{"initialbuffering"}min=? [ F "done" ], R{numRestarts}min=? [ F "done" ]) 

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<typename SparseMaModelType>
+        SparseMaMultiObjectiveModelChecker<SparseMaModelType>::SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model) : SparseMarkovAutomatonCslModelChecker<SparseMaModelType>(model) {
+            // Intentionally left empty.
+        }
+        
+        template<typename SparseMaModelType>
+        bool SparseMaMultiObjectiveModelChecker<SparseMaModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
+            // A formula without multi objective (sub)formulas can be handled by the base class
+            if(SparseMarkovAutomatonCslModelChecker<SparseMaModelType>::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<typename SparseMaModelType>
+        std::unique_ptr<CheckResult> SparseMaMultiObjectiveModelChecker<SparseMaModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> 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<CheckResult> result;
+            
+#ifdef STORM_HAVE_CARL
+            storm::utility::Stopwatch swPreprocessing;
+            auto preprocessorData = helper::SparseMultiObjectivePreprocessor<SparseMaModelType>::preprocess(checkTask.getFormula(), this->getModel());
+            swPreprocessing.pause();
+            STORM_LOG_DEBUG("Preprocessing done. Data: " << preprocessorData);
+            
+            storm::utility::Stopwatch swHelper;
+            auto resultData = helper::SparseMultiObjectiveHelper<SparseMaModelType, storm::RationalNumber>::check(preprocessorData);
+            swHelper.pause();
+            STORM_LOG_DEBUG("Modelchecking done.");
+            
+            storm::utility::Stopwatch swPostprocessing;
+            result = helper::SparseMultiObjectivePostprocessor<SparseMaModelType, storm::RationalNumber>::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<storm::models::sparse::MarkovAutomaton<double>>;
+    }
+}

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 SparseMaModelType>
+        class SparseMaMultiObjectiveModelChecker : public SparseMarkovAutomatonCslModelChecker<SparseMaModelType> {
+        public:
+            typedef typename SparseMaModelType::ValueType ValueType;
+            typedef typename SparseMaModelType::RewardModelType RewardModelType;
+            
+            explicit SparseMaMultiObjectiveModelChecker(SparseMaModelType const& model);
+            
+            virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
+
+            virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) override;
+            
+        private:
+
+
+        };
+    } // namespace modelchecker
+} // namespace storm
+
+#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMAMULTIOBJECTIVEMODELCHECKER_H_ */

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp

@@ -54,7 +54,7 @@ namespace storm {
             result = helper::SparseMultiObjectivePostprocessor<SparseMdpModelType, storm::RationalNumber>::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;
         }

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::models::sparse::Mdp<double>, storm::RationalNumber>;
+            template class SparseMultiObjectiveHelper<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
 #endif
         }
     }

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::models::sparse::Mdp<double>, storm::RationalNumber>;
+            template class SparseMultiObjectivePostprocessor<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>;
 #endif
             
         }

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<storm::models::sparse::Mdp<double>>;
+            template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;
 
             
         }

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<storm::models::sparse::Mdp<double>>;
             template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<double>() const;
+            template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;
+            template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getInitialStateResultOfObjectives<double>() const;
 #ifdef STORM_HAVE_CARL
             template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
+            template std::vector<storm::RationalNumber> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>::getInitialStateResultOfObjectives<storm::RationalNumber>() const;
 #endif
             
         }

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

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<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
-            result = modelchecker.check(task);
+            if(modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
+            } else {
+                storm::modelchecker::SparseMaMultiObjectiveModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> 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.");
         }