diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index d70646cb5..3b46b28b3 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/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 void SparseMdpRewardBoundedPcaaWeightVectorChecker::check(std::vector const& weightVector) { + ++numChecks; + + // In case we want to export the cdf, we will collect the corresponding data + std::vector> 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().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) { + std::vector 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(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().isExportCdfSet()) { + std::vector 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(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index 36cba968d..836aafce6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -82,7 +82,7 @@ namespace storm { void updateCachedData(typename MultiDimensionalRewardUnfolding::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector const& weightVector); storm::utility::Stopwatch swAll, swDataUpdate, swEqBuilding, swLinEqSolving, swMinMaxSolving, swAux1, swAux2, swAux3; - uint64_t numSchedChanges, numCheckedEpochs; + uint64_t numSchedChanges, numCheckedEpochs, numChecks; MultiDimensionalRewardUnfolding rewardUnfolding; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 44f94296d..7b26d43d6 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/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(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 53216e240..053b144e3 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/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;