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