Browse Source

Flag for printing information about model generated from DFT

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
f6faf9e3a5
  1. 4
      src/storm-dft/api/storm-dft.h
  2. 6
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  3. 4
      src/storm-dft/modelchecker/dft/DFTModelChecker.h

4
src/storm-dft/api/storm-dft.h

@ -69,7 +69,7 @@ namespace storm {
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation,
bool enableDC, bool printOutput) { bool enableDC, bool printOutput) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0); typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
if (printOutput) { if (printOutput) {
modelChecker.printTimings(); modelChecker.printTimings();
@ -95,7 +95,7 @@ namespace storm {
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred,
bool allowModularisation, bool enableDC, double approximationError, bool printOutput) { bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC,
approximationError); approximationError);
if (printOutput) { if (printOutput) {

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

@ -348,9 +348,13 @@ namespace storm {
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet()); typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet());
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);
explorationTimer.stop(); explorationTimer.stop();
// Print model information
if (printInfo) {
model->printModelInformationToStream(std::cout);
}
// Export the model if required // Export the model if required
// TODO move this outside of the model checker? // TODO move this outside of the model checker?
if (ioSettings.isExportExplicitSet()) { if (ioSettings.isExportExplicitSet()) {

4
src/storm-dft/modelchecker/dft/DFTModelChecker.h

@ -25,7 +25,7 @@ namespace storm {
/*! /*!
* Constructor. * Constructor.
*/ */
DFTModelChecker() {
DFTModelChecker(bool printOutput) : printInfo(printOutput) {
} }
/*! /*!
@ -58,6 +58,8 @@ namespace storm {
private: private:
bool printInfo;
// Timing values // Timing values
storm::utility::Stopwatch buildingTimer; storm::utility::Stopwatch buildingTimer;
storm::utility::Stopwatch explorationTimer; storm::utility::Stopwatch explorationTimer;

Loading…
Cancel
Save