diff --git a/src/settings/Option.cpp b/src/settings/Option.cpp index b5cba7759..cba074b58 100644 --- a/src/settings/Option.cpp +++ b/src/settings/Option.cpp @@ -2,6 +2,7 @@ #include #include +#include #include "ArgumentBase.h" #include "Argument.h" @@ -211,4 +212,4 @@ namespace storm { return out; } } -} \ No newline at end of file +} diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 07eefee1d..760ffe039 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -1,6 +1,7 @@ #include "src/storage/BitVectorHashMap.h" #include +#include #include "src/utility/macros.h" diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 8f176048e..f8bf6b368 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -1,3 +1,5 @@ +#include + #include "src/storage/dd/Bdd.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/Odd.h" @@ -360,4 +362,4 @@ namespace storm { template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; } -} \ No newline at end of file +} diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 3d93d4107..c30e6e5ba 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -46,6 +46,8 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) model->printModelInformationToStream(std::cout); + std::cout << "No. states (Explored): " << model->getNumberOfStates() << std::endl; + std::cout << "No. transitions (Explored): " << model->getNumberOfTransitions() << std::endl; if (model->getNumberOfStates() > 500 && model->isOfType(storm::models::ModelType::Ctmc)) { std::cout << "Bisimulation..." << std::endl; @@ -53,6 +55,9 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) model->printModelInformationToStream(std::cout); } + std::cout << "No. states (Bisimulation): " << model->getNumberOfStates() << std::endl; + std::cout << "No. transitions (Bisimulation): " << model->getNumberOfTransitions() << std::endl; + // Model checking std::cout << "Model checking..." << std::endl; std::unique_ptr result(storm::verifySparseModel(model, formulas[0])); diff --git a/src/utility/macros.h b/src/utility/macros.h index 4f70b1691..16dd4d70e 100644 --- a/src/utility/macros.h +++ b/src/utility/macros.h @@ -2,6 +2,7 @@ #define STORM_UTILITY_MACROS_H_ #include +#include #include "storm-config.h" #ifndef STORM_LOGGING_FRAMEWORK @@ -272,4 +273,4 @@ LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console." STORM_PRINT(message); \ } -#endif /* STORM_UTILITY_MACROS_H_ */ \ No newline at end of file +#endif /* STORM_UTILITY_MACROS_H_ */