export of cdf's

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@@ -9,6 +9,9 @@
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/solver/LinearEquationSolver.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/utility/export.h"
+#include "storm/settings/modules/IOSettings.h"
 
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/InvalidOperationException.h"
@@ -17,6 +20,7 @@
 #include "storm/exceptions/UnexpectedException.h"
 #include "storm/exceptions/UncheckedRequirementException.h"
 
+
 namespace storm {
     namespace modelchecker {
         namespace multiobjective {
@@ -29,18 +33,45 @@ namespace storm {
                 
                 numSchedChanges = 0;
                 numCheckedEpochs = 0;
+                numChecks = 0;
             }
             
             template <class SparseMdpModelType>
             void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::check(std::vector<ValueType> const& weightVector) {
+                ++numChecks;
+                
+                // In case we want to export the cdf, we will collect the corresponding data
+                std::vector<std::vector<ValueType>> cdfData;
+                
                 auto initEpoch = rewardUnfolding.getStartEpoch();
                 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
-                
                 EpochCheckingData cachedData;
                 for (auto const& epoch : epochOrder) {
                     computeEpochSolution(epoch, weightVector, cachedData);
+                    if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
+                        std::vector<ValueType> cdfEntry;
+                        for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) {
+                            uint64_t offset = rewardUnfolding.getDimension(i).isUpperBounded ? 0 : 1;
+                            cdfEntry.push_back(storm::utility::convertNumber<ValueType>(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) * rewardUnfolding.getDimension(i).scalingFactor);
+                        }
+                        auto const& solution = rewardUnfolding.getInitialStateResult(epoch);
+                        auto solutionIt = solution.begin();
+                        ++solutionIt;
+                        cdfEntry.insert(cdfEntry.end(), solutionIt, solution.end());
+                        cdfData.push_back(std::move(cdfEntry));
+                    }
                 }
                 
+                if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet()) {
+                    std::vector<std::string> headers;
+                    for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) {
+                        headers.push_back("obj" + std::to_string(rewardUnfolding.getDimension(i).objectiveIndex) + ":" + rewardUnfolding.getDimension(i).formula->toString());
+                    }
+                    for (uint64_t i = 0; i < this->objectives.size(); ++i) {
+                        headers.push_back("obj" + std::to_string(i));
+                    }
+                    storm::utility::exportDataToCSVFile("cdf" + std::to_string(numChecks) + ".csv", cdfData, headers);
+                }
                 auto solution = rewardUnfolding.getInitialStateResult(initEpoch);
                 // Todo: we currently assume precise results...
                 auto solutionIt = solution.begin();

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h

@@ -82,7 +82,7 @@ namespace storm {
                 void updateCachedData(typename MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector);
                 
                 storm::utility::Stopwatch swAll, swDataUpdate, swEqBuilding, swLinEqSolving, swMinMaxSolving, swAux1, swAux2, swAux3;
-                uint64_t numSchedChanges, numCheckedEpochs;
+                uint64_t numSchedChanges, numCheckedEpochs, numChecks;
                 
                 MultiDimensionalRewardUnfolding<ValueType, false> rewardUnfolding;
                 

src/storm/settings/modules/IOSettings.cpp

@@ -20,6 +20,8 @@ namespace storm {
             const std::string IOSettings::exportDotOptionName = "exportdot";
             const std::string IOSettings::exportExplicitOptionName = "exportexplicit";
             const std::string IOSettings::exportJaniDotOptionName = "exportjanidot";
+            const std::string IOSettings::exportCdfOptionName = "exportcdf";
+            const std::string IOSettings::exportCdfOptionShortName = "cdf";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
             const std::string IOSettings::explicitDrnOptionName = "explicit-drn";
@@ -57,6 +59,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.")
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setShortName(exportCdfOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
@@ -256,11 +259,15 @@ namespace storm {
             bool IOSettings::isBuildChoiceLabelsSet() const {
                 return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet();
             }
-
-           bool IOSettings::isBuildStateValuationsSet() const {
+            
+            bool IOSettings::isBuildStateValuationsSet() const {
                 return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet();
             }
 
+            bool IOSettings::isExportCdfSet() const {
+                return this->getOption(exportCdfOptionName).getHasOptionBeenSet();
+            }
+
             bool IOSettings::isPropertySet() const {
                 return this->getOption(propertyOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/IOSettings.h

@@ -316,6 +316,8 @@ namespace storm {
                  * @return
                  */
                 bool isBuildStateValuationsSet() const;
+                
+                bool isExportCdfSet() const;
 
                 bool check() const override;
                 void finalize() override;
@@ -328,6 +330,8 @@ namespace storm {
                 static const std::string exportDotOptionName;
                 static const std::string exportJaniDotOptionName;
                 static const std::string exportExplicitOptionName;
+                static const std::string exportCdfOptionName;
+                static const std::string exportCdfOptionShortName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;
                 static const std::string explicitDrnOptionName;