-
Notifications
You must be signed in to change notification settings - Fork 0
/
automata.h
94 lines (72 loc) · 2.7 KB
/
automata.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
typedef struct Automata Automata;
typedef struct Node Node;
typedef struct Arrow Arrow;
typedef struct Counter_Action Counter_Action;
typedef struct Point Point;
typedef struct Exploration Exploration;
struct Automata {
int nb_nodes; // number of nodes of the nda
int nb_nodes_capacity; // capacity of the array storing the nodes
Node * nodes;
int nb_counters;
};
struct Node {
int success; // boolean
int nb_arrows; // number of arrows of the node
int nb_arrows_capacity; // capacity of the arrays storing the arrows
Arrow * arrows;
};
struct Arrow {
int label; // which letter must be read to follow the arrow
int label_max; // for labels interval: [label-label_max]. disabled by label_max == label
int epsilon; // boolean TRUE for epsilon arrows, FALSE otherwise
int dest; // the node that is pointed by the arrow. index in the nodes array
int nb_counters_actions;
int nb_counters_actions_capacity;
Counter_Action * counters_actions;
};
struct Counter_Action {
int num_counter;
int action;
int action_param;
};
struct Point {
int num_node; // in which node is the point
int num_arrow_next; // the next arrow to be followed (must be a existing arrow num)
int nb_labels_used; // the nb of labels used to reach this point
};
struct Exploration {
int nb_points;
int nb_points_capacity;
Point * points;
int nb_counters_by_point;
int nb_counters;
int nb_counters_capacity;
int * counters; // the counters for each point
};
// constants for counter actions
enum { ACTION_SET, ACTION_ADD, ACTION_AT_LEAST, ACTION_AT_MOST };
int new_automata (Automata * res_automata, int nb_nodes_capacity, int nb_counters);
int add_node (Automata * automata, int success, int nb_arrows_capacity);
int add_label_arrow (
Automata * automata, int num_node, int label, int dest, int nb_counters_actions_capacity);
int add_epsilon_arrow (
Automata * automata, int num_node, int dest, int nb_counters_actions_capacity);
int add_interval_arrow (
Automata * automata, int num_node, int label, int label_max,
int dest, int nb_counters_actions_capacity
);
int add_counter_action (
Automata * automata, int num_node, int num_arrow,
int num_counter, int action, int action_param);
char * automata_to_string (Automata automata);
char * automata_to_dot (Automata automata);
void free_automata (Automata nda);
int apply_counters_actions (int * counters, Arrow arrow);
void explore_step (Exploration * expl, Automata automata, int * labels, int nb_labels);
void explore_farthest_success_node (
Automata automata, int start_num_node, int * labels, int nb_labels,
int * res_num_node, int * res_nb_labels_used, int * res_counters,
int * res_nb_explorations_steps, int * res_max_nb_points_reached
);
void free_exploration (Exploration expl);