forked from jurajmajor/ltl3tela
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathautomaton.hpp
250 lines (184 loc) · 7.13 KB
/
automaton.hpp
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
/*
Copyright (c) 2016 Juraj Major
This file is part of LTL3TELA.
LTL3TELA is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
LTL3TELA is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with LTL3TELA. If not, see <http://www.gnu.org/licenses/>.
*/
#ifndef AUTOMATON_H
#define AUTOMATON_H
#include <algorithm>
#include <map>
#include <stack>
#include <string>
#include <sstream>
#include <spot/tl/print.hh>
#include <queue>
#include <vector>
#include <spot/tl/unabbrev.hh>
#include <spot/misc/escape.hh>
#include <spot/twa/acc.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/sccfilter.hh>
#include "utils.hpp"
typedef unsigned acc_mark;
class Edge {
protected:
// target set of the edge
std::set<unsigned> targets;
// the acceptance label
std::set<acc_mark> marks;
// the transition labels in BDD
bdd label;
public:
Edge(bdd l);
// adds a state or a set of states to the target set
void add_target(unsigned state_id);
void add_target(std::set<unsigned> state_ids);
// removes a state from the target set
void remove_target(unsigned state_id);
// replaces the target set with given set
void replace_target_set(std::set<unsigned> state_ids);
// adds an acceptance mark or a set of them
void add_mark(unsigned ix);
void add_mark(std::set<unsigned> ixs);
// removes an acceptance mark
void remove_mark(unsigned ix);
// removes all acceptance marks
void clear_marks();
// returns the target set
std::set<unsigned> get_targets() const;
// returns the acceptance label
std::set<unsigned> get_marks() const;
// returns the transition label
bdd get_label() const;
// sets the transition label
void set_label(bdd l);
int dominates(Edge* other, std::set<unsigned> o1, std::set<unsigned> o2, std::set<acc_mark> inf_marks) const;
int dominates(Edge* other, std::set<acc_mark> inf_marks) const;
};
template<typename T> class Automaton {
protected:
// vector of names of states
std::vector<T> states;
// vector of edges
std::vector<Edge*> edges;
// state_edges maps a set of edges to each state
std::vector<std::set<unsigned>> state_edges;
std::vector<std::set<unsigned>>* spot_id_to_slaa_set = nullptr; // this has to be nullptr for SLAA
// a set of Inf-marks used in the automaton
std::set<acc_mark> inf_marks;
// the set of initial configurations
std::set<std::set<unsigned>> init_sets;
public:
// returns a state ID by its name, possibly creating a new one
unsigned get_state_id(T f);
// returns a name of the state with the given ID
T state_name(unsigned state_id);
// checks whether a state with given name already exists
bool state_exists(T f);
// returns the number of states
unsigned states_count();
// creates an edge and returns its ID (index in the `edges' set)
unsigned create_edge(bdd label);
// creates an edge with given source state, labels and target set
void add_edge(unsigned from, bdd label, std::set<unsigned> to, std::set<acc_mark> marks = std::set<acc_mark>());
// copies the given edge to the source `from'
void add_edge(unsigned from, unsigned edge_id);
// copies the given edges to the source `from'
void add_edge(unsigned from, std::set<unsigned> edge_ids);
// removes the given edge from the source
void remove_edge(unsigned state_id, unsigned edge_id);
// returns a pointer to the edge specified by ID
Edge* get_edge(unsigned edge_id) const;
// returns state_edges[state_id]
std::set<unsigned> get_state_edges(unsigned state_id) const;
// returns the registered Inf-marks
std::set<acc_mark> get_inf_marks() const;
// registers the marks in the set `inf_marks'
void remember_inf_mark(acc_mark mark);
void remember_inf_mark(std::set<acc_mark> marks);
// removes states unreachable from the initial states
void remove_unreachable_states();
// returns an edge ID that is a (mark-preserving or mark-discarding) product of given edges
unsigned edge_product(unsigned e1, unsigned e2, bool preserve_mark_sets);
// for the family of sets { M_1, ..., M_n } of edges,
// returns set of products of each n edges from distinct M_i
std::set<unsigned> product(std::set<std::set<unsigned>> edges_sets, bool preserve_mark_sets);
~Automaton();
};
class SLAA : public Automaton<spot::formula> {
protected:
spot::formula phi;
public:
// each U-subformula has its own acceptance condition
// (Fin(x) & (Fin(y_1) | ... | Fin(y_i))
// x and y_i are stored in fin and fin_disj members
// if such formula appears as a direct subformula of G,
// the condition changes to (...) | Inf(z)
// this z is stored in inf
typedef struct {
acc_mark fin;
acc_mark inf;
std::set<acc_mark> fin_disj;
} acc_phi;
// the set representation of resultant acceptance condition
typedef std::set<std::set<std::set<std::pair<acc_mark, acc_mark>>>> ac_representation;
// Spot structures
spot::twa_graph_ptr spot_aut;
spot::bdd_dict_ptr spot_bdd_dict;
// getter for the input formula
spot::formula get_input_formula() const;
// acceptance formula of each Until state
std::map<spot::formula, acc_phi> acc;
// sets the Spot acceptance condition from acc
void build_acc();
// removes marks from non-looping transitions
void remove_unnecessary_marks();
// returns a set of initial configurations
std::set<std::set<unsigned>> get_init_sets() const;
// adds an initial configuration
void add_init_set(std::set<unsigned> init_set);
// converts the automaton to single-owner
// the output argument tgba_mark_owners contains pairs of mark j and its owner q
// such that all loops over q contain j as the only mark
ac_representation mark_transformation(std::map<acc_mark, unsigned>& tgba_mark_owners);
std::set<std::set<acc_mark>> get_minimal_models_of_acc_cond() const;
// postprocessing: remove dominated transition w.r.t. acceptance condition
void apply_extended_domination();
// prints the automaton in HOA format
void print_hoaf();
// prints the automaton in DOT format
void print_dot();
SLAA(spot::formula f, spot::bdd_dict_ptr dict = nullptr);
};
class NA : public Automaton<unsigned> {
public:
// merges edges with the same source and target
void merge_edges();
// merges states with the same outgoing transitions
void merge_equivalent_states();
// returns true if two given states are equivalent,
// with the equivalence test from LTL2BA or LTL3BA
bool states_equivalent(unsigned s1, unsigned s2, unsigned eq_level);
// setter and getter of the init states are wrappers
// over the structure of initial configurations
// sets the init state
void set_init_state(unsigned s);
// returns the init state
unsigned get_init_state() const;
NA(std::vector<std::set<unsigned>>* sets);
};
#endif