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

polished cli output a bit

tempestpy_adaptions
dehnert 8 years ago
parent
c86a80ceeb
commit
75d513235a
1 changed files with 6 additions and 6 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. 12
      src/storm/cli/entrypoints.h

12
src/storm/cli/entrypoints.h
View File

@ -75,7 +75,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
for (auto const& property : properties) { for (auto const& property : properties) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush(); std::cout.flush();
storm::utility::Stopwatch modelCheckingWatch(true); storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
@ -97,7 +97,7 @@ namespace storm {
for (auto const& property : properties) { for (auto const& property : properties) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs."); STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs.");
STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush(); std::cout.flush();
storm::utility::Stopwatch modelCheckingWatch(true); storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
@ -122,7 +122,7 @@ namespace storm {
void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
typedef double ValueType; typedef double ValueType;
for (auto const& property : properties) { for (auto const& property : properties) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush(); std::cout.flush();
storm::utility::Stopwatch modelCheckingWatch(true); storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
@ -144,7 +144,7 @@ namespace storm {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs."); STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
for (auto const& property : formulas) { for (auto const& property : formulas) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush(); std::cout.flush();
bool formulaSupported = false; bool formulaSupported = false;
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
@ -199,7 +199,7 @@ namespace storm {
template<storm::dd::DdType DdType> template<storm::dd::DdType DdType>
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& property : formulas) { for (auto const& property : formulas) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush(); std::cout.flush();
storm::utility::Stopwatch modelCheckingWatch(true); storm::utility::Stopwatch modelCheckingWatch(true);
@ -220,7 +220,7 @@ namespace storm {
template<storm::dd::DdType DdType> template<storm::dd::DdType DdType>
void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& property : formulas) { for (auto const& property : formulas) {
STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush(); std::cout.flush();
storm::utility::Stopwatch modelCheckingWatch(true); storm::utility::Stopwatch modelCheckingWatch(true);

Write Preview
Loading…
Cancel
Save