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_mao *	sataf_mao_create (size_t size, const sataf_mao_methods *methods)
	Allocation and initialization of a MAO. More...

static sataf_mao *	sataf_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_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. More...

uint32_t	sataf_mao_get_alphabet_size (sataf_mao *self)
	The size of the alphabet used by self. More...

sataf_mao *	sataf_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_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*. More...

sataf_mao *	sataf_mao_create_one (uint32_t alphabet_size)
	Create a MAO recognizing $\Sigma^*$ . More...

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*. More...

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. More...

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. More...

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. More...

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) More...

sataf_mao *	sataf_mao_create_not (sataf_mao *a)
	Create a MAO encoding the complement of a. More...

sataf_mao *	sataf_mao_create_or (sataf_mao a1, sataf_mao a2)
	Create a MAO encoding the union of two languages. More...

sataf_mao *	sataf_mao_create_and (sataf_mao a1, sataf_mao a2)
	Create a MAO encoding the intersection of two languages. More...

sataf_mao *	sataf_mao_create_multi_or (ccl_list *operands)
	Create a MAO encoding the union of a finite set of languages. More...

sataf_mao *	sataf_mao_create_multi_and (ccl_list *operands)
	Create a MAO encoding the intersection of a finite set of languages. More...

sataf_mao *	sataf_mao_create_imply (sataf_mao a1, sataf_mao a2)
	Create a MAO encoding $L_{a_1} \Rightarrow L_{a_2}$ . More...

sataf_mao *	sataf_mao_create_equiv (sataf_mao a1, sataf_mao a2)
	Create a MAO encoding $L_{a_1} \Leftrightarrow L_{a_2}$ . More...

sataf_mao *	sataf_mao_create_forall (sataf_mao *a)
	Create a MAO encoding the intersection of residues of . More...

sataf_mao *	sataf_mao_create_exists (sataf_mao *a)
	Create a MAO encoding the union of residues of . 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

a	the 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

size	the size in bytes required to store the object
methods	the 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_size the 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

a1	the first language
a2	the 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_size the 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

a1	the first MAO argument
a2	the 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

a	the 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

a	the 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_size	the size of the reference alphabet
is_final	the acceptance condition
nb_states	the number of states if the automaton
s0	the index of the initial state
succ	the 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

a1	the first MAO argument
a2	the 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

i	the 'if' argument
t	the 'then' argument
e	the '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_size	the size of the alphabet
a	the 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

operands the 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

operands the 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

a	the 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_size the 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

a1	the first language
a2	the 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_size the 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

log	the CCL output stream
self	the MAO translated into DOT
alphabet	an array of strings used as letters
graph_name	used to name the graph in the DOT file format
graph_type	the 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

a	the 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

self	the MAO argument
other	the 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

self	the 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

self	the 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

self	the 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

self	the 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

self	the MAO argument
sa	the shared automaton pointing the SCC
q0	the 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_size	the size of the entries
init	a pointer to the function initializing entries
init_data	a pointer to data used bu the init function
clean	a 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

self	the 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

self	the 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

self	the MAO argument
letter	the 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

log	the CCL output stream
self	the MAO translated into DOT
alphabet	an array of strings used as letters
graph_name	used to name the graph in the DOT file format
graph_type	the 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

self	the MAO argument

Precondition: self != NULL

Returns: a "human-readable" corresponding to self

Data Structures

Typedefs

Functions

Detailed Description

Typedef Documentation

Function Documentation