spot 2.12.2
parseaut.hh
Go to the documentation of this file.
1// A Bison parser, made by GNU Bison 3.8.2.
2
3// Skeleton interface for Bison LALR(1) parsers in C++
4
5// Copyright (C) 2002-2015, 2018-2021 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 <https://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
33
39// C++ LALR(1) parser skeleton written by Akim Demaille.
40
41// DO NOT RELY ON FEATURES THAT ARE NOT DOCUMENTED in the manual,
42// especially those whose name start with YY_ or yy_. They are
43// private implementation details that can be changed or removed.
44
45#ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
46# define YY_HOAYY_PARSEAUT_HH_INCLUDED
47// "%code requires" blocks.
48#line 32 "parseaut.yy"
49
50#include "config.h"
51#include <spot/misc/common.hh>
52#include <spot/priv/robin_hood.hh>
53#include <string>
54#include <cstring>
55#include <sstream>
56#include <unordered_map>
57#include <algorithm>
58#include <spot/twa/formula2bdd.hh>
59#include <spot/parseaut/public.hh>
60#include "spot/priv/accmap.hh"
61#include <spot/tl/parse.hh>
62#include <spot/twaalgos/alternation.hh>
63#include <spot/twaalgos/game.hh>
64
65using namespace std::string_literals;
66
67#ifndef HAVE_STRVERSCMP
68// If the libc does not have this, a version is compiled in lib/.
69extern "C" int strverscmp(const char *s1, const char *s2);
70#endif
71
72// Work around Bison not letting us write
73// %lex-param { res.h->errors, res.fcache }
74#define PARSE_ERROR_LIST res.h->errors, res.fcache
75
76 inline namespace hoayy_support
77 {
78 typedef std::map<int, bdd> map_t;
79
80 /* Cache parsed formulae. Labels on arcs are frequently identical
81 and it would be a waste of time to parse them to formula
82 over and over, and to register all their atomic_propositions in
83 the bdd_dict. Keep the bdd result around so we can reuse
84 it. */
85 typedef robin_hood::unordered_flat_map<std::string, bdd> formula_cache;
86
87 typedef std::pair<int, std::string*> pair;
88 typedef spot::twa_graph::namer<std::string> named_tgba_t;
89
90 // Note: because this parser is meant to be used on a stream of
91 // automata, it tries hard to recover from errors, so that we get a
92 // chance to reach the end of the current automaton in order to
93 // process the next one. Several variables below are used to keep
94 // track of various error conditions.
95 enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
96 Implicit_Labels };
97 enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
98
99 struct result_
100 {
102 {
103 bool declared = false;
104 bool used = false;
105 spot::location used_loc;
106 };
107 spot::parsed_aut_ptr h;
108 spot::twa_ptr aut_or_ks;
110 std::string format_version;
111 spot::location format_version_loc;
113 formula_cache fcache;
114 named_tgba_t* namer = nullptr;
115 spot::acc_mapper_int* acc_mapper = nullptr;
116 std::vector<int> ap;
117 std::vector<int> controllable_ap;
118 bool has_controllable_ap = false;
119 std::vector<spot::location> controllable_ap_loc;
120 spot::location controllable_aps_loc;
121 std::vector<bdd> guards;
122 std::vector<bdd>::const_iterator cur_guard;
123 // If "Alias: ..." occurs before "AP: ..." in the HOA format we
124 // are in trouble because the parser would like to turn each
125 // alias into a BDD, yet the atomic proposition have not been
126 // declared yet. We solve that by using arbitrary BDD variables
127 // numbers (in fact we use the same number given in the Alias:
128 // definition) and keeping track of the highest variable number
129 // we have seen (unknown_ap_max). Once AP: is encountered,
130 // we can remap everything. If AP: is never encountered an
131 // unknown_ap_max is non-negative, then we can signal an error.
132 int unknown_ap_max = -1;
133 spot::location unknown_ap_max_location;
134 bool in_alias = false;
135 map_t dest_map;
136 std::vector<state_info> info_states; // States declared and used.
137 // Mapping of edges in the HOA file to edges in the automaton.
138 // Edges are counted from 0 in the HOA file and from 1 in the
139 // automaton. Given edge #i in the HOA file, edge_map[i] gives
140 // corresponding edge in the automaton, or 0 if that edge was
141 // removed (because labeled by bddfalse). This map is used to
142 // update properties such as highlight_edges after the automaton
143 // has been read. Note that the parser may also introduce
144 // unlisted edges, e.g., a bddfalse self-loop to hold the
145 // acceptance of a state without declared outgoing edge. Those
146 // added edges are not a concern for this edge_map.
147 std::vector<unsigned> edge_map;
148 std::vector<std::pair<spot::location,
149 std::vector<unsigned>>> start; // Initial states;
150 std::unordered_map<std::string, bdd> alias;
151 std::vector<std::string> alias_order;
153 {
154 spot::location loc;
155 bool val;
156 operator bool() const
157 {
158 return val;
159 };
160 };
161 std::unordered_map<std::string, prop_info> props;
162 spot::location states_loc;
163 spot::location ap_loc;
164 spot::location state_label_loc;
165 spot::location accset_loc;
166 spot::acc_cond::mark_t acc_state;
167 spot::acc_cond::mark_t neg_acc_sets = {};
168 spot::acc_cond::mark_t pos_acc_sets = {};
169 int plus;
170 int minus;
171 std::vector<std::string>* state_names = nullptr;
172 std::map<unsigned, unsigned>* highlight_edges = nullptr;
173 std::map<unsigned, unsigned>* highlight_states = nullptr;
174 std::map<unsigned, unsigned> states_map;
175 std::vector<bool>* state_player = nullptr;
176 spot::location state_player_loc;
177 std::set<int> ap_set;
178 unsigned cur_state;
179 int states = -1;
180 int ap_count = -1;
181 int accset = -1;
182 bdd state_label;
183 bdd cur_label;
184 bool has_state_label = false;
185 bool ignore_more_ap = false; // Set to true after the first "AP:"
186 // line has been read.
187 bool ignore_acc = false; // Set to true in case of missing
188 // Acceptance: lines.
189 bool ignore_acc_silent = false;
190 bool ignore_more_acc = false; // Set to true after the first
191 // "Acceptance:" line has been read.
192
193 label_style_t label_style = Mixed_Labels;
194 acc_style_t acc_style = Mixed_Acc;
195
196 bool accept_all_needed = false;
197 bool accept_all_seen = false;
198 bool aliased_states = false;
199
200 spot::trival universal = spot::trival::maybe();
201 spot::trival existential = spot::trival::maybe();
202 spot::trival complete = spot::trival::maybe();
203 bool trans_acc_seen = false;
204
205 std::map<std::string, spot::location> labels;
206
207 prop_info prop_is_true(const std::string& p)
208 {
209 auto i = props.find(p);
210 if (i == props.end())
211 return prop_info{spot::location(), false};
212 return i->second;
213 }
214
215 prop_info prop_is_false(const std::string& p)
216 {
217 auto i = props.find(p);
218 if (i == props.end())
219 return prop_info{spot::location(), false};
220 return prop_info{i->second.loc, !i->second.val};
221 }
222
223 ~result_()
224 {
225 delete namer;
226 delete acc_mapper;
227 }
228 };
229 }
230
231#line 232 "parseaut.hh"
232
233
234# include <cstdlib> // std::abort
235# include <iostream>
236# include <stdexcept>
237# include <string>
238# include <vector>
239
240#if defined __cplusplus
241# define YY_CPLUSPLUS __cplusplus
242#else
243# define YY_CPLUSPLUS 199711L
244#endif
245
246// Support move semantics when possible.
247#if 201103L <= YY_CPLUSPLUS
248# define YY_MOVE std::move
249# define YY_MOVE_OR_COPY move
250# define YY_MOVE_REF(Type) Type&&
251# define YY_RVREF(Type) Type&&
252# define YY_COPY(Type) Type
253#else
254# define YY_MOVE
255# define YY_MOVE_OR_COPY copy
256# define YY_MOVE_REF(Type) Type&
257# define YY_RVREF(Type) const Type&
258# define YY_COPY(Type) const Type&
259#endif
260
261// Support noexcept when possible.
262#if 201103L <= YY_CPLUSPLUS
263# define YY_NOEXCEPT noexcept
264# define YY_NOTHROW
265#else
266# define YY_NOEXCEPT
267# define YY_NOTHROW throw ()
268#endif
269
270// Support constexpr when possible.
271#if 201703 <= YY_CPLUSPLUS
272# define YY_CONSTEXPR constexpr
273#else
274# define YY_CONSTEXPR
275#endif
276
277
278
279#ifndef YY_ATTRIBUTE_PURE
280# if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
281# define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
282# else
283# define YY_ATTRIBUTE_PURE
284# endif
285#endif
286
287#ifndef YY_ATTRIBUTE_UNUSED
288# if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
289# define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
290# else
291# define YY_ATTRIBUTE_UNUSED
292# endif
293#endif
294
295/* Suppress unused-variable warnings by "using" E. */
296#if ! defined lint || defined __GNUC__
297# define YY_USE(E) ((void) (E))
298#else
299# define YY_USE(E) /* empty */
300#endif
301
302/* Suppress an incorrect diagnostic about yylval being uninitialized. */
303#if defined __GNUC__ && ! defined __ICC && 406 <= __GNUC__ * 100 + __GNUC_MINOR__
304# if __GNUC__ * 100 + __GNUC_MINOR__ < 407
305# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
306 _Pragma ("GCC diagnostic push") \
307 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")
308# else
309# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
310 _Pragma ("GCC diagnostic push") \
311 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
312 _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
313# endif
314# define YY_IGNORE_MAYBE_UNINITIALIZED_END \
315 _Pragma ("GCC diagnostic pop")
316#else
317# define YY_INITIAL_VALUE(Value) Value
318#endif
319#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
320# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
321# define YY_IGNORE_MAYBE_UNINITIALIZED_END
322#endif
323#ifndef YY_INITIAL_VALUE
324# define YY_INITIAL_VALUE(Value) /* Nothing. */
325#endif
326
327#if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
328# define YY_IGNORE_USELESS_CAST_BEGIN \
329 _Pragma ("GCC diagnostic push") \
330 _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
331# define YY_IGNORE_USELESS_CAST_END \
332 _Pragma ("GCC diagnostic pop")
333#endif
334#ifndef YY_IGNORE_USELESS_CAST_BEGIN
335# define YY_IGNORE_USELESS_CAST_BEGIN
336# define YY_IGNORE_USELESS_CAST_END
337#endif
338
339# ifndef YY_CAST
340# ifdef __cplusplus
341# define YY_CAST(Type, Val) static_cast<Type> (Val)
342# define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
343# else
344# define YY_CAST(Type, Val) ((Type) (Val))
345# define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
346# endif
347# endif
348# ifndef YY_NULLPTR
349# if defined __cplusplus
350# if 201103L <= __cplusplus
351# define YY_NULLPTR nullptr
352# else
353# define YY_NULLPTR 0
354# endif
355# else
356# define YY_NULLPTR ((void*)0)
357# endif
358# endif
359
360/* Debug traces. */
361#ifndef HOAYYDEBUG
362# if defined YYDEBUG
363#if YYDEBUG
364# define HOAYYDEBUG 1
365# else
366# define HOAYYDEBUG 0
367# endif
368# else /* ! defined YYDEBUG */
369# define HOAYYDEBUG 1
370# endif /* ! defined YYDEBUG */
371#endif /* ! defined HOAYYDEBUG */
372
373namespace hoayy {
374#line 375 "parseaut.hh"
375
376
377
378
380 class parser
381 {
382 public:
383#ifdef HOAYYSTYPE
384# ifdef __GNUC__
385# pragma GCC message "bison: do not #define HOAYYSTYPE in C++, use %define api.value.type"
386# endif
387 typedef HOAYYSTYPE value_type;
388#else
391 {
392#line 221 "parseaut.yy"
393
394 std::string* str;
395 unsigned int num;
396 int b;
398 pair* p;
399 std::list<pair>* list;
401 std::vector<unsigned>* states;
402
403#line 404 "parseaut.hh"
404
405 };
406#endif
409
411 typedef spot::location location_type;
412
414 struct syntax_error : std::runtime_error
415 {
416 syntax_error (const location_type& l, const std::string& m)
417 : std::runtime_error (m)
418 , location (l)
419 {}
420
421 syntax_error (const syntax_error& s)
422 : std::runtime_error (s.what ())
423 , location (s.location)
424 {}
425
426 ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
427
428 location_type location;
429 };
430
432 struct token
433 {
434 enum token_kind_type
435 {
436 HOAYYEMPTY = -2,
437 ENDOFFILE = 0, // "end of file"
438 HOAYYerror = 256, // error
439 HOAYYUNDEF = 257, // "invalid token"
440 HOA = 258, // "HOA:"
441 STATES = 259, // "States:"
442 START = 260, // "Start:"
443 AP = 261, // "AP:"
444 ALIAS = 262, // "Alias:"
445 ACCEPTANCE = 263, // "Acceptance:"
446 ACCNAME = 264, // "acc-name:"
447 CONTROLLABLE_AP = 265, // "controllable-AP:"
448 TOOL = 266, // "tool:"
449 NAME = 267, // "name:"
450 PROPERTIES = 268, // "properties:"
451 BODY = 269, // "--BODY--"
452 END = 270, // "--END--"
453 STATE = 271, // "State:"
454 SPOT_HIGHLIGHT_EDGES = 272, // "spot.highlight.edges:"
455 SPOT_HIGHLIGHT_STATES = 273, // "spot.highlight.states:"
456 SPOT_STATE_PLAYER = 274, // "spot.state-player:"
457 IDENTIFIER = 275, // "identifier"
458 HEADERNAME = 276, // "header name"
459 ANAME = 277, // "alias name"
460 STRING = 278, // "string"
461 INT = 279, // "integer"
462 LINEDIRECTIVE = 280, // "#line"
463 BDD = 281, // BDD
464 ENDDSTAR = 282, // "end of DSTAR automaton"
465 DRA = 283, // "DRA"
466 DSA = 284, // "DSA"
467 V2 = 285, // "v2"
468 EXPLICIT = 286, // "explicit"
469 ACCPAIRS = 287, // "Acceptance-Pairs:"
470 ACCSIG = 288, // "Acc-Sig:"
471 ENDOFHEADER = 289, // "---"
472 NEVER = 290, // "never"
473 SKIP = 291, // "skip"
474 IF = 292, // "if"
475 FI = 293, // "fi"
476 DO = 294, // "do"
477 OD = 295, // "od"
478 ARROW = 296, // "->"
479 GOTO = 297, // "goto"
480 FALSE = 298, // "false"
481 ATOMIC = 299, // "atomic"
482 ASSERT = 300, // "assert"
483 FORMULA = 301, // "boolean formula"
484 PGAME = 302, // "start of PGSolver game"
485 ENDPGAME = 303, // "end of PGSolver game"
486 ENDAUT = 304, // "-1"
487 LBTT = 305, // "LBTT header"
488 INT_S = 306, // "state acceptance"
489 LBTT_EMPTY = 307, // "acceptance sets for empty automaton"
490 ACC = 308, // "acceptance set"
491 STATE_NUM = 309, // "state number"
492 DEST_NUM = 310 // "destination number"
493 };
495 typedef token_kind_type yytokentype;
496 };
497
499 typedef token::token_kind_type token_kind_type;
500
502 typedef token_kind_type token_type;
503
506 {
508 {
510 S_YYEMPTY = -2,
511 S_YYEOF = 0, // "end of file"
512 S_YYerror = 1, // error
513 S_YYUNDEF = 2, // "invalid token"
514 S_HOA = 3, // "HOA:"
515 S_STATES = 4, // "States:"
516 S_START = 5, // "Start:"
517 S_AP = 6, // "AP:"
518 S_ALIAS = 7, // "Alias:"
519 S_ACCEPTANCE = 8, // "Acceptance:"
520 S_ACCNAME = 9, // "acc-name:"
521 S_CONTROLLABLE_AP = 10, // "controllable-AP:"
522 S_TOOL = 11, // "tool:"
523 S_NAME = 12, // "name:"
524 S_PROPERTIES = 13, // "properties:"
525 S_BODY = 14, // "--BODY--"
526 S_END = 15, // "--END--"
527 S_STATE = 16, // "State:"
528 S_SPOT_HIGHLIGHT_EDGES = 17, // "spot.highlight.edges:"
529 S_SPOT_HIGHLIGHT_STATES = 18, // "spot.highlight.states:"
530 S_SPOT_STATE_PLAYER = 19, // "spot.state-player:"
531 S_IDENTIFIER = 20, // "identifier"
532 S_HEADERNAME = 21, // "header name"
533 S_ANAME = 22, // "alias name"
534 S_STRING = 23, // "string"
535 S_INT = 24, // "integer"
536 S_25_ = 25, // '['
537 S_LINEDIRECTIVE = 26, // "#line"
538 S_BDD = 27, // BDD
539 S_ENDDSTAR = 28, // "end of DSTAR automaton"
540 S_DRA = 29, // "DRA"
541 S_DSA = 30, // "DSA"
542 S_V2 = 31, // "v2"
543 S_EXPLICIT = 32, // "explicit"
544 S_ACCPAIRS = 33, // "Acceptance-Pairs:"
545 S_ACCSIG = 34, // "Acc-Sig:"
546 S_ENDOFHEADER = 35, // "---"
547 S_36_ = 36, // '|'
548 S_37_ = 37, // '&'
549 S_38_ = 38, // '!'
550 S_NEVER = 39, // "never"
551 S_SKIP = 40, // "skip"
552 S_IF = 41, // "if"
553 S_FI = 42, // "fi"
554 S_DO = 43, // "do"
555 S_OD = 44, // "od"
556 S_ARROW = 45, // "->"
557 S_GOTO = 46, // "goto"
558 S_FALSE = 47, // "false"
559 S_ATOMIC = 48, // "atomic"
560 S_ASSERT = 49, // "assert"
561 S_FORMULA = 50, // "boolean formula"
562 S_PGAME = 51, // "start of PGSolver game"
563 S_ENDPGAME = 52, // "end of PGSolver game"
564 S_ENDAUT = 53, // "-1"
565 S_LBTT = 54, // "LBTT header"
566 S_INT_S = 55, // "state acceptance"
567 S_LBTT_EMPTY = 56, // "acceptance sets for empty automaton"
568 S_ACC = 57, // "acceptance set"
569 S_STATE_NUM = 58, // "state number"
570 S_DEST_NUM = 59, // "destination number"
571 S_60_t_ = 60, // 't'
572 S_61_f_ = 61, // 'f'
573 S_62_ = 62, // '('
574 S_63_ = 63, // ')'
575 S_64_ = 64, // ']'
576 S_65_ = 65, // '{'
577 S_66_ = 66, // '}'
578 S_67_ = 67, // '+'
579 S_68_ = 68, // '-'
580 S_69_ = 69, // ';'
581 S_70_ = 70, // ','
582 S_71_ = 71, // ':'
583 S_YYACCEPT = 72, // $accept
584 S_aut = 73, // aut
585 S_74_1 = 74, // $@1
586 S_75_aut_1 = 75, // aut-1
587 S_hoa = 76, // hoa
588 S_string_opt = 77, // string_opt
589 S_BOOLEAN = 78, // BOOLEAN
590 S_header = 79, // header
591 S_version = 80, // version
592 S_81_format_version = 81, // format-version
593 S_82_2 = 82, // $@2
594 S_83_controllable_aps = 83, // controllable-aps
595 S_aps = 84, // aps
596 S_85_3 = 85, // $@3
597 S_86_header_items = 86, // header-items
598 S_87_header_item = 87, // header-item
599 S_88_4 = 88, // $@4
600 S_89_5 = 89, // $@5
601 S_90_6 = 90, // $@6
602 S_91_7 = 91, // $@7
603 S_92_8 = 92, // $@8
604 S_93_ap_names = 93, // ap-names
605 S_94_ap_name = 94, // ap-name
606 S_95_acc_spec = 95, // acc-spec
607 S_properties = 96, // properties
608 S_97_highlight_edges = 97, // highlight-edges
609 S_98_highlight_states = 98, // highlight-states
610 S_99_state_player = 99, // state-player
611 S_100_header_spec = 100, // header-spec
612 S_101_state_conj_2 = 101, // state-conj-2
613 S_102_init_state_conj_2 = 102, // init-state-conj-2
614 S_103_label_expr = 103, // label-expr
615 S_104_acc_set = 104, // acc-set
616 S_105_acceptance_cond = 105, // acceptance-cond
617 S_body = 106, // body
618 S_107_state_num = 107, // state-num
619 S_108_checked_state_num = 108, // checked-state-num
620 S_states = 109, // states
621 S_state = 110, // state
622 S_111_state_name = 111, // state-name
623 S_label = 112, // label
624 S_113_state_label_opt = 113, // state-label_opt
625 S_114_trans_label = 114, // trans-label
626 S_115_acc_sig = 115, // acc-sig
627 S_116_acc_sets = 116, // acc-sets
628 S_117_state_acc_opt = 117, // state-acc_opt
629 S_118_trans_acc_opt = 118, // trans-acc_opt
630 S_119_labeled_edges = 119, // labeled-edges
631 S_120_some_labeled_edges = 120, // some-labeled-edges
632 S_121_incorrectly_unlabeled_edge = 121, // incorrectly-unlabeled-edge
633 S_122_labeled_edge = 122, // labeled-edge
634 S_123_state_conj_checked = 123, // state-conj-checked
635 S_124_unlabeled_edges = 124, // unlabeled-edges
636 S_125_unlabeled_edge = 125, // unlabeled-edge
637 S_126_incorrectly_labeled_edge = 126, // incorrectly-labeled-edge
638 S_dstar = 127, // dstar
639 S_dstar_type = 128, // dstar_type
640 S_dstar_header = 129, // dstar_header
641 S_dstar_sizes = 130, // dstar_sizes
642 S_dstar_state_id = 131, // dstar_state_id
643 S_sign = 132, // sign
644 S_dstar_accsigs = 133, // dstar_accsigs
645 S_dstar_state_accsig = 134, // dstar_state_accsig
646 S_dstar_transitions = 135, // dstar_transitions
647 S_dstar_states = 136, // dstar_states
648 S_pgamestart = 137, // pgamestart
649 S_pgame = 138, // pgame
650 S_pgame_nodes = 139, // pgame_nodes
651 S_pgame_succs = 140, // pgame_succs
652 S_pgame_node = 141, // pgame_node
653 S_never = 142, // never
654 S_143_9 = 143, // $@9
655 S_144_nc_states = 144, // nc-states
656 S_145_nc_one_ident = 145, // nc-one-ident
657 S_146_nc_ident_list = 146, // nc-ident-list
658 S_147_nc_transition_block = 147, // nc-transition-block
659 S_148_nc_state = 148, // nc-state
660 S_149_nc_transitions = 149, // nc-transitions
661 S_150_nc_formula_or_ident = 150, // nc-formula-or-ident
662 S_151_nc_formula = 151, // nc-formula
663 S_152_nc_opt_dest = 152, // nc-opt-dest
664 S_153_nc_src_dest = 153, // nc-src-dest
665 S_154_nc_transition = 154, // nc-transition
666 S_lbtt = 155, // lbtt
667 S_156_lbtt_header_states = 156, // lbtt-header-states
668 S_157_lbtt_header = 157, // lbtt-header
669 S_158_lbtt_body = 158, // lbtt-body
670 S_159_lbtt_states = 159, // lbtt-states
671 S_160_lbtt_state = 160, // lbtt-state
672 S_161_lbtt_acc = 161, // lbtt-acc
673 S_162_lbtt_guard = 162, // lbtt-guard
674 S_163_lbtt_transitions = 163 // lbtt-transitions
675 };
676 };
677
680
683
690 template <typename Base>
691 struct basic_symbol : Base
692 {
694 typedef Base super_type;
695
697 basic_symbol () YY_NOEXCEPT
698 : value ()
699 , location ()
700 {}
701
702#if 201103L <= YY_CPLUSPLUS
705 : Base (std::move (that))
706 , value (std::move (that.value))
707 , location (std::move (that.location))
708 {}
709#endif
710
714 basic_symbol (typename Base::kind_type t,
715 YY_MOVE_REF (location_type) l);
716
718 basic_symbol (typename Base::kind_type t,
719 YY_RVREF (value_type) v,
720 YY_RVREF (location_type) l);
721
724 {
725 clear ();
726 }
727
728
729
731 void clear () YY_NOEXCEPT
732 {
733 Base::clear ();
734 }
735
737 std::string name () const YY_NOEXCEPT
738 {
739 return parser::symbol_name (this->kind ());
740 }
741
743 symbol_kind_type type_get () const YY_NOEXCEPT;
744
746 bool empty () const YY_NOEXCEPT;
747
750
753
756
757 private:
758#if YY_CPLUSPLUS < 201103L
760 basic_symbol& operator= (const basic_symbol& that);
761#endif
762 };
763
765 struct by_kind
766 {
768 typedef token_kind_type kind_type;
769
771 by_kind () YY_NOEXCEPT;
772
773#if 201103L <= YY_CPLUSPLUS
775 by_kind (by_kind&& that) YY_NOEXCEPT;
776#endif
777
779 by_kind (const by_kind& that) YY_NOEXCEPT;
780
782 by_kind (kind_type t) YY_NOEXCEPT;
783
784
785
787 void clear () YY_NOEXCEPT;
788
790 void move (by_kind& that);
791
794 symbol_kind_type kind () const YY_NOEXCEPT;
795
797 symbol_kind_type type_get () const YY_NOEXCEPT;
798
802 };
803
806
809 {};
810
812 parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
813 virtual ~parser ();
814
815#if 201103L <= YY_CPLUSPLUS
817 parser (const parser&) = delete;
819 parser& operator= (const parser&) = delete;
820#endif
821
825
828 virtual int parse ();
829
830#if HOAYYDEBUG
832 std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
834 void set_debug_stream (std::ostream &);
835
837 typedef int debug_level_type;
839 debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
842#endif
843
847 virtual void error (const location_type& loc, const std::string& msg);
848
850 void error (const syntax_error& err);
851
854 static std::string symbol_name (symbol_kind_type yysymbol);
855
856
857
859 {
860 public:
861 context (const parser& yyparser, const symbol_type& yyla);
862 const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
863 symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
864 const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
865
869 int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
870
871 private:
872 const parser& yyparser_;
873 const symbol_type& yyla_;
874 };
875
876 private:
877#if YY_CPLUSPLUS < 201103L
879 parser (const parser&);
881 parser& operator= (const parser&);
882#endif
883
884
886 typedef short state_type;
887
889 int yy_syntax_error_arguments_ (const context& yyctx,
890 symbol_kind_type yyarg[], int yyargn) const;
891
894 virtual std::string yysyntax_error_ (const context& yyctx) const;
898 static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
899
902 static bool yy_pact_value_is_default_ (int yyvalue) YY_NOEXCEPT;
903
906 static bool yy_table_value_is_error_ (int yyvalue) YY_NOEXCEPT;
907
908 static const short yypact_ninf_;
909 static const short yytable_ninf_;
910
914 static symbol_kind_type yytranslate_ (int t) YY_NOEXCEPT;
915
917 static std::string yytnamerr_ (const char *yystr);
918
920 static const char* const yytname_[];
921
922
923 // Tables.
924 // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
925 // STATE-NUM.
926 static const short yypact_[];
927
928 // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
929 // Performed when YYTABLE does not specify something else to do. Zero
930 // means the default is an error.
931 static const unsigned char yydefact_[];
932
933 // YYPGOTO[NTERM-NUM].
934 static const short yypgoto_[];
935
936 // YYDEFGOTO[NTERM-NUM].
937 static const short yydefgoto_[];
938
939 // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
940 // positive, shift that token. If negative, reduce the rule whose
941 // number is the opposite. If YYTABLE_NINF, syntax error.
942 static const short yytable_[];
943
944 static const short yycheck_[];
945
946 // YYSTOS[STATE-NUM] -- The symbol kind of the accessing symbol of
947 // state STATE-NUM.
948 static const unsigned char yystos_[];
949
950 // YYR1[RULE-NUM] -- Symbol kind of the left-hand side of rule RULE-NUM.
951 static const unsigned char yyr1_[];
952
953 // YYR2[RULE-NUM] -- Number of symbols on the right-hand side of rule RULE-NUM.
954 static const signed char yyr2_[];
955
956
957#if HOAYYDEBUG
958 // YYRLINE[YYN] -- Source line where rule number YYN was defined.
959 static const short yyrline_[];
961 virtual void yy_reduce_print_ (int r) const;
963 virtual void yy_stack_print_ () const;
964
966 int yydebug_;
968 std::ostream* yycdebug_;
969
973 template <typename Base>
974 void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
975#endif
976
981 template <typename Base>
982 void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
983
984 private:
986 struct by_state
987 {
989 by_state () YY_NOEXCEPT;
990
992 typedef state_type kind_type;
993
995 by_state (kind_type s) YY_NOEXCEPT;
996
998 by_state (const by_state& that) YY_NOEXCEPT;
999
1001 void clear () YY_NOEXCEPT;
1002
1004 void move (by_state& that);
1005
1008 symbol_kind_type kind () const YY_NOEXCEPT;
1009
1012 enum { empty_state = 0 };
1013
1016 state_type state;
1017 };
1018
1020 struct stack_symbol_type : basic_symbol<by_state>
1021 {
1023 typedef basic_symbol<by_state> super_type;
1025 stack_symbol_type ();
1027 stack_symbol_type (YY_RVREF (stack_symbol_type) that);
1029 stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
1030#if YY_CPLUSPLUS < 201103L
1033 stack_symbol_type& operator= (stack_symbol_type& that);
1034
1037 stack_symbol_type& operator= (const stack_symbol_type& that);
1038#endif
1039 };
1040
1042 template <typename T, typename S = std::vector<T> >
1043 class stack
1044 {
1045 public:
1046 // Hide our reversed order.
1047 typedef typename S::iterator iterator;
1048 typedef typename S::const_iterator const_iterator;
1049 typedef typename S::size_type size_type;
1050 typedef typename std::ptrdiff_t index_type;
1051
1052 stack (size_type n = 200) YY_NOEXCEPT
1053 : seq_ (n)
1054 {}
1055
1056#if 201103L <= YY_CPLUSPLUS
1058 stack (const stack&) = delete;
1060 stack& operator= (const stack&) = delete;
1061#endif
1062
1066 const T&
1067 operator[] (index_type i) const
1068 {
1069 return seq_[size_type (size () - 1 - i)];
1070 }
1071
1075 T&
1076 operator[] (index_type i)
1077 {
1078 return seq_[size_type (size () - 1 - i)];
1079 }
1080
1084 void
1085 push (YY_MOVE_REF (T) t)
1086 {
1087 seq_.push_back (T ());
1088 operator[] (0).move (t);
1089 }
1090
1092 void
1093 pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1094 {
1095 for (; 0 < n; --n)
1096 seq_.pop_back ();
1097 }
1098
1100 void
1101 clear () YY_NOEXCEPT
1102 {
1103 seq_.clear ();
1104 }
1105
1107 index_type
1108 size () const YY_NOEXCEPT
1109 {
1110 return index_type (seq_.size ());
1111 }
1112
1114 const_iterator
1115 begin () const YY_NOEXCEPT
1116 {
1117 return seq_.begin ();
1118 }
1119
1121 const_iterator
1122 end () const YY_NOEXCEPT
1123 {
1124 return seq_.end ();
1125 }
1126
1128 class slice
1129 {
1130 public:
1131 slice (const stack& stack, index_type range) YY_NOEXCEPT
1132 : stack_ (stack)
1133 , range_ (range)
1134 {}
1135
1136 const T&
1137 operator[] (index_type i) const
1138 {
1139 return stack_[range_ - i];
1140 }
1141
1142 private:
1143 const stack& stack_;
1144 index_type range_;
1145 };
1146
1147 private:
1148#if YY_CPLUSPLUS < 201103L
1150 stack (const stack&);
1152 stack& operator= (const stack&);
1153#endif
1155 S seq_;
1156 };
1157
1158
1160 typedef stack<stack_symbol_type> stack_type;
1161
1163 stack_type yystack_;
1164
1170 void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1171
1178 void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
1179
1181 void yypop_ (int n = 1) YY_NOEXCEPT;
1182
1184 enum
1185 {
1186 yylast_ = 271,
1187 yynnts_ = 92,
1188 yyfinal_ = 29
1189 };
1190
1191
1192 // User arguments.
1193 void* scanner;
1194 result_& res;
1195 spot::location initial_loc;
1196
1197 };
1198
1199
1200} // hoayy
1201#line 1202 "parseaut.hh"
1202
1203
1204
1205
1206#endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:859
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1129
A Bison parser.
Definition: parseaut.hh:381
std::ostream & debug_stream() const
The current debugging stream.
debug_level_type debug_level() const
The current debugging level.
void error(const syntax_error &err)
Report a syntax error.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:502
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:679
token::token_kind_type token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:499
spot::location location_type
Symbol locations.
Definition: parseaut.hh:411
void set_debug_stream(std::ostream &)
Set the current debugging stream.
virtual int parse()
static const symbol_kind_type YYNTOKENS
The number of tokens.
Definition: parseaut.hh:682
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:837
value_type semantic_type
Backward compatibility (Bison 3.8).
Definition: parseaut.hh:408
void set_debug_level(debug_level_type l)
Set the current debugging level.
virtual void error(const location_type &loc, const std::string &msg)
parser(void *scanner_yyarg, result_ &res_yyarg, spot::location initial_loc_yyarg)
Build a parser object.
An environment that describes atomic propositions.
Definition: environment.hh:29
Definition: ngraph.hh:32
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
Definition: parseaut.hh:692
Base super_type
Alias to Base.
Definition: parseaut.hh:694
location_type location
The location.
Definition: parseaut.hh:755
basic_symbol()
Default constructor.
Definition: parseaut.hh:697
bool empty() const
Whether empty.
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
value_type value
The semantic value.
Definition: parseaut.hh:752
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:731
basic_symbol(const basic_symbol &that)
Copy constructor.
void move(basic_symbol &s)
Destructive move, s is emptied into this.
basic_symbol(typename Base::kind_type t, const value_type &v, const location_type &l)
Constructor for symbols with semantic value.
basic_symbol(typename Base::kind_type t, location_type &l)
Constructor for valueless symbols.
std::string name() const
The user-facing name of this symbol.
Definition: parseaut.hh:737
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:723
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:766
void move(by_kind &that)
Steal the symbol kind from that.
symbol_kind_type kind_
Definition: parseaut.hh:801
by_kind()
Default constructor.
void clear()
Record that this symbol is empty.
symbol_kind_type kind() const
by_kind(kind_type t)
Constructor from (external) token numbers.
by_kind(const by_kind &that)
Copy constructor.
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
token_kind_type kind_type
The symbol kind as needed by the constructor.
Definition: parseaut.hh:768
Symbol kinds.
Definition: parseaut.hh:506
symbol_kind_type
Definition: parseaut.hh:508
@ YYNTOKENS
Number of tokens.
Definition: parseaut.hh:509
"External" symbols: returned by the scanner.
Definition: parseaut.hh:809
Syntax errors thrown from user actions.
Definition: parseaut.hh:415
Token kinds.
Definition: parseaut.hh:433
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:495
Definition: parseaut.hh:153
Definition: parseaut.hh:102
Definition: parseaut.hh:100
An acceptance formula.
Definition: acc.hh:470
An acceptance mark.
Definition: acc.hh:84
Definition: public.hh:99
Symbol semantic values.
Definition: parseaut.hh:391

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4