Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
print.cpp
Go to the documentation of this file.
2
3#include "resources.h" // This header knows what to include for memory consumption
5#include "storm/utility/cli.h"
7
8#include <boost/algorithm/string/replace.hpp>
9#include <ctime>
10
11#ifdef STORM_HAVE_GLPK
12#include "glpk.h"
13#endif
14#ifdef STORM_HAVE_GUROBI
15#include "gurobi_c.h"
16#endif
17#ifdef STORM_HAVE_MATHSAT
18#include "mathsat.h"
19#endif
20#ifdef STORM_HAVE_SOPLEX
21#include "soplex.h"
22#endif
23#ifdef STORM_HAVE_SPOT
24#include <spot/misc/version.hh>
25#endif
26#ifdef STORM_HAVE_XERCES
27#include <xercesc/util/XercesVersion.hpp>
28#endif
29#ifdef STORM_HAVE_Z3
30#include "z3.h"
31#endif
32
33namespace storm {
34namespace cli {
35
36std::string shellQuoteSingleIfNecessary(const std::string& arg) {
37 // quote empty argument
38 if (arg.empty()) {
39 return "''";
40 }
41
42 if (arg.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_./=") != std::string::npos) {
43 // contains potentially unsafe character, needs quoting
44 if (arg.find('\'') != std::string::npos) {
45 // contains ', we have to replace all ' with '\''
46 std::string escaped(arg);
47 boost::replace_all(escaped, "'", "'\\''");
48 return "'" + escaped + "'";
49 } else {
50 return "'" + arg + "'";
51 }
52 }
53
54 return arg;
55}
56
57void printHeader(std::string const& name, const int argc, const char** argv) {
59#ifndef NDEBUG
60 STORM_PRINT("DEBUG BUILD\n");
61#endif
62 // "Compute" the command line argument string with which storm was invoked.
63 std::stringstream commandStream;
64 for (int i = 1; i < argc; ++i) {
65 commandStream << " " << shellQuoteSingleIfNecessary(argv[i]);
66 }
67
68 std::string command = commandStream.str();
69
70 if (!command.empty()) {
71 STORM_PRINT('\n');
72 std::time_t result = std::time(nullptr);
73 STORM_PRINT("Date: " << std::ctime(&result));
74 STORM_PRINT("Command line arguments:" << commandStream.str() << '\n');
75 STORM_PRINT("Current working directory: " << storm::utility::cli::getCurrentWorkingDirectory() << "\n\n");
76 }
77}
78
82
83 // Print configuration options
84#ifdef STORM_USE_CLN_EA
85 STORM_PRINT("Using CLN numbers for exact arithmetic.\n");
86#else
87 STORM_PRINT("Using GMP numbers for exact arithmetic.\n");
88#endif
89#ifdef STORM_USE_CLN_RF
90 STORM_PRINT("Using CLN numbers for rational functions.\n");
91#else
92 STORM_PRINT("Using GMP numbers for rational functions.\n");
93#endif
94
95 // Print linked dependencies
96 STORM_PRINT("Linked with CArL v" << STORM_CARL_VERSION << ".\n");
97#ifdef STORM_HAVE_GLPK
98 STORM_PRINT("Linked with GLPK v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << ".\n");
99#else
100 STORM_PRINT("Not linked with GLPK.\n");
101#endif
102#ifdef STORM_HAVE_GMM
103 STORM_PRINT("Linked with GMM.\n");
104#else
105 STORM_PRINT("Not linked with GMM.\n");
106#endif
107#ifdef STORM_HAVE_GUROBI
108 STORM_PRINT("Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << ".\n");
109#else
110 STORM_PRINT("Not linked with Gurobi.\n");
111#endif
112#ifdef STORM_HAVE_MATHSAT
113 char* msatVersion = msat_get_version();
114 STORM_PRINT("Linked with " << msatVersion << ".\n");
115 msat_free(msatVersion);
116#else
117 STORM_PRINT("Not linked with MathSat.\n");
118#endif
119#ifdef STORM_HAVE_SOPLEX
120 STORM_PRINT("Linked with Soplex v" << SOPLEX_VERSION << ".\n");
121#else
122 STORM_PRINT("Not linked with Soplex.\n");
123#endif
124#ifdef STORM_HAVE_SPOT
125 STORM_PRINT("Linked with Spot v" << spot::version() << ".\n");
126#else
127 STORM_PRINT("Not linked with Spot.\n");
128#endif
129#ifdef STORM_HAVE_XERCES
130 STORM_PRINT("Linked with Xerces-C v" << gXercesMajVersion << "." << gXercesMinVersion << "." << gXercesRevision << ".\n");
131#else
132 STORM_PRINT("Not linked with Xerces-C.\n");
133#endif
134#ifdef STORM_HAVE_Z3
135 unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
136 Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
137#ifdef STORM_HAVE_Z3_OPTIMIZE
138 STORM_PRINT("Linked with Z3 Theorem Prover v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber
139 << " (with optimization features).\n");
140#else
141 STORM_PRINT("Linked with Z3 Theorem Prover v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << ".\n");
142#endif
143#else
144 STORM_PRINT("Not linked with Z3 Theorem Prover\n");
145#endif
146 STORM_PRINT("\n");
147}
148
149void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) {
150 struct rusage ru;
151 getrusage(RUSAGE_SELF, &ru);
152
153 std::cout << "\nPerformance statistics:\n";
154#ifdef MACOS
155 // For Mac OS, this is returned in bytes.
156 uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024;
157#endif
158#ifdef LINUX
159 // For Linux, this is returned in kilobytes.
160 uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024;
161#endif
162 std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB\n";
163 char oldFillChar = std::cout.fill('0');
164 std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << ru.ru_utime.tv_usec / 1000 << "s\n";
165 if (wallclockMilliseconds != 0) {
166 std::cout << " * wallclock time: " << (wallclockMilliseconds / 1000) << "." << std::setw(3) << (wallclockMilliseconds % 1000) << "s\n";
167 }
168 std::cout.fill(oldFillChar);
169}
170
171} // namespace cli
172} // namespace storm
#define STORM_PRINT(message)
Define the macros that print information and optionally also log it.
Definition macros.h:62
void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds)
Definition print.cpp:149
std::string shellQuoteSingleIfNecessary(const std::string &arg)
For a command-line argument, returns a quoted version with single quotes if it contains unsafe charac...
Definition print.cpp:36
void printHeader(std::string const &name, const int argc, const char **argv)
Definition print.cpp:57
void printVersion()
Definition print.cpp:79
std::string getCurrentWorkingDirectory()
Definition cli.cpp:15
LabParser.cpp.
static std::string longVersionString()
static std::string shortVersionString()
static std::string buildInfo()