1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2012-2018, 2021 Laboratoire de Recherche et Développement 3 // de l'Epita (LRDE). 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 #include "config.h" 21 #include <spot/twaalgos/isdet.hh> 22 #include <spot/twaalgos/sccinfo.hh> 23 24 namespace spot 25 { 26 namespace 27 { 28 template<bool count> 29 static 30 unsigned count_nondet_states_aux(const const_twa_graph_ptr & aut)31 count_nondet_states_aux(const const_twa_graph_ptr& aut) 32 { 33 unsigned nondet_states = 0; 34 unsigned ns = aut->num_states(); 35 for (unsigned src = 0; src < ns; ++src) 36 { 37 bdd available = bddtrue; 38 for (auto& t: aut->out(src)) 39 if (!bdd_implies(t.cond, available)) 40 { 41 ++nondet_states; 42 break; 43 } 44 else 45 { 46 available -= t.cond; 47 } 48 // If we are not counting non-deterministic states, abort as 49 // soon as possible. 50 if (!count && nondet_states) 51 break; 52 } 53 std::const_pointer_cast<twa_graph>(aut) 54 ->prop_universal(!nondet_states); 55 return nondet_states; 56 } 57 } 58 59 unsigned count_nondet_states(const const_twa_graph_ptr & aut)60 count_nondet_states(const const_twa_graph_ptr& aut) 61 { 62 if (aut->prop_universal()) 63 return 0; 64 return count_nondet_states_aux<true>(aut); 65 } 66 67 bool is_universal(const const_twa_graph_ptr & aut)68 is_universal(const const_twa_graph_ptr& aut) 69 { 70 trival d = aut->prop_universal(); 71 if (d.is_known()) 72 return d.is_true(); 73 return !count_nondet_states_aux<false>(aut); 74 } 75 76 bool is_deterministic(const const_twa_graph_ptr & aut)77 is_deterministic(const const_twa_graph_ptr& aut) 78 { 79 return aut->is_existential() && is_universal(aut); 80 } 81 82 void highlight_nondet_states(twa_graph_ptr & aut,unsigned color)83 highlight_nondet_states(twa_graph_ptr& aut, unsigned color) 84 { 85 if (aut->prop_universal()) 86 return; 87 unsigned ns = aut->num_states(); 88 auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>> 89 ("highlight-states"); 90 bool universal = true; 91 for (unsigned src = 0; src < ns; ++src) 92 { 93 bdd available = bddtrue; 94 for (auto& t: aut->out(src)) 95 if (!bdd_implies(t.cond, available)) 96 { 97 (*highlight)[src] = color; 98 universal = false; 99 } 100 else 101 { 102 available -= t.cond; 103 } 104 } 105 aut->prop_universal(universal); 106 } 107 108 void highlight_nondet_edges(twa_graph_ptr & aut,unsigned color)109 highlight_nondet_edges(twa_graph_ptr& aut, unsigned color) 110 { 111 if (aut->prop_universal()) 112 return; 113 unsigned ns = aut->num_states(); 114 auto* highlight = aut->get_or_set_named_prop<std::map<unsigned, unsigned>> 115 ("highlight-edges"); 116 bool universal = true; 117 for (unsigned src = 0; src < ns; ++src) 118 { 119 // Make a first pass to gather non-deterministic labels 120 bdd available = bddtrue; 121 bdd extra = bddfalse; 122 for (auto& t: aut->out(src)) 123 if (!bdd_implies(t.cond, available)) 124 { 125 extra |= (t.cond - available); 126 universal = false; 127 } 128 else 129 { 130 available -= t.cond; 131 } 132 // Second pass to gather the relevant edges. 133 if (!universal) 134 for (auto& t: aut->out(src)) 135 if (bdd_have_common_assignment(t.cond, extra)) 136 (*highlight)[aut->get_graph().index_of_edge(t)] = color; 137 } 138 aut->prop_universal(universal); 139 } 140 highlight_semidet_sccs(scc_info & si,unsigned color)141 void highlight_semidet_sccs(scc_info& si, unsigned color) 142 { 143 auto det_sccs = semidet_sccs(si); 144 if (det_sccs.empty()) 145 return; 146 auto aut = si.get_aut(); 147 auto* highlight = std::const_pointer_cast<twa_graph>(aut) 148 ->get_or_set_named_prop<std::map<unsigned, unsigned>>("highlight-states"); 149 for (unsigned scc = 0; scc < si.scc_count(); scc++) 150 { 151 if (det_sccs[scc]) 152 { 153 for (auto& t : si.states_of(scc)) 154 (*highlight)[t] = color; 155 } 156 } 157 } 158 159 bool is_complete(const const_twa_graph_ptr & aut)160 is_complete(const const_twa_graph_ptr& aut) 161 { 162 trival cp = aut->prop_complete(); 163 if (cp.is_known()) 164 return cp.is_true(); 165 unsigned ns = aut->num_states(); 166 for (unsigned src = 0; src < ns; ++src) 167 { 168 bdd available = bddtrue; 169 for (auto& t: aut->out(src)) 170 available -= t.cond; 171 if (available != bddfalse) 172 { 173 std::const_pointer_cast<twa_graph>(aut)->prop_complete(false); 174 return false; 175 } 176 } 177 // The empty automaton is not complete since it does not have an 178 // initial state. 179 bool res = ns > 0; 180 std::const_pointer_cast<twa_graph>(aut)->prop_complete(res); 181 return res; 182 } 183 184 namespace 185 { 186 static bool check_semi_determism(const const_twa_graph_ptr & aut,bool and_determinism)187 check_semi_determism(const const_twa_graph_ptr& aut, bool and_determinism) 188 { 189 trival sd = aut->prop_semi_deterministic(); 190 if (sd.is_known() && 191 (!and_determinism || aut->prop_universal().is_known())) 192 return sd.is_true(); 193 scc_info si(aut); 194 si.determine_unknown_acceptance(); 195 unsigned nscc = si.scc_count(); 196 assert(nscc); 197 std::vector<bool> reachable_from_acc(nscc); 198 bool semi_det = true; 199 do // iterator of SCCs in reverse topological order 200 { 201 --nscc; 202 if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc]) 203 { 204 for (unsigned succ: si.succ(nscc)) 205 reachable_from_acc[succ] = true; 206 for (unsigned src: si.states_of(nscc)) 207 { 208 bdd available = bddtrue; 209 for (auto& t: aut->out(src)) 210 if (!bdd_implies(t.cond, available)) 211 { 212 semi_det = false; 213 goto done; 214 } 215 else 216 { 217 available -= t.cond; 218 } 219 } 220 } 221 } 222 while (nscc); 223 done: 224 std::const_pointer_cast<twa_graph>(aut) 225 ->prop_semi_deterministic(semi_det); 226 if (semi_det && and_determinism) 227 { 228 bool det = true; 229 nscc = si.scc_count(); 230 do // iterator of SCCs in reverse topological order 231 { 232 --nscc; 233 if (!si.is_accepting_scc(nscc) && !reachable_from_acc[nscc]) 234 { 235 for (unsigned src: si.states_of(nscc)) 236 { 237 bdd available = bddtrue; 238 for (auto& t: aut->out(src)) 239 if (!bdd_implies(t.cond, available)) 240 { 241 det = false; 242 goto done2; 243 } 244 else 245 { 246 available -= t.cond; 247 } 248 } 249 } 250 } 251 while (nscc); 252 done2: 253 std::const_pointer_cast<twa_graph>(aut)->prop_universal(det); 254 } 255 return semi_det; 256 } 257 } 258 semidet_sccs(scc_info & si)259 std::vector<bool> semidet_sccs(scc_info& si) 260 { 261 const_twa_graph_ptr aut = si.get_aut(); 262 trival sd = aut->prop_semi_deterministic(); 263 if (sd.is_known() && sd.is_false()) 264 return std::vector<bool>(); 265 si.determine_unknown_acceptance(); 266 unsigned nscc = si.scc_count(); 267 assert(nscc); 268 std::vector<bool> reachable_from_acc(nscc); 269 std::vector<bool> res(nscc); 270 bool semi_det = true; 271 do // iterator of SCCs in reverse topological order 272 { 273 --nscc; 274 if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc]) 275 { 276 for (unsigned succ: si.succ(nscc)) 277 reachable_from_acc[succ] = true; 278 for (unsigned src: si.states_of(nscc)) 279 { 280 bdd available = bddtrue; 281 for (auto& t: aut->out(src)) 282 if (!bdd_implies(t.cond, available)) 283 { 284 semi_det = false; 285 goto done; 286 } 287 else 288 { 289 available -= t.cond; 290 } 291 } 292 res[nscc] = true; 293 } 294 } 295 while (nscc); 296 done: 297 if (!semi_det) 298 return std::vector<bool>(); 299 return res; 300 } 301 302 bool is_semi_deterministic(const const_twa_graph_ptr & aut)303 is_semi_deterministic(const const_twa_graph_ptr& aut) 304 { 305 return check_semi_determism(aut, false); 306 } 307 check_determinism(twa_graph_ptr aut)308 void check_determinism(twa_graph_ptr aut) 309 { 310 check_semi_determism(aut, true); 311 } 312 313 unsigned count_univbranch_states(const const_twa_graph_ptr & aut)314 count_univbranch_states(const const_twa_graph_ptr& aut) 315 { 316 if (aut->is_existential()) 317 return 0; 318 unsigned res = 0; 319 unsigned ns = aut->num_states(); 320 for (unsigned s = 0; s < ns; ++s) 321 for (auto& e: aut->out(s)) 322 if (aut->is_univ_dest(e)) 323 { 324 ++res; 325 break; 326 } 327 return res; 328 } 329 330 unsigned count_univbranch_edges(const const_twa_graph_ptr & aut)331 count_univbranch_edges(const const_twa_graph_ptr& aut) 332 { 333 if (aut->is_existential()) 334 return 0; 335 unsigned res = aut->is_univ_dest(aut->get_init_state_number()); 336 for (auto& e: aut->edges()) 337 if (aut->is_univ_dest(e)) 338 ++res; 339 return res; 340 } 341 342 } 343