29 #ifndef __PRESTAF_AUTOMATA_H__ 
   30 # define __PRESTAF_AUTOMATA_H__ 
   33 # include <sataf/sataf.h> 
   48                                         int alpha_size, 
int b);
 
   54 prestaf_crt_add_variable_automaton(
sataf_msa *msa, uint32_t i, uint32_t n);
 
   60 prestaf_crt_inv_project_automaton(
sataf_msa *msa, 
int width, 
 
   61                                   const int *selection, 
int selsize);
 
   79 prestaf_crt_quantifier_automaton(
int forall, uint32_t i, uint32_t n, 
 
   83 prestaf_crt_quantifier_automaton2(
int forall, uint32_t i, uint32_t n, 
 
   87 prestaf_crt_unfolding_automaton(
int m,  
sataf_msa *fset);
 
   91                        const char *graph_name, 
const char *graph_type);
 
  100 prestaf_crt_from_exit_automaton (
int s0, 
sataf_ea *ea, 
const uint8_t *
final);
 
struct sataf_ea_st sataf_ea
Type for the data structure encoding Exit Automata. 
 
sataf_mao * prestaf_crt_linear_constraint_automaton(int type, const int *alpha, int alpha_size, int b)
 
struct sataf_mao_st sataf_mao
Type of a Marked Automaton Object (MAO). 
 
enum ccl_log_type_enum ccl_log_type
Enum that indicates which kind of message has to be displayed. Each kind of message can be displayed ...
 
A dynamic association table implemented by hashing. 
 
struct ccl_hash_st ccl_hash
abstract type of an hash table. 
 
struct sataf_msa_st sataf_msa
Type for the data structure encoding Marked Shared Automata.