spot 2.11.2.dev
mc.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015, 2016, 2017, 2019, 2020 Laboratoire de Recherche et
3// Developpement de l'Epita
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <iostream>
23#include <stdexcept>
24#include <string>
25#include <vector>
26#include <utility>
27
28#include <spot/misc/common.hh>
29
30namespace spot
31{
33 enum class SPOT_API mc_algorithm
34 {
37 CNDFS,
38 DEADLOCK,
40 SWARMING,
41 };
42
43 enum class SPOT_API mc_rvalue
44 {
45 DEADLOCK,
46 EMPTY,
47 FAILURE,
49 NOT_EMPTY,
50 SUCCESS,
51 };
52
55 struct SPOT_API ec_stats
56 {
57 std::vector<std::string> name;
58 std::vector<unsigned> walltime;
59 std::vector<unsigned> states;
60 std::vector<unsigned> transitions;
61 std::vector<int> sccs;
62 std::vector<mc_rvalue> value;
63 std::vector<bool> finisher;
64 std::string trace;
65 };
66
67 SPOT_API std::ostream& operator<<(std::ostream& os, const mc_algorithm& ma)
68 {
69 switch (ma)
70 {
72 os << "bloemen_ec"; break;
74 os << "bloemen_scc"; break;
76 os << "cndfs"; break;
78 os << "deadlock"; break;
80 os << "reachability"; break;
82 os << "swarming"; break;
83 }
84 return os;
85 }
86
87 SPOT_API std::ostream& operator<<(std::ostream& os, const mc_rvalue& mr)
88 {
89 switch (mr)
90 {
92 os << "deadlock"; break;
94 os << "empty"; break;
96 os << "failure"; break;
98 os << "no_deadlock"; break;
100 os << "not_empty"; break;
102 os << "success"; break;
103 }
104 return os;
105 }
106
107 SPOT_API std::ostream& operator<<(std::ostream& os, const ec_stats& es)
108 {
109 for (unsigned i = 0; i < es.name.size(); ++i)
110 {
111 os << "---- Thread number:\t" << i << '\n'
112 << " - Algorithm:\t\t" << es.name[i] << '\n'
113 << " - Walltime (ms):\t" << es.walltime[i] <<'\n'
114 << " - States:\t\t" << es.states[i] << '\n'
115 << " - Transitions:\t" << es.transitions[i] << '\n'
116 << " - Result:\t\t" << es.value[i] << '\n'
117 << " - SCCs:\t\t" << es.sccs[i] << '\n';
118
119 os << "CSV: tid,algorithm,walltime,states,transitions,"
120 "sccs,result,finisher\n"
121 << "@th_" << i << ',' << es.name[i] << ',' << es.walltime[i] << ','
122 << es.states[i] << ',' << es.transitions[i] << ','
123 << es.sccs[i] << ',' << es.value[i]
124 << ',' << es.finisher[i] << "\n\n";
125 }
126 return os;
127 }
128
131 SPOT_API const mc_rvalue operator|(const mc_rvalue& lhs, const mc_rvalue& rhs)
132 {
133 // Handle Deadlocks
134 if (lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::DEADLOCK)
135 return mc_rvalue::DEADLOCK;
138 if ((lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) ||
140 return mc_rvalue::DEADLOCK;
141
142 // Handle Emptiness
143 if (lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::EMPTY)
144 return mc_rvalue::EMPTY;
145 if (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::NOT_EMPTY)
147 if ((lhs == mc_rvalue::EMPTY && rhs == mc_rvalue::NOT_EMPTY) ||
148 (lhs == mc_rvalue::NOT_EMPTY && rhs == mc_rvalue::EMPTY))
149 return mc_rvalue::EMPTY;
150
151 // Handle Failure / Success
152 if (lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::FAILURE)
153 return mc_rvalue::FAILURE;
154 if (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::SUCCESS)
155 return mc_rvalue::SUCCESS;
156 if ((lhs == mc_rvalue::FAILURE && rhs == mc_rvalue::SUCCESS) ||
157 (lhs == mc_rvalue::SUCCESS && rhs == mc_rvalue::FAILURE))
158 return mc_rvalue::FAILURE;
159
160 throw std::runtime_error("Unable to compare these elements!");
161 }
162}
Definition: automata.hh:27
mc_algorithm
The list of parallel model-checking algorithms available.
Definition: mc.hh:34
@ 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:44
@ 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:131
This structure contains, for each thread, the collected information during the traversal.
Definition: mc.hh:56
std::vector< mc_rvalue > value
The return status.
Definition: mc.hh:62
std::vector< unsigned > walltime
Walltime for this thread in ms.
Definition: mc.hh:58
std::vector< bool > finisher
Is it the finisher thread?
Definition: mc.hh:63
std::vector< int > sccs
Number of SCCs or -1.
Definition: mc.hh:61
std::vector< unsigned > states
Number of states visited.
Definition: mc.hh:59
std::vector< unsigned > transitions
Number of transitions visited.
Definition: mc.hh:60
std::vector< std::string > name
The name of the algorithm used.
Definition: mc.hh:57
std::string trace
The output trace.
Definition: mc.hh:64

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