45 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
46 # define YY_HOAYY_PARSEAUT_HH_INCLUDED
48 #line 33 "parseaut.yy"
51 #include <spot/misc/common.hh>
52 #include <spot/priv/robin_hood.hh>
56 #include <unordered_map>
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>
64 using namespace std::string_literals;
66 #ifndef HAVE_STRVERSCMP
68 extern "C" int strverscmp(
const char *s1,
const char *s2);
73 #define PARSE_ERROR_LIST res.h->errors, res.fcache
75 inline namespace hoayy_support
77 typedef std::map<int, bdd> map_t;
84 typedef robin_hood::unordered_flat_map<std::string, bdd> formula_cache;
86 typedef std::pair<int, std::string*> pair;
94 enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
96 enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
102 bool declared =
false;
104 spot::location used_loc;
106 spot::parsed_aut_ptr h;
107 spot::twa_ptr aut_or_ks;
109 std::string format_version;
110 spot::location format_version_loc;
112 formula_cache fcache;
114 spot::acc_mapper_int* acc_mapper =
nullptr;
116 std::vector<bdd> guards;
117 std::vector<bdd>::const_iterator cur_guard;
127 int unknown_ap_max = -1;
128 spot::location unknown_ap_max_location;
129 bool in_alias =
false;
131 std::vector<state_info> info_states;
132 std::vector<std::pair<spot::location,
133 std::vector<unsigned>>> start;
134 std::unordered_map<std::string, bdd> alias;
139 operator bool()
const
144 std::unordered_map<std::string, prop_info> props;
145 spot::location states_loc;
146 spot::location ap_loc;
147 spot::location state_label_loc;
148 spot::location accset_loc;
154 std::vector<std::string>* state_names =
nullptr;
155 std::map<unsigned, unsigned>* highlight_edges =
nullptr;
156 std::map<unsigned, unsigned>* highlight_states =
nullptr;
157 std::map<unsigned, unsigned> states_map;
158 std::vector<bool>* state_player =
nullptr;
159 spot::location state_player_loc;
160 std::set<int> ap_set;
167 bool has_state_label =
false;
168 bool ignore_more_ap =
false;
170 bool ignore_acc =
false;
172 bool ignore_acc_silent =
false;
173 bool ignore_more_acc =
false;
176 label_style_t label_style = Mixed_Labels;
177 acc_style_t acc_style = Mixed_Acc;
179 bool accept_all_needed =
false;
180 bool accept_all_seen =
false;
181 bool aliased_states =
false;
186 bool trans_acc_seen =
false;
188 std::map<std::string, spot::location> labels;
190 prop_info prop_is_true(
const std::string& p)
192 auto i = props.find(p);
193 if (i == props.end())
194 return prop_info{spot::location(),
false};
198 prop_info prop_is_false(
const std::string& p)
200 auto i = props.find(p);
201 if (i == props.end())
202 return prop_info{spot::location(),
false};
203 return prop_info{i->second.loc, !i->second.val};
214 #line 215 "parseaut.hh"
219 # include <stdexcept>
223 #if defined __cplusplus
224 # define YY_CPLUSPLUS __cplusplus
226 # define YY_CPLUSPLUS 199711L
230 #if 201103L <= YY_CPLUSPLUS
231 # define YY_MOVE std::move
232 # define YY_MOVE_OR_COPY move
233 # define YY_MOVE_REF(Type) Type&&
234 # define YY_RVREF(Type) Type&&
235 # define YY_COPY(Type) Type
238 # define YY_MOVE_OR_COPY copy
239 # define YY_MOVE_REF(Type) Type&
240 # define YY_RVREF(Type) const Type&
241 # define YY_COPY(Type) const Type&
245 #if 201103L <= YY_CPLUSPLUS
246 # define YY_NOEXCEPT noexcept
250 # define YY_NOTHROW throw ()
254 #if 201703 <= YY_CPLUSPLUS
255 # define YY_CONSTEXPR constexpr
257 # define YY_CONSTEXPR
262 #ifndef YY_ATTRIBUTE_PURE
263 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
264 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
266 # define YY_ATTRIBUTE_PURE
270 #ifndef YY_ATTRIBUTE_UNUSED
271 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
272 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
274 # define YY_ATTRIBUTE_UNUSED
279 #if ! defined lint || defined __GNUC__
280 # define YY_USE(E) ((void) (E))
285 #if defined __GNUC__ && ! defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
287 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
288 _Pragma ("GCC diagnostic push") \
289 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
290 _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
291 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
292 _Pragma ("GCC diagnostic pop")
294 # define YY_INITIAL_VALUE(Value) Value
296 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
297 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
298 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
300 #ifndef YY_INITIAL_VALUE
301 # define YY_INITIAL_VALUE(Value)
304 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
305 # define YY_IGNORE_USELESS_CAST_BEGIN \
306 _Pragma ("GCC diagnostic push") \
307 _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
308 # define YY_IGNORE_USELESS_CAST_END \
309 _Pragma ("GCC diagnostic pop")
311 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
312 # define YY_IGNORE_USELESS_CAST_BEGIN
313 # define YY_IGNORE_USELESS_CAST_END
318 # define YY_CAST(Type, Val) static_cast<Type> (Val)
319 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
321 # define YY_CAST(Type, Val) ((Type) (Val))
322 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
326 # if defined __cplusplus
327 # if 201103L <= __cplusplus
328 # define YY_NULLPTR nullptr
330 # define YY_NULLPTR 0
333 # define YY_NULLPTR ((void*)0)
341 # define HOAYYDEBUG 1
343 # define HOAYYDEBUG 0
346 # define HOAYYDEBUG 1
351 #line 352 "parseaut.hh"
364 #line 205 "parseaut.yy"
371 std::list<pair>* list;
373 std::vector<unsigned>* states;
375 #line 376 "parseaut.hh"
388 : std::runtime_error (m)
393 : std::runtime_error (s.what ())
394 , location (s.location)
424 SPOT_HIGHLIGHT_EDGES = 271,
425 SPOT_HIGHLIGHT_STATES = 272,
426 SPOT_STATE_PLAYER = 273,
495 S_SPOT_HIGHLIGHT_EDGES = 16,
496 S_SPOT_HIGHLIGHT_STATES = 17,
497 S_SPOT_STATE_PLAYER = 18,
511 S_LINEDIRECTIVE = 32,
556 S_77_format_version = 77,
560 S_81_header_items = 81,
561 S_82_header_item = 82,
571 S_92_highlight_edges = 92,
572 S_93_highlight_states = 93,
573 S_94_state_player = 94,
574 S_95_header_spec = 95,
575 S_96_state_conj_2 = 96,
576 S_97_init_state_conj_2 = 97,
577 S_98_label_expr = 98,
579 S_100_acceptance_cond = 100,
581 S_102_state_num = 102,
582 S_103_checked_state_num = 103,
585 S_106_state_name = 106,
587 S_108_state_label_opt = 108,
588 S_109_trans_label = 109,
590 S_111_acc_sets = 111,
591 S_112_state_acc_opt = 112,
592 S_113_trans_acc_opt = 113,
593 S_114_labeled_edges = 114,
594 S_115_some_labeled_edges = 115,
595 S_116_incorrectly_unlabeled_edge = 116,
596 S_117_labeled_edge = 117,
597 S_118_state_conj_checked = 118,
598 S_119_unlabeled_edges = 119,
599 S_120_unlabeled_edge = 120,
600 S_121_incorrectly_labeled_edge = 121,
603 S_dstar_header = 124,
605 S_dstar_state_id = 126,
607 S_dstar_accsigs = 128,
608 S_dstar_state_accsig = 129,
609 S_dstar_transitions = 130,
610 S_dstar_states = 131,
613 S_134_nc_states = 134,
614 S_135_nc_one_ident = 135,
615 S_136_nc_ident_list = 136,
616 S_137_nc_transition_block = 137,
617 S_138_nc_state = 138,
618 S_139_nc_transitions = 139,
619 S_140_nc_formula_or_ident = 140,
620 S_141_nc_formula = 141,
621 S_142_nc_opt_dest = 142,
622 S_143_nc_src_dest = 143,
623 S_144_nc_transition = 144,
625 S_146_lbtt_header_states = 146,
626 S_147_lbtt_header = 147,
627 S_148_lbtt_body = 148,
628 S_149_lbtt_states = 149,
629 S_150_lbtt_state = 150,
630 S_151_lbtt_acc = 151,
631 S_152_lbtt_guard = 152,
632 S_153_lbtt_transitions = 153
648 template <
typename Base>
660 #if 201103L <= YY_CPLUSPLUS
663 : Base (std::move (that))
664 , value (std::move (that.value))
665 , location (std::move (that.location))
693 std::string
name () const YY_NOEXCEPT
695 return parser::symbol_name (this->kind ());
702 bool empty () const YY_NOEXCEPT;
714 #if YY_CPLUSPLUS < 201103L
726 #if 201103L <= YY_CPLUSPLUS
766 parser (
void* scanner_yyarg,
result_& res_yyarg, spot::location initial_loc_yyarg);
769 #if 201103L <= YY_CPLUSPLUS
788 void set_debug_stream (std::ostream &);
816 const symbol_type& lookahead ()
const YY_NOEXCEPT {
return yyla_; }
818 const location_type& location ()
const YY_NOEXCEPT {
return yyla_.location; }
831 #if YY_CPLUSPLUS < 201103L
840 typedef short state_type;
843 int yy_syntax_error_arguments_ (
const context& yyctx,
848 virtual std::string yysyntax_error_ (
const context& yyctx)
const;
852 static state_type yy_lr_goto_state_ (state_type yystate,
int yysym);
856 static bool yy_pact_value_is_default_ (
int yyvalue);
860 static bool yy_table_value_is_error_ (
int yyvalue);
862 static const short yypact_ninf_;
863 static const short yytable_ninf_;
871 static std::string yytnamerr_ (
const char *yystr);
874 static const char*
const yytname_[];
880 static const short yypact_[];
885 static const unsigned char yydefact_[];
888 static const short yypgoto_[];
891 static const short yydefgoto_[];
896 static const short yytable_[];
898 static const short yycheck_[];
902 static const unsigned char yystos_[];
905 static const unsigned char yyr1_[];
908 static const signed char yyr2_[];
913 static const short yyrline_[];
915 virtual void yy_reduce_print_ (
int r)
const;
917 virtual void yy_stack_print_ ()
const;
922 std::ostream* yycdebug_;
927 template <
typename Base>
935 template <
typename Base>
943 by_state () YY_NOEXCEPT;
946 typedef state_type kind_type;
949 by_state (kind_type s) YY_NOEXCEPT;
952 by_state (const by_state& that) YY_NOEXCEPT;
955 void clear () YY_NOEXCEPT;
958 void move (by_state& that);
966 enum { empty_state = 0 };
974 struct stack_symbol_type : basic_symbol<by_state>
977 typedef basic_symbol<by_state> super_type;
979 stack_symbol_type ();
981 stack_symbol_type (YY_RVREF (stack_symbol_type) that);
983 stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
984 #if YY_CPLUSPLUS < 201103L
987 stack_symbol_type& operator= (stack_symbol_type& that);
991 stack_symbol_type& operator= (
const stack_symbol_type& that);
996 template <
typename T,
typename S = std::vector<T> >
1001 typedef typename S::iterator iterator;
1002 typedef typename S::const_iterator const_iterator;
1003 typedef typename S::size_type size_type;
1004 typedef typename std::ptrdiff_t index_type;
1006 stack (size_type n = 200)
1010 #if 201103L <= YY_CPLUSPLUS
1012 stack (
const stack&) =
delete;
1014 stack& operator= (
const stack&) =
delete;
1021 operator[] (index_type i)
const
1023 return seq_[size_type (size () - 1 - i)];
1030 operator[] (index_type i)
1032 return seq_[size_type (size () - 1 - i)];
1039 push (YY_MOVE_REF (T) t)
1041 seq_.push_back (T ());
1042 operator[] (0).move (t);
1047 pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1055 clear () YY_NOEXCEPT
1062 size () const YY_NOEXCEPT
1064 return index_type (seq_.size ());
1069 begin () const YY_NOEXCEPT
1071 return seq_.begin ();
1076 end () const YY_NOEXCEPT
1085 slice (
const stack& stack, index_type range)
1091 operator[] (index_type i)
const
1093 return stack_[range_ - i];
1097 const stack& stack_;
1102 #if YY_CPLUSPLUS < 201103L
1104 stack (
const stack&);
1106 stack& operator= (
const stack&);
1114 typedef stack<stack_symbol_type> stack_type;
1117 stack_type yystack_;
1124 void yypush_ (
const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1132 void yypush_ (
const char* m, state_type s, YY_MOVE_REF (
symbol_type) sym);
1135 void yypop_ (
int n = 1);
1149 spot::location initial_loc;
1155 #line 1156 "parseaut.hh"
Definition: parseaut.hh:813
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1083
A Bison parser.
Definition: parseaut.hh:358
void error(const syntax_error &err)
Report a syntax error.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:470
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:637
std::ostream & debug_stream() const
The current debugging stream.
token::yytokentype token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:467
spot::location location_type
Symbol locations.
Definition: parseaut.hh:382
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:791
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:33
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
Definition: parseaut.hh:650
Base super_type
Alias to Base.
Definition: parseaut.hh:652
basic_symbol()
Default constructor.
Definition: parseaut.hh:655
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:687
basic_symbol(const basic_symbol &that)
Copy constructor.
basic_symbol(typename Base::kind_type t, location_type &l)
Constructor for valueless symbols.
basic_symbol(typename Base::kind_type t, const semantic_type &v, const location_type &l)
Constructor for symbols with semantic value.
std::string name() const
The user-facing name of this symbol.
Definition: parseaut.hh:693
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:681
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:722
by_kind()
Default constructor.
void clear()
Record that this symbol is empty.
by_kind(kind_type t)
Constructor from (external) token numbers.
by_kind(const by_kind &that)
Copy constructor.
token_kind_type kind_type
The symbol kind as needed by the constructor.
Definition: parseaut.hh:735
Symbol kinds.
Definition: parseaut.hh:474
symbol_kind_type
Definition: parseaut.hh:476
"External" symbols: returned by the scanner.
Definition: parseaut.hh:763
Syntax errors thrown from user actions.
Definition: parseaut.hh:386
Token kinds.
Definition: parseaut.hh:404
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:463
Definition: parseaut.hh:136
Definition: parseaut.hh:101
Definition: parseaut.hh:99
An acceptance formula.
Definition: acc.hh:487
An acceptance mark.
Definition: acc.hh:89
Symbol semantic values.
Definition: parseaut.hh:363