1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2017-2019 Laboratoire de Recherche et Développement de 3 // 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 <sstream> 22 #include <spot/tl/formula.hh> 23 #include <spot/tl/hierarchy.hh> 24 #include <spot/tl/nenoform.hh> 25 #include <spot/twaalgos/isdet.hh> 26 #include <spot/twaalgos/ltl2tgba_fm.hh> 27 #include <spot/twaalgos/minimize.hh> 28 #include <spot/twaalgos/postproc.hh> 29 #include <spot/twaalgos/remfin.hh> 30 #include <spot/twaalgos/sccfilter.hh> 31 #include <spot/twaalgos/strength.hh> 32 #include <spot/twaalgos/totgba.hh> 33 #include <spot/twaalgos/cobuchi.hh> 34 35 using namespace std::string_literals; 36 37 namespace spot 38 { 39 namespace 40 { 41 static bool cobuchi_realizable(spot::formula f,const const_twa_graph_ptr & aut)42 cobuchi_realizable(spot::formula f, 43 const const_twa_graph_ptr& aut) 44 { 45 // Find which algorithm must be performed between nsa_to_nca() and 46 // dnf_to_nca(). Throw an exception if none of them can be performed. 47 std::vector<acc_cond::rs_pair> pairs; 48 bool street_or_parity = aut->acc().is_streett_like(pairs) 49 || aut->acc().is_parity(); 50 if (!street_or_parity && !aut->get_acceptance().is_dnf()) 51 throw std::runtime_error("cobuchi_realizable() only works with " 52 "Streett-like, Parity or any " 53 "acceptance condition in DNF"); 54 55 // If !f is a DBA, it belongs to the recurrence class, which means 56 // f belongs to the persistence class (is cobuchi_realizable). 57 twa_graph_ptr not_aut = ltl_to_tgba_fm(formula::Not(f), aut->get_dict()); 58 not_aut = scc_filter(not_aut); 59 if (is_universal(not_aut)) 60 return true; 61 62 // Checks if f is cobuchi_realizable. 63 twa_graph_ptr cobuchi = street_or_parity ? nsa_to_nca(aut) 64 : dnf_to_nca(aut); 65 return !cobuchi->intersects(not_aut); 66 } 67 invalid_spot_pr_check()68 [[noreturn]] static void invalid_spot_pr_check() 69 { 70 throw std::runtime_error("invalid value for SPOT_PR_CHECK " 71 "(should be 1, 2, or 3)"); 72 } 73 74 static prcheck algo_to_perform(bool is_persistence,bool aut_given)75 algo_to_perform(bool is_persistence, bool aut_given) 76 { 77 static unsigned value = [&]() 78 { 79 int val; 80 try 81 { 82 auto s = getenv("SPOT_PR_CHECK"); 83 val = s ? std::stoi(s) : 0; 84 } 85 catch (const std::exception& e) 86 { 87 invalid_spot_pr_check(); 88 } 89 if (val < 0 || val > 3) 90 invalid_spot_pr_check(); 91 return val; 92 }(); 93 switch (value) 94 { 95 case 0: 96 if (aut_given && !is_persistence) 97 return prcheck::via_Parity; 98 else 99 return prcheck::via_CoBuchi; 100 case 1: 101 return prcheck::via_CoBuchi; 102 case 2: 103 return prcheck::via_Rabin; 104 case 3: 105 return prcheck::via_Parity; 106 default: 107 SPOT_UNREACHABLE(); 108 } 109 SPOT_UNREACHABLE(); 110 return prcheck::via_Parity; 111 } 112 113 static bool detbuchi_realizable(const twa_graph_ptr & aut)114 detbuchi_realizable(const twa_graph_ptr& aut) 115 { 116 if (is_universal(aut)) 117 return true; 118 119 bool want_old = algo_to_perform(false, true) == prcheck::via_Rabin; 120 if (want_old) 121 { 122 // if aut is a non-deterministic TGBA, we do 123 // TGBA->DPA->DRA->(D?)BA. The conversion from DRA to 124 // BA will preserve determinism if possible. 125 spot::postprocessor p; 126 p.set_type(spot::postprocessor::Generic); 127 p.set_pref(spot::postprocessor::Deterministic); 128 p.set_level(spot::postprocessor::Low); 129 auto dpa = p.run(aut); 130 if (dpa->acc().is_generalized_buchi()) 131 { 132 assert(is_deterministic(dpa)); 133 return true; 134 } 135 else 136 { 137 auto dra = to_generalized_rabin(dpa); 138 return rabin_is_buchi_realizable(dra); 139 } 140 } 141 // Converting reduce_parity() will produce a Büchi automaton (or 142 // an automaton with "t" or "f" acceptance) if the parity 143 // automaton is DBA-realizable. 144 spot::postprocessor p; 145 p.set_type(spot::postprocessor::Parity); 146 p.set_pref(spot::postprocessor::Deterministic); 147 p.set_level(spot::postprocessor::Low); 148 auto dpa = p.run(aut); 149 return dpa->acc().is_f() || dpa->acc().is_generalized_buchi(); 150 } 151 } 152 153 bool is_persistence(formula f,twa_graph_ptr aut,prcheck algo)154 is_persistence(formula f, twa_graph_ptr aut, prcheck algo) 155 { 156 if (f.is_syntactic_persistence()) 157 return true; 158 159 // Perform a quick simplification of the formula taking into account the 160 // following simplification's parameters: basics, synt_impl, event_univ. 161 spot::tl_simplifier simpl(spot::tl_simplifier_options(true, true, true)); 162 f = simpl.simplify(f); 163 if (f.is_syntactic_persistence()) 164 return true; 165 166 if (algo == prcheck::Auto) 167 algo = algo_to_perform(true, aut != nullptr); 168 169 switch (algo) 170 { 171 case prcheck::via_CoBuchi: 172 return cobuchi_realizable(f, aut ? aut : 173 ltl_to_tgba_fm(f, make_bdd_dict(), true)); 174 175 case prcheck::via_Rabin: 176 case prcheck::via_Parity: 177 return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f), 178 make_bdd_dict(), true)); 179 180 case prcheck::Auto: 181 SPOT_UNREACHABLE(); 182 } 183 184 SPOT_UNREACHABLE(); 185 } 186 187 bool is_recurrence(formula f,twa_graph_ptr aut,prcheck algo)188 is_recurrence(formula f, twa_graph_ptr aut, prcheck algo) 189 { 190 if (f.is_syntactic_recurrence()) 191 return true; 192 193 // Perform a quick simplification of the formula taking into account the 194 // following simplification's parameters: basics, synt_impl, event_univ. 195 spot::tl_simplifier simpl(spot::tl_simplifier_options(true, true, true)); 196 f = simpl.simplify(f); 197 if (f.is_syntactic_recurrence()) 198 return true; 199 200 if (algo == prcheck::Auto) 201 algo = algo_to_perform(true, aut != nullptr); 202 203 switch (algo) 204 { 205 case prcheck::via_CoBuchi: 206 return cobuchi_realizable(formula::Not(f), 207 ltl_to_tgba_fm(formula::Not(f), 208 make_bdd_dict(), true)); 209 210 case prcheck::via_Rabin: 211 case prcheck::via_Parity: 212 return detbuchi_realizable(aut ? aut : 213 ltl_to_tgba_fm(f, make_bdd_dict(), true)); 214 215 case prcheck::Auto: 216 SPOT_UNREACHABLE(); 217 } 218 219 SPOT_UNREACHABLE(); 220 } 221 222 invalid_spot_o_check()223 [[noreturn]] static void invalid_spot_o_check() 224 { 225 throw std::runtime_error("invalid value for SPOT_O_CHECK " 226 "(should be 1, 2, or 3)"); 227 } 228 229 // This private function is defined in minimize.cc for technical 230 // reasons. 231 SPOT_LOCAL bool is_wdba_realizable(formula f, twa_graph_ptr aut = nullptr); 232 233 bool is_obligation(formula f,twa_graph_ptr aut,ocheck algo)234 is_obligation(formula f, twa_graph_ptr aut, ocheck algo) 235 { 236 if (algo == ocheck::Auto) 237 { 238 static ocheck env_algo = []() 239 { 240 int val; 241 try 242 { 243 auto s = getenv("SPOT_O_CHECK"); 244 val = s ? std::stoi(s) : 0; 245 } 246 catch (const std::exception& e) 247 { 248 invalid_spot_o_check(); 249 } 250 if (val == 0) 251 return ocheck::via_WDBA; 252 else if (val == 1) 253 return ocheck::via_CoBuchi; 254 else if (val == 2) 255 return ocheck::via_Rabin; 256 else if (val == 3) 257 return ocheck::via_WDBA; 258 else 259 invalid_spot_o_check(); 260 }(); 261 algo = env_algo; 262 } 263 switch (algo) 264 { 265 case ocheck::via_WDBA: 266 return is_wdba_realizable(f, aut); 267 case ocheck::via_CoBuchi: 268 return (is_persistence(f, aut, prcheck::via_CoBuchi) 269 && is_recurrence(f, aut, prcheck::via_CoBuchi)); 270 case ocheck::via_Rabin: 271 return (is_persistence(f, aut, prcheck::via_Rabin) 272 && is_recurrence(f, aut, prcheck::via_Rabin)); 273 case ocheck::Auto: 274 SPOT_UNREACHABLE(); 275 } 276 SPOT_UNREACHABLE(); 277 } 278 279 mp_class(formula f)280 char mp_class(formula f) 281 { 282 if (f.is_syntactic_safety() && f.is_syntactic_guarantee()) 283 return 'B'; 284 auto dict = make_bdd_dict(); 285 auto aut = ltl_to_tgba_fm(f, dict, true); 286 auto min = minimize_obligation(aut, f); 287 if (aut != min) // An obligation. 288 { 289 scc_info si(min); 290 // The minimba WDBA can have some trivial accepting SCCs 291 // that we should ignore in is_terminal_automaton(). 292 bool g = is_terminal_automaton(min, &si, true); 293 bool s = is_safety_automaton(min, &si); 294 if (g) 295 return s ? 'B' : 'G'; 296 else 297 return s ? 'S' : 'O'; 298 } 299 // Not an obligation. Could by 'P', 'R', or 'T'. 300 if (is_recurrence(f, aut)) 301 return 'R'; 302 if (is_persistence(f, aut)) 303 return 'P'; 304 return 'T'; 305 } 306 mp_class(formula f,const char * opt)307 std::string mp_class(formula f, const char* opt) 308 { 309 return mp_class(mp_class(f), opt); 310 } 311 mp_class(char mpc,const char * opt)312 std::string mp_class(char mpc, const char* opt) 313 { 314 bool verbose = false; 315 bool wide = false; 316 if (opt) 317 for (;;) 318 switch (int o = *opt++) 319 { 320 case 'v': 321 verbose = true; 322 break; 323 case 'w': 324 wide = true; 325 break; 326 case ' ': 327 case '\t': 328 case '\n': 329 case ',': 330 break; 331 case '\0': 332 case ']': 333 goto break2; 334 default: 335 { 336 std::ostringstream err; 337 err << "unknown option '" << o << "' for mp_class()"; 338 throw std::runtime_error(err.str()); 339 } 340 } 341 break2: 342 std::string c(1, mpc); 343 if (wide) 344 { 345 switch (mpc) 346 { 347 case 'B': 348 c = "GSOPRT"; 349 break; 350 case 'G': 351 c = "GOPRT"; 352 break; 353 case 'S': 354 c = "SOPRT"; 355 break; 356 case 'O': 357 c = "OPRT"; 358 break; 359 case 'P': 360 c = "PT"; 361 break; 362 case 'R': 363 c = "RT"; 364 break; 365 case 'T': 366 break; 367 default: 368 throw std::runtime_error("mp_class() called with unknown class"); 369 } 370 } 371 if (!verbose) 372 return c; 373 374 std::ostringstream os; 375 bool first = true; 376 for (char ch: c) 377 { 378 if (first) 379 first = false; 380 else 381 os << ' '; 382 switch (ch) 383 { 384 case 'B': 385 os << "guarantee safety"; 386 break; 387 case 'G': 388 os << "guarantee"; 389 break; 390 case 'S': 391 os << "safety"; 392 break; 393 case 'O': 394 os << "obligation"; 395 break; 396 case 'P': 397 os << "persistence"; 398 break; 399 case 'R': 400 os << "recurrence"; 401 break; 402 case 'T': 403 os << "reactivity"; 404 break; 405 } 406 } 407 return os.str(); 408 } 409 nesting_depth(formula f,op oper)410 unsigned nesting_depth(formula f, op oper) 411 { 412 unsigned max_depth = 0; 413 for (formula child: f) 414 max_depth = std::max(max_depth, nesting_depth(child, oper)); 415 return max_depth + f.is(oper); 416 } 417 nesting_depth(formula f,const op * begin,const op * end)418 unsigned nesting_depth(formula f, const op* begin, const op* end) 419 { 420 unsigned max_depth = 0; 421 for (formula child: f) 422 max_depth = std::max(max_depth, nesting_depth(child, begin, end)); 423 bool matched = std::find(begin, end, f.kind()) != end; 424 return max_depth + matched; 425 } 426 nesting_depth(formula f,const char * opers)427 unsigned nesting_depth(formula f, const char* opers) 428 { 429 bool want_nnf = false; 430 std::vector<op> v; 431 for (;;) 432 switch (char c = *opers++) 433 { 434 case '~': 435 want_nnf = true; 436 break; 437 case '!': 438 v.push_back(op::Not); 439 break; 440 case '&': 441 v.push_back(op::And); 442 break; 443 case '|': 444 v.push_back(op::Or); 445 break; 446 case 'e': 447 v.push_back(op::Equiv); 448 break; 449 case 'F': 450 v.push_back(op::F); 451 break; 452 case 'G': 453 v.push_back(op::G); 454 break; 455 case 'i': 456 v.push_back(op::Implies); 457 break; 458 case 'M': 459 v.push_back(op::M); 460 break; 461 case 'R': 462 v.push_back(op::R); 463 break; 464 case 'U': 465 v.push_back(op::U); 466 break; 467 case 'W': 468 v.push_back(op::W); 469 break; 470 case 'X': 471 v.push_back(op::X); 472 break; 473 case '\0': 474 case ']': 475 goto break2; 476 default: 477 throw std::runtime_error 478 ("nesting_depth(): unknown operator '"s + c + '\''); 479 } 480 break2: 481 if (want_nnf) 482 f = negative_normal_form(f); 483 const op* vd = v.data(); 484 return nesting_depth(f, vd, vd + v.size()); 485 } 486 is_liveness(formula f)487 bool is_liveness(formula f) 488 { 489 return is_liveness_automaton(ltl_to_tgba_fm(f, spot::make_bdd_dict())); 490 } 491 } 492