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
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
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
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
77   is_deterministic(const const_twa_graph_ptr& aut)
78   {
79     return aut->is_existential() && is_universal(aut);
treyfer_crypt(uint8_t * pt,uint8_t * ct)80   }
81 
82   void
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
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 
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
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
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 
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
303   is_semi_deterministic(const const_twa_graph_ptr& aut)
304   {
305     return check_semi_determism(aut, false);
306   }
307 
308   void check_determinism(twa_graph_ptr aut)
309   {
310     check_semi_determism(aut, true);
311   }
312 
313   unsigned
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
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