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