spot 2.12.2
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
29namespace spot
30{
32 enum class SPOT_API mc_algorithm
33 {
36 CNDFS,
37 DEADLOCK,
39 SWARMING,
40 };
41
42 enum class SPOT_API mc_rvalue
43 {
44 DEADLOCK,
45 EMPTY,
46 FAILURE,
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;
93 os << "empty"; break;
95 os << "failure"; break;
97 os << "no_deadlock"; break;
99 os << "not_empty"; break;
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;
137 if ((lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::NO_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)
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.4