TaPAS  0.2
Data Structures | Macros | Typedefs | Functions
Marked Shared Automata

Data Structures

struct  sataf_msa_info
 Data structure gathering quantitative informations related to a MSA. This structure is filled by the function sataf_msa_get_info. More...
 

Macros

#define sataf_msa_empty   sataf_msa_zero
 Alias for the sataf_msa_zero function.
 
#define sataf_msa_all   sataf_msa_one
 Alias for the sataf_msa_one function.
 

Typedefs

typedef struct sataf_msa_st sataf_msa
 Type for the data structure encoding Marked Shared Automata.
 

Functions

sataf_msasataf_msa_find_or_add (sataf_sa *sa, uint32_t initial)
 Getting the unique MSA defined by the couple (sa,initial). More...
 
static uint32_t sataf_msa_get_state (sataf_msa *msa)
 Return the marked state defining msa. More...
 
static sataf_sasataf_msa_get_sa (sataf_msa *msa)
 Return the shared automaton defining msa. More...
 
static sataf_sasataf_msa_get_sa_no_ref (sataf_msa *msa)
 Return the shared automaton defining msa but without incrementing its counter of references. More...
 
static sataf_msasataf_msa_compute (sataf_mao *A)
 Minimize, canonicalize and share the given MAO A. More...
 
sataf_msasataf_msa_compute_with_transformer (sataf_mao *A, sataf_sa_transformer *T)
 Minimize, canonicalize and share the given MAO A. More...
 
sataf_maosataf_msa_to_mao (sataf_msa *msa)
 Create a MAO from msa. More...
 
void sataf_msa_log_info (ccl_log_type log, sataf_msa *msa)
 Display on log quantitative informations about the structure of msa. More...
 
void sataf_msa_get_info (sataf_msa *msa, sataf_msa_info *info)
 Retrieve quantitative informations related to msa. More...
 
sataf_msasataf_msa_succ (sataf_msa *msa, uint32_t a)
 Return the successor of msa by the letter a. More...
 
static int sataf_msa_is_final (sataf_msa *msa)
 Return if msa accepts the empty word. More...
 
static uint32_t sataf_msa_get_alphabet_size (sataf_msa *msa)
 Return the size of the alphabet. More...
 
static sataf_msasataf_msa_add_reference (sataf_msa *msa)
 Increment the counter of references of msa. More...
 
static void sataf_msa_del_reference (sataf_msa *msa)
 Decrement the counter of references of msa. More...
 
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. More...
 
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. More...
 
static int sataf_msa_is_zero (sataf_msa *msa)
 Check if msa is the one recognizing nothing. More...
 
static int sataf_msa_is_one (sataf_msa *msa)
 Check if msa is the one recognizing everything. More...
 
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 recognizing nothing. More...
 
int sataf_msa_is_included_in (sataf_msa *a1, sataf_msa *a2)
 Check the inclusion of $L_{a_1}$ in $L_{a_2}$. More...
 
sataf_msasataf_msa_zero (uint32_t alphabet_size)
 Return the empty language. More...
 
sataf_msasataf_msa_one (uint32_t alphabet_size)
 Compute $\Sigma^\star$. More...
 
sataf_msasataf_msa_epsilon (uint32_t alphabet_size)
 Create the singleton containing the empty word. More...
 
sataf_msasataf_msa_letter (uint32_t alphabet_size, uint32_t a)
 Create the singleton containing the letter a. More...
 
sataf_msasataf_msa_alphabet (uint32_t alphabet_size)
 Create the language equal to the alphabet of size alphabet_size. More...
 
sataf_msasataf_msa_ite (sataf_msa *i, sataf_msa *t, sataf_msa *e)
 Boolean operation : if-then-else. More...
 
sataf_msasataf_msa_not (sataf_msa *a)
 Boolean operation : complement. More...
 
sataf_msasataf_msa_or (sataf_msa *a1, sataf_msa *a2)
 Boolean operation : disjunction. More...
 
sataf_msasataf_msa_xor (sataf_msa *a1, sataf_msa *a2)
 Boolean operation : mutual exclusion. More...
 
sataf_msasataf_msa_and (sataf_msa *a1, sataf_msa *a2)
 Boolean operation : conjunction. More...
 
sataf_msasataf_msa_imply (sataf_msa *a1, sataf_msa *a2)
 Boolean operation : implication. More...
 
sataf_msasataf_msa_equiv (sataf_msa *a1, sataf_msa *a2)
 Boolean operation : equivalence. More...
 
sataf_msasataf_msa_forall (sataf_msa *a)
 Create the MSA encoding the intersection of residues of $L_a$. More...
 
sataf_msasataf_msa_exists (sataf_msa *a)
 Create the MSA encoding the union of residues of $L_a$. More...
 
sataf_msasataf_msa_concat (sataf_msa *a1, sataf_msa *a2)
 Concatenation of $L_{a_1}$ and $L_{a_2}$. More...
 
sataf_msasataf_msa_power (sataf_msa *a, int N)
 Exponentiation of $L_a$. More...
 
sataf_msasataf_msa_star (sataf_msa *a)
 Transitive closure of $L_a$. More...
 
int sataf_msa_is_detectable (sataf_msa *a1, sataf_msa *a2, ccl_list *acc)
 check if a1 is detectable in a2 More...
 
sataf_msasataf_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. More...
 
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. More...
 

Detailed Description

Function Documentation

static sataf_msa* sataf_msa_add_reference ( sataf_msa msa)
inlinestatic

Increment the counter of references of msa.

Parameters
msathe marked shared automaton
Precondition
msa != NULL
Returns
msa
sataf_msa* sataf_msa_alphabet ( uint32_t  alphabet_size)

Create the language equal to the alphabet of size alphabet_size.

Parameters
alphabet_sizethe size of the alphabet $\Sigma$
Precondition
alphabet_size > 0
Returns
$\Sigma$ such that $|\Sigma|$= alphabet_size
sataf_msa* sataf_msa_and ( sataf_msa a1,
sataf_msa a2 
)

Boolean operation : conjunction.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
the MSA encoding $L_{a_1}\cap L_{a_2}$
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.

This function finds an entry (a1,a2,a3,aux,R) then it returns a new reference to R. aux is a generic pointer which can be used to identify the cached operation (by using, for instance, the address of the function which implements the operation).

Parameters
a1the first MSA operand of the cached operation
a2the second MSA but optional operand
a3the third MSA but optional operand
auxa generic identifier.
Precondition
a1 != NULL
Returns
the MSA R if the cache contains an entry (a1,a2,a3,aux,R).
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.

This function puts a new record into the cache for MSA operations. The counter of references is incremented for each non-null $a_i$. The fourth parameter aux is copied as is. The new entry might overwrite an existing one; in this case, the replaced $a_i$ and $R$ are dereferenced.

Parameters
a1the first MSA operand
a2the second MSA but optional operand
a3the third MSA but optional operand
auxa generic identifier
Rthe result of the cached operation
Precondition
a1 != NULL
static sataf_msa* sataf_msa_compute ( sataf_mao A)
inlinestatic

Minimize, canonicalize and share the given MAO A.

This function is equivalent to sataf_msa_compute_with_transformer (A, NULL).

Parameters
Athe MAO to canonicalize
Precondition
A != NULL
Returns
the unique MSA encoding the same language than A.
sataf_msa* sataf_msa_compute_with_transformer ( sataf_mao A,
sataf_sa_transformer *  T 
)

Minimize, canonicalize and share the given MAO A.

This is the function transforming a generic automaton given as a MAO into the shared and canonical data structure called MSA.

Prior the call to the minimization algorithm the function T is called with the exit automaton and the binding function used to create the minimal shared component. This function can be used to change the acceptance condition.

Parameters
Athe MAO to canonicalize
Ta transformation function
Precondition
A != NULL
Returns
the unique MSA encoding the language recognized by A.
sataf_msa* sataf_msa_concat ( sataf_msa a1,
sataf_msa a2 
)

Concatenation of $L_{a_1}$ and $L_{a_2}$.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
the MSA encoding $L_{a_1}.L_{a_2}$.
static void sataf_msa_del_reference ( sataf_msa msa)
inlinestatic

Decrement the counter of references of msa.

When the counter of references of msa falls to zero the resources allocated to it are freed.

Parameters
msathe marked shared automaton
Precondition
msa != NULL
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.

Parameters
msathe displayed MSA.
logthe CCL output stream
alphabetan array of labels used as letters.
Precondition
msa != NULL
See Also
http://www.graphviz.org
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.

Parameters
msathe displayed MSA.
logthe CCL output stream
alphabetan array of labels used as letters.
Precondition
msa != NULL
See Also
http://www.graphviz.org
sataf_msa* sataf_msa_epsilon ( uint32_t  alphabet_size)

Create the singleton containing the empty word.

Parameters
alphabet_sizethe size of the alphabet $\Sigma$
Precondition
alphabet_size > 0
Returns
$\{\epsilon\}$
sataf_msa* sataf_msa_equiv ( sataf_msa a1,
sataf_msa a2 
)

Boolean operation : equivalence.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
the MSA encoding $\overline{L_{a_1}}\cap \overline{L_{a_2}}\cup L_{a_1}\cap L_{a_2}$
sataf_msa* sataf_msa_exists ( sataf_msa a)

Create the MSA encoding the union of residues of $L_a$.

Parameters
athe MAO argument
Precondition
a != NULL
Returns
the MSA encoding $\bigcup_{\alpha\in \Sigma} \alpha^{-1}L_a$
sataf_msa* sataf_msa_find_or_add ( sataf_sa sa,
uint32_t  initial 
)

Getting the unique MSA defined by the couple (sa,initial).

This function looks up in the unicity table of MSAs for the one defined by (sa, initial). The state initial must be a valid state of the strongly connected component defining sa.

Parameters
sathe shared automaton defining the result.
initialthe state to mark in sa
Precondition
sa != NULL
Returns
MSA(sa, initial).
sataf_msa* sataf_msa_forall ( sataf_msa a)

Create the MSA encoding the intersection of residues of $L_a$.

Parameters
athe MAO argument
Precondition
a != NULL
Returns
the MSA encoding $\bigcap_{\alpha\in \Sigma} \alpha^{-1}L_a$
static uint32_t sataf_msa_get_alphabet_size ( sataf_msa msa)
inlinestatic

Return the size of the alphabet.

Parameters
msathe considered marked shared automaton
Precondition
msa != NULL
Returns
the size of the underlying alphabet
void sataf_msa_get_info ( sataf_msa msa,
sataf_msa_info info 
)

Retrieve quantitative informations related to msa.

This function fills the structure pointed by info.

Parameters
msathe considered MSA
infostructure receiving values
Precondition
msa != NULL && info != NULL
static sataf_sa* sataf_msa_get_sa ( sataf_msa msa)
inlinestatic

Return the shared automaton defining msa.

Parameters
msathe considered MSA
Precondition
msa != NULL
Returns
the shared automaton defining msa.
static sataf_sa* sataf_msa_get_sa_no_ref ( sataf_msa msa)
inlinestatic

Return the shared automaton defining msa but without incrementing its counter of references.

Parameters
msathe considered MSA
Precondition
msa != NULL
Returns
the shared automaton defining msa.
static uint32_t sataf_msa_get_state ( sataf_msa msa)
inlinestatic

Return the marked state defining msa.

Parameters
msathe considered MSA
Precondition
msa != NULL
Returns
the marked state defining msa.
sataf_msa* sataf_msa_imply ( sataf_msa a1,
sataf_msa a2 
)

Boolean operation : implication.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
the MSA encoding $\overline{L_{a_1}}\cup L_{a_2}$
int sataf_msa_is_detectable ( sataf_msa a1,
sataf_msa a2,
ccl_list acc 
)

check if a1 is detectable in a2

This function checks if a1 is detectable in a2 i.e. if it is possible to change the acceptance condition of a2 in such a way that the obtained automaton recognize the same language than a1.

Parameters
a1automaton for which the detectability is checked
a2second operand
accthe list of states of a2 that have to accepting in order to obtain a2
Precondition
a1 != NULL
a2 != NULL
Returns
a non null value if a1 is detectable in a2.
static int sataf_msa_is_final ( sataf_msa msa)
inlinestatic

Return if msa accepts the empty word.

This function checks if the state of the automaton underlying to msa is accepting or not.

Parameters
msathe considered MSA
Precondition
msa != NULL
Returns
a non-null value if msa accepts $\epsilon$.
int sataf_msa_is_included_in ( sataf_msa a1,
sataf_msa a2 
)

Check the inclusion of $L_{a_1}$ in $L_{a_2}$.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
a non-null value iff $L_{a_1}\subseteq L_{a_2}$.
static int sataf_msa_is_one ( sataf_msa msa)
inlinestatic

Check if msa is the one recognizing everything.

Parameters
msathe marked shared automaton
Precondition
msa != NULL
Returns
a non-null value if msa recognizes all words.
static int sataf_msa_is_zero ( sataf_msa msa)
inlinestatic

Check if msa is the one recognizing nothing.

Parameters
msathe marked shared automaton
Precondition
msa != NULL
Returns
a non-null value if msa recognizes no word.
static int sataf_msa_is_zero_or_one ( sataf_msa msa)
inlinestatic

Check if msa is one of the two elementary MSAs i.e. either the one recognizing everything or the one recognizing nothing.

Parameters
msathe marked shared automaton
Precondition
msa != NULL
Returns
sataf_msa_is_one (msa) || sataf_msa_is_zero (msa)
sataf_msa* sataf_msa_ite ( sataf_msa i,
sataf_msa t,
sataf_msa e 
)

Boolean operation : if-then-else.

Parameters
ithe if MSA operand
tthe then MSA operand
ethe else MSA operand
Precondition
a1 != NULL && a2 != NULL && a3 != NULL
Returns
the MSA encoding $L_{a_1}\cap L_{a_2}\cup \overline{L_{a_1}}\cap L_{a_3}$
sataf_msa* sataf_msa_letter ( uint32_t  alphabet_size,
uint32_t  a 
)

Create the singleton containing the letter a.

Parameters
alphabet_sizethe size of the alphabet $\Sigma$
athe letter
Precondition
alphabet_size > 0
a < alphabet_size
Returns
$\{a\}$
void sataf_msa_log_info ( ccl_log_type  log,
sataf_msa msa 
)

Display on log quantitative informations about the structure of msa.

Parameters
msathe considered MSA
logthe CCL output stream
Precondition
msa != NULL
sataf_msa* sataf_msa_not ( sataf_msa a)

Boolean operation : complement.

Parameters
athe marked shared automata
Precondition
a != NULL
Returns
the MSA encoding $\Sigma^\star\setminus L_a$
sataf_msa* sataf_msa_one ( uint32_t  alphabet_size)

Compute $\Sigma^\star$.

Parameters
alphabet_sizethe size of the alphabet $\Sigma$
Precondition
alphabet_size > 0
Returns
the msa encoding $\Sigma^\star$ with $|\Sigma|$=alphabet_size
sataf_msa* sataf_msa_or ( sataf_msa a1,
sataf_msa a2 
)

Boolean operation : disjunction.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
the MSA encoding $L_{a_1}\cup L_{a_2}$
sataf_msa* sataf_msa_power ( sataf_msa a,
int  N 
)

Exponentiation of $L_a$.

Parameters
athe marked shared automaton
Nthe exponent
Precondition
a != NULL
N >= 0
Returns
the MSA encoding $L_a^N$
sataf_msa* sataf_msa_star ( sataf_msa a)

Transitive closure of $L_a$.

Parameters
athe marked shared automaton
Precondition
a != NULL
Returns
the MSA encoding $L_a^*$
sataf_msa* sataf_msa_succ ( sataf_msa msa,
uint32_t  a 
)

Return the successor of msa by the letter a.

Parameters
msathe considered MSA
athe letter
Precondition
msa != NULL
a < sataf_msa_get_alphabet_size (msa)
Returns
the successor MSA of msa by a
sataf_mao* sataf_msa_to_mao ( sataf_msa msa)

Create a MAO from msa.

Parameters
msathe considered MSA
Precondition
msa != NULL
Returns
a MAO having the same behaviors then msa
sataf_msa* sataf_msa_xor ( sataf_msa a1,
sataf_msa a2 
)

Boolean operation : mutual exclusion.

Parameters
a1, a2the marked shared automata
Precondition
a1 != NULL && a2 != NULL
Returns
the MSA encoding $L_{a_1}\oplus L_{a_2}$
sataf_msa* sataf_msa_zero ( uint32_t  alphabet_size)

Return the empty language.

Parameters
alphabet_sizethe size of the reference alphabet
Precondition
alphabet_size > 0
Returns
the empty language $\emptyset\subset\Sigma^\star$ for an alphabet $\Sigma$ of size alphabet_size.