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 30 namespace spot 31 { 32 /// \brief The list of parallel model-checking algorithms available 33 enum class SPOT_API mc_algorithm 34 { 35 BLOEMEN_EC, ///< \brief Bloemen.16.hvc emptiness check 36 BLOEMEN_SCC, ///< \brief Bloemen.16.ppopp SCC computation 37 CNDFS, ///< \brief Evangelista.12.atva emptiness check 38 DEADLOCK, ///< \brief Check wether there is a deadlock 39 REACHABILITY, ///< \brief Only perform a reachability algorithm 40 SWARMING, ///< \brief Holzmann.11.ieee applied to renault.13.lpar 41 }; 42 43 enum class SPOT_API mc_rvalue 44 { 45 DEADLOCK, ///< \brief A deadlock has been found 46 EMPTY, ///< \brief The product is empty 47 FAILURE, ///< \brief The Algorithm finished abnormally 48 NO_DEADLOCK, ///< \brief No deadlock has been found 49 NOT_EMPTY, ///< \brief The product is not empty 50 SUCCESS, ///< \brief The Algorithm finished normally 51 }; 52 53 /// \brief This structure contains, for each thread, the collected information 54 /// during the traversal 55 struct SPOT_API ec_stats 56 { 57 std::vector<std::string> name; ///< \brief The name of the algorithm used 58 std::vector<unsigned> walltime; ///< \brief Walltime for this thread in ms 59 std::vector<unsigned> states; ///< \brief Number of states visited 60 std::vector<unsigned> transitions; ///< \brief Number of transitions visited 61 std::vector<int> sccs; ///< \brief Number of SCCs or -1 62 std::vector<mc_rvalue> value; ///< \brief The return status 63 std::vector<bool> finisher; ///< \brief Is it the finisher thread? 64 std::string trace; ///< \brief The output trace 65 }; 66 operator <<(std::ostream & os,const mc_algorithm & ma)67 SPOT_API std::ostream& operator<<(std::ostream& os, const mc_algorithm& ma) 68 { 69 switch (ma) 70 { 71 case mc_algorithm::BLOEMEN_EC: 72 os << "bloemen_ec"; break; 73 case mc_algorithm::BLOEMEN_SCC: 74 os << "bloemen_scc"; break; 75 case mc_algorithm::CNDFS: 76 os << "cndfs"; break; 77 case mc_algorithm::DEADLOCK: 78 os << "deadlock"; break; 79 case mc_algorithm::REACHABILITY: 80 os << "reachability"; break; 81 case mc_algorithm::SWARMING: 82 os << "swarming"; break; 83 } 84 return os; 85 } 86 operator <<(std::ostream & os,const mc_rvalue & mr)87 SPOT_API std::ostream& operator<<(std::ostream& os, const mc_rvalue& mr) 88 { 89 switch (mr) 90 { 91 case mc_rvalue::DEADLOCK: 92 os << "deadlock"; break; 93 case mc_rvalue::EMPTY: 94 os << "empty"; break; 95 case mc_rvalue::FAILURE: 96 os << "failure"; break; 97 case mc_rvalue::NO_DEADLOCK: 98 os << "no_deadlock"; break; 99 case mc_rvalue::NOT_EMPTY: 100 os << "not_empty"; break; 101 case mc_rvalue::SUCCESS: 102 os << "success"; break; 103 } 104 return os; 105 } 106 operator <<(std::ostream & os,const ec_stats & es)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 129 /// \brief This function helps to find the output value from a set of threads 130 /// that may have different values. operator |(const mc_rvalue & lhs,const mc_rvalue & rhs)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; 136 if (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) 137 return mc_rvalue::NO_DEADLOCK; 138 if ((lhs == mc_rvalue::DEADLOCK && rhs == mc_rvalue::NO_DEADLOCK) || 139 (lhs == mc_rvalue::NO_DEADLOCK && rhs == mc_rvalue::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) 146 return 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 } 163