44 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED 45 # define YY_HOAYY_PARSEAUT_HH_INCLUDED 47 #line 33 "parseaut.yy" // lalr1.cc:401 50 #include <spot/misc/common.hh> 54 #include <unordered_map> 56 #include <spot/twa/formula2bdd.hh> 57 #include <spot/parseaut/public.hh> 58 #include "spot/priv/accmap.hh" 59 #include <spot/tl/parse.hh> 60 #include <spot/twaalgos/alternation.hh> 64 #ifndef HAVE_STRVERSCMP 66 extern "C" int strverscmp(
const char *s1,
const char *s2);
71 #define PARSE_ERROR_LIST res.h->errors 75 typedef std::map<int, bdd> map_t;
82 typedef std::map<std::string, bdd> formula_cache;
84 typedef std::pair<int, std::string*> pair;
92 enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
94 enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
100 bool declared =
false;
102 spot::location used_loc;
104 spot::parsed_aut_ptr h;
105 spot::twa_ptr aut_or_ks;
107 std::string format_version;
108 spot::location format_version_loc;
110 formula_cache fcache;
111 named_tgba_t* namer =
nullptr;
112 spot::acc_mapper_int* acc_mapper =
nullptr;
114 std::vector<bdd> guards;
115 std::vector<bdd>::const_iterator cur_guard;
125 int unknown_ap_max = -1;
126 spot::location unknown_ap_max_location;
127 bool in_alias =
false;
129 std::vector<state_info> info_states;
130 std::vector<std::pair<spot::location,
131 std::vector<unsigned>>> start;
132 std::unordered_map<std::string, bdd> alias;
137 operator bool()
const 142 std::unordered_map<std::string, prop_info> props;
143 spot::location states_loc;
144 spot::location ap_loc;
145 spot::location state_label_loc;
146 spot::location accset_loc;
152 std::vector<std::string>* state_names =
nullptr;
153 std::map<unsigned, unsigned>* highlight_edges =
nullptr;
154 std::map<unsigned, unsigned>* highlight_states =
nullptr;
155 std::map<unsigned, unsigned> states_map;
156 std::set<int> ap_set;
163 bool has_state_label =
false;
164 bool ignore_more_ap =
false;
166 bool ignore_acc =
false;
168 bool ignore_acc_silent =
false;
169 bool ignore_more_acc =
false;
172 label_style_t label_style = Mixed_Labels;
173 acc_style_t acc_style = Mixed_Acc;
175 bool accept_all_needed =
false;
176 bool accept_all_seen =
false;
177 bool aliased_states =
false;
182 bool trans_acc_seen =
false;
184 std::map<std::string, spot::location> labels;
186 prop_info prop_is_true(
const std::string& p)
188 auto i = props.find(p);
189 if (i == props.end())
190 return prop_info{spot::location(),
false};
194 prop_info prop_is_false(
const std::string& p)
196 auto i = props.find(p);
197 if (i == props.end())
198 return prop_info{spot::location(),
false};
199 return prop_info{i->second.loc, !i->second.val};
210 #line 211 "parseaut.hh" // lalr1.cc:401 215 # include <stdexcept> 219 #if defined __cplusplus 220 # define YY_CPLUSPLUS __cplusplus 222 # define YY_CPLUSPLUS 199711L 226 #if 201103L <= YY_CPLUSPLUS 227 # define YY_MOVE std::move 228 # define YY_MOVE_OR_COPY move 229 # define YY_MOVE_REF(Type) Type&& 230 # define YY_RVREF(Type) Type&& 231 # define YY_COPY(Type) Type 234 # define YY_MOVE_OR_COPY copy 235 # define YY_MOVE_REF(Type) Type& 236 # define YY_RVREF(Type) const Type& 237 # define YY_COPY(Type) const Type& 241 #if 201103L <= YY_CPLUSPLUS 242 # define YY_NOEXCEPT noexcept 246 # define YY_NOTHROW throw () 250 #if 201703 <= YY_CPLUSPLUS 251 # define YY_CONSTEXPR constexpr 253 # define YY_CONSTEXPR 259 # if (defined __GNUC__ \ 260 && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \ 261 || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C 262 # define YY_ATTRIBUTE(Spec) __attribute__(Spec) 264 # define YY_ATTRIBUTE(Spec) 268 #ifndef YY_ATTRIBUTE_PURE 269 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__)) 272 #ifndef YY_ATTRIBUTE_UNUSED 273 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__)) 277 #if ! defined lint || defined __GNUC__ 278 # define YYUSE(E) ((void) (E)) 283 #if defined __GNUC__ && ! defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__ 285 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \ 286 _Pragma ("GCC diagnostic push") \ 287 _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\ 288 _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"") 289 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \ 290 _Pragma ("GCC diagnostic pop") 292 # define YY_INITIAL_VALUE(Value) Value 294 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN 295 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN 296 # define YY_IGNORE_MAYBE_UNINITIALIZED_END 298 #ifndef YY_INITIAL_VALUE 299 # define YY_INITIAL_VALUE(Value) 303 # if defined __cplusplus 304 # if 201103L <= __cplusplus 305 # define YY_NULLPTR nullptr 307 # define YY_NULLPTR 0 310 # define YY_NULLPTR ((void*)0) 318 # define HOAYYDEBUG 1 320 # define HOAYYDEBUG 0 323 # define HOAYYDEBUG 1 329 #line 330 "parseaut.hh" // lalr1.cc:401 341 #line 202 "parseaut.yy" // lalr1.cc:401 348 std::list<pair>* list;
350 std::vector<unsigned>* states;
352 #line 353 "parseaut.hh" // lalr1.cc:401 363 syntax_error (
const location_type& l,
const std::string& m)
364 : std::runtime_error (m)
369 : std::runtime_error (s.what ())
370 , location (s.location)
375 location_type location;
397 SPOT_HIGHLIGHT_EDGES = 271,
398 SPOT_HIGHLIGHT_STATES = 272,
441 enum { empty_symbol = -2 };
452 template <
typename Base>
464 #if 201103L <= YY_CPLUSPLUS 473 YY_MOVE_REF (location_type) l);
477 YY_RVREF (semantic_type) v,
478 YY_RVREF (location_type) l);
493 bool empty ()
const YY_NOEXCEPT;
505 #if YY_CPLUSPLUS < 201103L 517 #if 201103L <= YY_CPLUSPLUS 539 symbol_number_type type_get () const YY_NOEXCEPT;
542 token_type
token () const YY_NOEXCEPT;
555 parser (
void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
564 virtual int parse ();
567 std::ostream& debug_stream ()
const YY_ATTRIBUTE_PURE;
570 void set_debug_stream (std::ostream &);
575 debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
577 void set_debug_level (debug_level_type l);
583 virtual void error (
const location_type& loc,
const std::string& msg);
596 typedef int state_type;
601 virtual std::string yysyntax_error_ (state_type yystate,
607 state_type yy_lr_goto_state_ (state_type yystate,
int yysym);
611 static bool yy_pact_value_is_default_ (
int yyvalue);
615 static bool yy_table_value_is_error_ (
int yyvalue);
617 static const short yypact_ninf_;
618 static const signed char yytable_ninf_;
621 static token_number_type yytranslate_ (
int t);
626 static const short yypact_[];
631 static const unsigned char yydefact_[];
634 static const short yypgoto_[];
637 static const short yydefgoto_[];
642 static const short yytable_[];
644 static const short yycheck_[];
648 static const unsigned char yystos_[];
651 static const unsigned char yyr1_[];
654 static const unsigned char yyr2_[];
658 static std::string yytnamerr_ (
const char *n);
662 static const char*
const yytname_[];
665 static const unsigned short yyrline_[];
667 virtual void yy_reduce_print_ (
int r);
669 virtual void yystack_print_ ();
674 std::ostream* yycdebug_;
679 template <
typename Base>
687 template <
typename Base>
695 by_state () YY_NOEXCEPT;
698 typedef state_type kind_type;
701 by_state (kind_type s) YY_NOEXCEPT;
704 by_state (const by_state& that) YY_NOEXCEPT;
707 void clear () YY_NOEXCEPT;
710 void move (by_state& that);
714 symbol_number_type type_get () const YY_NOEXCEPT;
717 enum { empty_state = -1 };
730 stack_symbol_type ();
732 stack_symbol_type (YY_RVREF (stack_symbol_type) that);
734 stack_symbol_type (state_type s, YY_MOVE_REF (
symbol_type) sym);
735 #if YY_CPLUSPLUS < 201103L 736 stack_symbol_type& operator= (stack_symbol_type& that);
743 template <
typename T,
typename S = std::vector<T> >
748 typedef typename S::reverse_iterator iterator;
749 typedef typename S::const_reverse_iterator const_iterator;
750 typedef typename S::size_type size_type;
752 stack (size_type n = 200)
760 operator[] (size_type i)
762 return seq_[size () - 1 - i];
771 return operator[] (size_type (i));
778 operator[] (size_type i)
const 780 return seq_[size () - 1 - i];
787 operator[] (
int i)
const 789 return operator[] (size_type (i));
796 push (YY_MOVE_REF (T) t)
798 seq_.push_back (T ());
799 operator[] (0).move (t);
804 pop (
int n = 1) YY_NOEXCEPT
819 size () const YY_NOEXCEPT
826 begin () const YY_NOEXCEPT
828 return seq_.rbegin ();
833 end () const YY_NOEXCEPT
842 slice (
const stack& stack,
int range)
848 operator[] (
int i)
const 850 return stack_[range_ - i];
859 stack (
const stack&);
860 stack& operator= (
const stack&);
867 typedef stack<stack_symbol_type> stack_type;
877 void yypush_ (
const char* m, YY_MOVE_REF (stack_symbol_type) sym);
885 void yypush_ (
const char* m, state_type s, YY_MOVE_REF (
symbol_type) sym);
888 void yypop_ (
int n = 1);
906 spot::location initial_loc;
912 #line 913 "parseaut.hh" // lalr1.cc:401 917 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED Definition: parseaut.hh:96
An environment that describes atomic propositions.
Definition: environment.hh:32
Symbol semantic values.
Definition: parseaut.hh:339
semantic_type value
The semantic value.
Definition: parseaut.hh:499
Syntax errors thrown from user actions.
Definition: parseaut.hh:361
Definition: parseaut.hh:98
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:435
Definition: parseaut.hh:328
Definition: parseaut.hh:133
Tokens.
Definition: parseaut.hh:379
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:512
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:526
Base super_type
Alias to Base.
Definition: parseaut.hh:456
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:444
A class implementing Kleene's three-valued logic.
Definition: trival.hh:33
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:481
basic_symbol()
Default constructor.
Definition: parseaut.hh:459
spot::location location_type
Symbol locations.
Definition: parseaut.hh:358
Definition: parseaut.hh:73
A Bison parser.
Definition: parseaut.hh:334
"External" symbols: returned by the scanner.
Definition: parseaut.hh:551
Present a slice of the top of a stack.
Definition: parseaut.hh:839
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:487
Definition: parseaut.hh:453
An acceptance formula.
Definition: acc.hh:486
location_type location
The location.
Definition: parseaut.hh:502
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:438
An acceptance mark.
Definition: acc.hh:87
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:573