Typedefs
typedef struct sataf_ea_st	sataf_ea
	Type for the data structure encoding Exit Automata.

Functions
static uint32_t	sataf_ea_encode_succ_as_local_state (uint32_t index)
	Encode the successor state index as a local state.

static uint32_t	sataf_ea_encode_succ_as_exit_state (uint32_t index)
	Encode the successor state index as an exit state.

static uint32_t	sataf_ea_decode_succ_state (uint32_t index)
	Decode the successor state index.

static int	sataf_ea_is_exit_state (uint32_t successor)
	Check if the given successor corresponds to an exit state or not.

static int	sataf_ea_is_local_state (uint32_t successor)
	Check if the given successor corresponds to a local state or not.

static uint32_t	sataf_ea_get_alphabet_size (sataf_ea *ea)
	Return the size of this alphabet used by the exit automaton ea. More...

static uint32_t	sataf_ea_get_nb_states (sataf_ea *ea)
	Return the number of local states of ea. More...

static uint32_t	sataf_ea_get_nb_exits (sataf_ea *ea)
	Return the number of exit states of ea. More...

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

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

static int	sataf_ea_is_zero (sataf_ea *ea)
	Check if ea accepts nothing. More...

static int	sataf_ea_is_one (sataf_ea *ea)
	Check if ea accepts any word. More...

static int	sataf_ea_is_zero_or_one (sataf_ea *ea)
	Check if ea recognizes anything or nothing. More...

sataf_ea *	sataf_ea_create (uint32_t nb_states, uint32_t nb_exits, uint32_t alphabet_size)
	Build an empty Exit Automaton data structure. More...

sataf_ea *	sataf_ea_complement (sataf_ea *ea)
	Build an EA isomorph to ea up to the acceptance condition which is negated. More...

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

sataf_ea *	sataf_ea_add_reference (sataf_ea *ea)
	Increment the counter of references of ea. More...

void	sataf_ea_del_reference (sataf_ea *ea)
	Decrement the counter of references of ea. More...

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

static void	sataf_ea_set_final (sataf_ea *ea, uint32_t s, int is_final)
	Change the acceptance condition for the state s. More...

void	sataf_ea_display_as_dot (sataf_ea ea, ccl_log_type log, const char *alphabet)
	Display the exit automaton in DOT graph format. More...

sataf_ea *	sataf_ea_minimize (sataf_ea ea, uint32_t h)
	Minimization of ea. More...

sataf_ea *	sataf_ea_find_or_add (sataf_ea *ea)
	Find or add ea in the unicity table. More...

sataf_ea *	sataf_ea_find (sataf_ea *ea)
	Return the unique version of ea if it exists. More...

int	sataf_ea_equals (sataf_ea ea1, sataf_ea ea2)
	Check that ea1 and ea2 are equal. More...

unsigned int	sataf_ea_hashcode (sataf_ea *ea)
	Hashcode of an EA The integer value is computed according to the transition function and the acceptance table of the EA. More...

void	sataf_ea_ut_statistics (ccl_log_type log)
	Display internal statistics about the use of EAs. In particular informations related to the unicity table. More...

Detailed Description

Function Documentation

sataf_ea* sataf_ea_add_reference ( sataf_ea * ea )

Increment the counter of references of ea.

This function is used to inform the library that ea is referenced one more time.

Parameters

ea	the exit automaton

Precondition: ea != NULL

Returns: ea

sataf_ea* sataf_ea_complement ( sataf_ea * ea )

Build an EA isomorph to ea up to the acceptance condition which is negated.

This function returns an EA strictly equal to ea except for the acceptance condition; this latter is inversed for each state. Thus, if ea is an automaton with no exit states, the resulting automaton recognizes exactly the complement of the language recognized by ea.

Parameters

ea	the exit automaton

Precondition: ea != NULL

sataf_ea* sataf_ea_create	(	uint32_t	nb_states,
		uint32_t	nb_exits,
		uint32_t	alphabet_size
	)

Build an empty Exit Automaton data structure.

This function allocates a new EA with nb_states local states, nb_exits exit states. The automaton reads word over the alphabet. The transition function and the acceptance condition are filled with zero thus the automaton is an automaton (not necessarily minimal) recognizing the empty language.

Parameters

nb_states	the number of local states
nb_exits	the number of exit states
alphabet_size	the size of the alphabet

Precondition: nb_states > 0; alphabet_size > 0

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.

This function constructs an EA like sataf_ea_create (nb_states, nb_exits, alphabet_size) but it fills the transition function and the acceptance condition with the arrays succ and is_final.

The array succ must have nb_states $\times$ alphabet_size entries. Each entry succ[alphabet_size*s+a] represents the encoded index of the successor of s following the letter a. If t is the index of the successor of s by a then the entry succ[alphabet_size*s+a] is:

sataf_ea_encode_succ_as_exit_state(t) if t is an exit state
sataf_ea_encode_succ_as_local_state(t) if t is a local state

The array is_final is assumed to have nb_states entries. is_final[i] must be non-null if and only if the local state i is accepting.

Parameters

nb_states	the number of local states of the new EA
nb_exits	its number of exit states
alphabet_size	the cardinal of the alphabet
is_final	the acceptance condition
succ	the transition function

Precondition: succ != NULL && is_final != NULL; nb_states > 0 && alphabet_size > 0

void sataf_ea_del_reference ( sataf_ea * ea )

Decrement the counter of references of ea.

If the counter of references of ea falls to zero, the memory allocated to it is freed.

Parameters

ea	the exit automaton

Precondition: ea != NULL

void sataf_ea_display_as_dot	(	sataf_ea *	ea,
		ccl_log_type	log,
		const char **	alphabet
	)

Display the exit automaton in DOT graph format.

Accepting states are drawn with a double circle and exit states with octagon. If an alphabet is given (i.e. not NULL) then its letters are used to label transitions in place of their index.

Parameters

ea	the exit automaton
log	the CCL output stream
alphabet	an optional array of strings used for letters

Precondition: ea != NULL

See Also: http://www.graphviz.org

int sataf_ea_equals	(	sataf_ea *	ea1,
		sataf_ea *	ea2
	)

Check that ea1 and ea2 are equal.

Two EAs are equal if they have the same number of (local and exit) states, the same alphabet size and if the transition function and acceptance table are equal.

Parameters

ea1, ea2 the compared EAs

Precondition: ea1 != NULL && ea2 != NULL

Returns: an non-null value if the content of ea1 and ea2 are equal.

sataf_ea* sataf_ea_find ( sataf_ea * ea )

Return the unique version of ea if it exists.

Parameters

ea	the exit automaton

Precondition: ea != NULL

Returns: the unique minimal EA isomorphic to ea or NULL if it is not present in the unicity table.

sataf_ea* sataf_ea_find_or_add ( sataf_ea * ea )

Find or add ea in the unicity table.

In order to share EAs, the library maintains a table containing a unique version of each minimal EAs computed by the sharing algorithm. Two check is two unique EAs are equal it is sufficient to test the equality of their address.

Parameters

ea	the exit automaton

Precondition: ea != NULL

Returns: ea or its unique equivalent.

static uint32_t sataf_ea_get_alphabet_size ( sataf_ea * ea )

static

Return the size of this alphabet used by the exit automaton ea.

Parameters

ea	the exit automaton

Precondition: ea != NULL

static uint32_t sataf_ea_get_nb_exits ( sataf_ea * ea )

inlinestatic

Return the number of exit states of ea.

Parameters

ea	the exit automaton

Precondition: ea != NULL

static uint32_t sataf_ea_get_nb_states ( sataf_ea * ea )

inlinestatic

Return the number of local states of ea.

Parameters

ea	the exit automaton

Precondition: ea != NULL

static uint32_t sataf_ea_get_successor	(	sataf_ea *	ea,
		uint32_t	state,
		uint32_t	a
	)

inlinestatic

Get the successor of state by the letter a.

As mentionned above, the returned integer encodes both the successor state the flag indicating if it is a local or an exit state.

Parameters

ea	the exit automaton
state	the considered state
a	the later used to go out of state.

Precondition: ea != NULL; state < sataf_ea_get_nb_states(ea); a < sataf_ea_get_alphabet_size(ea)

unsigned int sataf_ea_hashcode ( sataf_ea * ea )

Hashcode of an EA The integer value is computed according to the transition function and the acceptance table of the EA.

Parameters

ea	the exit automaton argument

Precondition: ea != NULL

Returns: an hashcode for ea

static int sataf_ea_is_final	(	sataf_ea *	ea,
		uint32_t	s
	)

inlinestatic

Return a non null value is the local state s of ea is accepting or not.

Parameters

ea	the exit automaton
s	the tested state

Precondition: ea != NULL; s < sataf_ea_get_nb_states(ea)

static int sataf_ea_is_one ( sataf_ea * ea )

inlinestatic

Check if ea accepts any word.

Parameters

ea	the exit automaton

Precondition: ea != NULL

static int sataf_ea_is_zero ( sataf_ea * ea )

inlinestatic

Check if ea accepts nothing.

Parameters

ea	the exit automaton

Precondition: ea != NULL

static int sataf_ea_is_zero_or_one ( sataf_ea * ea )

inlinestatic

Check if ea recognizes anything or nothing.

Parameters

ea	the exit automaton

Precondition: ea != NULL

sataf_ea* sataf_ea_minimize	(	sataf_ea *	ea,
		uint32_t *	h
	)

Minimization of ea.

This function computes the minimal exit automaton equivalent to ea. The array h must be of size sataf_ea_get_alphabet_size (ea). h is filled with the homomorphism mapping each state of ea to its equivalent class in the minimal EA.

Parameters

ea	the exit automaton
h	the homomorphism from ea to the minimal automaton.

Precondition: ea != NULL && h != NULL

Returns: the minimal EA recognizing the state language than ea

static void sataf_ea_set_final	(	sataf_ea *	ea,
		uint32_t	s,
		int	is_final
	)

inlinestatic

Change the acceptance condition for the state s.

Parameters

ea	the exit automaton
s	the state
is_final	a Boolean indicating if s is accepting or not

Precondition: ea != NULL; s < ea->nb_local_states

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.

The procedure changes the successor by the letter of the state src. The new successor is tgt which is considered as an exit state if is_exit is non-null. Note that, oppositely to sataf_ea_create_with_arrays, the state tgt is the actual index of the successor, not its encoded version.

Parameters

ea	the exit automaton
src	the source state
a	the letter labelling the transition
tgt	the index of the new successor
is_exit	a Boolean indicating if tgt is an exit state.

Precondition: ea != NULL; src < ea->nb_local_states; is_exit $\Rightarrow$ tgt < ea->nb_exit_states; $\neg$ is_exit $\Rightarrow$ tgt < ea->nb_local_states; a < ea->alphabet_size

void sataf_ea_ut_statistics ( ccl_log_type log )

Display internal statistics about the use of EAs. In particular informations related to the unicity table.

Parameters

log	the CCL output stream

Typedefs

Functions

Detailed Description

Function Documentation