TaPAS  0.2
Data Structures | Typedefs | Functions
Marked Automaton Objects

Data Structures

struct  sataf_mao_methods_st
 Structure gathering the methods applied to a Marked Automaton Object. More...
 

Typedefs

typedef struct sataf_mao_st sataf_mao
 Type of a Marked Automaton Object (MAO). More...
 
typedef struct sataf_mao_methods_st sataf_mao_methods
 Type of the data structure gathering methods that a Marked Automaton Object has to implement. This structure can be embedded in a larger one (as the first field) in order to create an inheritance of class interfaces.
 

Functions

sataf_maosataf_mao_create (size_t size, const sataf_mao_methods *methods)
 Allocation and initialization of a MAO. More...
 
static sataf_maosataf_mao_add_reference (sataf_mao *a)
 Increments the number of references to this MAP. More...
 
static void sataf_mao_del_reference (sataf_mao *a)
 Decrements the number of references to the given MAO. More...
 
char * sataf_mao_to_string (sataf_mao *self)
 Translate the MAO into a human readable form. More...
 
static const char * sataf_mao_get_type (sataf_mao *self)
 Return the type of the MAO self. More...
 
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. More...
 
int sataf_mao_no_cache (sataf_mao *self)
 Return if caching this object is interesting or not. More...
 
sataf_msasataf_mao_simplify (sataf_mao *self)
 Return the MSA corresponding to the MAO self if it is computable without the canonization algorithm. This function returns the result of the simplify method if it is implemented or NULL if not. More...
 
uint32_t sataf_mao_get_alphabet_size (sataf_mao *self)
 The size of the alphabet used by self. More...
 
sataf_maosataf_mao_succ (sataf_mao *self, uint32_t letter)
 Return the successor MAO of self by letter. More...
 
int sataf_mao_is_final (sataf_mao *self)
 Return if the Marked Automaton is accepting. More...
 
int sataf_mao_equals (sataf_mao *self, sataf_mao *other)
 Check if two MAO are equal. More...
 
unsigned int sataf_mao_hashcode (sataf_mao *self)
 Compute an hashcode for this MAO. More...
 
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. More...
 
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. More...
 
sataf_maosataf_mao_create_zero (uint32_t alphabet_size)
 Create a MAO encoding the empty language $\emptyset \subset \Sigma^*$ for a reference alphabet $\Sigma$ of size alphabet_size. More...
 
sataf_maosataf_mao_create_one (uint32_t alphabet_size)
 Create a MAO recognizing $\Sigma^*$. More...
 
sataf_maosataf_mao_create_epsilon (uint32_t alphabet_size)
 Create a MAO recognizing the singleton $\{\epsilon\} \subset \Sigma^*$ for a reference alphabet $\Sigma$ of size alphabet_size. More...
 
sataf_maosataf_mao_create_letter (uint32_t alphabet_size, uint32_t a)
 Create a MAO recognizing the singleton $\{a\} \subset \Sigma^*$ for a reference alphabet $\Sigma$ of size alphabet_size and one of its letter a. More...
 
sataf_maosataf_mao_create_alphabet (uint32_t alphabet_size)
 Create a MAO recognizing the entire alphabet $\Sigma$ that has a size equal to alphabet_size. More...
 
sataf_maosataf_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. More...
 
sataf_maosataf_mao_create_ite (sataf_mao *i, sataf_mao *t, sataf_mao *e)
 Create a MAO encoding the language if-then-else(i,t,e) More...
 
sataf_maosataf_mao_create_not (sataf_mao *a)
 Create a MAO encoding the complement of a. More...
 
sataf_maosataf_mao_create_or (sataf_mao *a1, sataf_mao *a2)
 Create a MAO encoding the union of two languages. More...
 
sataf_maosataf_mao_create_and (sataf_mao *a1, sataf_mao *a2)
 Create a MAO encoding the intersection of two languages. More...
 
sataf_maosataf_mao_create_multi_or (ccl_list *operands)
 Create a MAO encoding the union of a finite set of languages. More...
 
sataf_maosataf_mao_create_multi_and (ccl_list *operands)
 Create a MAO encoding the intersection of a finite set of languages. More...
 
sataf_maosataf_mao_create_imply (sataf_mao *a1, sataf_mao *a2)
 Create a MAO encoding $L_{a_1} \Rightarrow L_{a_2}$. More...
 
sataf_maosataf_mao_create_equiv (sataf_mao *a1, sataf_mao *a2)
 Create a MAO encoding $L_{a_1} \Leftrightarrow L_{a_2}$. More...
 
sataf_maosataf_mao_create_forall (sataf_mao *a)
 Create a MAO encoding the intersection of residues of $L_a$. More...
 
sataf_maosataf_mao_create_exists (sataf_mao *a)
 Create a MAO encoding the union of residues of $L_a$. More...
 
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. More...
 

Detailed Description

Typedef Documentation

typedef struct sataf_mao_st sataf_mao

Type of a Marked Automaton Object (MAO).

This type is used as an abstraction of derived objects. In order to create a new class of MAO, the first member of the derived class must be a field of type sataf_mao.

Definition at line 65 of file sataf.h.

Function Documentation

static sataf_mao* sataf_mao_add_reference ( sataf_mao a)
inlinestatic

Increments the number of references to this MAP.

This macro increments the counter of references of the considered object and returns the address of the object.

Parameters
athe referenced MAO
Precondition
a != NULL
Returns
a
sataf_mao* sataf_mao_create ( size_t  size,
const sataf_mao_methods methods 
)

Allocation and initialization of a MAO.

Parameters
sizethe size in bytes required to store the object
methodsthe pointers to the MAO methods
Precondition
size >= sizeof (sataf_mao)
methods != NULL
Returns
a newly allocated
sataf_mao* sataf_mao_create_alphabet ( uint32_t  alphabet_size)

Create a MAO recognizing the entire alphabet $\Sigma$ that has a size equal to alphabet_size.

Parameters
alphabet_sizethe size of the alphabet
Precondition
alphabet_size > 0
Returns
$\Sigma$
sataf_mao* sataf_mao_create_and ( sataf_mao a1,
sataf_mao a2 
)

Create a MAO encoding the intersection of two languages.

Parameters
a1the first language
a2the second language
Precondition
a1 != NULL && a2 != NULL
sataf_mao_get_alphabet_size (a1) == sataf_mao_get_alphabet_size (a2)
Returns
a MAO encoding the $L_{a_1}\cap L_{a_2}$
sataf_mao* sataf_mao_create_epsilon ( uint32_t  alphabet_size)

Create a MAO recognizing the singleton $\{\epsilon\} \subset \Sigma^*$ for a reference alphabet $\Sigma$ of size alphabet_size.

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

Create a MAO encoding $L_{a_1} \Leftrightarrow L_{a_2}$.

Parameters
a1the first MAO argument
a2the first MAO argument
Precondition
a1 != NULL && a2 != NULL
sataf_mao_get_alphabet_size (a1) == sataf_mao_get_alphabet_size (a2)
Returns
a MAO encoding the $L_{a_1}\Leftrightarrow L_{a_2}$
sataf_mao* sataf_mao_create_exists ( sataf_mao a)

Create a MAO encoding the union of residues of $L_a$.

Parameters
athe MAO argument
Precondition
a != NULL
Returns
a MAO encoding $\bigcup_{\alpha\in \Sigma} \alpha^{-1}L_a$
sataf_mao* sataf_mao_create_forall ( sataf_mao a)

Create a MAO encoding the intersection of residues of $L_a$.

Parameters
athe MAO argument
Precondition
a != NULL
Returns
a MAO encoding $\bigcap_{\alpha\in \Sigma} \alpha^{-1}L_a$
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.

This function creates a MAO encoding an automaton with nb_states, recognizing from the state s0 words over an alphabet of size alphabet_size. The acceptance condition is given by an array of Booleans is_final: the state i is accepting iff "is_final[i]" is non-null. The transition function of the resulting automaton is given by the array succ of size nb_states $\times$alphabet_size and such that succ[s $\times$ alphabet_size+a] is the successor of the state s by the letter a.

Parameters
alphabet_sizethe size of the reference alphabet
is_finalthe acceptance condition
nb_statesthe number of states if the automaton
s0the index of the initial state
succthe transition function
Precondition
is_final != NULL
nb_states > 0
s0 < nb_states
succ != NULL
Returns
the MAO encoding of the explicitly given automaton
sataf_mao* sataf_mao_create_imply ( sataf_mao a1,
sataf_mao a2 
)

Create a MAO encoding $L_{a_1} \Rightarrow L_{a_2}$.

Parameters
a1the first MAO argument
a2the first MAO argument
Precondition
a1 != NULL && a2 != NULL
sataf_mao_get_alphabet_size (a1) == sataf_mao_get_alphabet_size (a2)
Returns
a MAO encoding the $L_{a_1}\Rightarrow L_{a_2}$
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)

Parameters
ithe 'if' argument
tthe 'then' argument
ethe 'else' argument
Precondition
i != NULL && t != NULL && e != NULL
sataf_mao_get_alphabet_size (i) == sataf_mao_get_alphabet_size (t)
sataf_mao_get_alphabet_size (i) == sataf_mao_get_alphabet_size (e)
Returns
a MAO encoding then if-then-else(i,t,e)
sataf_mao* sataf_mao_create_letter ( uint32_t  alphabet_size,
uint32_t  a 
)

Create a MAO recognizing the singleton $\{a\} \subset \Sigma^*$ for a reference alphabet $\Sigma$ of size alphabet_size and one of its letter a.

Parameters
alphabet_sizethe size of the alphabet
athe recognized letter
Precondition
alphabet_size > 0
a < alphabet_size
Returns
$\{a\}$
sataf_mao* sataf_mao_create_multi_and ( ccl_list operands)

Create a MAO encoding the intersection of a finite set of languages.

Parameters
operandsthe set of languages
Precondition
operands != NULL
ccl_list_get_size (operands) > 0
Returns
a MAO encoding $\bigcap_{a\in operands} L_a$
sataf_mao* sataf_mao_create_multi_or ( ccl_list operands)

Create a MAO encoding the union of a finite set of languages.

Parameters
operandsthe set of languages
Precondition
operands != NULL
ccl_list_get_size (operands) > 0
Returns
a MAO encoding $\bigcup_{a\in operands} L_a$
sataf_mao* sataf_mao_create_not ( sataf_mao a)

Create a MAO encoding the complement of a.

Parameters
athe complemented MAO
Precondition
a != NULL
Returns
a MAO encoding then $\Sigma^*\setminus L_a$
sataf_mao* sataf_mao_create_one ( uint32_t  alphabet_size)

Create a MAO recognizing $\Sigma^*$.

Parameters
alphabet_sizethe size of the alphabet $\Sigma$
Precondition
alphabet_size > 0
Returns
$\Sigma^*$ with $|\Sigma| = \mbox{alphabet\_size}$
sataf_mao* sataf_mao_create_or ( sataf_mao a1,
sataf_mao a2 
)

Create a MAO encoding the union of two languages.

Parameters
a1the first language
a2the second language
Precondition
a1 != NULL && a2 != NULL
sataf_mao_get_alphabet_size (a1) == sataf_mao_get_alphabet_size (a2)
Returns
a MAO encoding the $L_{a_1}\cup L_{a_2}$
sataf_mao* sataf_mao_create_zero ( uint32_t  alphabet_size)

Create a MAO encoding the empty language $\emptyset \subset \Sigma^*$ for a reference alphabet $\Sigma$ of size alphabet_size.

Parameters
alphabet_sizethe size of the reference alphabet
Precondition
alphabet_size > 0
Returns
$\emptyset$
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.

The nodes are labelled by the result of the to_string method; if this one is not implemented then a unique integer is used. The array alphabet is used to label transition; if the array is NULL then the index of the letter is used.

Parameters
logthe CCL output stream
selfthe MAO translated into DOT
alphabetan array of strings used as letters
graph_nameused to name the graph in the DOT file format
graph_typethe DOT keyword defining the type of the graph (digraph or graph).
static void sataf_mao_del_reference ( sataf_mao a)
inlinestatic

Decrements the number of references to the given MAO.

This macro decrements the counter of references of the considered object. If this counter falls to zero then, if it is implemented, the destroy method is called on the object. The memory occupied by the object is then freed.

Parameters
athe dereferenced MAO
Precondition
a != NULL
int sataf_mao_equals ( sataf_mao self,
sataf_mao other 
)

Check if two MAO are equal.

Two MAOs are equal:

  • if they have the same type, and
  • if they have the same alphabet size, and
  • if the equals method returns a non-null value. If the method is not implemented then the function returns self == other.
Parameters
selfthe MAO argument
otherthe MAO argument
Precondition
self != NULL && otehr != NULL
Returns
a non-null value if self and other recognizes are the same objects.
uint32_t sataf_mao_get_alphabet_size ( sataf_mao self)

The size of the alphabet used by self.

Parameters
selfthe MAO argument
Precondition
self != NULL
Returns
the size of the alphabet
static const char* sataf_mao_get_type ( sataf_mao self)
inlinestatic

Return the type of the MAO self.

The type of a MAO is a constant string assigned to the static member type of the object. This type is used to compare objects (see sataf_mao_equals).

Parameters
selfthe MAO argument
Precondition
self != NULL
Returns
the string encoding the type of self
unsigned int sataf_mao_hashcode ( sataf_mao self)

Compute an hashcode for this MAO.

If the MAO does not implement the hashcode function the address self is returned.

Parameters
selfthe MAO argument
Precondition
self != NULL
Returns
an hashcode for self
int sataf_mao_is_final ( sataf_mao self)

Return if the Marked Automaton is accepting.

Parameters
selfthe MAO argument
Precondition
self != NULL
Returns
a non-null value if the state of the automaton corresponding to the MAO self is accepting.
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.

This method indicates to the implementation of the MAO that the sharing algorithm has identified this node to be the root of some SCC i.e. a shared automaton.

Parameters
selfthe MAO argument
sathe shared automaton pointing the SCC
q0the entry point in the SCC
Precondition
self != NULL
sa != NULL
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.

Parameters
memo_sizethe size of the entries
inita pointer to the function initializing entries
init_dataa pointer to data used bu the init function
cleana pointer to a function used to free resources allocated to an entry.
Returns
the newly created memorizer
int sataf_mao_no_cache ( sataf_mao self)

Return if caching this object is interesting or not.

This function returns the result of the no_cache method or 0 if it is no implemented.

Parameters
selfthe MAO argument
Precondition
self != NULL
Returns
a non-null value if self has not to be cached.
sataf_msa* sataf_mao_simplify ( sataf_mao self)

Return the MSA corresponding to the MAO self if it is computable without the canonization algorithm. This function returns the result of the simplify method if it is implemented or NULL if not.

Parameters
selfthe simplified MAO
Precondition
self != NULL
Returns
the MSA equivalent to self or NULL if the result is unknown.
sataf_mao* sataf_mao_succ ( sataf_mao self,
uint32_t  letter 
)

Return the successor MAO of self by letter.

Parameters
selfthe MAO argument
letterthe letter labelling the transition
Precondition
letter < sataf_mao_get_alphabet_size (self)
self implements the succ method.
Returns
a non-null value if the state of the automaton corresponding to the MAO self is accepting.
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.

If the object does not implement the to_dot method then the sataf_mao_default_to_dot is called.

Parameters
logthe CCL output stream
selfthe MAO translated into DOT
alphabetan array of strings used as letters
graph_nameused to name the graph in the DOT file format
graph_typethe DOT keyword defining the type of the graph (digraph or graph).
char* sataf_mao_to_string ( sataf_mao self)

Translate the MAO into a human readable form.

This funciton returns the result of the to_string method applied to self. If the MAO does not implement it then the string "\a type@ \a addr" is returned, where type is the result of sataf_mao_get_type and addr is the address of self.

Parameters
selfthe MAO argument
Precondition
self != NULL
Returns
a "human-readable" corresponding to self