1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2009-2010, 2012-2016, 2018-2019, 2021 Laboratoire de 3 // Recherche et Développement 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 <utility> 22 #include <algorithm> 23 #include <cassert> 24 #include <spot/tl/unabbrev.hh> 25 #include <spot/tl/nenoform.hh> 26 #include <spot/tl/contain.hh> 27 #include <spot/twaalgos/ltl2taa.hh> 28 29 namespace spot 30 { 31 namespace 32 { 33 /// \brief Recursively translate a formula into a TAA. 34 class ltl2taa_visitor final 35 { 36 public: ltl2taa_visitor(const taa_tgba_formula_ptr & res,language_containment_checker * lcc,bool refined=false,bool negated=false)37 ltl2taa_visitor(const taa_tgba_formula_ptr& res, 38 language_containment_checker* lcc, 39 bool refined = false, bool negated = false) 40 : res_(res), refined_(refined), negated_(negated), 41 lcc_(lcc), init_(), succ_() 42 { 43 } 44 45 taa_tgba_formula_ptr& result()46 result() 47 { 48 res_->set_init_state(init_); 49 return res_; 50 } 51 52 void visit(formula f)53 visit(formula f) 54 { 55 init_ = f; 56 switch (f.kind()) 57 { 58 case op::ff: 59 return; 60 case op::tt: 61 { 62 std::vector<formula> empty; 63 res_->create_transition(init_, empty); 64 succ_state ss = { empty, f, empty }; 65 succ_.emplace_back(ss); 66 return; 67 } 68 case op::eword: 69 SPOT_UNIMPLEMENTED(); 70 case op::ap: 71 { 72 res_->register_ap(f); 73 if (negated_) 74 f = formula::Not(f); 75 init_ = f; 76 std::vector<formula> empty; 77 taa_tgba::transition* t = res_->create_transition(init_, empty); 78 res_->add_condition(t, f); 79 succ_state ss = { empty, f, empty }; 80 succ_.emplace_back(ss); 81 return; 82 } 83 case op::X: 84 case op::strong_X: 85 { 86 ltl2taa_visitor v = recurse(f[0]); 87 std::vector<formula> dst; 88 std::vector<formula> a; 89 if (v.succ_.empty()) // Handle X(0) 90 return; 91 dst.emplace_back(v.init_); 92 res_->create_transition(init_, dst); 93 succ_state ss = { dst, formula::tt(), a }; 94 succ_.emplace_back(ss); 95 return; 96 } 97 case op::F: 98 case op::G: 99 SPOT_UNIMPLEMENTED(); // TBD 100 return; 101 case op::Not: 102 { 103 negated_ = true; 104 ltl2taa_visitor v = recurse(f[0]); 105 // Done in recurse 106 succ_ = v.succ_; 107 return; 108 } 109 case op::Closure: 110 case op::NegClosure: 111 case op::NegClosureMarked: 112 case op::Star: 113 case op::FStar: 114 case op::Xor: 115 case op::Implies: 116 case op::Equiv: 117 case op::UConcat: 118 case op::EConcat: 119 case op::EConcatMarked: 120 case op::Concat: 121 case op::Fusion: 122 case op::AndNLM: 123 case op::AndRat: 124 case op::OrRat: 125 case op::first_match: 126 SPOT_UNIMPLEMENTED(); 127 128 case op::U: 129 case op::W: 130 case op::R: 131 case op::M: 132 visit_binop(f); 133 return; 134 case op::And: 135 case op::Or: 136 visit_multop(f); 137 return; 138 } 139 } 140 141 void visit_binop(formula f)142 visit_binop(formula f) 143 { 144 ltl2taa_visitor v1 = recurse(f[0]); 145 ltl2taa_visitor v2 = recurse(f[1]); 146 147 std::vector<succ_state>::iterator i1; 148 std::vector<succ_state>::iterator i2; 149 taa_tgba::transition* t = nullptr; 150 bool contained = false; 151 bool strong = false; 152 153 switch (f.kind()) 154 { 155 case op::U: 156 strong = true; 157 SPOT_FALLTHROUGH; 158 case op::W: 159 if (refined_) 160 contained = lcc_->contained(f[0], f[1]); 161 for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) 162 { 163 // Refined rule 164 if (refined_ && contained) 165 i1->Q.erase 166 (remove(i1->Q.begin(), i1->Q.end(), v1.init_), i1->Q.end()); 167 168 i1->Q.emplace_back(init_); // Add the initial state 169 if (strong) 170 i1->acc.emplace_back(f[1]); 171 t = res_->create_transition(init_, i1->Q); 172 res_->add_condition(t, i1->condition); 173 if (strong) 174 res_->add_acceptance_condition(t, f[1]); 175 else 176 for (unsigned i = 0; i < i1->acc.size(); ++i) 177 res_->add_acceptance_condition(t, i1->acc[i]); 178 succ_.emplace_back(*i1); 179 } 180 for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) 181 { 182 t = res_->create_transition(init_, i2->Q); 183 res_->add_condition(t, i2->condition); 184 succ_.emplace_back(*i2); 185 } 186 return; 187 case op::M: // Strong Release 188 strong = true; 189 SPOT_FALLTHROUGH; 190 case op::R: // Weak Release 191 if (refined_) 192 contained = lcc_->contained(f[0], f[1]); 193 194 for (i2 = v2.succ_.begin(); i2 != v2.succ_.end(); ++i2) 195 { 196 for (i1 = v1.succ_.begin(); i1 != v1.succ_.end(); ++i1) 197 { 198 std::vector<formula> u; // Union 199 std::vector<formula> a; // Acceptance conditions 200 std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end())); 201 formula f = i1->condition; // Refined rule 202 if (!refined_ || !contained) 203 { 204 std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end())); 205 f = formula::And({f, i2->condition}); 206 } 207 t = res_->create_transition(init_, u); 208 res_->add_condition(t, f); 209 succ_state ss = { u, f, a }; 210 succ_.emplace_back(ss); 211 } 212 213 if (refined_) // Refined rule 214 i2->Q.erase 215 (remove(i2->Q.begin(), i2->Q.end(), v2.init_), i2->Q.end()); 216 217 218 i2->Q.emplace_back(init_); // Add the initial state 219 t = res_->create_transition(init_, i2->Q); 220 res_->add_condition(t, i2->condition); 221 222 if (strong) 223 { 224 i2->acc.emplace_back(f[0]); 225 res_->add_acceptance_condition(t, f[0]); 226 } 227 else if (refined_) 228 for (unsigned i = 0; i < i2->acc.size(); ++i) 229 res_->add_acceptance_condition(t, i2->acc[i]); 230 succ_.emplace_back(*i2); 231 } 232 return; 233 default: 234 SPOT_UNIMPLEMENTED(); 235 } 236 SPOT_UNREACHABLE(); 237 } 238 239 void visit_multop(formula f)240 visit_multop(formula f) 241 { 242 bool ok = true; 243 std::vector<ltl2taa_visitor> vs; 244 for (unsigned n = 0, s = f.size(); n < s; ++n) 245 { 246 vs.emplace_back(recurse(f[n])); 247 if (vs[n].succ_.empty()) // Handle 0 248 ok = false; 249 } 250 251 taa_tgba::transition* t = nullptr; 252 switch (f.kind()) 253 { 254 case op::And: 255 { 256 if (!ok) 257 return; 258 std::vector<succ_state> p = all_n_tuples(vs); 259 for (unsigned n = 0; n < p.size(); ++n) 260 { 261 if (refined_) 262 { 263 std::vector<formula> v; // All sub initial states. 264 sort(p[n].Q.begin(), p[n].Q.end()); 265 for (unsigned m = 0; m < f.size(); ++m) 266 { 267 if (!binary_search(p[n].Q.begin(), p[n].Q.end(), 268 vs[m].init_)) 269 break; 270 v.emplace_back(vs[m].init_); 271 } 272 273 if (v.size() == f.size()) 274 { 275 std::vector<formula> Q; 276 sort(v.begin(), v.end()); 277 for (unsigned m = 0; m < p[n].Q.size(); ++m) 278 if (!binary_search(v.begin(), v.end(), p[n].Q[m])) 279 Q.emplace_back(p[n].Q[m]); 280 Q.emplace_back(init_); 281 t = res_->create_transition(init_, Q); 282 res_->add_condition(t, p[n].condition); 283 for (unsigned i = 0; i < p[n].acc.size(); ++i) 284 res_->add_acceptance_condition(t, p[n].acc[i]); 285 succ_.emplace_back(p[n]); 286 continue; 287 } 288 } 289 t = res_->create_transition(init_, p[n].Q); 290 res_->add_condition(t, p[n].condition); 291 succ_.emplace_back(p[n]); 292 } 293 return; 294 } 295 case op::Or: 296 for (unsigned n = 0, s = f.size(); n < s; ++n) 297 for (auto i: vs[n].succ_) 298 { 299 t = res_->create_transition(init_, i.Q); 300 res_->add_condition(t, i.condition); 301 succ_.emplace_back(i); 302 } 303 return; 304 default: 305 SPOT_UNIMPLEMENTED(); 306 } 307 SPOT_UNREACHABLE(); 308 } 309 310 ltl2taa_visitor recurse(formula f)311 recurse(formula f) 312 { 313 ltl2taa_visitor v(res_, lcc_, refined_, negated_); 314 v.visit(f); 315 return v; 316 } 317 318 private: 319 taa_tgba_formula_ptr res_; 320 bool refined_; 321 bool negated_; 322 language_containment_checker* lcc_; 323 324 typedef std::insert_iterator<std::vector<formula>> ii; 325 326 struct succ_state 327 { 328 std::vector<formula> Q; // States 329 formula condition; 330 std::vector<formula> acc; 331 }; 332 333 formula init_; 334 std::vector<succ_state> succ_; 335 336 public: 337 std::vector<succ_state> all_n_tuples(const std::vector<ltl2taa_visitor> & vs)338 all_n_tuples(const std::vector<ltl2taa_visitor>& vs) 339 { 340 std::vector<succ_state> product; 341 342 std::vector<int> pos(vs.size()); 343 for (unsigned i = 0; i < vs.size(); ++i) 344 pos[i] = vs[i].succ_.size(); 345 346 // g++ (Debian 8.3.0-3) 8.3.0 in --coverage mode, 347 // and g++ 11.2.1-6 with -O3 -g -DNDEBUG 348 // both report a "potential null pointer dereference" on the 349 // while condition. 350 assert(pos.size() > 0); 351 SPOT_ASSUME(pos.data()); 352 while (pos[0] != 0) 353 { 354 std::vector<formula> u; // Union 355 std::vector<formula> a; // Acceptance conditions 356 formula f = formula::tt(); 357 for (unsigned i = 0; i < vs.size(); ++i) 358 { 359 if (vs[i].succ_.empty()) 360 continue; 361 const succ_state& ss(vs[i].succ_[pos[i] - 1]); 362 std::copy(ss.Q.begin(), ss.Q.end(), ii(u, u.end())); 363 f = formula::And({ss.condition, f}); 364 for (unsigned i = 0; i < ss.acc.size(); ++i) 365 { 366 formula g = ss.acc[i]; 367 a.emplace_back(g); 368 } 369 } 370 succ_state ss = { u, f, a }; 371 product.emplace_back(ss); 372 373 for (int i = vs.size() - 1; i >= 0; --i) 374 { 375 if (vs[i].succ_.empty()) 376 continue; 377 if (pos[i] > 1 || (i == 0 && pos[0] == 1)) 378 { 379 --pos[i]; 380 break; 381 } 382 else 383 pos[i] = vs[i].succ_.size(); 384 } 385 } 386 return product; 387 } 388 }; 389 } // anonymous 390 391 taa_tgba_formula_ptr ltl_to_taa(formula f,const bdd_dict_ptr & dict,bool refined_rules)392 ltl_to_taa(formula f, 393 const bdd_dict_ptr& dict, bool refined_rules) 394 { 395 // TODO: implement translation of F and G 396 auto f2 = negative_normal_form(unabbreviate(f, "^ieFG")); 397 auto res = make_taa_tgba_formula(dict); 398 language_containment_checker* lcc = 399 new language_containment_checker(make_bdd_dict(), 400 false, false, false, false); 401 ltl2taa_visitor v(res, lcc, refined_rules); 402 v.visit(f2); 403 auto taa = v.result(); 404 delete lcc; 405 taa->acc().set_generalized_buchi(); 406 return taa; 407 } 408 } 409