diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 7f11d1caa..8d655764e 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/utility/bitoperations.h" +#include "storm/utility/DirectEncodingExporter.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" @@ -354,6 +355,16 @@ namespace storm { model->printModelInformationToStream(std::cout); explorationTimer.stop(); + // Export the model if required + if (storm::settings::getModule().isExportExplicitSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + std::vector parameterNames; + // TODO fill parameter names + storm::exporter::explicitExportSparseModel(stream, model, parameterNames); + storm::utility::closeFile(stream); + } + // Model checking std::vector resultsValue = checkModel(model, properties); dft_results results; diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 8b968e756..a3883512f 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -6,7 +6,7 @@ #include "storm/utility/storm.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/ExplicitExporter.h" +#include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/Stopwatch.h" #include "storm/exceptions/NotImplementedException.h" diff --git a/src/storm/utility/ExplicitExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp similarity index 56% rename from src/storm/utility/ExplicitExporter.cpp rename to src/storm/utility/DirectEncodingExporter.cpp index 1f40ab538..194ba7763 100644 --- a/src/storm/utility/ExplicitExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -1,4 +1,4 @@ -#include "ExplicitExporter.h" +#include "DirectEncodingExporter.h" #include "storm/adapters/CarlAdapter.h" #include "storm/utility/constants.h" @@ -14,26 +14,24 @@ namespace storm { namespace exporter { + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { - bool embedded = false; - if(sparseModel->getType() == storm::models::ModelType::Ctmc || sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { - STORM_LOG_WARN("This format only supports discrete time models"); - embedded = true; - } - - STORM_LOG_THROW(embedded || sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - + + // Notice that for CTMCs we write the rate matrix instead of probabilities + + // Initialize std::vector exitRates; // Only for CTMCs and MAs. if(sparseModel->getType() == storm::models::ModelType::Ctmc) { exitRates = sparseModel->template as>()->getExitRateVector(); } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { exitRates = sparseModel->template as>()->getExitRates(); } - + + // Write header os << "// Exported by storm" << std::endl; os << "// Original model type: " << sparseModel->getType() << std::endl; - os << "@type: mdp" << std::endl; + os << "@type: " << sparseModel->getType() << std::endl; os << "@parameters" << std::endl; for (auto const& p : parameters) { os << p << " "; @@ -41,98 +39,93 @@ namespace storm { os << std::endl; os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; os << "@model" << std::endl; + storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { os << "state " << group; - - if (!embedded) { - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; - } - - if(rewardModelEntry.second.hasStateRewards()) { - os << rewardModelEntry.second.getStateRewardVector().at(group); - } else { - os << "0"; - } + + // Write state rewards + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; } - - if (!first) { - os << "]"; + + if(rewardModelEntry.second.hasStateRewards()) { + os << rewardModelEntry.second.getStateRewardVector().at(group); + } else { + os << "0"; } - } else { - // We currently only support the expected time. - os << " [" << storm::utility::one()/exitRates.at(group) << "]"; } - + + if (!first) { + os << "]"; + } + + // Write labels for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { os << " " << label; } os << std::endl; + + // Write probabilities typename storm::storage::SparseMatrix::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; typename storm::storage::SparseMatrix::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; - - - for (typename storm::storage::SparseMatrix::index_type i = start; i < end; ++i) { + + // Iterate over all actions + for (typename storm::storage::SparseMatrix::index_type row = start; row < end; ++row) { // Print the actual row. - os << "\taction " << i - start; - if (!embedded) { - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; - } - - if(rewardModelEntry.second.hasStateActionRewards()) { - os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); - } else { - os << "0"; - } - + os << "\taction " << row - start; + bool first = true; + // Write transition rewards + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; } - if (!first) { - os << "]"; + + if(rewardModelEntry.second.hasStateActionRewards()) { + os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row)); + } else { + os << "0"; } - } else { - // We currently only support the expected time. + + } + if (!first) { + os << "]"; } - - + // Write choice labeling if(sparseModel->hasChoiceLabeling()) { - //TODO + // TODO export choice labeling } os << std::endl; - - for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { + // Write probabilities + for(auto it = matrix.begin(row); it != matrix.end(row); ++it) { ValueType prob = it->getValue(); - if(embedded) { - prob = prob / exitRates.at(group); - } os << "\t\t" << it->getColumn() << " : "; os << storm::utility::to_string(prob) << std::endl; } } - } + } // end matrix iteration } template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - + +#ifdef STORM_HAVE_CARL template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); +#endif } } diff --git a/src/storm/utility/ExplicitExporter.h b/src/storm/utility/DirectEncodingExporter.h similarity index 59% rename from src/storm/utility/ExplicitExporter.h rename to src/storm/utility/DirectEncodingExporter.h index 964b1f10f..2ebee0092 100644 --- a/src/storm/utility/ExplicitExporter.h +++ b/src/storm/utility/DirectEncodingExporter.h @@ -6,10 +6,16 @@ namespace storm { namespace exporter { - + + /*! + * Exports a sparse model into the explicit DRN format. + * + * @param os Stream to export to + * @param sparseModel Model to export + * @param parameters List of parameters + */ template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); - } }