40 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED 41 # define YY_HOAYY_PARSEAUT_HH_INCLUDED 43 #line 33 "parseaut.yy" // lalr1.cc:377 46 #include <spot/misc/common.hh> 50 #include <unordered_map> 52 #include <spot/twa/formula2bdd.hh> 53 #include <spot/parseaut/public.hh> 54 #include "spot/priv/accmap.hh" 55 #include <spot/tl/parse.hh> 56 #include <spot/twaalgos/alternation.hh> 60 #ifndef HAVE_STRVERSCMP 62 extern "C" int strverscmp(
const char *s1,
const char *s2);
67 #define PARSE_ERROR_LIST res.h->errors 71 typedef std::map<int, bdd> map_t;
78 typedef std::map<std::string, bdd> formula_cache;
80 typedef std::pair<int, std::string*> pair;
88 enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
90 enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
96 bool declared =
false;
98 spot::location used_loc;
100 spot::parsed_aut_ptr h;
101 spot::twa_ptr aut_or_ks;
103 std::string format_version;
104 spot::location format_version_loc;
106 formula_cache fcache;
107 named_tgba_t* namer =
nullptr;
108 spot::acc_mapper_int* acc_mapper =
nullptr;
110 std::vector<bdd> guards;
111 std::vector<bdd>::const_iterator cur_guard;
121 int unknown_ap_max = -1;
122 spot::location unknown_ap_max_location;
123 bool in_alias =
false;
125 std::vector<state_info> info_states;
126 std::vector<std::pair<spot::location,
127 std::vector<unsigned>>> start;
128 std::unordered_map<std::string, bdd> alias;
133 operator bool()
const 138 std::unordered_map<std::string, prop_info> props;
139 spot::location states_loc;
140 spot::location ap_loc;
141 spot::location state_label_loc;
142 spot::location accset_loc;
148 std::vector<std::string>* state_names =
nullptr;
149 std::map<unsigned, unsigned>* highlight_edges =
nullptr;
150 std::map<unsigned, unsigned>* highlight_states =
nullptr;
151 std::map<unsigned, unsigned> states_map;
152 std::set<int> ap_set;
159 bool has_state_label =
false;
160 bool ignore_more_ap =
false;
162 bool ignore_acc =
false;
164 bool ignore_acc_silent =
false;
165 bool ignore_more_acc =
false;
168 label_style_t label_style = Mixed_Labels;
169 acc_style_t acc_style = Mixed_Acc;
171 bool accept_all_needed =
false;
172 bool accept_all_seen =
false;
173 bool aliased_states =
false;
178 bool trans_acc_seen =
false;
180 std::map<std::string, spot::location> labels;
182 prop_info prop_is_true(
const std::string& p)
184 auto i = props.find(p);
185 if (i == props.end())
186 return prop_info{spot::location(),
false};
190 prop_info prop_is_false(
const std::string& p)
192 auto i = props.find(p);
193 if (i == props.end())
194 return prop_info{spot::location(),
false};
195 return prop_info{i->second.loc, !i->second.val};
206 #line 207 "parseaut.hh" // lalr1.cc:377 211 # include <stdexcept> 219 # if (defined __GNUC__ \ 220 && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \ 221 || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C 222 # define YY_ATTRIBUTE(Spec) __attribute__(Spec) 224 # define YY_ATTRIBUTE(Spec) 228 #ifndef YY_ATTRIBUTE_PURE 229 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__)) 232 #ifndef YY_ATTRIBUTE_UNUSED 233 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__)) 236 #if !defined _Noreturn \ 237 && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112) 238 # if defined _MSC_VER && 1200 <= _MSC_VER 239 # define _Noreturn __declspec (noreturn) 241 # define _Noreturn YY_ATTRIBUTE ((__noreturn__)) 246 #if ! defined lint || defined __GNUC__ 247 # define YYUSE(E) ((void) (E)) 252 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__ 254 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \ 255 _Pragma ("GCC diagnostic push") \ 256 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\ 257 _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"") 258 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \ 259 _Pragma ("GCC diagnostic pop") 261 # define YY_INITIAL_VALUE(Value) Value 263 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN 264 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN 265 # define YY_IGNORE_MAYBE_UNINITIALIZED_END 267 #ifndef YY_INITIAL_VALUE 268 # define YY_INITIAL_VALUE(Value) 278 #line 279 "parseaut.hh" // lalr1.cc:377 292 #line 202 "parseaut.yy" // lalr1.cc:377 299 std::list<pair>* list;
301 std::vector<unsigned>* states;
303 #line 304 "parseaut.hh" // lalr1.cc:377 314 syntax_error (
const location_type& l,
const std::string& m);
315 location_type location;
337 SPOT_HIGHLIGHT_EDGES = 271,
338 SPOT_HIGHLIGHT_STATES = 272,
381 enum { empty_symbol = -2 };
392 template <
typename Base>
406 const location_type& l);
410 const semantic_type& v,
411 const location_type& l);
459 symbol_number_type type_get ()
const;
462 token_type
token ()
const;
475 parser (
void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
480 virtual int parse ();
483 std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
486 void set_debug_stream (
std::ostream &);
491 debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
493 void set_debug_level (debug_level_type l);
499 virtual void error (
const location_type& loc,
const std::string& msg);
510 typedef int state_type;
515 virtual std::string yysyntax_error_ (state_type yystate,
516 const symbol_type& yyla)
const;
521 state_type yy_lr_goto_state_ (state_type yystate,
int yysym);
525 static bool yy_pact_value_is_default_ (
int yyvalue);
529 static bool yy_table_value_is_error_ (
int yyvalue);
531 static const short int yypact_ninf_;
532 static const signed char yytable_ninf_;
535 static token_number_type yytranslate_ (
int t);
540 static const short int yypact_[];
545 static const unsigned char yydefact_[];
548 static const short int yypgoto_[];
551 static const short int yydefgoto_[];
556 static const short int yytable_[];
558 static const short int yycheck_[];
562 static const unsigned char yystos_[];
565 static const unsigned char yyr1_[];
568 static const unsigned char yyr2_[];
572 static std::string yytnamerr_ (
const char *n);
576 static const char*
const yytname_[];
579 static const unsigned short int yyrline_[];
581 virtual void yy_reduce_print_ (
int r);
583 virtual void yystack_print_ ();
587 std::ostream* yycdebug_;
592 template <
typename Base>
600 template <
typename Base>
611 typedef state_type kind_type;
614 by_state (kind_type s);
617 by_state (
const by_state& other);
623 void move (by_state& that);
627 symbol_number_type type_get ()
const;
630 enum { empty_state = -1 };
643 stack_symbol_type ();
645 stack_symbol_type (state_type s, symbol_type& sym);
647 stack_symbol_type& operator= (
const stack_symbol_type& that);
661 void yypush_ (
const char* m, stack_symbol_type& s);
669 void yypush_ (
const char* m, state_type s, symbol_type& sym);
672 void yypop_ (
unsigned int n = 1);
690 spot::location initial_loc;
696 #line 697 "parseaut.hh" // lalr1.cc:377 701 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED Definition: parseaut.hh:92
An environment that describes atomic propositions.
Definition: environment.hh:32
Symbol semantic values.
Definition: parseaut.hh:290
semantic_type value
The semantic value.
Definition: parseaut.hh:426
Syntax errors thrown from user actions.
Definition: parseaut.hh:312
Definition: bitset.hh:405
Definition: parseaut.hh:94
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:375
Definition: parseaut.hh:277
Definition: parseaut.hh:129
Tokens.
Definition: parseaut.hh:319
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:437
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:446
Base super_type
Alias to Base.
Definition: parseaut.hh:396
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:384
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
int type
Definition: parseaut.hh:467
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:471
spot::location location_type
Symbol locations.
Definition: parseaut.hh:309
Definition: parseaut.hh:69
A Bison parser.
Definition: parseaut.hh:285
Definition: parseaut.hh:393
An acceptance formulas.
Definition: acc.hh:444
location_type location
The location.
Definition: parseaut.hh:429
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:378
An acceptance mark.
Definition: acc.hh:81
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:489