1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2016-2018 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 <numeric>
22 #include <spot/twa/twa.hh>
23 #include <spot/twaalgos/dualize.hh>
24 #include <spot/twaalgos/isdet.hh>
25 #include <spot/twaalgos/langmap.hh>
26 #include <spot/twaalgos/remfin.hh>
27 
28 namespace spot
29 {
30   std::vector<unsigned>
language_map(const const_twa_graph_ptr & aut)31   language_map(const const_twa_graph_ptr& aut)
32   {
33     if (!is_deterministic(aut))
34       throw std::runtime_error(
35           "language_map only works with deterministic automata");
36 
37     unsigned n_states = aut->num_states();
38     std::vector<unsigned> res(n_states);
39     std::iota(std::begin(res), std::end(res), 0);
40 
41     std::vector<twa_graph_ptr> alt_init_st_auts(n_states);
42     std::vector<twa_graph_ptr> compl_alt_init_st_auts(n_states);
43 
44     // Prepare all automata needed.
45     for (unsigned i = 0; i < n_states; ++i)
46       {
47         twa_graph_ptr c = make_twa_graph(aut, twa::prop_set::all());
48         assert(c); // for some reason g++ 7.3 thinks this could be null
49         c->set_init_state(i);
50         alt_init_st_auts[i] = c;
51         compl_alt_init_st_auts[i] = remove_fin(dualize(c));
52       }
53 
54     for (unsigned i = 1; i < n_states; ++i)
55       for (unsigned j = 0; j < i; ++j)
56         {
57           if (res[j] != j)
58             continue;
59 
60           if (!alt_init_st_auts[i]->intersects(compl_alt_init_st_auts[j])
61               && (!compl_alt_init_st_auts[i]->intersects(alt_init_st_auts[j])))
62             {
63               res[i] = res[j];
64               break;
65             }
66         }
67 
68     return res;
69   }
70 
highlight_languages(twa_graph_ptr & aut)71   void highlight_languages(twa_graph_ptr& aut)
72   {
73     std::vector<unsigned> lang = language_map(aut);
74     unsigned lang_sz = lang.size();
75     std::vector<unsigned> cnt(lang_sz, 0);
76     for (unsigned v: lang)
77       {
78         assert(v < lang_sz);
79         ++cnt[v];
80       }
81 
82     unsigned color = 0;
83     auto hs = new std::map<unsigned, unsigned>;
84     aut->set_named_prop("highlight-states", hs);
85 
86     assert(lang_sz == aut->num_states());
87 
88     // Give a unique color number to each state that has not a unique
89     // language.  This assumes that lang[i] <= i, as guaranteed by
90     // language_map.
91     for (unsigned i = 0; i < lang_sz; ++i)
92       {
93         unsigned v = lang[i];
94         if (cnt[v] > 1)
95           {
96             if (v == i)
97               lang[i] = color++;
98             else
99               assert(v < i);
100             (*hs)[i] = lang[v];
101           }
102       }
103   }
104 }
105