TaPAS  0.2
Typedefs | Functions
Exit Automata

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_easataf_ea_create (uint32_t nb_states, uint32_t nb_exits, uint32_t alphabet_size)
 Build an empty Exit Automaton data structure. More...
 
sataf_easataf_ea_complement (sataf_ea *ea)
 Build an EA isomorph to ea up to the acceptance condition which is negated. More...
 
sataf_easataf_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_easataf_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_easataf_ea_minimize (sataf_ea *ea, uint32_t *h)
 Minimization of ea. More...
 
sataf_easataf_ea_find_or_add (sataf_ea *ea)
 Find or add ea in the unicity table. More...
 
sataf_easataf_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
eathe 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
eathe 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_statesthe number of local states
nb_exitsthe number of exit states
alphabet_sizethe 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_statesthe number of local states of the new EA
nb_exitsits number of exit states
alphabet_sizethe cardinal of the alphabet
is_finalthe acceptance condition
succthe 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
eathe 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
eathe exit automaton
logthe CCL output stream
alphabetan 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, ea2the 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
eathe 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
eathe 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
eathe 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
eathe 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
eathe 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
eathe exit automaton
statethe considered state
athe 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
eathe 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
eathe exit automaton
sthe 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
eathe exit automaton
Precondition
ea != NULL
static int sataf_ea_is_zero ( sataf_ea ea)
inlinestatic

Check if ea accepts nothing.

Parameters
eathe 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
eathe 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
eathe exit automaton
hthe 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
eathe exit automaton
sthe state
is_finala 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
eathe exit automaton
srcthe source state
athe letter labelling the transition
tgtthe index of the new successor
is_exita 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
logthe CCL output stream