Awali
Another Weighted Automata library
universal.hh
Go to the documentation of this file.
1 // This file is part of Awali.
2 // Copyright 2016-2022 Sylvain Lombardy, Victor Marsault, Jacques Sakarovitch
3 //
4 // Awali is a free software: you can redistribute it and/or modify
5 // it under the terms of the GNU General Public License as published by
6 // the Free Software Foundation, either version 3 of the License, or
7 // (at your option) any later version.
8 //
9 // This program is distributed in the hope that it will be useful,
10 // but WITHOUT ANY WARRANTY; without even the implied warranty of
11 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 // GNU General Public License for more details.
13 //
14 // You should have received a copy of the GNU General Public License
15 // along with this program. If not, see <http://www.gnu.org/licenses/>.
16 
17 #ifndef AWALI_ALGOS_UNIVERSAL_HH
18 # define AWALI_ALGOS_UNIVERSAL_HH
19 
20 # include <map>
21 
22 #include <awali/sttc/misc/set.hh>
25 #include <awali/sttc/weightset/fwd.hh> // b
26 
27 namespace awali { namespace sttc {
28 
29  namespace internal
30  {
32  template <typename Aut>
34  {
35  public:
36  static_assert(labelset_t_of<Aut>::is_free(),
37  "requires free labelset");
38  static_assert(std::is_same<weightset_t_of<Aut>, b>::value,
39  "requires Boolean weights");
40 
41  using automaton_t = Aut;
42  using state_set_t = std::set<state_t>;
43  using pstate_t = std::set<state_set_t>;
44  using map_t = std::map<state_t, state_set_t>;
45 
47  automaton_t operator()(const Aut& automaton)
48  {
49  if (!is_deterministic(automaton))
50  return work_(determinize(automaton,false));
51  else if (!is_complete(automaton))
52  return work_(complete(automaton));
53  else
54  return work_(automaton);
55  }
56 
57  private:
61  automaton_t work_(const automaton_t& aut)
62  {
63  // The initial state of automaton.
64  state_t i = aut->dst_of(aut->initial_transitions().front());
65 
66  // compute the co-determinized of the minimal automaton
67  // and retrieve the origin of each state.
68  const auto transposed = transpose(aut);
69  auto codet = determinize(transposed);
70  auto h=codet->history();
71  map_t origin = dynamic_cast<partition_history<automaton_t>*>(h.get())->origins();
72 
73  // the 'origin' is a map from co_det's state_t to
74  // minimal's state_set_t.
75  // let 'transp_states' be the image of 'origin'.
76  pstate_t transp_states = image(origin);
77 
78  // the universal automaton's state set is its intersection closure.
79  pstate_t univers_states(intersection_closure(transp_states));
80 
81  // The universal automaton.
82  automaton_t res = make_shared_ptr<automaton_t>(aut->context());
83 
84  // The final states of aut.
85  std::set<state_t> automaton_finals;
86  for (auto t: aut->final_transitions())
87  automaton_finals.insert(aut->src_of(t));
88 
89  // we have to save the state set associated to each automaton.
90  map_t subset_label;
91 
92  // X = univers_states \ {}.
93  for (const auto s: univers_states)
94  if (!s.empty())
95  {
96  state_t new_s = res->add_state();
97  subset_label[new_s] = s;
98  // J = { X | i in X }
99  if (has(s, i))
100  res->set_initial(new_s);
101  // U = { X | X \subset T }
102  if (subset(s, automaton_finals))
103  res->set_final(new_s);
104  }
105 
106  // Finally, the transition set.
107  for (const auto x: res->states())
108  for (const auto y: res->states())
109  for (const auto a: *res->labelset())
110  {
111  bool cont = false;
112  state_set_t delta_ret;
113  for (auto s: subset_label[x])
114  {
115  bool empty = true;
116  for (auto t: aut->out(s, a))
117  {
118  empty = false;
119  delta_ret.insert(aut->dst_of(t));
120  }
121  if (empty)
122  {
123  cont = true;
124  break;
125  }
126  }
127  // case 1: \exists p \in X, p.a = {}
128  if (cont)
129  continue;
130  // case 2: X.a \subset Y?
131  if (subset(delta_ret, subset_label[y]))
132  res->new_transition(x, y, a);
133  }
134  return res;
135  }
136  };
137  }
138 
139  template <class Aut>
140  inline
141  Aut
142  universal(const Aut& a)
143  {
145  return universal(a);
146  }
147 
148 }}//end of ns awali::stc
149 
150 #endif // !AWALI_ALGOS_UNIVERSAL_HH
The Boolean semring.
Definition: b.hh:38
Functor for universal.
Definition: universal.hh:34
Aut automaton_t
Definition: universal.hh:41
std::map< state_t, state_set_t > map_t
Definition: universal.hh:44
std::set< state_set_t > pstate_t
Definition: universal.hh:43
std::set< state_t > state_set_t
Definition: universal.hh:42
automaton_t operator()(const Aut &automaton)
The universal automaton of automaton.
Definition: universal.hh:47
specialisation of history_base
Definition: partition_history.hh:43
json_ast_t empty()
Builds an empty json_ast_t.
Definition: json_ast.hh:33
static constexpr TOP< void > value
Definition: priority.hh:93
bool subset(const Container1 &set1, const Container2 &set2) ATTRIBUTE_PURE
Whether set1 ⊆ set2.
Definition: set.hxx:105
bool has(const std::map< Key, Value, Compare, Alloc > &s, const Key &e)
Definition: map.hh:53
std::set< typename std::map< Key, Value, Comp, Alloc >::mapped_type > image(const std::map< Key, Value, Comp, Alloc > &m)
The set of values of a map.
Definition: set.hxx:33
bool is_deterministic(const Aut &aut, state_t s)
Whether state s is deterministic in aut.
Definition: is_deterministic.hxx:48
std::set< std::set< T, Compare, Alloc > > intersection_closure(std::set< std::set< T, Compare, Alloc >> pset)
The set of all the intersections of the sets in pset.
auto complete(const Aut &aut, bool keep_history=true) -> decltype(copy(aut, keep_history))
Completion of a deterministic automaton.
Definition: complete.hh:90
bool is_complete(const Aut &aut)
Whether aut is complete.
Definition: is_complete.hh:28
Aut universal(const Aut &a)
Definition: universal.hh:142
typename internal::labelset_t_of_impl< internal::base_t< ValueSet > >::type labelset_t_of
Helper to retrieve the type of the labelset of a value set.
Definition: traits.hh:76
auto determinize(const Aut &a, bool keep_history=true) -> mutable_automaton< context_t_of< Aut >>
Determinization of the automaton.
Definition: determinize.hh:41
AutOut transpose(Aut &aut, bool keep_history=true)
Definition: transpose.hh:79
typename internal::weightset_t_of_impl< internal::base_t< ValueSet > >::type weightset_t_of
Helper to retrieve the type of the weightset of a value set.
Definition: traits.hh:86
Main namespace of Awali.
Definition: ato.hh:22
unsigned state_t
Definition: types.hh:21