Vaucanson 1.4
|
00001 // ltl_to_pair.hh: this file is part of the Vaucanson project. 00002 // 00003 // Vaucanson, a generic library for finite state machines. 00004 // 00005 // Copyright (C) 2008, 2009 The Vaucanson Group. 00006 // 00007 // This program is free software; you can redistribute it and/or 00008 // modify it under the terms of the GNU General Public License 00009 // as published by the Free Software Foundation; either version 2 00010 // of the License, or (at your option) any later version. 00011 // 00012 // The complete GNU General Public Licence Notice can be found as the 00013 // `COPYING' file in the root directory. 00014 // 00015 // The Vaucanson Group consists of people listed in the `AUTHORS' file. 00016 // 00017 #ifndef VCSN_ALGORITHMS_LTL_TO_PAIR_HH 00018 # define VCSN_ALGORITHMS_LTL_TO_PAIR_HH 00019 00020 # include <map> 00021 # include <set> 00022 # include <utility> 00023 # include <string> 00024 00025 # include <vaucanson/automata/concept/automata.hh> 00026 # include <vaucanson/automata/concept/transducer.hh> 00027 # include <vaucanson/algebra/concept/freemonoid_product.hh> 00028 # include <vaucanson/algebra/implementation/alphabets/alphabet_set.hh> 00029 # include <vaucanson/algebra/implementation/monoid/free_monoid.hh> 00030 00031 // Needed for the operator<< on pairs 00032 # include <vaucanson/algebra/implementation/letter/couple_letter.hh> 00033 00047 // INTERFACE: void ltl_to_pair(const Automaton& a, LtlToPair& b) { return vcsn::ltl_to_pair(*a, *b); } 00048 // INTERFACE: LtlToPair ltl_to_pair(const Automaton& a) { return vcsn::ltl_to_pair(*a); } 00049 00050 namespace vcsn 00051 { 00054 00055 00056 00057 00058 00059 // Helper to mute an FMP into its corresponding pair automaton. 00060 template <typename S, typename T> 00061 struct mute_ltl_to_pair 00062 { 00063 // The automaton type. 00064 typedef Element<S, T> automaton_t; 00065 00066 // The free monoid product type. 00067 typedef typename automaton_t::monoid_elt_t::set_t monoid_set_elt_t; 00068 00069 // The semiring type. 00070 typedef typename automaton_t::semiring_t semiring_t; 00071 00072 // The first alphabet type. 00073 typedef typename monoid_set_elt_t:: 00074 first_monoid_t::alphabet_t first_alphabet_t; 00075 00076 // The second alphabet type. 00077 typedef typename monoid_set_elt_t:: 00078 second_monoid_t::alphabet_t second_alphabet_t; 00079 00080 // The first letter type. 00081 typedef typename first_alphabet_t::set_t::letter_t first_letter_t; 00082 00083 // The second letter type. 00084 typedef typename second_alphabet_t::set_t::letter_t second_letter_t; 00085 00086 // The return letter type. 00087 typedef std::pair<first_letter_t, second_letter_t> ret_letter_t; 00088 00089 // The return alphabet type. 00090 00091 // 1 - structure 00092 typedef typename algebra::AlphabetSet<ret_letter_t> ret_alphabet_set_t; 00093 00094 // 2 - implementation 00095 typedef std::set<ret_letter_t> ret_alphabet_impl_t; 00096 00097 // 3 - element 00098 typedef Element<ret_alphabet_set_t, ret_alphabet_impl_t> 00099 ret_alphabet_t; 00100 00101 typedef algebra::FreeMonoid<ret_alphabet_t> ret_monoid_t; 00102 00103 typedef Element<ret_monoid_t, std::basic_string<ret_letter_t> > 00104 ret_monoid_elt_t; 00105 00106 // Helper to calculate the Cartesian product of two 00107 // alphabets: E = {(a,x)| a \in A, x \in B}. 00108 static ret_alphabet_t 00109 cartesian_product(const first_alphabet_t& A, 00110 const second_alphabet_t& B); 00111 00112 // The muted automaton type. 00113 00114 // 1 - structure 00115 typedef typename algebra:: 00116 mute_series_traits<typename automaton_t::series_set_t, 00117 typename automaton_t::semiring_t, 00118 algebra::FreeMonoid<ret_alphabet_t> >::ret 00119 ret_series_set_t; 00120 typedef Automata<ret_series_set_t, typename automaton_t::kind_t> ret_set_t; 00121 00122 // 2 - implementation 00123 typedef typename mute_graph_impl_monoid_traits<typename automaton_t:: 00124 value_t, typename ret_monoid_elt_t::value_t, ret_letter_t>::ret 00125 ret_impl_t; 00126 00127 // 3 - element 00128 typedef Element<ret_set_t, ret_impl_t> ret; 00129 00130 // Automaton "makers". 00131 static inline ret 00132 make_automaton(const ret_alphabet_t& A) 00133 { 00134 semiring_t semiring; 00135 ret_monoid_t freemonoid(A); 00136 typename ret::series_set_t series(semiring, freemonoid); 00137 return ret(Automata<typename ret::series_set_t, typename ret::kind_t>(series)); 00138 } 00139 00140 static ret 00141 make_automaton(const automaton_t&); 00142 00143 // Series converter. 00144 static typename ret::series_set_elt_t 00145 series_convert(const ret_series_set_t&, 00146 const typename automaton_t::series_set_elt_t&); 00147 }; 00148 00149 template <typename S, typename T> 00150 void 00151 ltl_to_pair(const Element<S, T>& ltl, 00152 typename mute_ltl_to_pair<S, T>::ret& res); 00153 00154 template <typename S, typename T> 00155 typename mute_ltl_to_pair<S, T>::ret 00156 ltl_to_pair(const Element<S, T>& ltl); 00157 00159 00162 } // ! vcsn 00163 00164 # if !defined VCSN_USE_INTERFACE_ONLY && !defined VCSN_USE_LIB 00165 # include <vaucanson/algorithms/ltl_to_pair.hxx> 00166 # endif // ! VCSN_USE_INTERFACE_ONLY 00167 00168 #endif // ! VCSN_ALGORITHMS_LTL_TO_PAIR_HH