27#include <spot/misc/common.hh>
56 std::vector<std::string>
name;
66 SPOT_API std::ostream& operator<<(std::ostream& os,
const mc_algorithm& ma)
71 os <<
"bloemen_ec";
break;
73 os <<
"bloemen_scc";
break;
77 os <<
"deadlock";
break;
79 os <<
"reachability";
break;
81 os <<
"swarming";
break;
86 SPOT_API std::ostream& operator<<(std::ostream& os,
const mc_rvalue& mr)
91 os <<
"deadlock";
break;
95 os <<
"failure";
break;
97 os <<
"no_deadlock";
break;
99 os <<
"not_empty";
break;
101 os <<
"success";
break;
106 SPOT_API std::ostream& operator<<(std::ostream& os,
const ec_stats& es)
108 for (
unsigned i = 0; i < es.name.size(); ++i)
110 os <<
"---- Thread number:\t" << i <<
'\n'
111 <<
" - Algorithm:\t\t" << es.name[i] <<
'\n'
112 <<
" - Walltime (ms):\t" << es.walltime[i] <<
'\n'
113 <<
" - States:\t\t" << es.states[i] <<
'\n'
114 <<
" - Transitions:\t" << es.transitions[i] <<
'\n'
115 <<
" - Result:\t\t" << es.value[i] <<
'\n'
116 <<
" - SCCs:\t\t" << es.sccs[i] <<
'\n';
118 os <<
"CSV: tid,algorithm,walltime,states,transitions,"
119 "sccs,result,finisher\n"
120 <<
"@th_" << i <<
',' << es.name[i] <<
',' << es.walltime[i] <<
','
121 << es.states[i] <<
',' << es.transitions[i] <<
','
122 << es.sccs[i] <<
',' << es.value[i]
123 <<
',' << es.finisher[i] <<
"\n\n";
159 throw std::runtime_error(
"Unable to compare these elements!");
Definition: automata.hh:26
mc_algorithm
The list of parallel model-checking algorithms available.
Definition: mc.hh:33
@ CNDFS
Evangelista.12.atva emptiness check.
@ REACHABILITY
Only perform a reachability algorithm.
@ SWARMING
Holzmann.11.ieee applied to renault.13.lpar.
@ DEADLOCK
Check wether there is a deadlock.
@ BLOEMEN_SCC
Bloemen.16.ppopp SCC computation.
@ BLOEMEN_EC
Bloemen.16.hvc emptiness check.
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ NO_DEADLOCK
No deadlock has been found.
@ FAILURE
The Algorithm finished abnormally.
@ DEADLOCK
A deadlock has been found.
@ EMPTY
The product is empty.
@ SUCCESS
The Algorithm finished normally.
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:130
This structure contains, for each thread, the collected information during the traversal.
Definition: mc.hh:55
std::vector< mc_rvalue > value
The return status.
Definition: mc.hh:61
std::vector< unsigned > walltime
Walltime for this thread in ms.
Definition: mc.hh:57
std::vector< bool > finisher
Is it the finisher thread?
Definition: mc.hh:62
std::vector< int > sccs
Number of SCCs or -1.
Definition: mc.hh:60
std::vector< unsigned > states
Number of states visited.
Definition: mc.hh:58
std::vector< unsigned > transitions
Number of transitions visited.
Definition: mc.hh:59
std::vector< std::string > name
The name of the algorithm used.
Definition: mc.hh:56
std::string trace
The output trace.
Definition: mc.hh:63