Browse Source

..

Former-commit-id: a5386c4130
tempestpy_adaptions
TimQu 9 years ago
parent
commit
ea828243ee
  1. 29
      src/cli/entrypoints.h

29
src/cli/entrypoints.h

@ -138,6 +138,13 @@ namespace storm {
storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas); storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
std::cout << "INPUTMODEL_INFO;" <<
storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
model->getNumberOfStates() << ";" <<
model->getNumberOfTransitions() << ";" << std::endl;
// Preprocess the model if needed. // Preprocess the model if needed.
BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas); BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
@ -181,6 +188,12 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
} }
} }
std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
std::cout << "DONE_MODEL_INFO;" <<
storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
model->getNumberOfStates() << ";" <<
model->getNumberOfTransitions() << ";" << std::endl;
} }
template<typename ValueType> template<typename ValueType>
@ -198,12 +211,7 @@ namespace storm {
STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>()); std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>());
std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
std::cout << "INPUTMODEL_INFO;" <<
storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
model->getNumberOfStates() << ";" <<
model->getNumberOfTransitions() << ";" << std::endl;
// Preprocess the model if needed. // Preprocess the model if needed.
BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas);
@ -214,14 +222,7 @@ namespace storm {
if (!formulas.empty()) { if (!formulas.empty()) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas); verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
}
std::cout << "PrintingInfo;Filename;Constants;NumStates;NumTransitions" << std::endl;
std::cout << "DONE_MODEL_INFO;" <<
storm::settings::generalSettings().getSymbolicModelFilename() << ";" <<
storm::settings::generalSettings().getConstantDefinitionString() << ";" <<
model->getNumberOfStates() << ";" <<
model->getNumberOfTransitions() << ";" << std::endl;
}
} }
} }
} }

Loading…
Cancel
Save