Added LRA Environment

src/storm/environment/SubEnvironment.cpp

@@ -8,6 +8,7 @@
 #include "storm/environment/solver/EigenSolverEnvironment.h"
 #include "storm/environment/solver/GmmxxSolverEnvironment.h"
 #include "storm/environment/solver/NativeSolverEnvironment.h"
+#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/MultiplierEnvironment.h"
 #include "storm/environment/solver/GameSolverEnvironment.h"
@@ -63,6 +64,7 @@ namespace storm {
     template class SubEnvironment<EigenSolverEnvironment>;
     template class SubEnvironment<GmmxxSolverEnvironment>;
     template class SubEnvironment<NativeSolverEnvironment>;
+    template class SubEnvironment<LongRunAverageSolverEnvironment>;
     template class SubEnvironment<MinMaxSolverEnvironment>;
     template class SubEnvironment<MultiplierEnvironment>;
     template class SubEnvironment<GameSolverEnvironment>;

src/storm/environment/solver/LongRunAverageSolverEnvironment.cpp

@@ -0,0 +1,94 @@
+#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/LongRunAverageSolverSettings.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    
+    LongRunAverageSolverEnvironment::LongRunAverageSolverEnvironment() {
+        auto const& lraSettings = storm::settings::getModule<storm::settings::modules::LongRunAverageSolverSettings>();
+        detMethod = lraSettings.getDetLraMethod();
+        detMethodSetFromDefault = lraSettings.isDetLraMethodSetFromDefaultValue();
+        nondetMethod = lraSettings.getNondetLraMethod();
+        nondetMethodSetFromDefault = lraSettings.isNondetLraMethodSetFromDefaultValue();
+        precision = storm::utility::convertNumber<storm::RationalNumber>(lraSettings.getPrecision());
+        relative = lraSettings.isRelativePrecision();
+        if (lraSettings.isMaximalIterationCountSet()) {
+            maxIters = lraSettings.getMaximalIterationCount();
+        }
+        aperiodicFactor = lraSettings.getAperiodicFactor();
+    }
+    
+    LongRunAverageSolverEnvironment::~LongRunAverageSolverEnvironment() {
+        // Intentionally left empty
+    }
+    
+    storm::solver::LraMethod const& LongRunAverageSolverEnvironment::getDetLraMethod() const {
+        return detMethod;
+    }
+    
+    bool const& LongRunAverageSolverEnvironment::isDetLraMethodSetFromDefault() const {
+        return detMethodSetFromDefault;
+    }
+    
+    void LongRunAverageSolverEnvironment::setDetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault) {
+        detMethod = value;
+        detMethodSetFromDefault = isSetFromDefault;
+    }
+    
+    storm::solver::LraMethod const& LongRunAverageSolverEnvironment::getNondetLraMethod() const {
+        return nondetMethod;
+    }
+    
+    bool const& LongRunAverageSolverEnvironment::isNondetLraMethodSetFromDefault() const {
+        return nondetMethodSetFromDefault;
+    }
+    
+    void LongRunAverageSolverEnvironment::setNondetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault) {
+        nondetMethod = value;
+        nondetMethodSetFromDefault = isSetFromDefault;
+    }
+    
+    storm::RationalNumber const& LongRunAverageSolverEnvironment::getPrecision() const {
+        return precision;
+    }
+    
+    void LongRunAverageSolverEnvironment::setPrecision(storm::RationalNumber value) {
+        precision  = value;
+    }
+    
+    bool const& LongRunAverageSolverEnvironment::getRelativeTerminationCriterion() const {
+        return relative;
+    }
+    
+    void LongRunAverageSolverEnvironment::setRelativeTerminationCriterion(bool value) {
+        relative = value;
+    }
+    
+    bool LongRunAverageSolverEnvironment::isMaximalIterationCountSet() const {
+        return maxIters.is_initialized();
+    }
+    
+    uint64_t LongRunAverageSolverEnvironment::getMaximalIterationCount() const {
+        return maxIters.get();
+    }
+    
+    void LongRunAverageSolverEnvironment::setMaximalIterationCount(uint64_t value) {
+        maxIters = value;
+    }
+    
+    void LongRunAverageSolverEnvironment::unsetMaximalIterationCount() {
+        maxIters = boost::none;
+    }
+    
+    storm::RationalNumber const& LongRunAverageSolverEnvironment::getAperiodicFactor() const {
+        return aperiodicFactor;
+    }
+    
+    void LongRunAverageSolverEnvironment::setAperiodicFactor(storm::RationalNumber value) {
+        aperiodicFactor  = value;
+    }
+
+}

src/storm/environment/solver/LongRunAverageSolverEnvironment.h

@@ -0,0 +1,49 @@
+#pragma once
+
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/solver/SolverSelectionOptions.h"
+
+namespace storm {
+    
+    class LongRunAverageSolverEnvironment {
+    public:
+        
+        LongRunAverageSolverEnvironment();
+        ~LongRunAverageSolverEnvironment();
+        
+        storm::solver::LraMethod const& getDetLraMethod() const;
+        bool const& isDetLraMethodSetFromDefault() const;
+        void setDetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault = false);
+
+        storm::solver::LraMethod const& getNondetLraMethod() const;
+        bool const& isNondetLraMethodSetFromDefault() const;
+        void setNondetLraMethod(storm::solver::LraMethod value, bool isSetFromDefault = false);
+        
+        storm::RationalNumber const& getPrecision() const;
+        void setPrecision(storm::RationalNumber value);
+        bool const& getRelativeTerminationCriterion() const;
+        void setRelativeTerminationCriterion(bool value);
+
+        bool isMaximalIterationCountSet() const;
+        uint64_t getMaximalIterationCount() const;
+        void setMaximalIterationCount(uint64_t value);
+        void unsetMaximalIterationCount();
+        
+        storm::RationalNumber const& getAperiodicFactor() const;
+        void setAperiodicFactor(storm::RationalNumber value);
+
+    private:
+        storm::solver::LraMethod detMethod;
+        bool detMethodSetFromDefault;
+        
+        storm::solver::LraMethod nondetMethod;
+        bool nondetMethodSetFromDefault;
+        
+        storm::RationalNumber precision;
+        bool relative;
+        boost::optional<uint64_t> maxIters;
+        
+        storm::RationalNumber aperiodicFactor;
+    };
+}
+

src/storm/environment/solver/SolverEnvironment.cpp

@@ -1,5 +1,6 @@
 #include "storm/environment/solver/SolverEnvironment.h"
 
+#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/MultiplierEnvironment.h"
 #include "storm/environment/solver/EigenSolverEnvironment.h"
@@ -29,6 +30,14 @@ namespace storm {
         // Intentionally left empty
     }
     
+    LongRunAverageSolverEnvironment& SolverEnvironment::lra() {
+        return longRunAverageSolverEnvironment.get();
+    }
+    
+    LongRunAverageSolverEnvironment const& SolverEnvironment::lra() const {
+        return longRunAverageSolverEnvironment.get();
+    }
+    
     MinMaxSolverEnvironment& SolverEnvironment::minMax() {
         return minMaxSolverEnvironment.get();
     }

src/storm/environment/solver/SolverEnvironment.h

@@ -14,6 +14,7 @@ namespace storm {
     class EigenSolverEnvironment;
     class GmmxxSolverEnvironment;
     class NativeSolverEnvironment;
+    class LongRunAverageSolverEnvironment;
     class MinMaxSolverEnvironment;
     class MultiplierEnvironment;
     class GameSolverEnvironment;
@@ -31,6 +32,8 @@ namespace storm {
         GmmxxSolverEnvironment const& gmmxx() const;
         NativeSolverEnvironment& native();
         NativeSolverEnvironment const& native() const;
+        LongRunAverageSolverEnvironment& lra();
+        LongRunAverageSolverEnvironment const& lra() const;
         MinMaxSolverEnvironment& minMax();
         MinMaxSolverEnvironment const& minMax() const;
         MultiplierEnvironment& multiplier();
@@ -56,6 +59,7 @@ namespace storm {
         SubEnvironment<NativeSolverEnvironment> nativeSolverEnvironment;
         SubEnvironment<GameSolverEnvironment> gameSolverEnvironment;
         SubEnvironment<TopologicalSolverEnvironment> topologicalSolverEnvironment;
+        SubEnvironment<LongRunAverageSolverEnvironment> longRunAverageSolverEnvironment;
         SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
         SubEnvironment<MultiplierEnvironment> multiplierEnvironment;
       

src/storm/solver/SolverSelectionOptions.h

@@ -9,7 +9,7 @@ namespace storm {
         ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, TopologicalCuda, ViToPi)
         ExtendEnumsWithSelectionField(MultiplierType, Native, Gmmxx)
         ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration)
-        ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration)
+        ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration, GainBiasEquations, LraDistributionEquations)
 
         ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3)
         ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological)