40 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED 41 # define YY_HOAYY_PARSEAUT_HH_INCLUDED 43 #line 32 "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> 58 #ifndef HAVE_STRVERSCMP 60 extern "C" int strverscmp(
const char *s1,
const char *s2);
65 #define PARSE_ERROR_LIST res.h->errors 69 typedef std::map<int, bdd> map_t;
76 typedef std::map<std::string, bdd> formula_cache;
78 typedef std::pair<int, std::string*> pair;
86 enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
88 enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
94 bool declared =
false;
96 spot::location used_loc;
98 spot::parsed_aut_ptr h;
99 spot::twa_ptr aut_or_ks;
101 std::string format_version;
102 spot::location format_version_loc;
104 formula_cache fcache;
105 named_tgba_t* namer =
nullptr;
106 spot::acc_mapper_int* acc_mapper =
nullptr;
108 std::vector<bdd> guards;
109 std::vector<bdd>::const_iterator cur_guard;
119 int unknown_ap_max = -1;
120 spot::location unknown_ap_max_location;
121 bool in_alias =
false;
123 std::vector<state_info> info_states;
124 std::vector<std::pair<spot::location,
125 std::vector<unsigned>>> start;
126 std::unordered_map<std::string, bdd> alias;
131 operator bool()
const 136 std::unordered_map<std::string, prop_info> props;
137 spot::location states_loc;
138 spot::location ap_loc;
139 spot::location state_label_loc;
140 spot::location accset_loc;
146 std::vector<std::string>* state_names =
nullptr;
147 std::map<unsigned, unsigned>* highlight_edges =
nullptr;
148 std::map<unsigned, unsigned>* highlight_states =
nullptr;
149 std::map<unsigned, unsigned> states_map;
150 std::set<int> ap_set;
157 bool has_state_label =
false;
158 bool ignore_more_ap =
false;
160 bool ignore_acc =
false;
162 bool ignore_acc_silent =
false;
163 bool ignore_more_acc =
false;
166 label_style_t label_style = Mixed_Labels;
167 acc_style_t acc_style = Mixed_Acc;
169 bool accept_all_needed =
false;
170 bool accept_all_seen =
false;
171 bool aliased_states =
false;
176 bool trans_acc_seen =
false;
178 std::map<std::string, spot::location> labels;
180 prop_info prop_is_true(
const std::string& p)
182 auto i = props.find(p);
183 if (i == props.end())
184 return prop_info{spot::location(),
false};
188 prop_info prop_is_false(
const std::string& p)
190 auto i = props.find(p);
191 if (i == props.end())
192 return prop_info{spot::location(),
false};
193 return prop_info{i->second.loc, !i->second.val};
204 #line 205 "parseaut.hh" // lalr1.cc:377 209 # include <stdexcept> 217 # if (defined __GNUC__ \ 218 && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \ 219 || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C 220 # define YY_ATTRIBUTE(Spec) __attribute__(Spec) 222 # define YY_ATTRIBUTE(Spec) 226 #ifndef YY_ATTRIBUTE_PURE 227 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__)) 230 #ifndef YY_ATTRIBUTE_UNUSED 231 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__)) 234 #if !defined _Noreturn \ 235 && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112) 236 # if defined _MSC_VER && 1200 <= _MSC_VER 237 # define _Noreturn __declspec (noreturn) 239 # define _Noreturn YY_ATTRIBUTE ((__noreturn__)) 244 #if ! defined lint || defined __GNUC__ 245 # define YYUSE(E) ((void) (E)) 250 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__ 252 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \ 253 _Pragma ("GCC diagnostic push") \ 254 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\ 255 _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"") 256 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \ 257 _Pragma ("GCC diagnostic pop") 259 # define YY_INITIAL_VALUE(Value) Value 261 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN 262 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN 263 # define YY_IGNORE_MAYBE_UNINITIALIZED_END 265 #ifndef YY_INITIAL_VALUE 266 # define YY_INITIAL_VALUE(Value) 276 #line 277 "parseaut.hh" // lalr1.cc:377 290 #line 199 "parseaut.yy" // lalr1.cc:377 297 std::list<pair>* list;
299 std::vector<unsigned>* states;
301 #line 302 "parseaut.hh" // lalr1.cc:377 312 syntax_error (
const location_type& l,
const std::string& m);
313 location_type location;
335 SPOT_HIGHLIGHT_EDGES = 271,
336 SPOT_HIGHLIGHT_STATES = 272,
379 enum { empty_symbol = -2 };
390 template <
typename Base>
404 const location_type& l);
408 const semantic_type& v,
409 const location_type& l);
457 symbol_number_type type_get ()
const;
460 token_type
token ()
const;
473 parser (
void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
478 virtual int parse ();
481 std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
484 void set_debug_stream (
std::ostream &);
489 debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
491 void set_debug_level (debug_level_type l);
497 virtual void error (
const location_type& loc,
const std::string& msg);
508 typedef int state_type;
513 virtual std::string yysyntax_error_ (state_type yystate,
514 const symbol_type& yyla)
const;
519 state_type yy_lr_goto_state_ (state_type yystate,
int yysym);
523 static bool yy_pact_value_is_default_ (
int yyvalue);
527 static bool yy_table_value_is_error_ (
int yyvalue);
529 static const short int yypact_ninf_;
530 static const signed char yytable_ninf_;
533 static token_number_type yytranslate_ (
int t);
538 static const short int yypact_[];
543 static const unsigned char yydefact_[];
546 static const short int yypgoto_[];
549 static const short int yydefgoto_[];
554 static const short int yytable_[];
556 static const short int yycheck_[];
560 static const unsigned char yystos_[];
563 static const unsigned char yyr1_[];
566 static const unsigned char yyr2_[];
570 static std::string yytnamerr_ (
const char *n);
574 static const char*
const yytname_[];
577 static const unsigned short int yyrline_[];
579 virtual void yy_reduce_print_ (
int r);
581 virtual void yystack_print_ ();
585 std::ostream* yycdebug_;
590 template <
typename Base>
598 template <
typename Base>
609 typedef state_type kind_type;
612 by_state (kind_type s);
615 by_state (
const by_state& other);
621 void move (by_state& that);
625 symbol_number_type type_get ()
const;
628 enum { empty_state = -1 };
641 stack_symbol_type ();
643 stack_symbol_type (state_type s, symbol_type& sym);
645 stack_symbol_type& operator= (
const stack_symbol_type& that);
659 void yypush_ (
const char* m, stack_symbol_type& s);
667 void yypush_ (
const char* m, state_type s, symbol_type& sym);
670 void yypop_ (
unsigned int n = 1);
688 spot::location initial_loc;
694 #line 695 "parseaut.hh" // lalr1.cc:377 699 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED Definition: parseaut.hh:90
An environment that describes atomic propositions.
Definition: environment.hh:32
Symbol semantic values.
Definition: parseaut.hh:288
semantic_type value
The semantic value.
Definition: parseaut.hh:424
Syntax errors thrown from user actions.
Definition: parseaut.hh:310
Definition: bitset.hh:405
Definition: parseaut.hh:92
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:373
Definition: parseaut.hh:275
Definition: parseaut.hh:127
Tokens.
Definition: parseaut.hh:317
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:435
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:444
Base super_type
Alias to Base.
Definition: parseaut.hh:394
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:382
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
int type
Definition: parseaut.hh:465
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:469
spot::location location_type
Symbol locations.
Definition: parseaut.hh:307
Definition: parseaut.hh:67
A Bison parser.
Definition: parseaut.hh:283
Definition: parseaut.hh:391
location_type location
The location.
Definition: parseaut.hh:427
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:376
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:487