TaPAS  0.2
sataf.h
1 /*
2  * sataf.h -- SATAF library main header file
3  *
4  * This file is a part of the SATAF library.
5  *
6  * Copyright (C) 2010 CNRS UMR 5800 & Universit√© Bordeaux I (see AUTHORS file).
7  *
8  * This program is free software; you can redistribute it and/or modify
9  * it under the terms of the GNU General Public License as published by
10  * the Free Software Foundation; either version 2 of the License, or
11  * (at your option) any later version.
12  *
13  * This program is distributed in the hope that it will be useful,
14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16  * GNU General Public License for more details.
17  *
18  * You should have received a copy of the GNU General Public License
19  * along with this program; if not, write to the Free Software
20  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
21  * 02110-1301 USA
22  */
23 
43 #ifndef __SATAF_H__
44 # define __SATAF_H__
45 
46 # include <tapas-config.h>
47 
48 # include <ccl/ccl-list.h>
49 # include <ccl/ccl-hash.h>
50 # include <ccl/ccl-log.h>
51 
52 BEGIN_C_DECLS
53 
65 typedef struct sataf_mao_st sataf_mao;
66 
81 typedef struct sataf_msa_st sataf_msa;
90 typedef struct sataf_sa_st sataf_sa;
99 typedef struct sataf_ea_st sataf_ea;
110 {
118  const char *type;
119 
126  size_t (*size) (sataf_mao *self);
127 
136  void (*destroy) (sataf_mao *self);
137 
146  int (*no_cache) (sataf_mao *self);
147 
158  void (*is_root_of_scc) (sataf_mao *self, sataf_sa *sa, int q0);
159 
169  sataf_msa *(*simplify) (sataf_mao *self);
170 
180  uint32_t (*get_alphabet_size) (sataf_mao *self);
181 
188  char *(*to_string) (sataf_mao *self);
189 
202  sataf_mao *(*succ) (sataf_mao *self, uint32_t a);
203 
213  int (*is_final) (sataf_mao *self);
214 
227  int (*equals) (sataf_mao *self, sataf_mao *other);
228 
234  unsigned int (*hashcode) (sataf_mao *self);
235 
241  void (*to_dot) (ccl_log_type log, sataf_mao *self, const char **alphabet,
242  const char *graph_name, const char *graph_type);
243 };
254 typedef struct
255 {
261 
269 
274  uint32_t nb_states;
275 
279  uint32_t depth;
280  uint32_t to0;
281 
285  uint32_t refcount;
293 typedef void sataf_sa_transformer (sataf_ea *ea, sataf_sa **bind_sa,
294  uint32_t *bind_init);
297  /* --------------- */
298 
302 typedef struct sataf_mao_memorizer_st sataf_mao_memorizer;
303 
307 typedef struct {
308  sataf_mao *A;
309 } sataf_mao_memo;
310 
314 typedef void sataf_mao_memo_init_proc (sataf_mao_memo *m, void *data);
315 
319 typedef void sataf_mao_memo_clean_proc (sataf_mao_memo *m);
320 
321  /* --------------- */
322 
337 extern int
338 sataf_init (int msa_op_cache_size, int mao_sharing_cache_size,
339  int ea_ut_table_size, int ea_ut_max_fill_degree,
340  int sa_ut_table_size, int sa_ut_max_fill_degree,
341  int msa_ut_table_size, int msa_ut_max_fill_degree);
342 
346 extern void
347 sataf_terminate (void);
348 
354 extern void
355 sataf_log_statistics (ccl_log_type log);
356 
371 extern sataf_mao *
372 sataf_mao_create (size_t size, const sataf_mao_methods *methods);
373 
385 static inline sataf_mao *
387 
399 static inline void
401 
415 extern char *
417 
430 static inline const char *
432 
447 extern void
448 sataf_mao_is_root_of_scc (sataf_mao *self, sataf_sa *sa, int q0);
449 
461 extern int
463 
475 extern sataf_msa *
477 
485 extern uint32_t
487 
500 extern sataf_mao *
501 sataf_mao_succ (sataf_mao *self, uint32_t letter);
502 
511 extern int
513 
532 extern int
533 sataf_mao_equals (sataf_mao *self, sataf_mao *other);
534 
546 extern unsigned int
548 
562 extern void
563 sataf_mao_to_dot (ccl_log_type log, sataf_mao *self, const char **alphabet,
564  const char *graph_name, const char *graph_type);
565 
581 extern void
583  const char **alphabet, const char *graph_name,
584  const char *graph_type);
585 
594 extern sataf_mao *
595 sataf_mao_create_zero (uint32_t alphabet_size);
596 
604 extern sataf_mao *
605 sataf_mao_create_one (uint32_t alphabet_size);
606 
616 extern sataf_mao *
617 sataf_mao_create_epsilon (uint32_t alphabet_size);
618 
630 extern sataf_mao *
631 sataf_mao_create_letter (uint32_t alphabet_size, uint32_t a);
632 
641 extern sataf_mao *
642 sataf_mao_create_alphabet (uint32_t alphabet_size);
643 
669 extern sataf_mao *
670 sataf_mao_create_from_arrays (uint32_t nb_states, uint32_t alphabet_size,
671  uint32_t s0, const uint8_t *is_final,
672  const uint32_t *succ);
673 
687 extern sataf_mao *
689 
699 extern sataf_mao *
701 
713 extern sataf_mao *
715 
727 extern sataf_mao *
729 
740 extern sataf_mao *
742 
753 extern sataf_mao *
755 
767 extern sataf_mao *
769 
781 extern sataf_mao *
783 
793 extern sataf_mao *
795 
805 extern sataf_mao *
807 
808 
820 extern sataf_mao_memorizer *
821 sataf_mao_memorizer_create (size_t memo_size, sataf_mao_memo_init_proc *init,
822  void *init_data, sataf_mao_memo_clean_proc *clean);
823 
827 extern void
828 sataf_mao_memorizer_delete (sataf_mao_memorizer *M);
829 
833 extern sataf_mao_memo *
834 sataf_mao_memorizer_remind (sataf_mao_memorizer *M, sataf_mao *A);
835 
839 extern sataf_mao_memo *
840 sataf_mao_memorizer_succ (sataf_mao_memorizer *M, sataf_mao *A, int a);
841 
852 static inline uint32_t
853 sataf_ea_encode_succ_as_local_state (uint32_t index);
854 
855 
859 static inline uint32_t
860 sataf_ea_encode_succ_as_exit_state (uint32_t index);
861 
865 static inline uint32_t
866 sataf_ea_decode_succ_state (uint32_t index);
867 
871 static inline int
872 sataf_ea_is_exit_state (uint32_t successor);
873 
874 
878 static inline int
879 sataf_ea_is_local_state (uint32_t successor);
880 
886 static uint32_t
888 
894 static inline uint32_t
896 
902 static inline uint32_t
904 
913 static inline int
914 sataf_ea_is_final (sataf_ea *ea, uint32_t s);
915 
928 static inline uint32_t
929 sataf_ea_get_successor (sataf_ea *ea, uint32_t state, uint32_t a);
930 
936 static inline int
938 
944 static inline int
946 
947 
953 static inline int
955 
971 extern sataf_ea *
972 sataf_ea_create (uint32_t nb_states, uint32_t nb_exits,
973  uint32_t alphabet_size);
974 
987 extern sataf_ea *
989 
1018 extern sataf_ea *
1019 sataf_ea_create_with_arrays (uint32_t nb_states, uint32_t nb_exits,
1020  uint32_t alphabet_size, const uint8_t *is_final,
1021  const uint32_t *succ);
1022 
1032 extern sataf_ea *
1034 
1044 extern void
1046 
1067 extern void
1068 sataf_ea_set_successor (sataf_ea *ea, uint32_t src, uint32_t a, uint32_t tgt,
1069  int is_exit);
1070 
1080 static inline void
1081 sataf_ea_set_final (sataf_ea *ea, uint32_t s, int is_final);
1082 
1098 extern void
1100  const char **alphabet);
1101 
1117 extern sataf_ea *
1118 sataf_ea_minimize (sataf_ea *ea, uint32_t *h);
1119 
1133 extern sataf_ea *
1135 
1145 extern sataf_ea *
1146 sataf_ea_find (sataf_ea *ea);
1147 
1159 extern int
1160 sataf_ea_equals (sataf_ea *ea1, sataf_ea *ea2);
1161 
1172 extern unsigned int
1174 
1181 extern void
1183 
1197 extern sataf_sa *
1198 sataf_sa_create_one (uint32_t alphabet_size);
1199 
1207 extern sataf_sa *
1208 sataf_sa_create_zero (uint32_t alphabet_size);
1209 
1217 static inline sataf_sa *
1219 
1228 static inline void
1230 
1248 extern sataf_sa *
1249 sataf_sa_find_or_add (sataf_ea *ea, sataf_sa **bind_sa, uint32_t *bind_init);
1250 
1273 extern void
1274 sataf_sa_display_as_dot (sataf_sa *sa, ccl_log_type log, int marked_state,
1275  const char **alphabet, int with_info);
1276 
1289 extern void
1291 
1300 static inline int
1302 
1309 static inline uint32_t
1311 
1320 static inline int
1322 
1331 static inline int
1333 
1339 extern void
1341 
1342 extern void
1343 sataf_sa_exists_closure (sataf_ea *ea, sataf_sa **bind_sa,
1344  uint32_t *bind_init);
1345 
1346 extern void
1347 sataf_sa_forall_closure (sataf_ea *ea, sataf_sa **bind_sa,
1348  uint32_t *bind_init);
1349 /* @} */
1350 
1366 extern sataf_msa *
1367 sataf_msa_find_or_add (sataf_sa *sa, uint32_t initial);
1368 
1376 static inline uint32_t
1378 
1386 static inline sataf_sa *
1388 
1397 static inline sataf_sa *
1399 
1409 static inline sataf_msa *
1411 
1428 extern sataf_msa *
1429 sataf_msa_compute_with_transformer (sataf_mao *A, sataf_sa_transformer *T);
1430 
1438 extern sataf_mao *
1439 sataf_msa_to_mao (sataf_msa * msa);
1440 
1449 extern void
1451 
1460 extern void
1462 
1472 extern sataf_msa *
1473 sataf_msa_succ (sataf_msa *msa, uint32_t a);
1474 
1484 static inline int
1486 
1494 static inline uint32_t
1496 
1504 static inline sataf_msa *
1506 
1515 static inline void
1517 
1527 extern void
1529  const char **alphabet, int with_info);
1530 
1541 extern void
1543  const char **alphabet);
1544 
1552 static inline int
1554 
1562 static inline int
1564 
1573 static inline int
1575 
1583 extern int
1585 
1586 
1594 extern sataf_msa *
1595 sataf_msa_zero (uint32_t alphabet_size);
1596 
1600 # define sataf_msa_empty sataf_msa_zero
1601 
1609 extern sataf_msa *
1610 sataf_msa_one (uint32_t alphabet_size);
1611 
1615 # define sataf_msa_all sataf_msa_one
1616 
1623 extern sataf_msa *
1624 sataf_msa_epsilon (uint32_t alphabet_size);
1625 
1626 extern int
1627 sataf_msa_is_epsilon (sataf_msa *msa);
1628 
1637 extern sataf_msa *
1638 sataf_msa_letter (uint32_t alphabet_size, uint32_t a);
1639 
1646 extern sataf_msa *
1647 sataf_msa_alphabet (uint32_t alphabet_size);
1648 
1659 extern sataf_msa *
1661 
1669 extern sataf_msa *
1671 
1679 extern sataf_msa *
1680 sataf_msa_or (sataf_msa *a1, sataf_msa *a2);
1681 
1689 extern sataf_msa *
1690 sataf_msa_xor (sataf_msa *a1, sataf_msa *a2);
1691 
1699 extern sataf_msa *
1700 sataf_msa_and (sataf_msa *a1, sataf_msa *a2);
1701 
1709 extern sataf_msa *
1711 
1720 extern sataf_msa *
1722 
1730 extern sataf_msa *
1732 
1740 extern sataf_msa *
1742 
1750 extern sataf_msa *
1752 
1762 extern sataf_msa *
1763 sataf_msa_power (sataf_msa *a, int N);
1764 
1772 extern sataf_msa *
1774 
1775 extern sataf_msa *
1776 sataf_msa_change_acceptance (sataf_msa *a, ccl_hash *cond);
1777 
1793 extern int
1795 
1812 extern sataf_msa *
1814  const void *aux);
1815 
1832 extern void
1834  const void *aux, sataf_msa *R);
1835 
1838 # include <sataf/sataf-inline.h>
1839 
1840 extern int
1841 sataf_msa_are_complements (sataf_msa *a1, sataf_msa *a2);
1842 
1843 END_C_DECLS
1844 
1845 
1846 #endif /* ! __SATAF_H__ */
static int sataf_sa_is_one(sataf_sa *sa)
Return if sa is the shared automaton accepting any word.
sataf_msa * sataf_msa_equiv(sataf_msa *a1, sataf_msa *a2)
Boolean operation : equivalence.
unsigned int sataf_mao_hashcode(sataf_mao *self)
Compute an hashcode for this MAO.
sataf_msa * sataf_msa_epsilon(uint32_t alphabet_size)
Create the singleton containing the empty word.
sataf_msa * sataf_msa_letter(uint32_t alphabet_size, uint32_t a)
Create the singleton containing the letter a.
void sataf_ea_del_reference(sataf_ea *ea)
Decrement the counter of references of ea.
sataf_msa * sataf_msa_concat(sataf_msa *a1, sataf_msa *a2)
Concatenation of and .
static uint32_t sataf_ea_get_nb_states(sataf_ea *ea)
Return the number of local states of ea.
sataf_ea * sataf_ea_minimize(sataf_ea *ea, uint32_t *h)
Minimization of ea.
size_t(* size)(sataf_mao *self)
Returnsthe actual size of the object self.
Definition: sataf.h:126
char * sataf_mao_to_string(sataf_mao *self)
Translate the MAO into a human readable form.
void sataf_ea_ut_statistics(ccl_log_type log)
Display internal statistics about the use of EAs. In particular informations related to the unicity t...
static int sataf_sa_is_zero(sataf_sa *sa)
Return if sa is the shared automaton accepting no word.
void sataf_sa_display_as_dot(sataf_sa *sa, ccl_log_type log, int marked_state, const char **alphabet, int with_info)
Display the shared automaton sa in DOT file format.
sataf_mao * sataf_mao_create_epsilon(uint32_t alphabet_size)
Create a MAO recognizing the singleton for a reference alphabet of size alphabet_size.
const char * type
A constant string of characters indicating the type of the MAO.
Definition: sataf.h:118
Structure gathering the methods applied to a Marked Automaton Object.
Definition: sataf.h:109
static uint32_t sataf_sa_get_alphabet_size(sataf_sa *sa)
Return the size of the alphabet.
sataf_mao * sataf_mao_create_multi_and(ccl_list *operands)
Create a MAO encoding the intersection of a finite set of languages.
void sataf_mao_is_root_of_scc(sataf_mao *self, sataf_sa *sa, int q0)
Notify the MAO that it has been identified as the root of a SCC.
struct sataf_ea_st sataf_ea
Type for the data structure encoding Exit Automata.
Definition: sataf.h:99
sataf_mao * sataf_mao_create_one(uint32_t alphabet_size)
Create a MAO recognizing .
void sataf_ea_display_as_dot(sataf_ea *ea, ccl_log_type log, const char **alphabet)
Display the exit automaton in DOT graph format.
int sataf_ea_equals(sataf_ea *ea1, sataf_ea *ea2)
Check that ea1 and ea2 are equal.
Generic simple linked list.
sataf_msa * sataf_msa_star(sataf_msa *a)
Transitive closure of .
static uint32_t sataf_msa_get_alphabet_size(sataf_msa *msa)
Return the size of the alphabet.
static uint32_t sataf_msa_get_state(sataf_msa *msa)
Return the marked state defining msa.
static int sataf_msa_is_final(sataf_msa *msa)
Return if msa accepts the empty word.
int sataf_msa_is_included_in(sataf_msa *a1, sataf_msa *a2)
Check the inclusion of in .
static int sataf_ea_is_one(sataf_ea *ea)
Check if ea accepts any word.
void sataf_msa_display_as_dot(sataf_msa *msa, ccl_log_type log, const char **alphabet, int with_info)
Display the given MSA into the DOT file format.
static const char * sataf_mao_get_type(sataf_mao *self)
Return the type of the MAO self.
sataf_msa * sataf_msa_ite(sataf_msa *i, sataf_msa *t, sataf_msa *e)
Boolean operation : if-then-else.
sataf_mao * sataf_mao_create_and(sataf_mao *a1, sataf_mao *a2)
Create a MAO encoding the intersection of two languages.
static int sataf_ea_is_zero(sataf_ea *ea)
Check if ea accepts nothing.
sataf_sa * sataf_sa_create_one(uint32_t alphabet_size)
Create the unique SA recognizing all words on an alphabet of size alphabet_size.
sataf_mao * sataf_mao_succ(sataf_mao *self, uint32_t letter)
Return the successor MAO of self by letter.
sataf_msa * sataf_msa_succ(sataf_msa *msa, uint32_t a)
Return the successor of msa by the letter a.
sataf_ea * sataf_ea_create_with_arrays(uint32_t nb_states, uint32_t nb_exits, uint32_t alphabet_size, const uint8_t *is_final, const uint32_t *succ)
Build an EA with the transition function succ and the acceptance condition is_final.
static int sataf_msa_is_one(sataf_msa *msa)
Check if msa is the one recognizing everything.
sataf_mao * sataf_mao_create_equiv(sataf_mao *a1, sataf_mao *a2)
Create a MAO encoding .
sataf_mao * sataf_mao_create_exists(sataf_mao *a)
Create a MAO encoding the union of residues of .
sataf_ea * sataf_ea_complement(sataf_ea *ea)
Build an EA isomorph to ea up to the acceptance condition which is negated.
static sataf_mao * sataf_mao_add_reference(sataf_mao *a)
Increments the number of references to this MAP.
static uint32_t sataf_ea_encode_succ_as_exit_state(uint32_t index)
Encode the successor state index as an exit state.
static int sataf_ea_is_exit_state(uint32_t successor)
Check if the given successor corresponds to an exit state or not.
uint32_t(* get_alphabet_size)(sataf_mao *self)
Size of the reference alphabet.
Definition: sataf.h:180
sataf_mao * sataf_mao_create_letter(uint32_t alphabet_size, uint32_t a)
Create a MAO recognizing the singleton for a reference alphabet of size alphabet_size and one of it...
void(* destroy)(sataf_mao *self)
Free ressources allocated to this MAO.
Definition: sataf.h:136
void sataf_msa_log_info(ccl_log_type log, sataf_msa *msa)
Display on log quantitative informations about the structure of msa.
int sataf_mao_no_cache(sataf_mao *self)
Return if caching this object is interesting or not.
sataf_mao * sataf_mao_create_zero(uint32_t alphabet_size)
Create a MAO encoding the empty language for a reference alphabet of size alphabet_size.
sataf_ea * sataf_ea_create(uint32_t nb_states, uint32_t nb_exits, uint32_t alphabet_size)
Build an empty Exit Automaton data structure.
static sataf_msa * sataf_msa_add_reference(sataf_msa *msa)
Increment the counter of references of msa.
sataf_msa * sataf_msa_imply(sataf_msa *a1, sataf_msa *a2)
Boolean operation : implication.
static sataf_msa * sataf_msa_compute(sataf_mao *A)
Minimize, canonicalize and share the given MAO A.
struct sataf_mao_st sataf_mao
Type of a Marked Automaton Object (MAO).
Definition: sataf.h:65
static sataf_sa * sataf_msa_get_sa(sataf_msa *msa)
Return the shared automaton defining msa.
static int sataf_ea_is_final(sataf_ea *ea, uint32_t s)
Return a non null value is the local state s of ea is accepting or not.
static void sataf_ea_set_final(sataf_ea *ea, uint32_t s, int is_final)
Change the acceptance condition for the state s.
int sataf_msa_is_detectable(sataf_msa *a1, sataf_msa *a2, ccl_list *acc)
check if a1 is detectable in a2
sataf_mao * sataf_mao_create_or(sataf_mao *a1, sataf_mao *a2)
Create a MAO encoding the union of two languages.
void(* to_dot)(ccl_log_type log, sataf_mao *self, const char **alphabet, const char *graph_name, const char *graph_type)
Display the automaton in DOT file format.
Definition: sataf.h:241
static int sataf_ea_is_local_state(uint32_t successor)
Check if the given successor corresponds to a local state or not.
sataf_msa * sataf_msa_zero(uint32_t alphabet_size)
Return the empty language.
void(* is_root_of_scc)(sataf_mao *self, sataf_sa *sa, int q0)
Notify the MAO that it has been identified as the root of a SCC.
Definition: sataf.h:158
uint32_t refcount
The number of references to the MSA.
Definition: sataf.h:285
sataf_mao * sataf_mao_create_multi_or(ccl_list *operands)
Create a MAO encoding the union of a finite set of languages.
static int sataf_msa_is_zero_or_one(sataf_msa *msa)
Check if msa is one of the two elementary MSAs i.e. either the one recognizing everything or the one ...
int(* equals)(sataf_mao *self, sataf_mao *other)
Check if two instance are equal.
Definition: sataf.h:227
sataf_msa * sataf_msa_compute_with_transformer(sataf_mao *A, sataf_sa_transformer *T)
Minimize, canonicalize and share the given MAO A.
static int sataf_msa_is_zero(sataf_msa *msa)
Check if msa is the one recognizing nothing.
void sataf_mao_default_to_dot(ccl_log_type log, sataf_mao *self, const char **alphabet, const char *graph_name, const char *graph_type)
Display a MAO in DOT file format.
sataf_msa * sataf_msa_not(sataf_msa *a)
Boolean operation : complement.
void sataf_ea_set_successor(sataf_ea *ea, uint32_t src, uint32_t a, uint32_t tgt, int is_exit)
Change the successor of the given state.
static uint32_t sataf_ea_get_alphabet_size(sataf_ea *ea)
Return the size of this alphabet used by the exit automaton ea.
uint32_t nb_states
Total number of states. This is exactly the number of states of the minimal automaton.
Definition: sataf.h:274
sataf_sa * sataf_sa_find_or_add(sataf_ea *ea, sataf_sa **bind_sa, uint32_t *bind_init)
Look-up in the SA-unicity-table for a shared automaton defined by ea and the binding function (bind_s...
unsigned int(* hashcode)(sataf_mao *self)
Hashcode for the MAO self.
Definition: sataf.h:234
int(* is_final)(sataf_mao *self)
Indicates if self is accepting.
Definition: sataf.h:213
sataf_mao * sataf_mao_create_not(sataf_mao *a)
Create a MAO encoding the complement of a.
struct ccl_list_st ccl_list
Type of a generic list.
Definition: ccl-list.h:33
void sataf_msa_get_info(sataf_msa *msa, sataf_msa_info *info)
Retrieve quantitative informations related to msa.
sataf_mao * sataf_mao_create_forall(sataf_mao *a)
Create a MAO encoding the intersection of residues of .
static int sataf_ea_is_zero_or_one(sataf_ea *ea)
Check if ea recognizes anything or nothing.
sataf_mao * sataf_mao_create_alphabet(uint32_t alphabet_size)
Create a MAO recognizing the entire alphabet that has a size equal to alphabet_size.
sataf_msa * sataf_msa_power(sataf_msa *a, int N)
Exponentiation of .
sataf_msa * sataf_msa_or(sataf_msa *a1, sataf_msa *a2)
Boolean operation : disjunction.
uint32_t depth
The height of the MSA in the DAG of SCCs.
Definition: sataf.h:279
static void sataf_sa_del_reference(sataf_sa *sa)
Decrement the number of references to sa.
static sataf_sa * sataf_sa_add_reference(sataf_sa *sa)
Add one the counter of references to sa.
static int sataf_sa_is_zero_or_one(sataf_sa *sa)
Check if sa accepts nothing or accepts nothing.
int(* no_cache)(sataf_mao *self)
Caching this MAO is not relevant.
Definition: sataf.h:146
sataf_mao * sataf_mao_create_from_arrays(uint32_t nb_states, uint32_t alphabet_size, uint32_t s0, const uint8_t *is_final, const uint32_t *succ)
Create a MAO encoding an automaton given its transition function and its acceptance condition...
void sataf_sa_table_statistics(ccl_log_type log)
Display internal statistics about the use of SAs. In particular informations related to the unicity t...
static uint32_t sataf_ea_encode_succ_as_local_state(uint32_t index)
Encode the successor state index as a local state.
sataf_ea * sataf_ea_find_or_add(sataf_ea *ea)
Find or add ea in the unicity table.
sataf_mao * sataf_mao_create(size_t size, const sataf_mao_methods *methods)
Allocation and initialization of a MAO.
sataf_mao * sataf_msa_to_mao(sataf_msa *msa)
Create a MAO from msa.
static void sataf_mao_del_reference(sataf_mao *a)
Decrements the number of references to the given MAO.
sataf_msa * sataf_mao_simplify(sataf_mao *self)
Return the MSA corresponding to the MAO self if it is computable without the canonization algorithm...
static sataf_sa * sataf_msa_get_sa_no_ref(sataf_msa *msa)
Return the shared automaton defining msa but without incrementing its counter of references.
sataf_mao_memorizer * sataf_mao_memorizer_create(size_t memo_size, sataf_mao_memo_init_proc *init, void *init_data, sataf_mao_memo_clean_proc *clean)
Create a new memorizer.
enum ccl_log_type_enum ccl_log_type
Enum that indicates which kind of message has to be displayed. Each kind of message can be displayed ...
Definition: ccl-log.h:50
int sataf_mao_equals(sataf_mao *self, sataf_mao *other)
Check if two MAO are equal.
int sataf_mao_is_final(sataf_mao *self)
Return if the Marked Automaton is accepting.
uint32_t nb_exit_automata
Number of Exit Automata in this MSA. This is the number of non isomorphic strongly connected componen...
Definition: sataf.h:268
static uint32_t sataf_ea_get_successor(sataf_ea *ea, uint32_t state, uint32_t a)
Get the successor of state by the letter a.
Data structure gathering quantitative informations related to a MSA. This structure is filled by the ...
Definition: sataf.h:254
unsigned int sataf_ea_hashcode(sataf_ea *ea)
Hashcode of an EA The integer value is computed according to the transition function and the acceptan...
static uint32_t sataf_ea_decode_succ_state(uint32_t index)
Decode the successor state index.
sataf_msa * sataf_msa_and(sataf_msa *a1, sataf_msa *a2)
Boolean operation : conjunction.
static void sataf_msa_del_reference(sataf_msa *msa)
Decrement the counter of references of msa.
sataf_sa * sataf_sa_create_zero(uint32_t alphabet_size)
Create the unique SA recognizing no words on an alphabet of size alphabet_size.
void sataf_msa_display_as_olddot(sataf_msa *msa, ccl_log_type log, const char **alphabet)
Another function used to display the given MSA into the DOT file format.
A dynamic association table implemented by hashing.
sataf_mao * sataf_mao_create_imply(sataf_mao *a1, sataf_mao *a2)
Create a MAO encoding .
sataf_msa * sataf_msa_cache_get(sataf_msa *a1, sataf_msa *a2, sataf_msa *a3, const void *aux)
Look for a result in the cache over MSA operations.
sataf_msa * sataf_msa_find_or_add(sataf_sa *sa, uint32_t initial)
Getting the unique MSA defined by the couple (sa,initial).
sataf_msa * sataf_msa_exists(sataf_msa *a)
Create the MSA encoding the union of residues of .
struct ccl_hash_st ccl_hash
abstract type of an hash table.
Definition: ccl-hash.h:57
sataf_msa * sataf_msa_xor(sataf_msa *a1, sataf_msa *a2)
Boolean operation : mutual exclusion.
void sataf_msa_cache_put(sataf_msa *a1, sataf_msa *a2, sataf_msa *a3, const void *aux, sataf_msa *R)
Add en entry into the cache for MSA operations.
sataf_ea * sataf_ea_add_reference(sataf_ea *ea)
Increment the counter of references of ea.
sataf_msa * sataf_msa_forall(sataf_msa *a)
Create the MSA encoding the intersection of residues of .
void sataf_sa_display_scc_as_dot(sataf_sa *sa, ccl_log_type log)
Display the graph of SCCs composing the shared automaton sa.
sataf_msa * sataf_msa_one(uint32_t alphabet_size)
Compute .
uint32_t nb_shared_automata
Number of Shared Automata used by the MSA. This number represents the number of strongly connected co...
Definition: sataf.h:260
Message displayer.
sataf_msa * sataf_msa_alphabet(uint32_t alphabet_size)
Create the language equal to the alphabet of size alphabet_size.
sataf_mao * sataf_mao_create_ite(sataf_mao *i, sataf_mao *t, sataf_mao *e)
Create a MAO encoding the language if-then-else(i,t,e)
sataf_ea * sataf_ea_find(sataf_ea *ea)
Return the unique version of ea if it exists.
struct sataf_sa_st sataf_sa
Type for the data structure encoding Shared Automata.
Definition: sataf.h:90
struct sataf_msa_st sataf_msa
Type for the data structure encoding Marked Shared Automata.
Definition: sataf.h:81
uint32_t sataf_mao_get_alphabet_size(sataf_mao *self)
The size of the alphabet used by self.
void sataf_mao_to_dot(ccl_log_type log, sataf_mao *self, const char **alphabet, const char *graph_name, const char *graph_type)
Display a MAO in DOT file format.
static uint32_t sataf_ea_get_nb_exits(sataf_ea *ea)
Return the number of exit states of ea.