diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index f47f4bc10..dab863e69 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -76,6 +76,7 @@ namespace storm { void verifySparseModel(std::shared_ptr> model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { for (auto const& property : properties) { std::cout << std::endl << "Model checking property: " << property << " ..."; + std::cout.flush(); std::unique_ptr result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; @@ -96,6 +97,7 @@ namespace storm { 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."); std::cout << std::endl << "Model checking property: " << property << " ..."; + std::cout.flush(); std::unique_ptr result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; @@ -119,6 +121,7 @@ namespace storm { typedef double ValueType; for (auto const& property : properties) { std::cout << std::endl << "Model checking property: " << property << " ..."; + std::cout.flush(); std::unique_ptr result(storm::verifySymbolicModelWithAbstractionRefinementEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; @@ -138,6 +141,7 @@ namespace storm { for (auto const& property : formulas) { std::cout << std::endl << "Model checking property: " << property << " ..."; + std::cout.flush(); bool formulaSupported = false; std::unique_ptr result; @@ -187,6 +191,7 @@ namespace storm { void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& property : formulas) { std::cout << std::endl << "Model checking property: " << property << " ..."; + std::cout.flush(); std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { @@ -205,6 +210,7 @@ namespace storm { void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& property : formulas) { std::cout << std::endl << "Model checking property: " << property << " ..."; + std::cout.flush(); std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index 17e175a04..c26ede01d 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -5,7 +5,7 @@ namespace storm { std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { - return os << "Obtain " << toString(fe.getFilterType()) << " the 'initial'-states with values described by '" << *fe.getFormula() << "'"; + return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'"; } Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment)