sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Build all labels for DFT model if export is enabled

tempestpy_adaptions
Matthias Volk 7 years ago
parent
87edc3abe0
commit
006ccaa2ee
1 changed files with 3 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

6
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -204,7 +204,7 @@ namespace storm {
// Build a single CTMC // Build a single CTMC
STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ..."); STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC); storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
builder.buildModel(labeloptions, 0, 0.0); builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel(); std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
explorationTimer.stop(); explorationTimer.stop();
@ -256,7 +256,7 @@ namespace storm {
STORM_LOG_DEBUG("Building Model..."); STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC); storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
builder.buildModel(labeloptions, 0, 0.0); builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel(); std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout); //model->printModelInformationToStream(std::cout);
@ -288,7 +288,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult; std::vector<ValueType> newResult;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC); storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
// TODO Matthias: compute approximation for all properties simultaneously? // TODO Matthias: compute approximation for all properties simultaneously?
std::shared_ptr<const storm::logic::Formula> property = properties[0]; std::shared_ptr<const storm::logic::Formula> property = properties[0];

Write Preview
Loading…
Cancel
Save