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

Print model information

main
Matthias Volk 9 years ago
parent
21e16a9222
commit
1c2426b0f4
4 changed files with 15 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
  2. 2
      src/storm-dft/generator/DftNextStateGenerator.cpp
  3. 19
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  4. 8
      src/storm/utility/storm.h

2
src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
View File

@ -525,8 +525,6 @@ namespace storm {
}
}
STORM_LOG_DEBUG("No. states: " << model->getNumberOfStates());
STORM_LOG_DEBUG("No. transitions: " << model->getNumberOfTransitions());
if (model->getNumberOfStates() <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix());
} else {

2
src/storm-dft/generator/DftNextStateGenerator.cpp
View File

@ -45,7 +45,7 @@ namespace storm {
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state));
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;

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

@ -194,9 +194,6 @@ namespace storm {
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
@ -219,8 +216,8 @@ namespace storm {
composedModel = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
bisimulationTimer.stop();
STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates());
STORM_LOG_DEBUG("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
if (composedModel->getNumberOfStates() <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix());
} else {
@ -228,6 +225,7 @@ namespace storm {
}
}
composedModel->printModelInformationToStream(std::cout);
return composedModel;
} else {
// No composition was possible
@ -249,9 +247,7 @@ namespace storm {
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
model->printModelInformationToStream(std::cout);
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
return model->template as<storm::models::sparse::Ctmc<ValueType>>();
@ -308,8 +304,7 @@ namespace storm {
STORM_LOG_INFO("Getting model for lower bound...");
model = builder.getModelApproximation(probabilityFormula ? false : true);
// We only output the info from the lower bound as the info for the upper bound is the same
STORM_LOG_INFO("No. states: " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions());
model->printModelInformationToStream(std::cout);
buildingTimer.stop();
// Check lower bounds
@ -356,9 +351,7 @@ namespace storm {
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions;
model = builder.buildModel(labeloptions);
}
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
model->printModelInformationToStream(std::cout);
explorationTimer.stop();
// Model checking

8
src/storm/utility/storm.h
View File

@ -192,6 +192,10 @@ namespace storm {
storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
bisimulationDecomposition.computeBisimulationDecomposition();
model = bisimulationDecomposition.getQuotient();
// Print some information about the model after the bisimulation
model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("Bisimulation done. ");
return model;
}
@ -208,6 +212,10 @@ namespace storm {
storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
bisimulationDecomposition.computeBisimulationDecomposition();
model = bisimulationDecomposition.getQuotient();
// Print some information about the model after the bisimulation
model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("Bisimulation done.");
return model;
}

Write Preview
Loading…
Cancel
Save