spot  2.3.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
parseaut.hh
Go to the documentation of this file.
1 // A Bison parser, made by GNU Bison 3.0.2.
2 
3 // Skeleton interface for Bison LALR(1) parsers in C++
4 
5 // Copyright (C) 2002-2013 Free Software Foundation, Inc.
6 
7 // This program is free software: you can redistribute it and/or modify
8 // it under the terms of the GNU General Public License as published by
9 // the Free Software Foundation, either version 3 of the License, or
10 // (at your option) any later version.
11 
12 // This program is distributed in the hope that it will be useful,
13 // but WITHOUT ANY WARRANTY; without even the implied warranty of
14 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 // GNU General Public License for more details.
16 
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 // As a special exception, you may create a larger work that contains
21 // part or all of the Bison parser skeleton and distribute that work
22 // under terms of your choice, so long as that work isn't itself a
23 // parser generator using the skeleton or a modified version thereof
24 // as a parser skeleton. Alternatively, if you modify or redistribute
25 // the parser skeleton itself, you may (at your option) remove this
26 // special exception, which will cause the skeleton and the resulting
27 // Bison output files to be licensed under the GNU General Public
28 // License without this special exception.
29 
30 // This special exception was added by the Free Software Foundation in
31 // version 2.2 of Bison.
32 
38 // C++ LALR(1) parser skeleton written by Akim Demaille.
39 
40 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
41 # define YY_HOAYY_PARSEAUT_HH_INCLUDED
42 // // "%code requires" blocks.
43 #line 31 "parseaut.yy" // lalr1.cc:372
44 
45 #include "config.h"
46 #include <spot/misc/common.hh>
47 #include <string>
48 #include <cstring>
49 #include <sstream>
50 #include <unordered_map>
51 #include <algorithm>
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>
57 
58 #ifndef HAVE_STRVERSCMP
59 // If the libc does not have this, a version is compiled in lib/.
60 extern "C" int strverscmp(const char *s1, const char *s2);
61 #endif
62 
63 // Work around Bison not letting us write
64 // %lex-param { res.h->errors }
65 #define PARSE_ERROR_LIST res.h->errors
66 
67  inline namespace hoayy_support
68  {
69  typedef std::map<int, bdd> map_t;
70 
71  /* Cache parsed formulae. Labels on arcs are frequently identical
72  and it would be a waste of time to parse them to formula
73  over and over, and to register all their atomic_propositions in
74  the bdd_dict. Keep the bdd result around so we can reuse
75  it. */
76  typedef std::map<std::string, bdd> formula_cache;
77 
78  typedef std::pair<int, std::string*> pair;
79  typedef spot::twa_graph::namer<std::string> named_tgba_t;
80 
81  // Note: because this parser is meant to be used on a stream of
82  // automata, it tries hard to recover from errors, so that we get a
83  // chance to reach the end of the current automaton in order to
84  // process the next one. Several variables below are used to keep
85  // track of various error conditions.
86  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
87  Implicit_Labels };
88  enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
89 
90  struct result_
91  {
92  struct state_info
93  {
94  bool declared = false;
95  bool used = false;
96  spot::location used_loc;
97  };
98  spot::parsed_aut_ptr h;
99  spot::twa_ptr aut_or_ks;
101  std::string format_version;
102  spot::location format_version_loc;
103  spot::environment* env;
104  formula_cache fcache;
105  named_tgba_t* namer = nullptr;
106  spot::acc_mapper_int* acc_mapper = nullptr;
107  std::vector<int> ap;
108  std::vector<bdd> guards;
109  std::vector<bdd>::const_iterator cur_guard;
110  map_t dest_map;
111  std::vector<state_info> info_states; // States declared and used.
112  std::vector<std::pair<spot::location,
113  std::vector<unsigned>>> start; // Initial states;
114  std::unordered_map<std::string, bdd> alias;
115  struct prop_info
116  {
117  spot::location loc;
118  bool val;
119  operator bool() const
120  {
121  return val;
122  };
123  };
124  std::unordered_map<std::string, prop_info> props;
125  spot::location states_loc;
126  spot::location ap_loc;
127  spot::location state_label_loc;
128  spot::location accset_loc;
129  spot::acc_cond::mark_t acc_state;
130  spot::acc_cond::mark_t neg_acc_sets = 0U;
131  spot::acc_cond::mark_t pos_acc_sets = 0U;
132  int plus;
133  int minus;
134  std::vector<std::string>* state_names = nullptr;
135  std::map<unsigned, unsigned>* highlight_edges = nullptr;
136  std::map<unsigned, unsigned>* highlight_states = nullptr;
137  std::map<unsigned, unsigned> states_map;
138  std::set<int> ap_set;
139  unsigned cur_state;
140  int states = -1;
141  int ap_count = -1;
142  int accset = -1;
143  bdd state_label;
144  bdd cur_label;
145  bool has_state_label = false;
146  bool ignore_more_ap = false; // Set to true after the first "AP:"
147  // line has been read.
148  bool ignore_acc = false; // Set to true in case of missing
149  // Acceptance: lines.
150  bool ignore_acc_silent = false;
151  bool ignore_more_acc = false; // Set to true after the first
152  // "Acceptance:" line has been read.
153 
154  label_style_t label_style = Mixed_Labels;
155  acc_style_t acc_style = Mixed_Acc;
156 
157  bool accept_all_needed = false;
158  bool accept_all_seen = false;
159  bool aliased_states = false;
160 
161  spot::trival deterministic = spot::trival::maybe();
162  bool complete = false;
163  bool trans_acc_seen = false;
164 
165  std::map<std::string, spot::location> labels;
166 
167  prop_info prop_is_true(const std::string& p)
168  {
169  auto i = props.find(p);
170  if (i == props.end())
171  return prop_info{spot::location(), false};
172  return i->second;
173  }
174 
175  prop_info prop_is_false(const std::string& p)
176  {
177  auto i = props.find(p);
178  if (i == props.end())
179  return prop_info{spot::location(), false};
180  return prop_info{i->second.loc, !i->second.val};
181  }
182 
183  ~result_()
184  {
185  delete namer;
186  delete acc_mapper;
187  }
188  };
189  }
190 
191 #line 192 "parseaut.hh" // lalr1.cc:372
192 
193 
194 # include <vector>
195 # include <iostream>
196 # include <stdexcept>
197 # include <string>
198 # include "stack.hh"
199 
200 
201 
202 #ifndef YY_ATTRIBUTE
203 # if (defined __GNUC__ \
204  && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \
205  || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C
206 # define YY_ATTRIBUTE(Spec) __attribute__(Spec)
207 # else
208 # define YY_ATTRIBUTE(Spec) /* empty */
209 # endif
210 #endif
211 
212 #ifndef YY_ATTRIBUTE_PURE
213 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__))
214 #endif
215 
216 #ifndef YY_ATTRIBUTE_UNUSED
217 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__))
218 #endif
219 
220 #if !defined _Noreturn \
221  && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112)
222 # if defined _MSC_VER && 1200 <= _MSC_VER
223 # define _Noreturn __declspec (noreturn)
224 # else
225 # define _Noreturn YY_ATTRIBUTE ((__noreturn__))
226 # endif
227 #endif
228 
229 /* Suppress unused-variable warnings by "using" E. */
230 #if ! defined lint || defined __GNUC__
231 # define YYUSE(E) ((void) (E))
232 #else
233 # define YYUSE(E) /* empty */
234 #endif
235 
236 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
237 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
238 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
239  _Pragma ("GCC diagnostic push") \
240  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
241  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
242 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
243  _Pragma ("GCC diagnostic pop")
244 #else
245 # define YY_INITIAL_VALUE(Value) Value
246 #endif
247 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
248 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
249 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
250 #endif
251 #ifndef YY_INITIAL_VALUE
252 # define YY_INITIAL_VALUE(Value) /* Nothing. */
253 #endif
254 
255 /* Debug traces. */
256 #ifndef YYDEBUG
257 # define YYDEBUG 1
258 #endif
259 
260 
261 namespace hoayy {
262 #line 263 "parseaut.hh" // lalr1.cc:372
263 
264 
265 
266 
267 
269  class parser
270  {
271  public:
272 #ifndef YYSTYPE
273  union semantic_type
275  {
276  #line 185 "parseaut.yy" // lalr1.cc:372
277 
278  std::string* str;
279  unsigned int num;
280  int b;
282  pair* p;
283  std::list<pair>* list;
285  std::vector<unsigned>* states;
286 
287 #line 288 "parseaut.hh" // lalr1.cc:372
288  };
289 #else
290  typedef YYSTYPE semantic_type;
291 #endif
292  typedef spot::location location_type;
294 
296  struct syntax_error : std::runtime_error
297  {
298  syntax_error (const location_type& l, const std::string& m);
299  location_type location;
300  };
301 
303  struct token
304  {
305  enum yytokentype
306  {
307  ENDOFFILE = 0,
308  HOA = 258,
309  STATES = 259,
310  START = 260,
311  AP = 261,
312  ALIAS = 262,
313  ACCEPTANCE = 263,
314  ACCNAME = 264,
315  TOOL = 265,
316  NAME = 266,
317  PROPERTIES = 267,
318  BODY = 268,
319  END = 269,
320  STATE = 270,
321  SPOT_HIGHLIGHT_EDGES = 271,
322  SPOT_HIGHLIGHT_STATES = 272,
323  IDENTIFIER = 273,
324  HEADERNAME = 274,
325  ANAME = 275,
326  STRING = 276,
327  INT = 277,
328  DRA = 278,
329  DSA = 279,
330  V2 = 280,
331  EXPLICIT = 281,
332  ACCPAIRS = 282,
333  ACCSIG = 283,
334  ENDOFHEADER = 284,
335  NEVER = 285,
336  SKIP = 286,
337  IF = 287,
338  FI = 288,
339  DO = 289,
340  OD = 290,
341  ARROW = 291,
342  GOTO = 292,
343  FALSE = 293,
344  ATOMIC = 294,
345  ASSERT = 295,
346  FORMULA = 296,
347  ENDAUT = 297,
348  ENDDSTAR = 298,
349  LBTT = 299,
350  INT_S = 300,
351  LBTT_EMPTY = 301,
352  ACC = 302,
353  STATE_NUM = 303,
354  DEST_NUM = 304
355  };
356  };
357 
359  typedef token::yytokentype token_type;
360 
362  typedef int symbol_number_type;
363 
365  typedef unsigned char token_number_type;
366 
373  template <typename Base>
374  struct basic_symbol : Base
375  {
377  typedef Base super_type;
378 
380  basic_symbol ();
381 
383  basic_symbol (const basic_symbol& other);
384 
386  basic_symbol (typename Base::kind_type t,
387  const location_type& l);
388 
390  basic_symbol (typename Base::kind_type t,
391  const semantic_type& v,
392  const location_type& l);
393 
394  ~basic_symbol ();
395 
397  void move (basic_symbol& s);
398 
400  semantic_type value;
401 
403  location_type location;
404 
405  private:
407  basic_symbol& operator= (const basic_symbol& other);
408  };
409 
411  struct by_type
412  {
414  by_type ();
415 
417  by_type (const by_type& other);
418 
420  typedef token_type kind_type;
421 
423  by_type (kind_type t);
424 
426  void move (by_type& that);
427 
430  symbol_number_type type_get () const;
431 
433  token_type token () const;
434 
435  enum { empty = 0 };
436 
439  token_number_type type;
440  };
441 
444 
445 
447  parser (result_& res_yyarg, spot::location initial_loc_yyarg);
448  virtual ~parser ();
449 
452  virtual int parse ();
453 
454 #if YYDEBUG
455  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
458  void set_debug_stream (std::ostream &);
459 
461  typedef int debug_level_type;
463  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
465  void set_debug_level (debug_level_type l);
466 #endif
467 
471  virtual void error (const location_type& loc, const std::string& msg);
472 
474  void error (const syntax_error& err);
475 
476  private:
478  parser (const parser&);
479  parser& operator= (const parser&);
480 
482  typedef int state_type;
483 
487  virtual std::string yysyntax_error_ (state_type yystate,
488  symbol_number_type yytoken) const;
489 
493  state_type yy_lr_goto_state_ (state_type yystate, int yysym);
494 
497  static bool yy_pact_value_is_default_ (int yyvalue);
498 
501  static bool yy_table_value_is_error_ (int yyvalue);
502 
503  static const short int yypact_ninf_;
504  static const signed char yytable_ninf_;
505 
507  static token_number_type yytranslate_ (int t);
508 
509  // Tables.
510  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
511  // STATE-NUM.
512  static const short int yypact_[];
513 
514  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
515  // Performed when YYTABLE does not specify something else to do. Zero
516  // means the default is an error.
517  static const unsigned char yydefact_[];
518 
519  // YYPGOTO[NTERM-NUM].
520  static const short int yypgoto_[];
521 
522  // YYDEFGOTO[NTERM-NUM].
523  static const short int yydefgoto_[];
524 
525  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
526  // positive, shift that token. If negative, reduce the rule whose
527  // number is the opposite. If YYTABLE_NINF, syntax error.
528  static const short int yytable_[];
529 
530  static const short int yycheck_[];
531 
532  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
533  // symbol of state STATE-NUM.
534  static const unsigned char yystos_[];
535 
536  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
537  static const unsigned char yyr1_[];
538 
539  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
540  static const unsigned char yyr2_[];
541 
542 
544  static std::string yytnamerr_ (const char *n);
545 
546 
548  static const char* const yytname_[];
549 #if YYDEBUG
550  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
551  static const unsigned short int yyrline_[];
553  virtual void yy_reduce_print_ (int r);
555  virtual void yystack_print_ ();
556 
557  // Debugging.
558  int yydebug_;
559  std::ostream* yycdebug_;
560 
564  template <typename Base>
565  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
566 #endif
567 
572  template <typename Base>
573  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
574 
575  private:
577  struct by_state
578  {
580  by_state ();
581 
583  typedef state_type kind_type;
584 
586  by_state (kind_type s);
587 
589  by_state (const by_state& other);
590 
592  void move (by_state& that);
593 
596  symbol_number_type type_get () const;
597 
598  enum { empty = 0 };
599 
601  state_type state;
602  };
603 
605  struct stack_symbol_type : basic_symbol<by_state>
606  {
608  typedef basic_symbol<by_state> super_type;
610  stack_symbol_type ();
612  stack_symbol_type (state_type s, symbol_type& sym);
614  stack_symbol_type& operator= (const stack_symbol_type& that);
615  };
616 
618  typedef stack<stack_symbol_type> stack_type;
619 
621  stack_type yystack_;
622 
628  void yypush_ (const char* m, stack_symbol_type& s);
629 
636  void yypush_ (const char* m, state_type s, symbol_type& sym);
637 
639  void yypop_ (unsigned int n = 1);
640 
641  // Constants.
642  enum
643  {
644  yyeof_ = 0,
645  yylast_ = 235,
646  yynnts_ = 82,
647  yyempty_ = -2,
648  yyfinal_ = 24,
649  yyterror_ = 1,
650  yyerrcode_ = 256,
651  yyntokens_ = 65
652  };
653 
654 
655  // User arguments.
656  result_& res;
657  spot::location initial_loc;
658  };
659 
660 
661 
662 } // hoayy
663 #line 664 "parseaut.hh" // lalr1.cc:372
664 
665 
666 
667 
668 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
token_number_type type
Definition: parseaut.hh:439
void move(by_type &that)
Steal the symbol type from that.
debug_level_type debug_level() const
The current debugging level.
Definition: parseaut.hh:90
An environment that describes atomic propositions.
Definition: environment.hh:32
Symbol semantic values.
Definition: parseaut.hh:274
semantic_type value
The semantic value.
Definition: parseaut.hh:400
void move(basic_symbol &s)
Destructive move, s is emptied into this.
Syntax errors thrown from user actions.
Definition: parseaut.hh:296
void set_debug_level(debug_level_type l)
Set the current debugging level.
Definition: formula.hh:1671
Definition: parseaut.hh:92
virtual void error(const location_type &loc, const std::string &msg)
token_type token() const
The token.
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:359
Definition: parseaut.hh:261
virtual int parse()
Definition: public.hh:92
Definition: parseaut.hh:115
Tokens.
Definition: parseaut.hh:303
std::ostream & debug_stream() const
The current debugging stream.
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:411
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:420
Base super_type
Alias to Base.
Definition: parseaut.hh:377
symbol_number_type type_get() const
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:365
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:443
basic_symbol()
Default constructor.
spot::location location_type
Symbol locations.
Definition: parseaut.hh:293
Definition: parseaut.hh:67
A Bison parser.
Definition: parseaut.hh:269
parser(result_ &res_yyarg, spot::location initial_loc_yyarg)
Build a parser object.
Definition: parseaut.hh:374
void set_debug_stream(std::ostream &)
Set the current debugging stream.
by_type()
Default constructor.
Definition: acc.hh:300
location_type location
The location.
Definition: parseaut.hh:403
int symbol_number_type
Internal symbol number.
Definition: parseaut.hh:362
Definition: acc.hh:34
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:461

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Feb 20 2017 07:08:25 for spot by doxygen 1.8.8