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