Browse Source

Supporting export of generated Markov chain from DFT

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
9656d2c253
  1. 15
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

15
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@ -342,23 +342,24 @@ namespace storm {
return results;
} else {
// Build a single Markov Automaton
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet());
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
model->printModelInformationToStream(std::cout);
explorationTimer.stop();
// Export the model if required
// TODO move this outside of the model checker?
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) {
std::ofstream stream;
storm::utility::openFile(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), stream);
if (ioSettings.isExportExplicitSet()) {
std::vector<std::string> parameterNames;
// TODO fill parameter names
storm::exporter::explicitExportSparseModel(stream, model, parameterNames);
storm::utility::closeFile(stream);
storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames);
}
if (ioSettings.isExportDotSet()) {
storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename());
}
// Model checking

Loading…
Cancel
Save