45#ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
46# define YY_HOAYY_PARSEAUT_HH_INCLUDED
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>
63#include <spot/twaalgos/game.hh>
65using namespace std::string_literals;
67#ifndef HAVE_STRVERSCMP
69extern "C" int strverscmp(
const char *s1,
const char *s2);
74#define PARSE_ERROR_LIST res.h->errors, res.fcache
76 inline namespace hoayy_support
78 typedef std::map<int, bdd> map_t;
85 typedef robin_hood::unordered_flat_map<std::string, bdd> formula_cache;
87 typedef std::pair<int, std::string*> pair;
95 enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
97 enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
103 bool declared =
false;
105 spot::location used_loc;
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;
115 spot::acc_mapper_int* acc_mapper =
nullptr;
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;
132 int unknown_ap_max = -1;
133 spot::location unknown_ap_max_location;
134 bool in_alias =
false;
136 std::vector<state_info> info_states;
147 std::vector<unsigned> edge_map;
148 std::vector<std::pair<spot::location,
149 std::vector<unsigned>>> start;
150 std::unordered_map<std::string, bdd> alias;
151 std::vector<std::string> alias_order;
156 operator bool()
const
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;
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;
184 bool has_state_label =
false;
185 bool ignore_more_ap =
false;
187 bool ignore_acc =
false;
189 bool ignore_acc_silent =
false;
190 bool ignore_more_acc =
false;
193 label_style_t label_style = Mixed_Labels;
194 acc_style_t acc_style = Mixed_Acc;
196 bool accept_all_needed =
false;
197 bool accept_all_seen =
false;
198 bool aliased_states =
false;
203 bool trans_acc_seen =
false;
205 std::map<std::string, spot::location> labels;
207 prop_info prop_is_true(
const std::string& p)
209 auto i = props.find(p);
210 if (i == props.end())
211 return prop_info{spot::location(),
false};
215 prop_info prop_is_false(
const std::string& p)
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};
231#line 232 "parseaut.hh"
240#if defined __cplusplus
241# define YY_CPLUSPLUS __cplusplus
243# define YY_CPLUSPLUS 199711L
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
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&
262#if 201103L <= YY_CPLUSPLUS
263# define YY_NOEXCEPT noexcept
267# define YY_NOTHROW throw ()
271#if 201703 <= YY_CPLUSPLUS
272# define YY_CONSTEXPR constexpr
279#ifndef YY_ATTRIBUTE_PURE
280# if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
281# define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
283# define YY_ATTRIBUTE_PURE
287#ifndef YY_ATTRIBUTE_UNUSED
288# if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
289# define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
291# define YY_ATTRIBUTE_UNUSED
296#if ! defined lint || defined __GNUC__
297# define YY_USE(E) ((void) (E))
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\"")
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\"")
314# define YY_IGNORE_MAYBE_UNINITIALIZED_END \
315 _Pragma ("GCC diagnostic pop")
317# define YY_INITIAL_VALUE(Value) Value
319#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
320# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
321# define YY_IGNORE_MAYBE_UNINITIALIZED_END
323#ifndef YY_INITIAL_VALUE
324# define YY_INITIAL_VALUE(Value)
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")
334#ifndef YY_IGNORE_USELESS_CAST_BEGIN
335# define YY_IGNORE_USELESS_CAST_BEGIN
336# define YY_IGNORE_USELESS_CAST_END
341# define YY_CAST(Type, Val) static_cast<Type> (Val)
342# define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
344# define YY_CAST(Type, Val) ((Type) (Val))
345# define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
349# if defined __cplusplus
350# if 201103L <= __cplusplus
351# define YY_NULLPTR nullptr
356# define YY_NULLPTR ((void*)0)
374#line 375 "parseaut.hh"
385# pragma GCC message "bison: do not #define HOAYYSTYPE in C++, use %define api.value.type"
392#line 221 "parseaut.yy"
399 std::list<pair>* list;
401 std::vector<unsigned>* states;
403#line 404 "parseaut.hh"
417 : std::runtime_error (m)
422 : std::runtime_error (s.what ())
423 , location (s.location)
447 CONTROLLABLE_AP = 265,
454 SPOT_HIGHLIGHT_EDGES = 272,
455 SPOT_HIGHLIGHT_STATES = 273,
456 SPOT_STATE_PLAYER = 274,
521 S_CONTROLLABLE_AP = 10,
528 S_SPOT_HIGHLIGHT_EDGES = 17,
529 S_SPOT_HIGHLIGHT_STATES = 18,
530 S_SPOT_STATE_PLAYER = 19,
537 S_LINEDIRECTIVE = 26,
592 S_81_format_version = 81,
594 S_83_controllable_aps = 83,
597 S_86_header_items = 86,
598 S_87_header_item = 87,
608 S_97_highlight_edges = 97,
609 S_98_highlight_states = 98,
610 S_99_state_player = 99,
611 S_100_header_spec = 100,
612 S_101_state_conj_2 = 101,
613 S_102_init_state_conj_2 = 102,
614 S_103_label_expr = 103,
616 S_105_acceptance_cond = 105,
618 S_107_state_num = 107,
619 S_108_checked_state_num = 108,
622 S_111_state_name = 111,
624 S_113_state_label_opt = 113,
625 S_114_trans_label = 114,
627 S_116_acc_sets = 116,
628 S_117_state_acc_opt = 117,
629 S_118_trans_acc_opt = 118,
630 S_119_labeled_edges = 119,
631 S_120_some_labeled_edges = 120,
632 S_121_incorrectly_unlabeled_edge = 121,
633 S_122_labeled_edge = 122,
634 S_123_state_conj_checked = 123,
635 S_124_unlabeled_edges = 124,
636 S_125_unlabeled_edge = 125,
637 S_126_incorrectly_labeled_edge = 126,
640 S_dstar_header = 129,
642 S_dstar_state_id = 131,
644 S_dstar_accsigs = 133,
645 S_dstar_state_accsig = 134,
646 S_dstar_transitions = 135,
647 S_dstar_states = 136,
655 S_144_nc_states = 144,
656 S_145_nc_one_ident = 145,
657 S_146_nc_ident_list = 146,
658 S_147_nc_transition_block = 147,
659 S_148_nc_state = 148,
660 S_149_nc_transitions = 149,
661 S_150_nc_formula_or_ident = 150,
662 S_151_nc_formula = 151,
663 S_152_nc_opt_dest = 152,
664 S_153_nc_src_dest = 153,
665 S_154_nc_transition = 154,
667 S_156_lbtt_header_states = 156,
668 S_157_lbtt_header = 157,
669 S_158_lbtt_body = 158,
670 S_159_lbtt_states = 159,
671 S_160_lbtt_state = 160,
672 S_161_lbtt_acc = 161,
673 S_162_lbtt_guard = 162,
674 S_163_lbtt_transitions = 163
690 template <
typename Base>
702#if 201103L <= YY_CPLUSPLUS
705 : Base (std::
move (that))
737 std::string
name () const YY_NOEXCEPT
758#if YY_CPLUSPLUS < 201103L
773#if 201103L <= YY_CPLUSPLUS
812 parser (
void* scanner_yyarg,
result_& res_yyarg, spot::location initial_loc_yyarg);
815#if 201103L <= YY_CPLUSPLUS
862 const symbol_type& lookahead ()
const YY_NOEXCEPT {
return yyla_; }
864 const location_type& location ()
const YY_NOEXCEPT {
return yyla_.location; }
877#if YY_CPLUSPLUS < 201103L
886 typedef short state_type;
889 int yy_syntax_error_arguments_ (
const context& yyctx,
894 virtual std::string yysyntax_error_ (
const context& yyctx)
const;
898 static state_type yy_lr_goto_state_ (state_type yystate,
int yysym);
902 static bool yy_pact_value_is_default_ (
int yyvalue) YY_NOEXCEPT;
906 static bool yy_table_value_is_error_ (
int yyvalue) YY_NOEXCEPT;
908 static const short yypact_ninf_;
909 static const short yytable_ninf_;
917 static std::string yytnamerr_ (
const char *yystr);
920 static const char*
const yytname_[];
926 static const short yypact_[];
931 static const unsigned char yydefact_[];
934 static const short yypgoto_[];
937 static const short yydefgoto_[];
942 static const short yytable_[];
944 static const short yycheck_[];
948 static const unsigned char yystos_[];
951 static const unsigned char yyr1_[];
954 static const signed char yyr2_[];
959 static const short yyrline_[];
961 virtual void yy_reduce_print_ (
int r)
const;
963 virtual void yy_stack_print_ ()
const;
968 std::ostream* yycdebug_;
973 template <
typename Base>
981 template <
typename Base>
989 by_state () YY_NOEXCEPT;
998 by_state (const by_state& that) YY_NOEXCEPT;
1001 void clear () YY_NOEXCEPT;
1004 void move (by_state& that);
1012 enum { empty_state = 0 };
1020 struct stack_symbol_type : basic_symbol<by_state>
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);
1037 stack_symbol_type& operator= (
const stack_symbol_type& that);
1042 template <
typename T,
typename S = std::vector<T> >
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;
1052 stack (size_type n = 200) YY_NOEXCEPT
1056#if 201103L <= YY_CPLUSPLUS
1058 stack (
const stack&) =
delete;
1060 stack& operator= (
const stack&) =
delete;
1067 operator[] (index_type i)
const
1069 return seq_[size_type (size () - 1 - i)];
1076 operator[] (index_type i)
1078 return seq_[size_type (size () - 1 - i)];
1085 push (YY_MOVE_REF (T) t)
1087 seq_.push_back (T ());
1088 operator[] (0).move (t);
1093 pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1101 clear () YY_NOEXCEPT
1108 size () const YY_NOEXCEPT
1110 return index_type (seq_.size ());
1115 begin () const YY_NOEXCEPT
1117 return seq_.begin ();
1122 end () const YY_NOEXCEPT
1131 slice (
const stack& stack, index_type range) YY_NOEXCEPT
1137 operator[] (index_type i)
const
1139 return stack_[range_ - i];
1143 const stack& stack_;
1148#if YY_CPLUSPLUS < 201103L
1150 stack (
const stack&);
1152 stack& operator= (
const stack&);
1160 typedef stack<stack_symbol_type> stack_type;
1163 stack_type yystack_;
1170 void yypush_ (
const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1178 void yypush_ (
const char* m, state_type s, YY_MOVE_REF (
symbol_type) sym);
1181 void yypop_ (
int n = 1) YY_NOEXCEPT;
1195 spot::location initial_loc;
1201#line 1202 "parseaut.hh"
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.
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
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
Symbol semantic values.
Definition: parseaut.hh:391