spot  2.12.1
mc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <iostream>
22 #include <stdexcept>
23 #include <string>
24 #include <vector>
25 #include <utility>
26 
27 #include <spot/misc/common.hh>
28 
29 namespace spot
30 {
32  enum class SPOT_API mc_algorithm
33  {
34  BLOEMEN_EC,
35  BLOEMEN_SCC,
36  CNDFS,
37  DEADLOCK,
38  REACHABILITY,
39  SWARMING,
40  };
41 
42  enum class SPOT_API mc_rvalue
43  {
44  DEADLOCK,
45  EMPTY,
46  FAILURE,
47  NO_DEADLOCK,
48  NOT_EMPTY,
49  SUCCESS,
50  };
51 
54  struct SPOT_API ec_stats
55  {
56  std::vector<std::string> name;
57  std::vector<unsigned> walltime;
58  std::vector<unsigned> states;
59  std::vector<unsigned> transitions;
60  std::vector<int> sccs;
61  std::vector<mc_rvalue> value;
62  std::vector<bool> finisher;
63  std::string trace;
64  };
65 
66  SPOT_API std::ostream& operator<<(std::ostream& os, const mc_algorithm& ma)
67  {
68  switch (ma)
69  {
71  os << "bloemen_ec"; break;
73  os << "bloemen_scc"; break;
75  os << "cndfs"; break;
77  os << "deadlock"; break;
79  os << "reachability"; break;
81  os << "swarming"; break;
82  }
83  return os;
84  }
85 
86  SPOT_API std::ostream& operator<<(std::ostream& os, const mc_rvalue& mr)
87  {
88  switch (mr)
89  {
91  os << "deadlock"; break;
92  case mc_rvalue::EMPTY:
93  os << "empty"; break;
94  case mc_rvalue::FAILURE:
95  os << "failure"; break;
97  os << "no_deadlock"; break;
99  os << "not_empty"; break;
100  case mc_rvalue::SUCCESS:
101  os << "success"; break;
102  }
103  return os;
104  }
105 
106  SPOT_API std::ostream& operator<<(std::ostream& os, const ec_stats& es)
107  {
108  for (unsigned i = 0; i < es.name.size(); ++i)
109  {
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';
117 
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";
124  }
125  return os;
126  }
127 
130  SPOT_API const mc_rvalue operator|(const mc_rvalue& lhs, const mc_rvalue& rhs)
131  {
132  // Handle Deadlocks
133  if (lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::DEADLOCK)
134  return mc_rvalue::DEADLOCK;
135  if (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK)
136  return mc_rvalue::NO_DEADLOCK;
137  if ((lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) ||
138  (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::DEADLOCK))
139  return mc_rvalue::DEADLOCK;
140 
141  // Handle Emptiness
142  if (lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::EMPTY)
143  return mc_rvalue::EMPTY;
144  if (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::NOT_EMPTY)
145  return mc_rvalue::NOT_EMPTY;
146  if ((lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::NOT_EMPTY) ||
147  (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::EMPTY))
148  return mc_rvalue::EMPTY;
149 
150  // Handle Failure / Success
151  if (lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::FAILURE)
152  return mc_rvalue::FAILURE;
153  if (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::SUCCESS)
154  return mc_rvalue::SUCCESS;
155  if ((lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::SUCCESS) ||
156  (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::FAILURE))
157  return mc_rvalue::FAILURE;
158 
159  throw std::runtime_error("Unable to compare these elements!");
160  }
161 }
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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1