1 // A Bison parser, made by GNU Bison 3.7.5.
2
3 // Skeleton implementation 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 <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
33 // DO NOT RELY ON FEATURES THAT ARE NOT DOCUMENTED in the manual,
34 // especially those whose name start with YY_ or yy_. They are
35 // private implementation details that can be changed or removed.
36
37
38 // Take the name prefix into account.
39 #define yylex hoayylex
40
41
42
43 #include "parseaut.hh"
44
45
46 // Unqualified %code blocks.
47 #line 217 "parseaut.yy"
48
49 #include <sstream>
50
51 /* parseaut.hh and parsedecl.hh include each other recursively.
52 We must ensure that YYSTYPE is declared (by the above %union)
53 before parsedecl.hh uses it. */
54 #include <spot/parseaut/parsedecl.hh>
55
56 static void fill_guards(result_& res);
57
58 #line 59 "parseaut.cc"
59
60
61 #ifndef YY_
62 # if defined YYENABLE_NLS && YYENABLE_NLS
63 # if ENABLE_NLS
64 # include <libintl.h> // FIXME: INFRINGES ON USER NAME SPACE.
65 # define YY_(msgid) dgettext ("bison-runtime", msgid)
66 # endif
67 # endif
68 # ifndef YY_
69 # define YY_(msgid) msgid
70 # endif
71 #endif
72
73
74 // Whether we are compiled with exception support.
75 #ifndef YY_EXCEPTIONS
76 # if defined __GNUC__ && !defined __EXCEPTIONS
77 # define YY_EXCEPTIONS 0
78 # else
79 # define YY_EXCEPTIONS 1
80 # endif
81 #endif
82
83 #define YYRHSLOC(Rhs, K) ((Rhs)[K].location)
84 /* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N].
85 If N is 0, then set CURRENT to the empty location which ends
86 the previous symbol: RHS[0] (always defined). */
87
88 # ifndef YYLLOC_DEFAULT
89 # define YYLLOC_DEFAULT(Current, Rhs, N) \
90 do \
91 if (N) \
92 { \
93 (Current).begin = YYRHSLOC (Rhs, 1).begin; \
94 (Current).end = YYRHSLOC (Rhs, N).end; \
95 } \
96 else \
97 { \
98 (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end; \
99 } \
100 while (false)
101 # endif
102
103
104 // Enable debugging if requested.
105 #if HOAYYDEBUG
106
107 // A pseudo ostream that takes yydebug_ into account.
108 # define YYCDEBUG if (yydebug_) (*yycdebug_)
109
110 # define YY_SYMBOL_PRINT(Title, Symbol) \
111 do { \
112 if (yydebug_) \
113 { \
114 *yycdebug_ << Title << ' '; \
115 yy_print_ (*yycdebug_, Symbol); \
116 *yycdebug_ << '\n'; \
117 } \
118 } while (false)
119
120 # define YY_REDUCE_PRINT(Rule) \
121 do { \
122 if (yydebug_) \
123 yy_reduce_print_ (Rule); \
124 } while (false)
125
126 # define YY_STACK_PRINT() \
127 do { \
128 if (yydebug_) \
129 yy_stack_print_ (); \
130 } while (false)
131
132 #else // !HOAYYDEBUG
133
134 # define YYCDEBUG if (false) std::cerr
135 # define YY_SYMBOL_PRINT(Title, Symbol) YY_USE (Symbol)
136 # define YY_REDUCE_PRINT(Rule) static_cast<void> (0)
137 # define YY_STACK_PRINT() static_cast<void> (0)
138
139 #endif // !HOAYYDEBUG
140
141 #define yyerrok (yyerrstatus_ = 0)
142 #define yyclearin (yyla.clear ())
143
144 #define YYACCEPT goto yyacceptlab
145 #define YYABORT goto yyabortlab
146 #define YYERROR goto yyerrorlab
147 #define YYRECOVERING() (!!yyerrstatus_)
148
149 namespace hoayy {
150 #line 151 "parseaut.cc"
151
152 /// Build a parser object.
parser(void * scanner_yyarg,result_ & res_yyarg,spot::location initial_loc_yyarg)153 parser::parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg)
154 #if HOAYYDEBUG
155 : yydebug_ (false),
156 yycdebug_ (&std::cerr),
157 #else
158 :
159 #endif
160 scanner (scanner_yyarg),
161 res (res_yyarg),
162 initial_loc (initial_loc_yyarg)
163 {}
164
~parser()165 parser::~parser ()
166 {}
167
~syntax_error()168 parser::syntax_error::~syntax_error () YY_NOEXCEPT YY_NOTHROW
169 {}
170
171 /*---------------.
172 | symbol kinds. |
173 `---------------*/
174
175 // basic_symbol.
176 template <typename Base>
basic_symbol(const basic_symbol & that)177 parser::basic_symbol<Base>::basic_symbol (const basic_symbol& that)
178 : Base (that)
179 , value (that.value)
180 , location (that.location)
181 {}
182
183
184 /// Constructor for valueless symbols.
185 template <typename Base>
basic_symbol(typename Base::kind_type t,YY_MOVE_REF (location_type)l)186 parser::basic_symbol<Base>::basic_symbol (typename Base::kind_type t, YY_MOVE_REF (location_type) l)
187 : Base (t)
188 , value ()
189 , location (l)
190 {}
191
192 template <typename Base>
basic_symbol(typename Base::kind_type t,YY_RVREF (semantic_type)v,YY_RVREF (location_type)l)193 parser::basic_symbol<Base>::basic_symbol (typename Base::kind_type t, YY_RVREF (semantic_type) v, YY_RVREF (location_type) l)
194 : Base (t)
195 , value (YY_MOVE (v))
196 , location (YY_MOVE (l))
197 {}
198
199 template <typename Base>
200 parser::symbol_kind_type
type_get() const201 parser::basic_symbol<Base>::type_get () const YY_NOEXCEPT
202 {
203 return this->kind ();
204 }
205
206 template <typename Base>
207 bool
empty() const208 parser::basic_symbol<Base>::empty () const YY_NOEXCEPT
209 {
210 return this->kind () == symbol_kind::S_YYEMPTY;
211 }
212
213 template <typename Base>
214 void
move(basic_symbol & s)215 parser::basic_symbol<Base>::move (basic_symbol& s)
216 {
217 super_type::move (s);
218 value = YY_MOVE (s.value);
219 location = YY_MOVE (s.location);
220 }
221
222 // by_kind.
by_kind()223 parser::by_kind::by_kind ()
224 : kind_ (symbol_kind::S_YYEMPTY)
225 {}
226
227 #if 201103L <= YY_CPLUSPLUS
by_kind(by_kind && that)228 parser::by_kind::by_kind (by_kind&& that)
229 : kind_ (that.kind_)
230 {
231 that.clear ();
232 }
233 #endif
234
by_kind(const by_kind & that)235 parser::by_kind::by_kind (const by_kind& that)
236 : kind_ (that.kind_)
237 {}
238
by_kind(token_kind_type t)239 parser::by_kind::by_kind (token_kind_type t)
240 : kind_ (yytranslate_ (t))
241 {}
242
243 void
clear()244 parser::by_kind::clear () YY_NOEXCEPT
245 {
246 kind_ = symbol_kind::S_YYEMPTY;
247 }
248
249 void
move(by_kind & that)250 parser::by_kind::move (by_kind& that)
251 {
252 kind_ = that.kind_;
253 that.clear ();
254 }
255
256 parser::symbol_kind_type
kind() const257 parser::by_kind::kind () const YY_NOEXCEPT
258 {
259 return kind_;
260 }
261
262 parser::symbol_kind_type
type_get() const263 parser::by_kind::type_get () const YY_NOEXCEPT
264 {
265 return this->kind ();
266 }
267
268
269 // by_state.
by_state()270 parser::by_state::by_state () YY_NOEXCEPT
271 : state (empty_state)
272 {}
273
by_state(const by_state & that)274 parser::by_state::by_state (const by_state& that) YY_NOEXCEPT
275 : state (that.state)
276 {}
277
278 void
clear()279 parser::by_state::clear () YY_NOEXCEPT
280 {
281 state = empty_state;
282 }
283
284 void
move(by_state & that)285 parser::by_state::move (by_state& that)
286 {
287 state = that.state;
288 that.clear ();
289 }
290
by_state(state_type s)291 parser::by_state::by_state (state_type s) YY_NOEXCEPT
292 : state (s)
293 {}
294
295 parser::symbol_kind_type
kind() const296 parser::by_state::kind () const YY_NOEXCEPT
297 {
298 if (state == empty_state)
299 return symbol_kind::S_YYEMPTY;
300 else
301 return YY_CAST (symbol_kind_type, yystos_[+state]);
302 }
303
stack_symbol_type()304 parser::stack_symbol_type::stack_symbol_type ()
305 {}
306
stack_symbol_type(YY_RVREF (stack_symbol_type)that)307 parser::stack_symbol_type::stack_symbol_type (YY_RVREF (stack_symbol_type) that)
308 : super_type (YY_MOVE (that.state), YY_MOVE (that.value), YY_MOVE (that.location))
309 {
310 #if 201103L <= YY_CPLUSPLUS
311 // that is emptied.
312 that.state = empty_state;
313 #endif
314 }
315
stack_symbol_type(state_type s,YY_MOVE_REF (symbol_type)that)316 parser::stack_symbol_type::stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) that)
317 : super_type (s, YY_MOVE (that.value), YY_MOVE (that.location))
318 {
319 // that is emptied.
320 that.kind_ = symbol_kind::S_YYEMPTY;
321 }
322
323 #if YY_CPLUSPLUS < 201103L
324 parser::stack_symbol_type&
operator =(const stack_symbol_type & that)325 parser::stack_symbol_type::operator= (const stack_symbol_type& that)
326 {
327 state = that.state;
328 value = that.value;
329 location = that.location;
330 return *this;
331 }
332
333 parser::stack_symbol_type&
operator =(stack_symbol_type & that)334 parser::stack_symbol_type::operator= (stack_symbol_type& that)
335 {
336 state = that.state;
337 value = that.value;
338 location = that.location;
339 // that is emptied.
340 that.state = empty_state;
341 return *this;
342 }
343 #endif
344
345 template <typename Base>
346 void
yy_destroy_(const char * yymsg,basic_symbol<Base> & yysym) const347 parser::yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const
348 {
349 if (yymsg)
350 YY_SYMBOL_PRINT (yymsg, yysym);
351
352 // User destructor.
353 switch (yysym.kind ())
354 {
355 case symbol_kind::S_IDENTIFIER: // "identifier"
356 #line 308 "parseaut.yy"
357 { delete (yysym.value.str); }
358 #line 359 "parseaut.cc"
359 break;
360
361 case symbol_kind::S_HEADERNAME: // "header name"
362 #line 308 "parseaut.yy"
363 { delete (yysym.value.str); }
364 #line 365 "parseaut.cc"
365 break;
366
367 case symbol_kind::S_ANAME: // "alias name"
368 #line 308 "parseaut.yy"
369 { delete (yysym.value.str); }
370 #line 371 "parseaut.cc"
371 break;
372
373 case symbol_kind::S_STRING: // "string"
374 #line 308 "parseaut.yy"
375 { delete (yysym.value.str); }
376 #line 377 "parseaut.cc"
377 break;
378
379 case symbol_kind::S_24_: // '['
380 #line 308 "parseaut.yy"
381 { delete (yysym.value.str); }
382 #line 383 "parseaut.cc"
383 break;
384
385 case symbol_kind::S_LINEDIRECTIVE: // "#line"
386 #line 308 "parseaut.yy"
387 { delete (yysym.value.str); }
388 #line 389 "parseaut.cc"
389 break;
390
391 case symbol_kind::S_BDD: // BDD
392 #line 309 "parseaut.yy"
393 { bdd_delref((yysym.value.b)); }
394 #line 395 "parseaut.cc"
395 break;
396
397 case symbol_kind::S_FORMULA: // "boolean formula"
398 #line 308 "parseaut.yy"
399 { delete (yysym.value.str); }
400 #line 401 "parseaut.cc"
401 break;
402
403 case symbol_kind::S_string_opt: // string_opt
404 #line 308 "parseaut.yy"
405 { delete (yysym.value.str); }
406 #line 407 "parseaut.cc"
407 break;
408
409 case symbol_kind::S_96_state_conj_2: // state-conj-2
410 #line 312 "parseaut.yy"
411 { delete (yysym.value.states); }
412 #line 413 "parseaut.cc"
413 break;
414
415 case symbol_kind::S_97_init_state_conj_2: // init-state-conj-2
416 #line 312 "parseaut.yy"
417 { delete (yysym.value.states); }
418 #line 419 "parseaut.cc"
419 break;
420
421 case symbol_kind::S_98_label_expr: // label-expr
422 #line 309 "parseaut.yy"
423 { bdd_delref((yysym.value.b)); }
424 #line 425 "parseaut.cc"
425 break;
426
427 case symbol_kind::S_100_acceptance_cond: // acceptance-cond
428 #line 311 "parseaut.yy"
429 { delete (yysym.value.code); }
430 #line 431 "parseaut.cc"
431 break;
432
433 case symbol_kind::S_118_state_conj_checked: // state-conj-checked
434 #line 312 "parseaut.yy"
435 { delete (yysym.value.states); }
436 #line 437 "parseaut.cc"
437 break;
438
439 case symbol_kind::S_135_nc_one_ident: // nc-one-ident
440 #line 308 "parseaut.yy"
441 { delete (yysym.value.str); }
442 #line 443 "parseaut.cc"
443 break;
444
445 case symbol_kind::S_136_nc_ident_list: // nc-ident-list
446 #line 308 "parseaut.yy"
447 { delete (yysym.value.str); }
448 #line 449 "parseaut.cc"
449 break;
450
451 case symbol_kind::S_137_nc_transition_block: // nc-transition-block
452 #line 327 "parseaut.yy"
453 {
454 for (auto i = (yysym.value.list)->begin(); i != (yysym.value.list)->end(); ++i)
455 {
456 bdd_delref(i->first);
457 delete i->second;
458 }
459 delete (yysym.value.list);
460 }
461 #line 462 "parseaut.cc"
462 break;
463
464 case symbol_kind::S_139_nc_transitions: // nc-transitions
465 #line 327 "parseaut.yy"
466 {
467 for (auto i = (yysym.value.list)->begin(); i != (yysym.value.list)->end(); ++i)
468 {
469 bdd_delref(i->first);
470 delete i->second;
471 }
472 delete (yysym.value.list);
473 }
474 #line 475 "parseaut.cc"
475 break;
476
477 case symbol_kind::S_140_nc_formula_or_ident: // nc-formula-or-ident
478 #line 308 "parseaut.yy"
479 { delete (yysym.value.str); }
480 #line 481 "parseaut.cc"
481 break;
482
483 case symbol_kind::S_141_nc_formula: // nc-formula
484 #line 309 "parseaut.yy"
485 { bdd_delref((yysym.value.b)); }
486 #line 487 "parseaut.cc"
487 break;
488
489 case symbol_kind::S_142_nc_opt_dest: // nc-opt-dest
490 #line 308 "parseaut.yy"
491 { delete (yysym.value.str); }
492 #line 493 "parseaut.cc"
493 break;
494
495 case symbol_kind::S_143_nc_src_dest: // nc-src-dest
496 #line 310 "parseaut.yy"
497 { bdd_delref((yysym.value.p)->first); delete (yysym.value.p)->second; delete (yysym.value.p); }
498 #line 499 "parseaut.cc"
499 break;
500
501 case symbol_kind::S_144_nc_transition: // nc-transition
502 #line 310 "parseaut.yy"
503 { bdd_delref((yysym.value.p)->first); delete (yysym.value.p)->second; delete (yysym.value.p); }
504 #line 505 "parseaut.cc"
505 break;
506
507 default:
508 break;
509 }
510 }
511
512 #if HOAYYDEBUG
513 template <typename Base>
514 void
yy_print_(std::ostream & yyo,const basic_symbol<Base> & yysym) const515 parser::yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const
516 {
517 std::ostream& yyoutput = yyo;
518 YY_USE (yyoutput);
519 if (yysym.empty ())
520 yyo << "empty symbol";
521 else
522 {
523 symbol_kind_type yykind = yysym.kind ();
524 yyo << (yykind < YYNTOKENS ? "token" : "nterm")
525 << ' ' << yysym.name () << " ("
526 << yysym.location << ": ";
527 switch (yykind)
528 {
529 case symbol_kind::S_IDENTIFIER: // "identifier"
530 #line 335 "parseaut.yy"
531 {
532 if ((yysym.value.str))
533 debug_stream() << *(yysym.value.str);
534 else
535 debug_stream() << "\"\""; }
536 #line 537 "parseaut.cc"
537 break;
538
539 case symbol_kind::S_HEADERNAME: // "header name"
540 #line 335 "parseaut.yy"
541 {
542 if ((yysym.value.str))
543 debug_stream() << *(yysym.value.str);
544 else
545 debug_stream() << "\"\""; }
546 #line 547 "parseaut.cc"
547 break;
548
549 case symbol_kind::S_ANAME: // "alias name"
550 #line 335 "parseaut.yy"
551 {
552 if ((yysym.value.str))
553 debug_stream() << *(yysym.value.str);
554 else
555 debug_stream() << "\"\""; }
556 #line 557 "parseaut.cc"
557 break;
558
559 case symbol_kind::S_STRING: // "string"
560 #line 335 "parseaut.yy"
561 {
562 if ((yysym.value.str))
563 debug_stream() << *(yysym.value.str);
564 else
565 debug_stream() << "\"\""; }
566 #line 567 "parseaut.cc"
567 break;
568
569 case symbol_kind::S_INT: // "integer"
570 #line 340 "parseaut.yy"
571 { debug_stream() << (yysym.value.num); }
572 #line 573 "parseaut.cc"
573 break;
574
575 case symbol_kind::S_24_: // '['
576 #line 335 "parseaut.yy"
577 {
578 if ((yysym.value.str))
579 debug_stream() << *(yysym.value.str);
580 else
581 debug_stream() << "\"\""; }
582 #line 583 "parseaut.cc"
583 break;
584
585 case symbol_kind::S_LINEDIRECTIVE: // "#line"
586 #line 335 "parseaut.yy"
587 {
588 if ((yysym.value.str))
589 debug_stream() << *(yysym.value.str);
590 else
591 debug_stream() << "\"\""; }
592 #line 593 "parseaut.cc"
593 break;
594
595 case symbol_kind::S_FORMULA: // "boolean formula"
596 #line 335 "parseaut.yy"
597 {
598 if ((yysym.value.str))
599 debug_stream() << *(yysym.value.str);
600 else
601 debug_stream() << "\"\""; }
602 #line 603 "parseaut.cc"
603 break;
604
605 case symbol_kind::S_LBTT: // "LBTT header"
606 #line 340 "parseaut.yy"
607 { debug_stream() << (yysym.value.num); }
608 #line 609 "parseaut.cc"
609 break;
610
611 case symbol_kind::S_INT_S: // "state acceptance"
612 #line 340 "parseaut.yy"
613 { debug_stream() << (yysym.value.num); }
614 #line 615 "parseaut.cc"
615 break;
616
617 case symbol_kind::S_LBTT_EMPTY: // "acceptance sets for empty automaton"
618 #line 340 "parseaut.yy"
619 { debug_stream() << (yysym.value.num); }
620 #line 621 "parseaut.cc"
621 break;
622
623 case symbol_kind::S_ACC: // "acceptance set"
624 #line 340 "parseaut.yy"
625 { debug_stream() << (yysym.value.num); }
626 #line 627 "parseaut.cc"
627 break;
628
629 case symbol_kind::S_STATE_NUM: // "state number"
630 #line 340 "parseaut.yy"
631 { debug_stream() << (yysym.value.num); }
632 #line 633 "parseaut.cc"
633 break;
634
635 case symbol_kind::S_DEST_NUM: // "destination number"
636 #line 340 "parseaut.yy"
637 { debug_stream() << (yysym.value.num); }
638 #line 639 "parseaut.cc"
639 break;
640
641 case symbol_kind::S_string_opt: // string_opt
642 #line 335 "parseaut.yy"
643 {
644 if ((yysym.value.str))
645 debug_stream() << *(yysym.value.str);
646 else
647 debug_stream() << "\"\""; }
648 #line 649 "parseaut.cc"
649 break;
650
651 case symbol_kind::S_96_state_conj_2: // state-conj-2
652 #line 313 "parseaut.yy"
653 {
654 auto& os = debug_stream();
655 os << '{';
656 bool notfirst = false;
657 for (auto i: *(yysym.value.states))
658 {
659 if (notfirst)
660 os << ", ";
661 else
662 notfirst = true;
663 os << i;
664 }
665 os << '}';
666 }
667 #line 668 "parseaut.cc"
668 break;
669
670 case symbol_kind::S_97_init_state_conj_2: // init-state-conj-2
671 #line 313 "parseaut.yy"
672 {
673 auto& os = debug_stream();
674 os << '{';
675 bool notfirst = false;
676 for (auto i: *(yysym.value.states))
677 {
678 if (notfirst)
679 os << ", ";
680 else
681 notfirst = true;
682 os << i;
683 }
684 os << '}';
685 }
686 #line 687 "parseaut.cc"
687 break;
688
689 case symbol_kind::S_99_acc_set: // acc-set
690 #line 340 "parseaut.yy"
691 { debug_stream() << (yysym.value.num); }
692 #line 693 "parseaut.cc"
693 break;
694
695 case symbol_kind::S_102_state_num: // state-num
696 #line 340 "parseaut.yy"
697 { debug_stream() << (yysym.value.num); }
698 #line 699 "parseaut.cc"
699 break;
700
701 case symbol_kind::S_103_checked_state_num: // checked-state-num
702 #line 340 "parseaut.yy"
703 { debug_stream() << (yysym.value.num); }
704 #line 705 "parseaut.cc"
705 break;
706
707 case symbol_kind::S_118_state_conj_checked: // state-conj-checked
708 #line 313 "parseaut.yy"
709 {
710 auto& os = debug_stream();
711 os << '{';
712 bool notfirst = false;
713 for (auto i: *(yysym.value.states))
714 {
715 if (notfirst)
716 os << ", ";
717 else
718 notfirst = true;
719 os << i;
720 }
721 os << '}';
722 }
723 #line 724 "parseaut.cc"
724 break;
725
726 case symbol_kind::S_sign: // sign
727 #line 340 "parseaut.yy"
728 { debug_stream() << (yysym.value.num); }
729 #line 730 "parseaut.cc"
730 break;
731
732 case symbol_kind::S_135_nc_one_ident: // nc-one-ident
733 #line 335 "parseaut.yy"
734 {
735 if ((yysym.value.str))
736 debug_stream() << *(yysym.value.str);
737 else
738 debug_stream() << "\"\""; }
739 #line 740 "parseaut.cc"
740 break;
741
742 case symbol_kind::S_136_nc_ident_list: // nc-ident-list
743 #line 335 "parseaut.yy"
744 {
745 if ((yysym.value.str))
746 debug_stream() << *(yysym.value.str);
747 else
748 debug_stream() << "\"\""; }
749 #line 750 "parseaut.cc"
750 break;
751
752 case symbol_kind::S_140_nc_formula_or_ident: // nc-formula-or-ident
753 #line 335 "parseaut.yy"
754 {
755 if ((yysym.value.str))
756 debug_stream() << *(yysym.value.str);
757 else
758 debug_stream() << "\"\""; }
759 #line 760 "parseaut.cc"
760 break;
761
762 case symbol_kind::S_142_nc_opt_dest: // nc-opt-dest
763 #line 335 "parseaut.yy"
764 {
765 if ((yysym.value.str))
766 debug_stream() << *(yysym.value.str);
767 else
768 debug_stream() << "\"\""; }
769 #line 770 "parseaut.cc"
770 break;
771
772 default:
773 break;
774 }
775 yyo << ')';
776 }
777 }
778 #endif
779
780 void
yypush_(const char * m,YY_MOVE_REF (stack_symbol_type)sym)781 parser::yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym)
782 {
783 if (m)
784 YY_SYMBOL_PRINT (m, sym);
785 yystack_.push (YY_MOVE (sym));
786 }
787
788 void
yypush_(const char * m,state_type s,YY_MOVE_REF (symbol_type)sym)789 parser::yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym)
790 {
791 #if 201103L <= YY_CPLUSPLUS
792 yypush_ (m, stack_symbol_type (s, std::move (sym)));
793 #else
794 stack_symbol_type ss (s, sym);
795 yypush_ (m, ss);
796 #endif
797 }
798
799 void
yypop_(int n)800 parser::yypop_ (int n)
801 {
802 yystack_.pop (n);
803 }
804
805 #if HOAYYDEBUG
806 std::ostream&
debug_stream() const807 parser::debug_stream () const
808 {
809 return *yycdebug_;
810 }
811
812 void
set_debug_stream(std::ostream & o)813 parser::set_debug_stream (std::ostream& o)
814 {
815 yycdebug_ = &o;
816 }
817
818
819 parser::debug_level_type
debug_level() const820 parser::debug_level () const
821 {
822 return yydebug_;
823 }
824
825 void
set_debug_level(debug_level_type l)826 parser::set_debug_level (debug_level_type l)
827 {
828 yydebug_ = l;
829 }
830 #endif // HOAYYDEBUG
831
832 parser::state_type
yy_lr_goto_state_(state_type yystate,int yysym)833 parser::yy_lr_goto_state_ (state_type yystate, int yysym)
834 {
835 int yyr = yypgoto_[yysym - YYNTOKENS] + yystate;
836 if (0 <= yyr && yyr <= yylast_ && yycheck_[yyr] == yystate)
837 return yytable_[yyr];
838 else
839 return yydefgoto_[yysym - YYNTOKENS];
840 }
841
842 bool
yy_pact_value_is_default_(int yyvalue)843 parser::yy_pact_value_is_default_ (int yyvalue)
844 {
845 return yyvalue == yypact_ninf_;
846 }
847
848 bool
yy_table_value_is_error_(int yyvalue)849 parser::yy_table_value_is_error_ (int yyvalue)
850 {
851 return yyvalue == yytable_ninf_;
852 }
853
854 int
operator ()()855 parser::operator() ()
856 {
857 return parse ();
858 }
859
860 int
parse()861 parser::parse ()
862 {
863 int yyn;
864 /// Length of the RHS of the rule being reduced.
865 int yylen = 0;
866
867 // Error handling.
868 int yynerrs_ = 0;
869 int yyerrstatus_ = 0;
870
871 /// The lookahead symbol.
872 symbol_type yyla;
873
874 /// The locations where the error started and ended.
875 stack_symbol_type yyerror_range[3];
876
877 /// The return value of parse ().
878 int yyresult;
879
880 #if YY_EXCEPTIONS
881 try
882 #endif // YY_EXCEPTIONS
883 {
884 YYCDEBUG << "Starting parse\n";
885
886
887 // User initialization code.
888 #line 202 "parseaut.yy"
889 { yyla.location = res.h->loc = initial_loc; }
890
891 #line 892 "parseaut.cc"
892
893
894 /* Initialize the stack. The initial state will be set in
895 yynewstate, since the latter expects the semantical and the
896 location values to have been already stored, initialize these
897 stacks with a primary value. */
898 yystack_.clear ();
899 yypush_ (YY_NULLPTR, 0, YY_MOVE (yyla));
900
901 /*-----------------------------------------------.
902 | yynewstate -- push a new symbol on the stack. |
903 `-----------------------------------------------*/
904 yynewstate:
905 YYCDEBUG << "Entering state " << int (yystack_[0].state) << '\n';
906 YY_STACK_PRINT ();
907
908 // Accept?
909 if (yystack_[0].state == yyfinal_)
910 YYACCEPT;
911
912 goto yybackup;
913
914
915 /*-----------.
916 | yybackup. |
917 `-----------*/
918 yybackup:
919 // Try to take a decision without lookahead.
920 yyn = yypact_[+yystack_[0].state];
921 if (yy_pact_value_is_default_ (yyn))
922 goto yydefault;
923
924 // Read a lookahead token.
925 if (yyla.empty ())
926 {
927 YYCDEBUG << "Reading a token\n";
928 #if YY_EXCEPTIONS
929 try
930 #endif // YY_EXCEPTIONS
931 {
932 yyla.kind_ = yytranslate_ (yylex (&yyla.value, &yyla.location, scanner, PARSE_ERROR_LIST));
933 }
934 #if YY_EXCEPTIONS
935 catch (const syntax_error& yyexc)
936 {
937 YYCDEBUG << "Caught exception: " << yyexc.what() << '\n';
938 error (yyexc);
939 goto yyerrlab1;
940 }
941 #endif // YY_EXCEPTIONS
942 }
943 YY_SYMBOL_PRINT ("Next token is", yyla);
944
945 if (yyla.kind () == symbol_kind::S_YYerror)
946 {
947 // The scanner already issued an error message, process directly
948 // to error recovery. But do not keep the error token as
949 // lookahead, it is too special and may lead us to an endless
950 // loop in error recovery. */
951 yyla.kind_ = symbol_kind::S_YYUNDEF;
952 goto yyerrlab1;
953 }
954
955 /* If the proper action on seeing token YYLA.TYPE is to reduce or
956 to detect an error, take that action. */
957 yyn += yyla.kind ();
958 if (yyn < 0 || yylast_ < yyn || yycheck_[yyn] != yyla.kind ())
959 {
960 goto yydefault;
961 }
962
963 // Reduce or error.
964 yyn = yytable_[yyn];
965 if (yyn <= 0)
966 {
967 if (yy_table_value_is_error_ (yyn))
968 goto yyerrlab;
969 yyn = -yyn;
970 goto yyreduce;
971 }
972
973 // Count tokens shifted since error; after three, turn off error status.
974 if (yyerrstatus_)
975 --yyerrstatus_;
976
977 // Shift the lookahead token.
978 yypush_ ("Shifting", state_type (yyn), YY_MOVE (yyla));
979 goto yynewstate;
980
981
982 /*-----------------------------------------------------------.
983 | yydefault -- do the default action for the current state. |
984 `-----------------------------------------------------------*/
985 yydefault:
986 yyn = yydefact_[+yystack_[0].state];
987 if (yyn == 0)
988 goto yyerrlab;
989 goto yyreduce;
990
991
992 /*-----------------------------.
993 | yyreduce -- do a reduction. |
994 `-----------------------------*/
995 yyreduce:
996 yylen = yyr2_[yyn];
997 {
998 stack_symbol_type yylhs;
999 yylhs.state = yy_lr_goto_state_ (yystack_[yylen].state, yyr1_[yyn]);
1000 /* If YYLEN is nonzero, implement the default value of the
1001 action: '$$ = $1'. Otherwise, use the top of the stack.
1002
1003 Otherwise, the following line sets YYLHS.VALUE to garbage.
1004 This behavior is undocumented and Bison users should not rely
1005 upon it. */
1006 if (yylen)
1007 yylhs.value = yystack_[yylen - 1].value;
1008 else
1009 yylhs.value = yystack_[0].value;
1010
1011 // Default location.
1012 {
1013 stack_type::slice range (yystack_, yylen);
1014 YYLLOC_DEFAULT (yylhs.location, range, yylen);
1015 yyerror_range[1].location = yylhs.location;
1016 }
1017
1018 // Perform the reduction.
1019 YY_REDUCE_PRINT (yyn);
1020 #if YY_EXCEPTIONS
1021 try
1022 #endif // YY_EXCEPTIONS
1023 {
1024 switch (yyn)
1025 {
1026 case 2: // aut: aut-1
1027 #line 343 "parseaut.yy"
1028 { res.h->loc = yylhs.location; YYACCEPT; }
1029 #line 1030 "parseaut.cc"
1030 break;
1031
1032 case 3: // $@1: %empty
1033 #line 347 "parseaut.yy"
1034 { res.h->filename = *(yystack_[0].value.str); }
1035 #line 1036 "parseaut.cc"
1036 break;
1037
1038 case 5: // aut: "end of file"
1039 #line 348 "parseaut.yy"
1040 { YYABORT; }
1041 #line 1042 "parseaut.cc"
1042 break;
1043
1044 case 6: // aut: error "end of file"
1045 #line 349 "parseaut.yy"
1046 { YYABORT; }
1047 #line 1048 "parseaut.cc"
1048 break;
1049
1050 case 7: // aut: error aut-1
1051 #line 351 "parseaut.yy"
1052 {
1053 error(yystack_[1].location, "leading garbage was ignored");
1054 res.h->loc = yystack_[0].location;
1055 YYACCEPT;
1056 }
1057 #line 1058 "parseaut.cc"
1058 break;
1059
1060 case 8: // aut-1: hoa
1061 #line 357 "parseaut.yy"
1062 { res.h->type = spot::parsed_aut_type::HOA; }
1063 #line 1064 "parseaut.cc"
1064 break;
1065
1066 case 9: // aut-1: never
1067 #line 358 "parseaut.yy"
1068 { res.h->type = spot::parsed_aut_type::NeverClaim; }
1069 #line 1070 "parseaut.cc"
1070 break;
1071
1072 case 10: // aut-1: lbtt
1073 #line 359 "parseaut.yy"
1074 { res.h->type = spot::parsed_aut_type::LBTT; }
1075 #line 1076 "parseaut.cc"
1076 break;
1077
1078 case 14: // string_opt: %empty
1079 #line 369 "parseaut.yy"
1080 { (yylhs.value.str) = nullptr; }
1081 #line 1082 "parseaut.cc"
1082 break;
1083
1084 case 15: // string_opt: "string"
1085 #line 370 "parseaut.yy"
1086 { (yylhs.value.str) = (yystack_[0].value.str); }
1087 #line 1088 "parseaut.cc"
1088 break;
1089
1090 case 18: // header: format-version header-items
1091 #line 374 "parseaut.yy"
1092 {
1093 bool v1plus = strverscmp("v1", res.format_version.c_str()) < 0;
1094 // Preallocate the states if we know their number.
1095 if (res.states >= 0)
1096 {
1097 unsigned states = res.states;
1098 for (auto& p : res.start)
1099 for (unsigned s: p.second)
1100 if ((unsigned) res.states <= s)
1101 {
1102 error(p.first, "initial state number is larger "
1103 "than state count...");
1104 error(res.states_loc, "... declared here.");
1105 states = std::max(states, s + 1);
1106 }
1107 if (res.opts.want_kripke)
1108 res.h->ks->new_states(states, bddfalse);
1109 else
1110 res.h->aut->new_states(states);
1111 res.info_states.resize(states);
1112 }
1113 if (res.accset < 0)
1114 {
1115 error(yylhs.location, "missing 'Acceptance:' header");
1116 res.ignore_acc = true;
1117 }
1118 if (res.unknown_ap_max >= 0 && !res.ignore_more_ap)
1119 {
1120 error(res.unknown_ap_max_location,
1121 "atomic proposition used in Alias without AP declaration");
1122 for (auto& p: res.alias)
1123 p.second = bddtrue;
1124 }
1125 // Process properties.
1126 {
1127 auto explicit_labels = res.prop_is_true("explicit-labels");
1128 auto implicit_labels = res.prop_is_true("implicit-labels");
1129
1130 if (implicit_labels)
1131 {
1132 if (res.opts.want_kripke)
1133 error(implicit_labels.loc,
1134 "Kripke structure may not use implicit labels");
1135
1136 if (explicit_labels)
1137 {
1138 error(implicit_labels.loc,
1139 "'properties: implicit-labels' is incompatible "
1140 "with...");
1141 error(explicit_labels.loc,
1142 "... 'properties: explicit-labels'.");
1143 }
1144 else
1145 {
1146 res.label_style = Implicit_Labels;
1147 }
1148 }
1149
1150 auto trans_labels = res.prop_is_true("trans-labels");
1151 auto state_labels = res.prop_is_true("state-labels");
1152
1153 if (trans_labels)
1154 {
1155 if (res.opts.want_kripke)
1156 error(trans_labels.loc,
1157 "Kripke structures may not use transition labels");
1158
1159 if (state_labels)
1160 {
1161 error(trans_labels.loc,
1162 "'properties: trans-labels' is incompatible with...");
1163 error(state_labels.loc,
1164 "... 'properties: state-labels'.");
1165 }
1166 else
1167 {
1168 if (res.label_style != Implicit_Labels)
1169 res.label_style = Trans_Labels;
1170 }
1171 }
1172 else if (state_labels)
1173 {
1174 if (res.label_style != Implicit_Labels)
1175 {
1176 res.label_style = State_Labels;
1177 }
1178 else
1179 {
1180 error(state_labels.loc,
1181 "'properties: state-labels' is incompatible with...");
1182 error(implicit_labels.loc,
1183 "... 'properties: implicit-labels'.");
1184 }
1185 }
1186
1187 if (res.opts.want_kripke && res.label_style != State_Labels)
1188 error(yylhs.location,
1189 "Kripke structures should use 'properties: state-labels'");
1190
1191 auto state_acc = res.prop_is_true("state-acc");
1192 auto trans_acc = res.prop_is_true("trans-acc");
1193 if (trans_acc)
1194 {
1195 if (state_acc)
1196 {
1197 error(trans_acc.loc,
1198 "'properties: trans-acc' is incompatible with...");
1199 error(state_acc.loc,
1200 "... 'properties: state-acc'.");
1201 }
1202 else
1203 {
1204 res.acc_style = Trans_Acc;
1205 }
1206 }
1207 else if (state_acc)
1208 {
1209 res.acc_style = State_Acc;
1210 }
1211
1212 if (auto univ_branch = res.prop_is_true("univ-branch"))
1213 if (res.opts.want_kripke)
1214 error(univ_branch.loc,
1215 "Kripke structures may not use 'properties: univ-branch'");
1216 }
1217 {
1218 unsigned ss = res.start.size();
1219 auto det = res.prop_is_true("deterministic");
1220 auto no_exist = res.prop_is_false("exist-branch");
1221 if (ss > 1)
1222 {
1223 if (det)
1224 {
1225 error(det.loc,
1226 "deterministic automata should have at most "
1227 "one initial state");
1228 res.universal = spot::trival::maybe();
1229 }
1230 else if (no_exist)
1231 {
1232 error(no_exist.loc,
1233 "universal automata should have at most "
1234 "one initial state");
1235 res.universal = spot::trival::maybe();
1236 }
1237 }
1238 else
1239 {
1240 // Assume the automaton is deterministic until proven
1241 // wrong, or unless we are building a Kripke structure.
1242 if (!res.opts.want_kripke)
1243 {
1244 res.universal = true;
1245 res.existential = true;
1246 }
1247 }
1248 for (auto& ss: res.start)
1249 {
1250 if (ss.second.size() > 1)
1251 {
1252 if (auto no_univ = res.prop_is_false("univ-branch"))
1253 {
1254 error(ss.first,
1255 "conjunct initial state despite...");
1256 error(no_univ.loc, "... property: !univ-branch");
1257 }
1258 else if (v1plus)
1259 if (auto det = res.prop_is_true("deterministic"))
1260 {
1261 error(ss.first,
1262 "conjunct initial state despite...");
1263 error(det.loc, "... property: deterministic");
1264 }
1265 res.existential = false;
1266 }
1267 }
1268 auto complete = res.prop_is_true("complete");
1269 if (ss < 1)
1270 {
1271 if (complete)
1272 {
1273 error(complete.loc,
1274 "complete automata should have at least "
1275 "one initial state");
1276 }
1277 res.complete = false;
1278 }
1279 else
1280 {
1281 // Assume the automaton is complete until proven
1282 // wrong.
1283 if (!res.opts.want_kripke)
1284 res.complete = true;
1285 }
1286 // if ap_count == 0, then a Kripke structure could be
1287 // declared complete, although that probably doesn't
1288 // matter.
1289 if (res.opts.want_kripke && complete && res.ap_count > 0)
1290 error(complete.loc,
1291 "Kripke structure may not be complete");
1292 }
1293 if (res.opts.trust_hoa)
1294 {
1295 auto& a = res.aut_or_ks;
1296 auto& p = res.props;
1297 auto e = p.end();
1298 auto si = p.find("stutter-invariant");
1299 if (si != e)
1300 {
1301 a->prop_stutter_invariant(si->second.val);
1302 auto i = p.find("stutter-sensitive");
1303 if (i != e && si->second.val == i->second.val)
1304 error(i->second.loc,
1305 "automaton cannot be both stutter-invariant"
1306 "and stutter-sensitive");
1307 }
1308 else
1309 {
1310 auto ss = p.find("stutter-sensitive");
1311 if (ss != e)
1312 a->prop_stutter_invariant(!ss->second.val);
1313 }
1314 auto iw = p.find("inherently-weak");
1315 auto vw = p.find("very-weak");
1316 auto w = p.find("weak");
1317 auto t = p.find("terminal");
1318 if (vw != e)
1319 {
1320 a->prop_very_weak(vw->second.val);
1321 if (w != e && !w->second.val && vw->second.val)
1322 {
1323 error(w->second.loc,
1324 "'properties: !weak' contradicts...");
1325 error(vw->second.loc,
1326 "... 'properties: very-weak' given here");
1327 }
1328 if (iw != e && !iw->second.val && vw->second.val)
1329 {
1330 error(iw->second.loc,
1331 "'properties: !inherently-weak' contradicts...");
1332 error(vw->second.loc,
1333 "... 'properties: very-weak' given here");
1334 }
1335 }
1336 if (iw != e)
1337 {
1338 a->prop_inherently_weak(iw->second.val);
1339 if (w != e && !iw->second.val && w->second.val)
1340 {
1341 error(w->second.loc, "'properties: weak' contradicts...");
1342 error(iw->second.loc,
1343 "... 'properties: !inherently-weak' given here");
1344 }
1345 if (t != e && !iw->second.val && t->second.val)
1346 {
1347 error(t->second.loc,
1348 "'properties: terminal' contradicts...");
1349 error(iw->second.loc,
1350 "... 'properties: !inherently-weak' given here");
1351 }
1352 }
1353 if (w != e)
1354 {
1355 a->prop_weak(w->second.val);
1356 if (t != e && !w->second.val && t->second.val)
1357 {
1358 error(t->second.loc,
1359 "'properties: terminal' contradicts...");
1360 error(w->second.loc,
1361 "... 'properties: !weak' given here");
1362 }
1363 }
1364 if (t != e)
1365 a->prop_terminal(t->second.val);
1366 auto u = p.find("unambiguous");
1367 if (u != e)
1368 {
1369 a->prop_unambiguous(u->second.val);
1370 auto d = p.find("deterministic");
1371 if (d != e && !u->second.val && d->second.val)
1372 {
1373 error(d->second.loc,
1374 "'properties: deterministic' contradicts...");
1375 error(u->second.loc,
1376 "... 'properties: !unambiguous' given here");
1377 }
1378 }
1379 auto sd = p.find("semi-deterministic");
1380 if (sd != e)
1381 {
1382 a->prop_semi_deterministic(sd->second.val);
1383 auto d = p.find("deterministic");
1384 if (d != e && !sd->second.val && d->second.val)
1385 {
1386 error(d->second.loc,
1387 "'properties: deterministic' contradicts...");
1388 error(sd->second.loc,
1389 "... 'properties: !semi-deterministic' given here");
1390 }
1391 }
1392 }
1393 }
1394 #line 1395 "parseaut.cc"
1395 break;
1396
1397 case 19: // version: "identifier"
1398 #line 678 "parseaut.yy"
1399 {
1400 res.format_version = *(yystack_[0].value.str);
1401 res.format_version_loc = yystack_[0].location;
1402 delete (yystack_[0].value.str);
1403 }
1404 #line 1405 "parseaut.cc"
1405 break;
1406
1407 case 20: // $@2: %empty
1408 #line 684 "parseaut.yy"
1409 { res.h->loc = yystack_[0].location; }
1410 #line 1411 "parseaut.cc"
1411 break;
1412
1413 case 22: // $@3: %empty
1414 #line 687 "parseaut.yy"
1415 {
1416 if (res.ignore_more_ap)
1417 {
1418 error(yystack_[1].location, "ignoring this redeclaration of APs...");
1419 error(res.ap_loc, "... previously declared here.");
1420 }
1421 else
1422 {
1423 res.ap_count = (yystack_[0].value.num);
1424 res.ap.reserve((yystack_[0].value.num));
1425 }
1426 }
1427 #line 1428 "parseaut.cc"
1428 break;
1429
1430 case 23: // aps: "AP:" "integer" $@3 ap-names
1431 #line 700 "parseaut.yy"
1432 {
1433 if (!res.ignore_more_ap)
1434 {
1435 res.ap_loc = yystack_[3].location + yystack_[2].location;
1436 if ((int) res.ap.size() != res.ap_count)
1437 {
1438 std::ostringstream out;
1439 out << "found " << res.ap.size()
1440 << " atomic propositions instead of the "
1441 << res.ap_count << " announced";
1442 error(yylhs.location, out.str());
1443 }
1444 res.ignore_more_ap = true;
1445 // If we have seen Alias: before AP: we have some variable
1446 // renaming to perform.
1447 if (res.unknown_ap_max >= 0)
1448 {
1449 int apsize = res.ap.size();
1450 if (apsize <= res.unknown_ap_max)
1451 {
1452 error(res.unknown_ap_max_location,
1453 "AP number is larger than the number of APs...");
1454 error(yystack_[3].location, "... declared here");
1455 }
1456 bddPair* pair = bdd_newpair();
1457 int max = std::min(res.unknown_ap_max, apsize - 1);
1458 for (int i = 0; i <= max; ++i)
1459 if (i != res.ap[i])
1460 bdd_setbddpair(pair, i, res.ap[i]);
1461 bdd extra = bddtrue;
1462 for (int i = apsize; i <= res.unknown_ap_max; ++i)
1463 extra &= bdd_ithvar(i);
1464 for (auto& p: res.alias)
1465 p.second = bdd_restrict(bdd_replace(p.second, pair), extra);
1466 bdd_freepair(pair);
1467 }
1468 }
1469 }
1470 #line 1471 "parseaut.cc"
1471 break;
1472
1473 case 26: // header-item: "States:" "integer"
1474 #line 742 "parseaut.yy"
1475 {
1476 if (res.states >= 0)
1477 {
1478 error(yylhs.location, "redefinition of the number of states...");
1479 error(res.states_loc, "... previously defined here.");
1480 }
1481 else
1482 {
1483 res.states_loc = yylhs.location;
1484 }
1485 if (((int) (yystack_[0].value.num)) < 0)
1486 {
1487 error(yylhs.location, "too many states for this implementation");
1488 YYABORT;
1489 }
1490 res.states = std::max(res.states, (int) (yystack_[0].value.num));
1491 }
1492 #line 1493 "parseaut.cc"
1493 break;
1494
1495 case 27: // header-item: "Start:" init-state-conj-2
1496 #line 760 "parseaut.yy"
1497 {
1498 res.start.emplace_back(yylhs.location, *(yystack_[0].value.states));
1499 delete (yystack_[0].value.states);
1500 }
1501 #line 1502 "parseaut.cc"
1502 break;
1503
1504 case 28: // header-item: "Start:" state-num
1505 #line 765 "parseaut.yy"
1506 {
1507 res.start.emplace_back(yylhs.location, std::vector<unsigned>{(yystack_[0].value.num)});
1508 }
1509 #line 1510 "parseaut.cc"
1510 break;
1511
1512 case 30: // $@4: %empty
1513 #line 769 "parseaut.yy"
1514 { res.in_alias=true; }
1515 #line 1516 "parseaut.cc"
1516 break;
1517
1518 case 31: // header-item: "Alias:" "alias name" $@4 label-expr
1519 #line 770 "parseaut.yy"
1520 {
1521 res.in_alias = false;
1522 if (!res.alias.emplace(*(yystack_[2].value.str), bdd_from_int((yystack_[0].value.b))).second)
1523 {
1524 std::ostringstream o;
1525 o << "ignoring redefinition of alias @" << *(yystack_[2].value.str);
1526 error(yylhs.location, o.str());
1527 }
1528 delete (yystack_[2].value.str);
1529 bdd_delref((yystack_[0].value.b));
1530 }
1531 #line 1532 "parseaut.cc"
1532 break;
1533
1534 case 32: // $@5: %empty
1535 #line 782 "parseaut.yy"
1536 {
1537 if (res.ignore_more_acc)
1538 {
1539 error(yystack_[1].location + yystack_[0].location, "ignoring this redefinition of the "
1540 "acceptance condition...");
1541 error(res.accset_loc, "... previously defined here.");
1542 }
1543 else if ((yystack_[0].value.num) > SPOT_MAX_ACCSETS)
1544 {
1545 error(yystack_[1].location + yystack_[0].location,
1546 "this implementation cannot support such a large "
1547 "number of acceptance sets");
1548 YYABORT;
1549 }
1550 else
1551 {
1552 res.aut_or_ks->acc().add_sets((yystack_[0].value.num));
1553 res.accset = (yystack_[0].value.num);
1554 res.accset_loc = yystack_[1].location + yystack_[0].location;
1555 }
1556 }
1557 #line 1558 "parseaut.cc"
1558 break;
1559
1560 case 33: // header-item: "Acceptance:" "integer" $@5 acceptance-cond
1561 #line 804 "parseaut.yy"
1562 {
1563 res.ignore_more_acc = true;
1564 // Not setting the acceptance in case of error will
1565 // force it to be true.
1566 if (res.opts.want_kripke && (!(yystack_[0].value.code)->is_t() || (yystack_[2].value.num) > 0))
1567 error(yystack_[2].location + yystack_[0].location,
1568 "the acceptance for Kripke structure must be '0 t'");
1569 else
1570 res.aut_or_ks->set_acceptance((yystack_[2].value.num), *(yystack_[0].value.code));
1571 delete (yystack_[0].value.code);
1572 }
1573 #line 1574 "parseaut.cc"
1574 break;
1575
1576 case 34: // header-item: "acc-name:" "identifier" acc-spec
1577 #line 816 "parseaut.yy"
1578 {
1579 delete (yystack_[1].value.str);
1580 }
1581 #line 1582 "parseaut.cc"
1582 break;
1583
1584 case 35: // header-item: "tool:" "string" string_opt
1585 #line 820 "parseaut.yy"
1586 {
1587 delete (yystack_[1].value.str);
1588 delete (yystack_[0].value.str);
1589 }
1590 #line 1591 "parseaut.cc"
1591 break;
1592
1593 case 36: // header-item: "name:" "string"
1594 #line 825 "parseaut.yy"
1595 {
1596 res.aut_or_ks->set_named_prop("automaton-name", (yystack_[0].value.str));
1597 }
1598 #line 1599 "parseaut.cc"
1599 break;
1600
1601 case 38: // $@6: %empty
1602 #line 830 "parseaut.yy"
1603 { res.highlight_edges = new std::map<unsigned, unsigned>; }
1604 #line 1605 "parseaut.cc"
1605 break;
1606
1607 case 40: // $@7: %empty
1608 #line 833 "parseaut.yy"
1609 { res.highlight_states = new std::map<unsigned, unsigned>; }
1610 #line 1611 "parseaut.cc"
1611 break;
1612
1613 case 42: // $@8: %empty
1614 #line 836 "parseaut.yy"
1615 { auto p = new std::vector<bool>;
1616 if (res.states >= 0)
1617 p->reserve(res.states);
1618 res.state_player = p;
1619 }
1620 #line 1621 "parseaut.cc"
1621 break;
1622
1623 case 43: // header-item: "spot.state-player:" $@8 state-player
1624 #line 841 "parseaut.yy"
1625 {
1626 res.state_player_loc = yylhs.location;
1627 }
1628 #line 1629 "parseaut.cc"
1629 break;
1630
1631 case 44: // header-item: "header name" header-spec
1632 #line 845 "parseaut.yy"
1633 {
1634 char c = (*(yystack_[1].value.str))[0];
1635 if (c >= 'A' && c <= 'Z')
1636 error(yylhs.location, "ignoring unsupported header \"" + *(yystack_[1].value.str) + ":\"\n\t"
1637 "(but the capital indicates information that should not"
1638 " be ignored)");
1639 delete (yystack_[1].value.str);
1640 }
1641 #line 1642 "parseaut.cc"
1642 break;
1643
1644 case 48: // ap-name: "string"
1645 #line 858 "parseaut.yy"
1646 {
1647 if (!res.ignore_more_ap)
1648 {
1649 auto f = res.env->require(*(yystack_[0].value.str));
1650 int b = 0;
1651 if (f == nullptr)
1652 {
1653 std::ostringstream out;
1654 out << "unknown atomic proposition \"" << *(yystack_[0].value.str) << "\"";
1655 error(yystack_[0].location, out.str());
1656 b = res.aut_or_ks->register_ap("$unknown$");
1657 }
1658 else
1659 {
1660 b = res.aut_or_ks->register_ap(f);
1661 if (!res.ap_set.emplace(b).second)
1662 {
1663 std::ostringstream out;
1664 out << "duplicate atomic proposition \"" << *(yystack_[0].value.str) << "\"";
1665 error(yystack_[0].location, out.str());
1666 }
1667 }
1668 res.ap.push_back(b);
1669 }
1670 delete (yystack_[0].value.str);
1671 }
1672 #line 1673 "parseaut.cc"
1673 break;
1674
1675 case 52: // acc-spec: acc-spec "identifier"
1676 #line 889 "parseaut.yy"
1677 {
1678 delete (yystack_[0].value.str);
1679 }
1680 #line 1681 "parseaut.cc"
1681 break;
1682
1683 case 54: // properties: properties "identifier"
1684 #line 894 "parseaut.yy"
1685 {
1686 bool val = true;
1687 // no-univ-branch was replaced by !univ-branch in HOA 1.1
1688 if (*(yystack_[0].value.str) == "no-univ-branch")
1689 {
1690 *(yystack_[0].value.str) = "univ-branch";
1691 val = false;
1692 }
1693 auto pos = res.props.emplace(*(yystack_[0].value.str), result_::prop_info{yystack_[0].location, val});
1694 if (pos.first->second.val != val)
1695 {
1696 std::ostringstream out(std::ios_base::ate);
1697 error(yystack_[0].location, "'properties: "s + (val ? "" : "!")
1698 + *(yystack_[0].value.str) + "' contradicts...");
1699 error(pos.first->second.loc,
1700 "... 'properties: "s + (val ? "!" : "") + *(yystack_[0].value.str)
1701 + "' previously given here.");
1702 }
1703 delete (yystack_[0].value.str);
1704 }
1705 #line 1706 "parseaut.cc"
1706 break;
1707
1708 case 55: // properties: properties '!' "identifier"
1709 #line 915 "parseaut.yy"
1710 {
1711 auto loc = yystack_[1].location + yystack_[0].location;
1712 auto pos =
1713 res.props.emplace(*(yystack_[0].value.str), result_::prop_info{loc, false});
1714 if (pos.first->second.val)
1715 {
1716 std::ostringstream out(std::ios_base::ate);
1717 error(loc, "'properties: !"s + *(yystack_[0].value.str) + "' contradicts...");
1718 error(pos.first->second.loc, "... 'properties: "s + *(yystack_[0].value.str)
1719 + "' previously given here.");
1720 }
1721 delete (yystack_[0].value.str);
1722 }
1723 #line 1724 "parseaut.cc"
1724 break;
1725
1726 case 57: // highlight-edges: highlight-edges "integer" "integer"
1727 #line 931 "parseaut.yy"
1728 {
1729 res.highlight_edges->emplace((yystack_[1].value.num), (yystack_[0].value.num));
1730 }
1731 #line 1732 "parseaut.cc"
1732 break;
1733
1734 case 59: // highlight-states: highlight-states "integer" "integer"
1735 #line 936 "parseaut.yy"
1736 {
1737 res.highlight_states->emplace((yystack_[1].value.num), (yystack_[0].value.num));
1738 }
1739 #line 1740 "parseaut.cc"
1740 break;
1741
1742 case 61: // state-player: state-player "integer"
1743 #line 942 "parseaut.yy"
1744 {
1745 if ((yystack_[0].value.num) != 0 && (yystack_[0].value.num) != 1)
1746 error(yystack_[0].location, "player should be 0 or 1");
1747 res.state_player->emplace_back((yystack_[0].value.num));
1748 }
1749 #line 1750 "parseaut.cc"
1750 break;
1751
1752 case 65: // header-spec: header-spec "string"
1753 #line 952 "parseaut.yy"
1754 {
1755 delete (yystack_[0].value.str);
1756 }
1757 #line 1758 "parseaut.cc"
1758 break;
1759
1760 case 66: // header-spec: header-spec "identifier"
1761 #line 956 "parseaut.yy"
1762 {
1763 delete (yystack_[0].value.str);
1764 }
1765 #line 1766 "parseaut.cc"
1766 break;
1767
1768 case 67: // state-conj-2: checked-state-num '&' checked-state-num
1769 #line 961 "parseaut.yy"
1770 {
1771 (yylhs.value.states) = new std::vector<unsigned>{(yystack_[2].value.num), (yystack_[0].value.num)};
1772 }
1773 #line 1774 "parseaut.cc"
1774 break;
1775
1776 case 68: // state-conj-2: state-conj-2 '&' checked-state-num
1777 #line 965 "parseaut.yy"
1778 {
1779 (yylhs.value.states) = (yystack_[2].value.states);
1780 (yylhs.value.states)->emplace_back((yystack_[0].value.num));
1781 }
1782 #line 1783 "parseaut.cc"
1783 break;
1784
1785 case 69: // init-state-conj-2: state-num '&' state-num
1786 #line 973 "parseaut.yy"
1787 {
1788 (yylhs.value.states) = new std::vector<unsigned>{(yystack_[2].value.num), (yystack_[0].value.num)};
1789 }
1790 #line 1791 "parseaut.cc"
1791 break;
1792
1793 case 70: // init-state-conj-2: init-state-conj-2 '&' state-num
1794 #line 977 "parseaut.yy"
1795 {
1796 (yylhs.value.states) = (yystack_[2].value.states);
1797 (yylhs.value.states)->emplace_back((yystack_[0].value.num));
1798 }
1799 #line 1800 "parseaut.cc"
1800 break;
1801
1802 case 71: // label-expr: 't'
1803 #line 983 "parseaut.yy"
1804 {
1805 (yylhs.value.b) = bddtrue.id();
1806 }
1807 #line 1808 "parseaut.cc"
1808 break;
1809
1810 case 72: // label-expr: 'f'
1811 #line 987 "parseaut.yy"
1812 {
1813 (yylhs.value.b) = bddfalse.id();
1814 }
1815 #line 1816 "parseaut.cc"
1816 break;
1817
1818 case 73: // label-expr: "integer"
1819 #line 991 "parseaut.yy"
1820 {
1821 if (res.in_alias && !res.ignore_more_ap)
1822 {
1823 // We are reading Alias: before AP: has been given.
1824 // Use $1 as temporary variable number. We will relabel
1825 // everything once AP: is known.
1826 if (res.unknown_ap_max < (int)(yystack_[0].value.num))
1827 {
1828 res.unknown_ap_max = (yystack_[0].value.num);
1829 res.unknown_ap_max_location = yystack_[0].location;
1830 int missing_vars = 1 + bdd_varnum() - (yystack_[0].value.num);
1831 if (missing_vars > 0)
1832 bdd_extvarnum(missing_vars);
1833 }
1834 (yylhs.value.b) = bdd_ithvar((yystack_[0].value.num)).id();
1835 }
1836 else if ((yystack_[0].value.num) >= res.ap.size())
1837 {
1838 error(yystack_[0].location, "AP number is larger than the number of APs...");
1839 error(res.ap_loc, "... declared here");
1840 (yylhs.value.b) = bddtrue.id();
1841 }
1842 else
1843 {
1844 (yylhs.value.b) = bdd_ithvar(res.ap[(yystack_[0].value.num)]).id();
1845 bdd_addref((yylhs.value.b));
1846 }
1847 }
1848 #line 1849 "parseaut.cc"
1849 break;
1850
1851 case 74: // label-expr: "alias name"
1852 #line 1020 "parseaut.yy"
1853 {
1854 auto i = res.alias.find(*(yystack_[0].value.str));
1855 if (i == res.alias.end())
1856 {
1857 error(yylhs.location, "unknown alias @" + *(yystack_[0].value.str));
1858 (yylhs.value.b) = 1;
1859 }
1860 else
1861 {
1862 (yylhs.value.b) = i->second.id();
1863 bdd_addref((yylhs.value.b));
1864 }
1865 delete (yystack_[0].value.str);
1866 }
1867 #line 1868 "parseaut.cc"
1868 break;
1869
1870 case 75: // label-expr: '!' label-expr
1871 #line 1035 "parseaut.yy"
1872 {
1873 (yylhs.value.b) = bdd_not((yystack_[0].value.b));
1874 bdd_delref((yystack_[0].value.b));
1875 bdd_addref((yylhs.value.b));
1876 }
1877 #line 1878 "parseaut.cc"
1878 break;
1879
1880 case 76: // label-expr: label-expr '&' label-expr
1881 #line 1041 "parseaut.yy"
1882 {
1883 (yylhs.value.b) = bdd_and((yystack_[2].value.b), (yystack_[0].value.b));
1884 bdd_delref((yystack_[2].value.b));
1885 bdd_delref((yystack_[0].value.b));
1886 bdd_addref((yylhs.value.b));
1887 }
1888 #line 1889 "parseaut.cc"
1889 break;
1890
1891 case 77: // label-expr: label-expr '|' label-expr
1892 #line 1048 "parseaut.yy"
1893 {
1894 (yylhs.value.b) = bdd_or((yystack_[2].value.b), (yystack_[0].value.b));
1895 bdd_delref((yystack_[2].value.b));
1896 bdd_delref((yystack_[0].value.b));
1897 bdd_addref((yylhs.value.b));
1898 }
1899 #line 1900 "parseaut.cc"
1900 break;
1901
1902 case 78: // label-expr: '(' label-expr ')'
1903 #line 1055 "parseaut.yy"
1904 {
1905 (yylhs.value.b) = (yystack_[1].value.b);
1906 }
1907 #line 1908 "parseaut.cc"
1908 break;
1909
1910 case 79: // acc-set: "integer"
1911 #line 1061 "parseaut.yy"
1912 {
1913 if ((int) (yystack_[0].value.num) >= res.accset)
1914 {
1915 if (!res.ignore_acc)
1916 {
1917 error(yystack_[0].location, "number is larger than the count "
1918 "of acceptance sets...");
1919 error(res.accset_loc, "... declared here.");
1920 }
1921 (yylhs.value.num) = -1U;
1922 }
1923 else
1924 {
1925 (yylhs.value.num) = (yystack_[0].value.num);
1926 }
1927 }
1928 #line 1929 "parseaut.cc"
1929 break;
1930
1931 case 80: // acceptance-cond: "identifier" '(' acc-set ')'
1932 #line 1079 "parseaut.yy"
1933 {
1934 if ((yystack_[1].value.num) != -1U)
1935 {
1936 res.pos_acc_sets |= res.aut_or_ks->acc().mark((yystack_[1].value.num));
1937 if (*(yystack_[3].value.str) == "Inf")
1938 {
1939 (yylhs.value.code) = new spot::acc_cond::acc_code
1940 (res.aut_or_ks->acc().inf({(yystack_[1].value.num)}));
1941 }
1942 else if (*(yystack_[3].value.str) == "Fin")
1943 {
1944 (yylhs.value.code) = new spot::acc_cond::acc_code
1945 (res.aut_or_ks->acc().fin({(yystack_[1].value.num)}));
1946 }
1947 else
1948 {
1949 error(yystack_[3].location, "unknown acceptance '"s + *(yystack_[3].value.str)
1950 + "', expected Fin or Inf");
1951 (yylhs.value.code) = new spot::acc_cond::acc_code;
1952 }
1953 }
1954 else
1955 {
1956 (yylhs.value.code) = new spot::acc_cond::acc_code;
1957 }
1958 delete (yystack_[3].value.str);
1959 }
1960 #line 1961 "parseaut.cc"
1961 break;
1962
1963 case 81: // acceptance-cond: "identifier" '(' '!' acc-set ')'
1964 #line 1107 "parseaut.yy"
1965 {
1966 if ((yystack_[1].value.num) != -1U)
1967 {
1968 res.neg_acc_sets |= res.aut_or_ks->acc().mark((yystack_[1].value.num));
1969 if (*(yystack_[4].value.str) == "Inf")
1970 (yylhs.value.code) = new spot::acc_cond::acc_code
1971 (res.aut_or_ks->acc().inf_neg({(yystack_[1].value.num)}));
1972 else
1973 (yylhs.value.code) = new spot::acc_cond::acc_code
1974 (res.aut_or_ks->acc().fin_neg({(yystack_[1].value.num)}));
1975 }
1976 else
1977 {
1978 (yylhs.value.code) = new spot::acc_cond::acc_code;
1979 }
1980 delete (yystack_[4].value.str);
1981 }
1982 #line 1983 "parseaut.cc"
1983 break;
1984
1985 case 82: // acceptance-cond: '(' acceptance-cond ')'
1986 #line 1125 "parseaut.yy"
1987 {
1988 (yylhs.value.code) = (yystack_[1].value.code);
1989 }
1990 #line 1991 "parseaut.cc"
1991 break;
1992
1993 case 83: // acceptance-cond: acceptance-cond '&' acceptance-cond
1994 #line 1129 "parseaut.yy"
1995 {
1996 *(yystack_[0].value.code) &= std::move(*(yystack_[2].value.code));
1997 (yylhs.value.code) = (yystack_[0].value.code);
1998 delete (yystack_[2].value.code);
1999 }
2000 #line 2001 "parseaut.cc"
2001 break;
2002
2003 case 84: // acceptance-cond: acceptance-cond '|' acceptance-cond
2004 #line 1135 "parseaut.yy"
2005 {
2006 *(yystack_[0].value.code) |= std::move(*(yystack_[2].value.code));
2007 (yylhs.value.code) = (yystack_[0].value.code);
2008 delete (yystack_[2].value.code);
2009 }
2010 #line 2011 "parseaut.cc"
2011 break;
2012
2013 case 85: // acceptance-cond: 't'
2014 #line 1141 "parseaut.yy"
2015 {
2016 (yylhs.value.code) = new spot::acc_cond::acc_code;
2017 }
2018 #line 2019 "parseaut.cc"
2019 break;
2020
2021 case 86: // acceptance-cond: 'f'
2022 #line 1145 "parseaut.yy"
2023 {
2024 {
2025 (yylhs.value.code) = new spot::acc_cond::acc_code
2026 (res.aut_or_ks->acc().fin({}));
2027 }
2028 }
2029 #line 2030 "parseaut.cc"
2030 break;
2031
2032 case 87: // body: states
2033 #line 1154 "parseaut.yy"
2034 {
2035 for (auto& p: res.start)
2036 for (unsigned s: p.second)
2037 if (s >= res.info_states.size() || !res.info_states[s].declared)
2038 {
2039 error(p.first, "initial state " + std::to_string(s) +
2040 " has no definition");
2041 // Pretend that the state is declared so we do not
2042 // mention it in the next loop.
2043 if (s < res.info_states.size())
2044 res.info_states[s].declared = true;
2045 res.complete = spot::trival::maybe();
2046 }
2047 unsigned n = res.info_states.size();
2048 // States with number above res.states have already caused a
2049 // diagnostic, so let not add another one.
2050 if (res.states >= 0)
2051 n = res.states;
2052 for (unsigned i = 0; i < n; ++i)
2053 {
2054 auto& p = res.info_states[i];
2055 if (!p.declared)
2056 {
2057 if (p.used)
2058 error(p.used_loc,
2059 "state " + std::to_string(i) + " has no definition");
2060 if (!p.used && res.complete)
2061 if (auto p = res.prop_is_true("complete"))
2062 {
2063 error(res.states_loc,
2064 "state " + std::to_string(i) +
2065 " has no definition...");
2066 error(p.loc, "... despite 'properties: complete'");
2067 }
2068 res.complete = false;
2069 }
2070 }
2071 if (res.complete)
2072 if (auto p = res.prop_is_false("complete"))
2073 {
2074 error(yystack_[0].location, "automaton is complete...");
2075 error(p.loc, "... despite 'properties: !complete'");
2076 }
2077 bool det_warned = false;
2078 if (res.universal && res.existential)
2079 if (auto p = res.prop_is_false("deterministic"))
2080 {
2081 error(yystack_[0].location, "automaton is deterministic...");
2082 error(p.loc, "... despite 'properties: !deterministic'");
2083 det_warned = true;
2084 }
2085 static bool tolerant = getenv("SPOT_HOA_TOLERANT");
2086 if (res.universal.is_true() && !det_warned && !tolerant)
2087 if (auto p = res.prop_is_true("exist-branch"))
2088 {
2089 error(yystack_[0].location, "automaton has no existential branching...");
2090 error(p.loc, "... despite 'properties: exist-branch'\n"
2091 "note: If this is an issue you cannot fix, you may disable "
2092 "this diagnostic\n by defining the SPOT_HOA_TOLERANT "
2093 "environment variable.");
2094 det_warned = true;
2095 }
2096 if (res.existential.is_true() && !det_warned && !tolerant)
2097 if (auto p = res.prop_is_true("univ-branch"))
2098 {
2099 error(yystack_[0].location, "automaton is has no universal branching...");
2100 error(p.loc, "... despite 'properties: univ-branch'\n"
2101 "note: If this is an issue you cannot fix, you may disable "
2102 "this diagnostic\n by defining the SPOT_HOA_TOLERANT "
2103 "environment variable.");
2104 det_warned = true;
2105 }
2106 if (res.state_player)
2107 if (unsigned spsz = res.state_player->size(); spsz != n)
2108 {
2109 error(res.state_player_loc,
2110 "ignoring state-player header because it has "s
2111 + std::to_string(spsz) + " entries while automaton has "
2112 + std::to_string(n) + " states");
2113 delete res.state_player;
2114 res.state_player = nullptr;
2115 }
2116 }
2117 #line 2118 "parseaut.cc"
2118 break;
2119
2120 case 88: // state-num: "integer"
2121 #line 1238 "parseaut.yy"
2122 {
2123 if (((int) (yystack_[0].value.num)) < 0)
2124 {
2125 error(yystack_[0].location, "state number is too large for this implementation");
2126 YYABORT;
2127 }
2128 (yylhs.value.num) = (yystack_[0].value.num);
2129 }
2130 #line 2131 "parseaut.cc"
2131 break;
2132
2133 case 89: // checked-state-num: state-num
2134 #line 1248 "parseaut.yy"
2135 {
2136 if ((int) (yystack_[0].value.num) >= res.states)
2137 {
2138 if (res.states >= 0)
2139 {
2140 error(yystack_[0].location, "state number is larger than state "
2141 "count...");
2142 error(res.states_loc, "... declared here.");
2143 }
2144 if (res.opts.want_kripke)
2145 {
2146 int missing =
2147 ((int) (yystack_[0].value.num)) - res.h->ks->num_states() + 1;
2148 if (missing >= 0)
2149 {
2150 res.h->ks->new_states(missing, bddfalse);
2151 res.info_states.resize
2152 (res.info_states.size() + missing);
2153 }
2154 }
2155 else
2156 {
2157 int missing =
2158 ((int) (yystack_[0].value.num)) - res.h->aut->num_states() + 1;
2159 if (missing >= 0)
2160 {
2161 res.h->aut->new_states(missing);
2162 res.info_states.resize
2163 (res.info_states.size() + missing);
2164 }
2165 }
2166 }
2167 // Remember the first place were a state is the
2168 // destination of a transition.
2169 if (!res.info_states[(yystack_[0].value.num)].used)
2170 {
2171 res.info_states[(yystack_[0].value.num)].used = true;
2172 res.info_states[(yystack_[0].value.num)].used_loc = yystack_[0].location;
2173 }
2174 (yylhs.value.num) = (yystack_[0].value.num);
2175 }
2176 #line 2177 "parseaut.cc"
2177 break;
2178
2179 case 91: // states: states state
2180 #line 1292 "parseaut.yy"
2181 {
2182 if ((res.universal.is_true() || res.complete.is_true()))
2183 {
2184 bdd available = bddtrue;
2185 bool det = true;
2186 for (auto& t: res.h->aut->out(res.cur_state))
2187 {
2188 if (det && !bdd_implies(t.cond, available))
2189 det = false;
2190 available -= t.cond;
2191 }
2192 if (res.universal.is_true() && !det)
2193 {
2194 res.universal = false;
2195 if (auto p = res.prop_is_true("deterministic"))
2196 {
2197 error(yystack_[0].location, "automaton is not deterministic...");
2198 error(p.loc,
2199 "... despite 'properties: deterministic'");
2200 }
2201 else if (auto p = res.prop_is_false("exist-branch"))
2202 {
2203 error(yystack_[0].location, "automaton has existential branching...");
2204 error(p.loc,
2205 "... despite 'properties: !exist-branch'");
2206 }
2207 }
2208 if (res.complete.is_true() && available != bddfalse)
2209 {
2210 res.complete = false;
2211 if (auto p = res.prop_is_true("complete"))
2212 {
2213 error(yystack_[0].location, "automaton is not complete...");
2214 error(p.loc, "... despite 'properties: complete'");
2215 }
2216 }
2217 }
2218 }
2219 #line 2220 "parseaut.cc"
2220 break;
2221
2222 case 93: // state: state-name unlabeled-edges
2223 #line 1332 "parseaut.yy"
2224 {
2225 if (!res.has_state_label) // Implicit labels
2226 {
2227 if (res.cur_guard != res.guards.end())
2228 error(yylhs.location, "not enough transitions for this state");
2229
2230 if (res.label_style == State_Labels)
2231 {
2232 error(yystack_[0].location, "these transitions have implicit labels but the"
2233 " automaton is...");
2234 error(res.props["state-labels"].loc, "... declared with "
2235 "'properties: state-labels'");
2236 // Do not repeat this message.
2237 res.label_style = Mixed_Labels;
2238 }
2239 res.cur_guard = res.guards.begin();
2240 }
2241 else if (res.opts.want_kripke)
2242 {
2243 res.h->ks->state_from_number(res.cur_state)->cond(res.state_label);
2244 }
2245
2246 }
2247 #line 2248 "parseaut.cc"
2248 break;
2249
2250 case 94: // state: error
2251 #line 1356 "parseaut.yy"
2252 {
2253 // Assume the worse. This skips the tests about determinism
2254 // we might perform on the state.
2255 res.universal = spot::trival::maybe();
2256 res.existential = spot::trival::maybe();
2257 res.complete = spot::trival::maybe();
2258 }
2259 #line 2260 "parseaut.cc"
2260 break;
2261
2262 case 95: // state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt
2263 #line 1366 "parseaut.yy"
2264 {
2265 res.cur_state = (yystack_[2].value.num);
2266 if (res.info_states[(yystack_[2].value.num)].declared)
2267 {
2268 std::ostringstream o;
2269 o << "redeclaration of state " << (yystack_[2].value.num);
2270 error(yystack_[4].location + yystack_[2].location, o.str());
2271 // The additional transitions from extra states might
2272 // led us to believe that the automaton is complete
2273 // while it is not if we ignore them.
2274 if (res.complete.is_true())
2275 res.complete = spot::trival::maybe();
2276 }
2277 res.info_states[(yystack_[2].value.num)].declared = true;
2278 res.acc_state = (yystack_[0].value.mark);
2279 if ((yystack_[1].value.str))
2280 {
2281 if (!res.state_names)
2282 res.state_names =
2283 new std::vector<std::string>(res.states > 0 ?
2284 res.states : 0);
2285 if (res.state_names->size() < (yystack_[2].value.num) + 1)
2286 res.state_names->resize((yystack_[2].value.num) + 1);
2287 (*res.state_names)[(yystack_[2].value.num)] = std::move(*(yystack_[1].value.str));
2288 delete (yystack_[1].value.str);
2289 }
2290 if (res.opts.want_kripke && !res.has_state_label)
2291 error(yylhs.location, "Kripke structures should have labeled states");
2292 }
2293 #line 2294 "parseaut.cc"
2294 break;
2295
2296 case 96: // label: '[' label-expr ']'
2297 #line 1396 "parseaut.yy"
2298 {
2299 res.cur_label = bdd_from_int((yystack_[1].value.b));
2300 bdd_delref((yystack_[1].value.b));
2301 if ((yystack_[2].value.str))
2302 res.fcache[*(yystack_[2].value.str)] = res.cur_label;
2303 delete (yystack_[2].value.str);
2304 }
2305 #line 2306 "parseaut.cc"
2306 break;
2307
2308 case 97: // label: BDD
2309 #line 1403 "parseaut.yy"
2310 { res.cur_label = bdd_from_int((yystack_[0].value.b)); }
2311 #line 2312 "parseaut.cc"
2312 break;
2313
2314 case 98: // label: '[' error ']'
2315 #line 1405 "parseaut.yy"
2316 {
2317 error(yylhs.location, "ignoring this invalid label");
2318 res.cur_label = bddtrue;
2319 delete (yystack_[2].value.str);
2320 }
2321 #line 2322 "parseaut.cc"
2322 break;
2323
2324 case 99: // state-label_opt: %empty
2325 #line 1410 "parseaut.yy"
2326 { res.has_state_label = false; }
2327 #line 2328 "parseaut.cc"
2328 break;
2329
2330 case 100: // state-label_opt: label
2331 #line 1412 "parseaut.yy"
2332 {
2333 res.has_state_label = true;
2334 res.state_label_loc = yystack_[0].location;
2335 res.state_label = res.cur_label;
2336 if (res.label_style == Trans_Labels
2337 || res.label_style == Implicit_Labels)
2338 {
2339 error(yylhs.location,
2340 "state label used although the automaton was...");
2341 if (res.label_style == Trans_Labels)
2342 error(res.props["trans-labels"].loc,
2343 "... declared with 'properties: trans-labels'"
2344 " here");
2345 else
2346 error(res.props["implicit-labels"].loc,
2347 "... declared with 'properties: implicit-labels'"
2348 " here");
2349 // Do not show this error anymore.
2350 res.label_style = Mixed_Labels;
2351 }
2352 }
2353 #line 2354 "parseaut.cc"
2354 break;
2355
2356 case 101: // trans-label: label
2357 #line 1434 "parseaut.yy"
2358 {
2359 if (res.has_state_label)
2360 {
2361 error(yystack_[0].location, "cannot label this edge because...");
2362 error(res.state_label_loc,
2363 "... the state is already labeled.");
2364 res.cur_label = res.state_label;
2365 }
2366 if (res.label_style == State_Labels
2367 || res.label_style == Implicit_Labels)
2368 {
2369 error(yylhs.location, "transition label used although the "
2370 "automaton was...");
2371 if (res.label_style == State_Labels)
2372 error(res.props["state-labels"].loc,
2373 "... declared with 'properties: state-labels' "
2374 "here");
2375 else
2376 error(res.props["implicit-labels"].loc,
2377 "... declared with 'properties: implicit-labels'"
2378 " here");
2379 // Do not show this error anymore.
2380 res.label_style = Mixed_Labels;
2381 }
2382 }
2383 #line 2384 "parseaut.cc"
2384 break;
2385
2386 case 102: // acc-sig: '{' acc-sets '}'
2387 #line 1461 "parseaut.yy"
2388 {
2389 (yylhs.value.mark) = (yystack_[1].value.mark);
2390 if (res.ignore_acc && !res.ignore_acc_silent)
2391 {
2392 error(yylhs.location, "ignoring acceptance sets because of "
2393 "missing acceptance condition");
2394 // Emit this message only once.
2395 res.ignore_acc_silent = true;
2396 }
2397 }
2398 #line 2399 "parseaut.cc"
2399 break;
2400
2401 case 103: // acc-sig: '{' error '}'
2402 #line 1472 "parseaut.yy"
2403 {
2404 error(yylhs.location, "ignoring this invalid acceptance set");
2405 }
2406 #line 2407 "parseaut.cc"
2407 break;
2408
2409 case 104: // acc-sets: %empty
2410 #line 1476 "parseaut.yy"
2411 {
2412 (yylhs.value.mark) = spot::acc_cond::mark_t({});
2413 }
2414 #line 2415 "parseaut.cc"
2415 break;
2416
2417 case 105: // acc-sets: acc-sets acc-set
2418 #line 1480 "parseaut.yy"
2419 {
2420 if (res.ignore_acc || (yystack_[0].value.num) == -1U)
2421 (yylhs.value.mark) = spot::acc_cond::mark_t({});
2422 else
2423 (yylhs.value.mark) = (yystack_[1].value.mark) | res.aut_or_ks->acc().mark((yystack_[0].value.num));
2424 }
2425 #line 2426 "parseaut.cc"
2426 break;
2427
2428 case 106: // state-acc_opt: %empty
2429 #line 1488 "parseaut.yy"
2430 {
2431 (yylhs.value.mark) = spot::acc_cond::mark_t({});
2432 }
2433 #line 2434 "parseaut.cc"
2434 break;
2435
2436 case 107: // state-acc_opt: acc-sig
2437 #line 1492 "parseaut.yy"
2438 {
2439 (yylhs.value.mark) = (yystack_[0].value.mark);
2440 if (res.acc_style == Trans_Acc)
2441 {
2442 error(yylhs.location, "state-based acceptance used despite...");
2443 error(res.props["trans-acc"].loc,
2444 "... declaration of transition-based acceptance.");
2445 res.acc_style = Mixed_Acc;
2446 }
2447 }
2448 #line 2449 "parseaut.cc"
2449 break;
2450
2451 case 108: // trans-acc_opt: %empty
2452 #line 1503 "parseaut.yy"
2453 {
2454 (yylhs.value.mark) = spot::acc_cond::mark_t({});
2455 }
2456 #line 2457 "parseaut.cc"
2457 break;
2458
2459 case 109: // trans-acc_opt: acc-sig
2460 #line 1507 "parseaut.yy"
2461 {
2462 (yylhs.value.mark) = (yystack_[0].value.mark);
2463 res.trans_acc_seen = true;
2464 if (res.acc_style == State_Acc)
2465 {
2466 error(yylhs.location, "trans-based acceptance used despite...");
2467 error(res.props["state-acc"].loc,
2468 "... declaration of state-based acceptance.");
2469 res.acc_style = Mixed_Acc;
2470 }
2471 }
2472 #line 2473 "parseaut.cc"
2473 break;
2474
2475 case 115: // incorrectly-unlabeled-edge: checked-state-num trans-acc_opt
2476 #line 1526 "parseaut.yy"
2477 {
2478 bdd cond = bddtrue;
2479 if (!res.has_state_label)
2480 error(yylhs.location, "missing label for this edge "
2481 "(previous edge is labeled)");
2482 else
2483 cond = res.state_label;
2484 if (cond != bddfalse)
2485 {
2486 if (res.opts.want_kripke)
2487 res.h->ks->new_edge(res.cur_state, (yystack_[1].value.num));
2488 else
2489 res.h->aut->new_edge(res.cur_state, (yystack_[1].value.num),
2490 cond,
2491 (yystack_[0].value.mark) | res.acc_state);
2492 }
2493 }
2494 #line 2495 "parseaut.cc"
2495 break;
2496
2497 case 116: // labeled-edge: trans-label checked-state-num trans-acc_opt
2498 #line 1544 "parseaut.yy"
2499 {
2500 if (res.cur_label != bddfalse)
2501 {
2502 if (res.opts.want_kripke)
2503 res.h->ks->new_edge(res.cur_state, (yystack_[1].value.num));
2504 else
2505 res.h->aut->new_edge(res.cur_state, (yystack_[1].value.num),
2506 res.cur_label, (yystack_[0].value.mark) | res.acc_state);
2507 }
2508 }
2509 #line 2510 "parseaut.cc"
2510 break;
2511
2512 case 117: // labeled-edge: trans-label state-conj-checked trans-acc_opt
2513 #line 1555 "parseaut.yy"
2514 {
2515 if (res.cur_label != bddfalse)
2516 {
2517 assert(!res.opts.want_kripke);
2518 res.h->aut->new_univ_edge(res.cur_state,
2519 (yystack_[1].value.states)->begin(), (yystack_[1].value.states)->end(),
2520 res.cur_label,
2521 (yystack_[0].value.mark) | res.acc_state);
2522 }
2523 delete (yystack_[1].value.states);
2524 }
2525 #line 2526 "parseaut.cc"
2526 break;
2527
2528 case 118: // state-conj-checked: state-conj-2
2529 #line 1568 "parseaut.yy"
2530 {
2531 (yylhs.value.states) = (yystack_[0].value.states);
2532 if (auto ub = res.prop_is_false("univ-branch"))
2533 {
2534 error(yystack_[0].location, "universal branch used despite"
2535 " previous declaration...");
2536 error(ub.loc, "... here");
2537 }
2538 res.existential = false;
2539 }
2540 #line 2541 "parseaut.cc"
2541 break;
2542
2543 case 122: // unlabeled-edge: checked-state-num trans-acc_opt
2544 #line 1586 "parseaut.yy"
2545 {
2546 bdd cond;
2547 if (res.has_state_label)
2548 {
2549 cond = res.state_label;
2550 }
2551 else
2552 {
2553 if (res.guards.empty())
2554 fill_guards(res);
2555 if (res.cur_guard == res.guards.end())
2556 {
2557 error(yylhs.location, "too many transitions for this state, "
2558 "ignoring this one");
2559 cond = bddfalse;
2560 }
2561 else
2562 {
2563 cond = *res.cur_guard++;
2564 }
2565 }
2566 if (cond != bddfalse)
2567 {
2568 if (res.opts.want_kripke)
2569 res.h->ks->new_edge(res.cur_state, (yystack_[1].value.num));
2570 else
2571 res.h->aut->new_edge(res.cur_state, (yystack_[1].value.num),
2572 cond, (yystack_[0].value.mark) | res.acc_state);
2573 }
2574 }
2575 #line 2576 "parseaut.cc"
2576 break;
2577
2578 case 123: // unlabeled-edge: state-conj-checked trans-acc_opt
2579 #line 1617 "parseaut.yy"
2580 {
2581 bdd cond;
2582 if (res.has_state_label)
2583 {
2584 cond = res.state_label;
2585 }
2586 else
2587 {
2588 if (res.guards.empty())
2589 fill_guards(res);
2590 if (res.cur_guard == res.guards.end())
2591 {
2592 error(yylhs.location, "too many transitions for this state, "
2593 "ignoring this one");
2594 cond = bddfalse;
2595 }
2596 else
2597 {
2598 cond = *res.cur_guard++;
2599 }
2600 }
2601 if (cond != bddfalse)
2602 {
2603 assert(!res.opts.want_kripke);
2604 res.h->aut->new_univ_edge(res.cur_state,
2605 (yystack_[1].value.states)->begin(), (yystack_[1].value.states)->end(),
2606 cond, (yystack_[0].value.mark) | res.acc_state);
2607 }
2608 delete (yystack_[1].value.states);
2609 }
2610 #line 2611 "parseaut.cc"
2611 break;
2612
2613 case 124: // incorrectly-labeled-edge: trans-label unlabeled-edge
2614 #line 1648 "parseaut.yy"
2615 {
2616 error(yystack_[1].location, "ignoring this label, because previous"
2617 " edge has no label");
2618 }
2619 #line 2620 "parseaut.cc"
2620 break;
2621
2622 case 126: // dstar: dstar_type error "end of DSTAR automaton"
2623 #line 1660 "parseaut.yy"
2624 {
2625 error(yylhs.location, "failed to parse this as an ltl2dstar automaton");
2626 }
2627 #line 2628 "parseaut.cc"
2628 break;
2629
2630 case 127: // dstar_type: "DRA"
2631 #line 1665 "parseaut.yy"
2632 {
2633 res.h->type = spot::parsed_aut_type::DRA;
2634 res.plus = 1;
2635 res.minus = 0;
2636 if (res.opts.want_kripke)
2637 {
2638 error(yylhs.location,
2639 "cannot read a Kripke structure out of a DSTAR automaton");
2640 YYABORT;
2641 }
2642 }
2643 #line 2644 "parseaut.cc"
2644 break;
2645
2646 case 128: // dstar_type: "DSA"
2647 #line 1677 "parseaut.yy"
2648 {
2649 res.h->type = spot::parsed_aut_type::DSA;
2650 res.plus = 0;
2651 res.minus = 1;
2652 if (res.opts.want_kripke)
2653 {
2654 error(yylhs.location,
2655 "cannot read a Kripke structure out of a DSTAR automaton");
2656 YYABORT;
2657 }
2658 }
2659 #line 2660 "parseaut.cc"
2660 break;
2661
2662 case 129: // dstar_header: dstar_sizes
2663 #line 1690 "parseaut.yy"
2664 {
2665 if (res.states < 0)
2666 error(yystack_[0].location, "missing state count");
2667 if (!res.ignore_more_acc)
2668 error(yystack_[0].location, "missing acceptance-pair count");
2669 if (res.start.empty())
2670 error(yystack_[0].location, "missing start-state number");
2671 if (!res.ignore_more_ap)
2672 error(yystack_[0].location, "missing atomic propositions definition");
2673
2674 if (res.states > 0)
2675 {
2676 res.h->aut->new_states(res.states);;
2677 res.info_states.resize(res.states);
2678 }
2679 res.acc_style = State_Acc;
2680 res.universal = true;
2681 res.existential = true;
2682 res.complete = true;
2683 fill_guards(res);
2684 res.cur_guard = res.guards.end();
2685 }
2686 #line 2687 "parseaut.cc"
2687 break;
2688
2689 case 132: // dstar_sizes: dstar_sizes "Acceptance-Pairs:" "integer"
2690 #line 1716 "parseaut.yy"
2691 {
2692 if (res.ignore_more_acc)
2693 {
2694 error(yystack_[2].location + yystack_[1].location, "ignoring this redefinition of the "
2695 "acceptance pairs...");
2696 error(res.accset_loc, "... previously defined here.");
2697 }
2698 else{
2699 res.accset = (yystack_[0].value.num);
2700 res.h->aut->set_acceptance(2 * (yystack_[0].value.num),
2701 res.h->type == spot::parsed_aut_type::DRA
2702 ? spot::acc_cond::acc_code::rabin((yystack_[0].value.num))
2703 : spot::acc_cond::acc_code::streett((yystack_[0].value.num)));
2704 res.accset_loc = yystack_[0].location;
2705 res.ignore_more_acc = true;
2706 }
2707 }
2708 #line 2709 "parseaut.cc"
2709 break;
2710
2711 case 133: // dstar_sizes: dstar_sizes "States:" "integer"
2712 #line 1734 "parseaut.yy"
2713 {
2714 if (res.states < 0)
2715 {
2716 res.states = (yystack_[0].value.num);
2717 }
2718 else
2719 {
2720 error(yylhs.location, "redeclaration of state count");
2721 if ((unsigned) res.states < (yystack_[0].value.num))
2722 res.states = (yystack_[0].value.num);
2723 }
2724 }
2725 #line 2726 "parseaut.cc"
2726 break;
2727
2728 case 134: // dstar_sizes: dstar_sizes "Start:" "integer"
2729 #line 1747 "parseaut.yy"
2730 {
2731 res.start.emplace_back(yystack_[0].location, std::vector<unsigned>{(yystack_[0].value.num)});
2732 }
2733 #line 2734 "parseaut.cc"
2734 break;
2735
2736 case 136: // dstar_state_id: "State:" "integer" string_opt
2737 #line 1753 "parseaut.yy"
2738 {
2739 if (res.cur_guard != res.guards.end())
2740 error(yystack_[2].location, "not enough transitions for previous state");
2741 if (res.states < 0 || (yystack_[1].value.num) >= (unsigned) res.states)
2742 {
2743 std::ostringstream o;
2744 if (res.states > 0)
2745 {
2746 o << "state numbers should be in the range [0.."
2747 << res.states - 1 << "]";
2748 }
2749 else
2750 {
2751 o << "no states have been declared";
2752 }
2753 error(yystack_[1].location, o.str());
2754 }
2755 else
2756 {
2757 res.info_states[(yystack_[1].value.num)].declared = true;
2758
2759 if ((yystack_[0].value.str))
2760 {
2761 if (!res.state_names)
2762 res.state_names =
2763 new std::vector<std::string>(res.states > 0 ?
2764 res.states : 0);
2765 if (res.state_names->size() < (yystack_[1].value.num) + 1)
2766 res.state_names->resize((yystack_[1].value.num) + 1);
2767 (*res.state_names)[(yystack_[1].value.num)] = std::move(*(yystack_[0].value.str));
2768 delete (yystack_[0].value.str);
2769 }
2770 }
2771
2772 res.cur_guard = res.guards.begin();
2773 res.dest_map.clear();
2774 res.cur_state = (yystack_[1].value.num);
2775 }
2776 #line 2777 "parseaut.cc"
2777 break;
2778
2779 case 137: // sign: '+'
2780 #line 1792 "parseaut.yy"
2781 { (yylhs.value.num) = res.plus; }
2782 #line 2783 "parseaut.cc"
2783 break;
2784
2785 case 138: // sign: '-'
2786 #line 1793 "parseaut.yy"
2787 { (yylhs.value.num) = res.minus; }
2788 #line 2789 "parseaut.cc"
2789 break;
2790
2791 case 139: // dstar_accsigs: %empty
2792 #line 1797 "parseaut.yy"
2793 {
2794 (yylhs.value.mark) = spot::acc_cond::mark_t({});
2795 }
2796 #line 2797 "parseaut.cc"
2797 break;
2798
2799 case 140: // dstar_accsigs: dstar_accsigs sign "integer"
2800 #line 1801 "parseaut.yy"
2801 {
2802 if (res.states < 0 || res.cur_state >= (unsigned) res.states)
2803 break;
2804 if (res.accset > 0 && (yystack_[0].value.num) < (unsigned) res.accset)
2805 {
2806 (yylhs.value.mark) = (yystack_[2].value.mark);
2807 (yylhs.value.mark).set((yystack_[0].value.num) * 2 + (yystack_[1].value.num));
2808 }
2809 else
2810 {
2811 std::ostringstream o;
2812 if (res.accset > 0)
2813 {
2814 o << "acceptance pairs should be in the range [0.."
2815 << res.accset - 1 << "]";
2816 }
2817 else
2818 {
2819 o << "no acceptance pairs have been declared";
2820 }
2821 error(yystack_[0].location, o.str());
2822 }
2823 }
2824 #line 2825 "parseaut.cc"
2825 break;
2826
2827 case 141: // dstar_state_accsig: "Acc-Sig:" dstar_accsigs
2828 #line 1825 "parseaut.yy"
2829 { (yylhs.value.mark) = (yystack_[0].value.mark); }
2830 #line 2831 "parseaut.cc"
2831 break;
2832
2833 case 143: // dstar_transitions: dstar_transitions "integer"
2834 #line 1829 "parseaut.yy"
2835 {
2836 std::pair<map_t::iterator, bool> i =
2837 res.dest_map.emplace((yystack_[0].value.num), *res.cur_guard);
2838 if (!i.second)
2839 i.first->second |= *res.cur_guard;
2840 ++res.cur_guard;
2841 }
2842 #line 2843 "parseaut.cc"
2843 break;
2844
2845 case 146: // dstar_states: dstar_states dstar_state_id dstar_state_accsig dstar_transitions
2846 #line 1840 "parseaut.yy"
2847 {
2848 for (auto i: res.dest_map)
2849 res.h->aut->new_edge(res.cur_state, i.first, i.second, (yystack_[1].value.mark));
2850 }
2851 #line 2852 "parseaut.cc"
2852 break;
2853
2854 case 147: // $@9: %empty
2855 #line 1850 "parseaut.yy"
2856 {
2857 if (res.opts.want_kripke)
2858 {
2859 error(yylhs.location, "cannot read a Kripke structure out of a never claim.");
2860 YYABORT;
2861 }
2862 res.namer = res.h->aut->create_namer<std::string>();
2863 res.h->aut->set_buchi();
2864 res.acc_style = State_Acc;
2865 res.pos_acc_sets = res.h->aut->acc().all_sets();
2866 }
2867 #line 2868 "parseaut.cc"
2868 break;
2869
2870 case 148: // never: "never" $@9 '{' nc-states '}'
2871 #line 1862 "parseaut.yy"
2872 {
2873 // Add an accept_all state if needed.
2874 if (res.accept_all_needed && !res.accept_all_seen)
2875 {
2876 unsigned n = res.namer->new_state("accept_all");
2877 res.h->aut->new_acc_edge(n, n, bddtrue);
2878 }
2879 // If we aliased existing state, we have some unreachable
2880 // states to remove.
2881 if (res.aliased_states)
2882 res.h->aut->purge_unreachable_states();
2883 res.info_states.resize(res.h->aut->num_states());
2884 // Pretend that we have declared all states.
2885 for (auto& p: res.info_states)
2886 p.declared = true;
2887 res.h->aut->register_aps_from_dict();
2888 }
2889 #line 2890 "parseaut.cc"
2890 break;
2891
2892 case 153: // nc-one-ident: "identifier" ':'
2893 #line 1886 "parseaut.yy"
2894 {
2895 auto r = res.labels.insert(std::make_pair(*(yystack_[1].value.str), yystack_[1].location));
2896 if (!r.second)
2897 {
2898 error(yystack_[1].location, "redefinition of "s + *(yystack_[1].value.str) + "...");
2899 error(r.first->second, "... "s + *(yystack_[1].value.str) + " previously defined here");
2900 }
2901 (yylhs.value.str) = (yystack_[1].value.str);
2902 }
2903 #line 2904 "parseaut.cc"
2904 break;
2905
2906 case 154: // nc-ident-list: nc-one-ident
2907 #line 1897 "parseaut.yy"
2908 {
2909 unsigned n = res.namer->new_state(*(yystack_[0].value.str));
2910 if (res.start.empty())
2911 {
2912 // The first state is initial.
2913 res.start.emplace_back(yylhs.location, std::vector<unsigned>{n});
2914 }
2915 (yylhs.value.str) = (yystack_[0].value.str);
2916 }
2917 #line 2918 "parseaut.cc"
2918 break;
2919
2920 case 155: // nc-ident-list: nc-ident-list nc-one-ident
2921 #line 1907 "parseaut.yy"
2922 {
2923 res.aliased_states |=
2924 res.namer->alias_state(res.namer->get_state(*(yystack_[1].value.str)), *(yystack_[0].value.str));
2925 // Keep any identifier that starts with accept.
2926 if (strncmp("accept", (yystack_[1].value.str)->c_str(), 6))
2927 {
2928 delete (yystack_[1].value.str);
2929 (yylhs.value.str) = (yystack_[0].value.str);
2930 }
2931 else
2932 {
2933 delete (yystack_[0].value.str);
2934 (yylhs.value.str) = (yystack_[1].value.str);
2935 }
2936 }
2937 #line 2938 "parseaut.cc"
2938 break;
2939
2940 case 156: // nc-transition-block: "if" nc-transitions "fi"
2941 #line 1925 "parseaut.yy"
2942 {
2943 (yylhs.value.list) = (yystack_[1].value.list);
2944 }
2945 #line 2946 "parseaut.cc"
2946 break;
2947
2948 case 157: // nc-transition-block: "do" nc-transitions "od"
2949 #line 1929 "parseaut.yy"
2950 {
2951 (yylhs.value.list) = (yystack_[1].value.list);
2952 }
2953 #line 2954 "parseaut.cc"
2954 break;
2955
2956 case 158: // nc-state: nc-ident-list "skip"
2957 #line 1935 "parseaut.yy"
2958 {
2959 if (*(yystack_[1].value.str) == "accept_all")
2960 res.accept_all_seen = true;
2961
2962 auto acc = !strncmp("accept", (yystack_[1].value.str)->c_str(), 6) ?
2963 res.h->aut->acc().all_sets() : spot::acc_cond::mark_t({});
2964 res.namer->new_edge(*(yystack_[1].value.str), *(yystack_[1].value.str), bddtrue, acc);
2965 delete (yystack_[1].value.str);
2966 }
2967 #line 2968 "parseaut.cc"
2968 break;
2969
2970 case 159: // nc-state: nc-ident-list
2971 #line 1944 "parseaut.yy"
2972 { delete (yystack_[0].value.str); }
2973 #line 2974 "parseaut.cc"
2974 break;
2975
2976 case 160: // nc-state: nc-ident-list "false"
2977 #line 1945 "parseaut.yy"
2978 { delete (yystack_[1].value.str); }
2979 #line 2980 "parseaut.cc"
2980 break;
2981
2982 case 161: // nc-state: nc-ident-list nc-transition-block
2983 #line 1947 "parseaut.yy"
2984 {
2985 auto acc = !strncmp("accept", (yystack_[1].value.str)->c_str(), 6) ?
2986 res.h->aut->acc().all_sets() : spot::acc_cond::mark_t({});
2987 for (auto& p: *(yystack_[0].value.list))
2988 {
2989 bdd c = bdd_from_int(p.first);
2990 bdd_delref(p.first);
2991 res.namer->new_edge(*(yystack_[1].value.str), *p.second, c, acc);
2992 delete p.second;
2993 }
2994 delete (yystack_[1].value.str);
2995 delete (yystack_[0].value.list);
2996 }
2997 #line 2998 "parseaut.cc"
2998 break;
2999
3000 case 162: // nc-transitions: %empty
3001 #line 1962 "parseaut.yy"
3002 { (yylhs.value.list) = new std::list<pair>; }
3003 #line 3004 "parseaut.cc"
3004 break;
3005
3006 case 163: // nc-transitions: nc-transitions nc-transition
3007 #line 1964 "parseaut.yy"
3008 {
3009 if ((yystack_[0].value.p))
3010 {
3011 (yystack_[1].value.list)->push_back(*(yystack_[0].value.p));
3012 delete (yystack_[0].value.p);
3013 }
3014 (yylhs.value.list) = (yystack_[1].value.list);
3015 }
3016 #line 3017 "parseaut.cc"
3017 break;
3018
3019 case 164: // nc-formula-or-ident: "boolean formula"
3020 #line 1973 "parseaut.yy"
3021 { (yylhs.value.str) = (yystack_[0].value.str); }
3022 #line 3023 "parseaut.cc"
3023 break;
3024
3025 case 165: // nc-formula-or-ident: "identifier"
3026 #line 1973 "parseaut.yy"
3027 { (yylhs.value.str) = (yystack_[0].value.str); }
3028 #line 3029 "parseaut.cc"
3029 break;
3030
3031 case 166: // nc-formula: nc-formula-or-ident
3032 #line 1976 "parseaut.yy"
3033 {
3034 auto i = res.fcache.find(*(yystack_[0].value.str));
3035 if (i == res.fcache.end())
3036 {
3037 auto pf = spot::parse_infix_boolean(*(yystack_[0].value.str), *res.env, debug_level(),
3038 true);
3039 for (auto& j: pf.errors)
3040 {
3041 // Adjust the diagnostic to the current position.
3042 spot::location here = yystack_[0].location;
3043 here.end.line = here.begin.line + j.first.end.line - 1;
3044 here.end.column = here.begin.column + j.first.end.column - 1;
3045 here.begin.line += j.first.begin.line - 1;
3046 here.begin.column += j.first.begin.column - 1;
3047 res.h->errors.emplace_back(here, j.second);
3048 }
3049 bdd cond = bddfalse;
3050 if (pf.f)
3051 cond = spot::formula_to_bdd(pf.f,
3052 res.h->aut->get_dict(), res.h->aut);
3053 (yylhs.value.b) = (res.fcache[*(yystack_[0].value.str)] = cond).id();
3054 }
3055 else
3056 {
3057 (yylhs.value.b) = i->second.id();
3058 }
3059 bdd_addref((yylhs.value.b));
3060 delete (yystack_[0].value.str);
3061 }
3062 #line 3063 "parseaut.cc"
3063 break;
3064
3065 case 167: // nc-formula: "false"
3066 #line 2006 "parseaut.yy"
3067 {
3068 (yylhs.value.b) = 0;
3069 }
3070 #line 3071 "parseaut.cc"
3071 break;
3072
3073 case 168: // nc-opt-dest: %empty
3074 #line 2012 "parseaut.yy"
3075 {
3076 (yylhs.value.str) = nullptr;
3077 }
3078 #line 3079 "parseaut.cc"
3079 break;
3080
3081 case 169: // nc-opt-dest: "->" "goto" "identifier"
3082 #line 2016 "parseaut.yy"
3083 {
3084 (yylhs.value.str) = (yystack_[0].value.str);
3085 }
3086 #line 3087 "parseaut.cc"
3087 break;
3088
3089 case 170: // nc-opt-dest: "->" "assert" "boolean formula"
3090 #line 2020 "parseaut.yy"
3091 {
3092 delete (yystack_[0].value.str);
3093 (yylhs.value.str) = new std::string("accept_all");
3094 res.accept_all_needed = true;
3095 }
3096 #line 3097 "parseaut.cc"
3097 break;
3098
3099 case 171: // nc-src-dest: nc-formula nc-opt-dest
3100 #line 2027 "parseaut.yy"
3101 {
3102 // If there is no destination, do ignore the transition.
3103 // This happens for instance with
3104 // if
3105 // :: false
3106 // fi
3107 if (!(yystack_[0].value.str))
3108 {
3109 (yylhs.value.p) = nullptr;
3110 }
3111 else
3112 {
3113 (yylhs.value.p) = new pair((yystack_[1].value.b), (yystack_[0].value.str));
3114 res.namer->new_state(*(yystack_[0].value.str));
3115 }
3116 }
3117 #line 3118 "parseaut.cc"
3118 break;
3119
3120 case 172: // nc-transition: ':' ':' "atomic" '{' nc-src-dest '}'
3121 #line 2046 "parseaut.yy"
3122 {
3123 (yylhs.value.p) = (yystack_[1].value.p);
3124 }
3125 #line 3126 "parseaut.cc"
3126 break;
3127
3128 case 173: // nc-transition: ':' ':' nc-src-dest
3129 #line 2050 "parseaut.yy"
3130 {
3131 (yylhs.value.p) = (yystack_[0].value.p);
3132 }
3133 #line 3134 "parseaut.cc"
3134 break;
3135
3136 case 174: // lbtt: lbtt-header lbtt-body "-1"
3137 #line 2059 "parseaut.yy"
3138 {
3139 auto& acc = res.h->aut->acc();
3140 unsigned num = acc.num_sets();
3141 res.h->aut->set_generalized_buchi(num);
3142 res.pos_acc_sets = acc.all_sets();
3143 assert(!res.states_map.empty());
3144 auto n = res.states_map.size();
3145 if (n != (unsigned) res.states)
3146 {
3147 std::ostringstream err;
3148 err << res.states << " states have been declared, but "
3149 << n << " different state numbers have been used";
3150 error(yylhs.location, err.str());
3151 }
3152 if (res.states_map.rbegin()->first > (unsigned) res.states)
3153 {
3154 // We have seen numbers larger that the total number of
3155 // states in the automaton. Usually this happens when the
3156 // states are numbered from 1 instead of 0, but the LBTT
3157 // documentation actually allow any number to be used.
3158 // What we have done is to map all input state numbers 0
3159 // <= .. < n to the digraph states with the same number,
3160 // and any time we saw a number larger than n, we mapped
3161 // it to a new state. The correspondence is given by
3162 // res.states_map. Now we just need to remove the useless
3163 // states we allocated.
3164 std::vector<unsigned> rename(res.h->aut->num_states(), -1U);
3165 unsigned s = 0;
3166 for (auto& i: res.states_map)
3167 rename[i.second] = s++;
3168 assert(s == (unsigned) res.states);
3169 for (auto& i: res.start)
3170 i.second.front() = rename[i.second.front()];
3171 res.h->aut->get_graph().defrag_states(rename, s);
3172 }
3173 res.info_states.resize(res.h->aut->num_states());
3174 for (auto& s: res.info_states)
3175 s.declared = true;
3176 res.h->aut->register_aps_from_dict();
3177 }
3178 #line 3179 "parseaut.cc"
3179 break;
3180
3181 case 175: // lbtt: lbtt-header-states "acceptance sets for empty automaton"
3182 #line 2100 "parseaut.yy"
3183 {
3184 res.h->aut->set_generalized_buchi((yystack_[0].value.num));
3185 res.pos_acc_sets = res.h->aut->acc().all_sets();
3186 }
3187 #line 3188 "parseaut.cc"
3188 break;
3189
3190 case 176: // lbtt-header-states: "LBTT header"
3191 #line 2106 "parseaut.yy"
3192 {
3193 if (res.opts.want_kripke)
3194 {
3195 error(yylhs.location,
3196 "cannot read a Kripke structure out of "
3197 "an LBTT automaton");
3198 YYABORT;
3199 }
3200 res.states = (yystack_[0].value.num);
3201 res.states_loc = yystack_[0].location;
3202 res.h->aut->new_states((yystack_[0].value.num));
3203 }
3204 #line 3205 "parseaut.cc"
3205 break;
3206
3207 case 177: // lbtt-header: lbtt-header-states "state acceptance"
3208 #line 2119 "parseaut.yy"
3209 {
3210 res.acc_mapper = new spot::acc_mapper_int(res.h->aut, (yystack_[0].value.num));
3211 res.acc_style = State_Acc;
3212 }
3213 #line 3214 "parseaut.cc"
3214 break;
3215
3216 case 178: // lbtt-header: lbtt-header-states "integer"
3217 #line 2124 "parseaut.yy"
3218 {
3219 res.acc_mapper = new spot::acc_mapper_int(res.h->aut, (yystack_[0].value.num));
3220 res.trans_acc_seen = true;
3221 }
3222 #line 3223 "parseaut.cc"
3223 break;
3224
3225 case 182: // lbtt-state: "state number" "integer" lbtt-acc
3226 #line 2133 "parseaut.yy"
3227 {
3228 if ((yystack_[2].value.num) >= (unsigned) res.states)
3229 {
3230 auto p = res.states_map.emplace((yystack_[2].value.num), 0);
3231 if (p.second)
3232 p.first->second = res.h->aut->new_state();
3233 res.cur_state = p.first->second;
3234 }
3235 else
3236 {
3237 res.states_map.emplace((yystack_[2].value.num), (yystack_[2].value.num));
3238 res.cur_state = (yystack_[2].value.num);
3239 }
3240 if ((yystack_[1].value.num))
3241 res.start.emplace_back(yystack_[2].location + yystack_[1].location,
3242 std::vector<unsigned>{res.cur_state});
3243 res.acc_state = (yystack_[0].value.mark);
3244 }
3245 #line 3246 "parseaut.cc"
3246 break;
3247
3248 case 183: // lbtt-acc: %empty
3249 #line 2151 "parseaut.yy"
3250 { (yylhs.value.mark) = spot::acc_cond::mark_t({}); }
3251 #line 3252 "parseaut.cc"
3252 break;
3253
3254 case 184: // lbtt-acc: lbtt-acc "acceptance set"
3255 #line 2153 "parseaut.yy"
3256 {
3257 (yylhs.value.mark) = (yystack_[1].value.mark);
3258 auto p = res.acc_mapper->lookup((yystack_[0].value.num));
3259 if (p.first)
3260 (yylhs.value.mark) |= p.second;
3261 else
3262 error(yystack_[0].location, "more acceptance sets used than declared");
3263 }
3264 #line 3265 "parseaut.cc"
3265 break;
3266
3267 case 185: // lbtt-guard: "string"
3268 #line 2162 "parseaut.yy"
3269 {
3270 auto pf = spot::parse_prefix_ltl(*(yystack_[0].value.str), *res.env);
3271 if (!pf.f || !pf.errors.empty())
3272 {
3273 std::string s = "failed to parse guard: ";
3274 s += *(yystack_[0].value.str);
3275 error(yylhs.location, s);
3276 }
3277 if (!pf.errors.empty())
3278 for (auto& j: pf.errors)
3279 {
3280 // Adjust the diagnostic to the current position.
3281 spot::location here = yystack_[0].location;
3282 here.end.line = here.begin.line + j.first.end.line - 1;
3283 here.end.column = here.begin.column + j.first.end.column - 1;
3284 here.begin.line += j.first.begin.line - 1;
3285 here.begin.column += j.first.begin.column - 1;
3286 res.h->errors.emplace_back(here, j.second);
3287 }
3288 if (!pf.f)
3289 {
3290 res.cur_label = bddtrue;
3291 }
3292 else
3293 {
3294 if (!pf.f.is_boolean())
3295 {
3296 error(yylhs.location,
3297 "non-Boolean transition label (replaced by true)");
3298 res.cur_label = bddtrue;
3299 }
3300 else
3301 {
3302 res.cur_label =
3303 formula_to_bdd(pf.f, res.h->aut->get_dict(), res.h->aut);
3304 }
3305 }
3306 delete (yystack_[0].value.str);
3307 }
3308 #line 3309 "parseaut.cc"
3309 break;
3310
3311 case 187: // lbtt-transitions: lbtt-transitions "destination number" lbtt-acc lbtt-guard
3312 #line 2203 "parseaut.yy"
3313 {
3314 unsigned dst = (yystack_[2].value.num);
3315 if (dst >= (unsigned) res.states)
3316 {
3317 auto p = res.states_map.emplace(dst, 0);
3318 if (p.second)
3319 p.first->second = res.h->aut->new_state();
3320 dst = p.first->second;
3321 }
3322 else
3323 {
3324 res.states_map.emplace(dst, dst);
3325 }
3326 res.h->aut->new_edge(res.cur_state, dst,
3327 res.cur_label,
3328 res.acc_state | (yystack_[1].value.mark));
3329 }
3330 #line 3331 "parseaut.cc"
3331 break;
3332
3333
3334 #line 3335 "parseaut.cc"
3335
3336 default:
3337 break;
3338 }
3339 }
3340 #if YY_EXCEPTIONS
3341 catch (const syntax_error& yyexc)
3342 {
3343 YYCDEBUG << "Caught exception: " << yyexc.what() << '\n';
3344 error (yyexc);
3345 YYERROR;
3346 }
3347 #endif // YY_EXCEPTIONS
3348 YY_SYMBOL_PRINT ("-> $$ =", yylhs);
3349 yypop_ (yylen);
3350 yylen = 0;
3351
3352 // Shift the result of the reduction.
3353 yypush_ (YY_NULLPTR, YY_MOVE (yylhs));
3354 }
3355 goto yynewstate;
3356
3357
3358 /*--------------------------------------.
3359 | yyerrlab -- here on detecting error. |
3360 `--------------------------------------*/
3361 yyerrlab:
3362 // If not already recovering from an error, report this error.
3363 if (!yyerrstatus_)
3364 {
3365 ++yynerrs_;
3366 context yyctx (*this, yyla);
3367 std::string msg = yysyntax_error_ (yyctx);
3368 error (yyla.location, YY_MOVE (msg));
3369 }
3370
3371
3372 yyerror_range[1].location = yyla.location;
3373 if (yyerrstatus_ == 3)
3374 {
3375 /* If just tried and failed to reuse lookahead token after an
3376 error, discard it. */
3377
3378 // Return failure if at end of input.
3379 if (yyla.kind () == symbol_kind::S_YYEOF)
3380 YYABORT;
3381 else if (!yyla.empty ())
3382 {
3383 yy_destroy_ ("Error: discarding", yyla);
3384 yyla.clear ();
3385 }
3386 }
3387
3388 // Else will try to reuse lookahead token after shifting the error token.
3389 goto yyerrlab1;
3390
3391
3392 /*---------------------------------------------------.
3393 | yyerrorlab -- error raised explicitly by YYERROR. |
3394 `---------------------------------------------------*/
3395 yyerrorlab:
3396 /* Pacify compilers when the user code never invokes YYERROR and
3397 the label yyerrorlab therefore never appears in user code. */
3398 if (false)
3399 YYERROR;
3400
3401 /* Do not reclaim the symbols of the rule whose action triggered
3402 this YYERROR. */
3403 yypop_ (yylen);
3404 yylen = 0;
3405 YY_STACK_PRINT ();
3406 goto yyerrlab1;
3407
3408
3409 /*-------------------------------------------------------------.
3410 | yyerrlab1 -- common code for both syntax error and YYERROR. |
3411 `-------------------------------------------------------------*/
3412 yyerrlab1:
3413 yyerrstatus_ = 3; // Each real token shifted decrements this.
3414 // Pop stack until we find a state that shifts the error token.
3415 for (;;)
3416 {
3417 yyn = yypact_[+yystack_[0].state];
3418 if (!yy_pact_value_is_default_ (yyn))
3419 {
3420 yyn += symbol_kind::S_YYerror;
3421 if (0 <= yyn && yyn <= yylast_
3422 && yycheck_[yyn] == symbol_kind::S_YYerror)
3423 {
3424 yyn = yytable_[yyn];
3425 if (0 < yyn)
3426 break;
3427 }
3428 }
3429
3430 // Pop the current state because it cannot handle the error token.
3431 if (yystack_.size () == 1)
3432 YYABORT;
3433
3434 yyerror_range[1].location = yystack_[0].location;
3435 yy_destroy_ ("Error: popping", yystack_[0]);
3436 yypop_ ();
3437 YY_STACK_PRINT ();
3438 }
3439 {
3440 stack_symbol_type error_token;
3441
3442 yyerror_range[2].location = yyla.location;
3443 YYLLOC_DEFAULT (error_token.location, yyerror_range, 2);
3444
3445 // Shift the error token.
3446 error_token.state = state_type (yyn);
3447 yypush_ ("Shifting", YY_MOVE (error_token));
3448 }
3449 goto yynewstate;
3450
3451
3452 /*-------------------------------------.
3453 | yyacceptlab -- YYACCEPT comes here. |
3454 `-------------------------------------*/
3455 yyacceptlab:
3456 yyresult = 0;
3457 goto yyreturn;
3458
3459
3460 /*-----------------------------------.
3461 | yyabortlab -- YYABORT comes here. |
3462 `-----------------------------------*/
3463 yyabortlab:
3464 yyresult = 1;
3465 goto yyreturn;
3466
3467
3468 /*-----------------------------------------------------.
3469 | yyreturn -- parsing is finished, return the result. |
3470 `-----------------------------------------------------*/
3471 yyreturn:
3472 if (!yyla.empty ())
3473 yy_destroy_ ("Cleanup: discarding lookahead", yyla);
3474
3475 /* Do not reclaim the symbols of the rule whose action triggered
3476 this YYABORT or YYACCEPT. */
3477 yypop_ (yylen);
3478 YY_STACK_PRINT ();
3479 while (1 < yystack_.size ())
3480 {
3481 yy_destroy_ ("Cleanup: popping", yystack_[0]);
3482 yypop_ ();
3483 }
3484
3485 return yyresult;
3486 }
3487 #if YY_EXCEPTIONS
3488 catch (...)
3489 {
3490 YYCDEBUG << "Exception caught: cleaning lookahead and stack\n";
3491 // Do not try to display the values of the reclaimed symbols,
3492 // as their printers might throw an exception.
3493 if (!yyla.empty ())
3494 yy_destroy_ (YY_NULLPTR, yyla);
3495
3496 while (1 < yystack_.size ())
3497 {
3498 yy_destroy_ (YY_NULLPTR, yystack_[0]);
3499 yypop_ ();
3500 }
3501 throw;
3502 }
3503 #endif // YY_EXCEPTIONS
3504 }
3505
3506 void
error(const syntax_error & yyexc)3507 parser::error (const syntax_error& yyexc)
3508 {
3509 error (yyexc.location, yyexc.what ());
3510 }
3511
3512 /* Return YYSTR after stripping away unnecessary quotes and
3513 backslashes, so that it's suitable for yyerror. The heuristic is
3514 that double-quoting is unnecessary unless the string contains an
3515 apostrophe, a comma, or backslash (other than backslash-backslash).
3516 YYSTR is taken from yytname. */
3517 std::string
yytnamerr_(const char * yystr)3518 parser::yytnamerr_ (const char *yystr)
3519 {
3520 if (*yystr == '"')
3521 {
3522 std::string yyr;
3523 char const *yyp = yystr;
3524
3525 for (;;)
3526 switch (*++yyp)
3527 {
3528 case '\'':
3529 case ',':
3530 goto do_not_strip_quotes;
3531
3532 case '\\':
3533 if (*++yyp != '\\')
3534 goto do_not_strip_quotes;
3535 else
3536 goto append;
3537
3538 append:
3539 default:
3540 yyr += *yyp;
3541 break;
3542
3543 case '"':
3544 return yyr;
3545 }
3546 do_not_strip_quotes: ;
3547 }
3548
3549 return yystr;
3550 }
3551
3552 std::string
symbol_name(symbol_kind_type yysymbol)3553 parser::symbol_name (symbol_kind_type yysymbol)
3554 {
3555 return yytnamerr_ (yytname_[yysymbol]);
3556 }
3557
3558
3559
3560 // parser::context.
context(const parser & yyparser,const symbol_type & yyla)3561 parser::context::context (const parser& yyparser, const symbol_type& yyla)
3562 : yyparser_ (yyparser)
3563 , yyla_ (yyla)
3564 {}
3565
3566 int
expected_tokens(symbol_kind_type yyarg[],int yyargn) const3567 parser::context::expected_tokens (symbol_kind_type yyarg[], int yyargn) const
3568 {
3569 // Actual number of expected tokens
3570 int yycount = 0;
3571
3572 int yyn = yypact_[+yyparser_.yystack_[0].state];
3573 if (!yy_pact_value_is_default_ (yyn))
3574 {
3575 /* Start YYX at -YYN if negative to avoid negative indexes in
3576 YYCHECK. In other words, skip the first -YYN actions for
3577 this state because they are default actions. */
3578 int yyxbegin = yyn < 0 ? -yyn : 0;
3579 // Stay within bounds of both yycheck and yytname.
3580 int yychecklim = yylast_ - yyn + 1;
3581 int yyxend = yychecklim < YYNTOKENS ? yychecklim : YYNTOKENS;
3582 for (int yyx = yyxbegin; yyx < yyxend; ++yyx)
3583 if (yycheck_[yyx + yyn] == yyx && yyx != symbol_kind::S_YYerror
3584 && !yy_table_value_is_error_ (yytable_[yyx + yyn]))
3585 {
3586 if (!yyarg)
3587 ++yycount;
3588 else if (yycount == yyargn)
3589 return 0;
3590 else
3591 yyarg[yycount++] = YY_CAST (symbol_kind_type, yyx);
3592 }
3593 }
3594
3595 if (yyarg && yycount == 0 && 0 < yyargn)
3596 yyarg[0] = symbol_kind::S_YYEMPTY;
3597 return yycount;
3598 }
3599
3600
3601
3602 int
yy_syntax_error_arguments_(const context & yyctx,symbol_kind_type yyarg[],int yyargn) const3603 parser::yy_syntax_error_arguments_ (const context& yyctx,
3604 symbol_kind_type yyarg[], int yyargn) const
3605 {
3606 /* There are many possibilities here to consider:
3607 - If this state is a consistent state with a default action, then
3608 the only way this function was invoked is if the default action
3609 is an error action. In that case, don't check for expected
3610 tokens because there are none.
3611 - The only way there can be no lookahead present (in yyla) is
3612 if this state is a consistent state with a default action.
3613 Thus, detecting the absence of a lookahead is sufficient to
3614 determine that there is no unexpected or expected token to
3615 report. In that case, just report a simple "syntax error".
3616 - Don't assume there isn't a lookahead just because this state is
3617 a consistent state with a default action. There might have
3618 been a previous inconsistent state, consistent state with a
3619 non-default action, or user semantic action that manipulated
3620 yyla. (However, yyla is currently not documented for users.)
3621 - Of course, the expected token list depends on states to have
3622 correct lookahead information, and it depends on the parser not
3623 to perform extra reductions after fetching a lookahead from the
3624 scanner and before detecting a syntax error. Thus, state merging
3625 (from LALR or IELR) and default reductions corrupt the expected
3626 token list. However, the list is correct for canonical LR with
3627 one exception: it will still contain any token that will not be
3628 accepted due to an error action in a later state.
3629 */
3630
3631 if (!yyctx.lookahead ().empty ())
3632 {
3633 if (yyarg)
3634 yyarg[0] = yyctx.token ();
3635 int yyn = yyctx.expected_tokens (yyarg ? yyarg + 1 : yyarg, yyargn - 1);
3636 return yyn + 1;
3637 }
3638 return 0;
3639 }
3640
3641 // Generate an error message.
3642 std::string
yysyntax_error_(const context & yyctx) const3643 parser::yysyntax_error_ (const context& yyctx) const
3644 {
3645 // Its maximum.
3646 enum { YYARGS_MAX = 5 };
3647 // Arguments of yyformat.
3648 symbol_kind_type yyarg[YYARGS_MAX];
3649 int yycount = yy_syntax_error_arguments_ (yyctx, yyarg, YYARGS_MAX);
3650
3651 char const* yyformat = YY_NULLPTR;
3652 switch (yycount)
3653 {
3654 #define YYCASE_(N, S) \
3655 case N: \
3656 yyformat = S; \
3657 break
3658 default: // Avoid compiler warnings.
3659 YYCASE_ (0, YY_("syntax error"));
3660 YYCASE_ (1, YY_("syntax error, unexpected %s"));
3661 YYCASE_ (2, YY_("syntax error, unexpected %s, expecting %s"));
3662 YYCASE_ (3, YY_("syntax error, unexpected %s, expecting %s or %s"));
3663 YYCASE_ (4, YY_("syntax error, unexpected %s, expecting %s or %s or %s"));
3664 YYCASE_ (5, YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s"));
3665 #undef YYCASE_
3666 }
3667
3668 std::string yyres;
3669 // Argument number.
3670 std::ptrdiff_t yyi = 0;
3671 for (char const* yyp = yyformat; *yyp; ++yyp)
3672 if (yyp[0] == '%' && yyp[1] == 's' && yyi < yycount)
3673 {
3674 yyres += symbol_name (yyarg[yyi++]);
3675 ++yyp;
3676 }
3677 else
3678 yyres += *yyp;
3679 return yyres;
3680 }
3681
3682
3683 const short parser::yypact_ninf_ = -171;
3684
3685 const short parser::yytable_ninf_ = -130;
3686
3687 const short
3688 parser::yypact_[] =
3689 {
3690 15, -171, 17, 128, -171, -171, -171, -171, -171, 23,
3691 -171, -171, 14, -171, -171, 94, -171, -171, 49, -171,
3692 -171, -171, 19, 48, 15, 30, -171, -171, 132, 46,
3693 98, -171, -171, -171, 68, 76, -171, -171, -171, -171,
3694 139, 137, 145, -171, 140, 141, 142, 146, 147, 149,
3695 150, 151, -171, -171, -171, -171, -171, -171, -171, -171,
3696 -171, -171, 148, -171, 102, -34, -171, 89, -171, -171,
3697 -171, 91, -171, 99, -171, -171, 143, 144, -171, -171,
3698 -171, -171, 152, -171, -6, -171, -171, -171, 54, 153,
3699 85, -171, 119, -171, -171, 139, -171, -171, -171, -171,
3700 -171, -171, 3, -171, -171, 141, 154, -171, 44, -171,
3701 141, -171, 99, -171, 114, 99, -171, 141, 141, -171,
3702 61, -8, 36, -171, -171, -171, 158, 157, 159, 160,
3703 -171, -171, -171, -171, -171, -171, -171, -171, 162, 163,
3704 164, -171, 127, -171, -171, -3, -23, 129, -171, -171,
3705 61, -171, -171, 61, 64, 152, 141, 141, 2, -171,
3706 -171, 44, 114, 114, -171, -171, -171, 141, -171, -171,
3707 -171, -171, 166, 120, 133, -171, -171, -8, 122, -171,
3708 -171, -171, -171, 168, 170, -171, 13, -171, -171, -171,
3709 -171, -1, -171, 131, -171, -171, -171, -171, 53, 61,
3710 61, -171, 114, -171, -171, 134, -15, -171, -171, -171,
3711 -171, -171, -171, 130, 75, -8, -8, -171, -171, -171,
3712 171, -171, 165, -171, -171, -10, -171, 161, -171, -171,
3713 -171, -171, -171, -171, -171, 176, 155, -171, 167, -171,
3714 152, -171, -171, -171, -171, 138, -171, -171, 169, -171,
3715 156, -171, -171, 97, 178, 59, 56, -171, -171, -171,
3716 -171, 180, -171, 172, 185, 173, -171, -171, -171, -171
3717 };
3718
3719 const unsigned char
3720 parser::yydefact_[] =
3721 {
3722 0, 5, 0, 0, 127, 128, 3, 147, 176, 0,
3723 2, 8, 0, 24, 11, 0, 9, 10, 0, 180,
3724 6, 7, 0, 0, 0, 0, 1, 90, 0, 0,
3725 0, 178, 177, 175, 0, 179, 13, 19, 21, 4,
3726 149, 0, 0, 45, 0, 0, 0, 0, 0, 0,
3727 0, 0, 53, 38, 40, 42, 62, 29, 25, 126,
3728 130, 174, 0, 186, 0, 0, 154, 159, 150, 12,
3729 94, 99, 91, 110, 26, 88, 27, 28, 22, 30,
3730 32, 49, 14, 36, 37, 56, 58, 60, 44, 0,
3731 0, 183, 181, 153, 148, 152, 158, 162, 162, 160,
3732 155, 161, 0, 97, 100, 0, 118, 89, 108, 101,
3733 0, 92, 111, 112, 108, 93, 119, 0, 0, 46,
3734 0, 0, 34, 15, 35, 54, 0, 39, 41, 43,
3735 66, 65, 64, 16, 17, 63, 144, 131, 0, 0,
3736 0, 135, 182, 183, 151, 0, 0, 0, 74, 73,
3737 0, 71, 72, 0, 0, 14, 0, 0, 0, 109,
3738 122, 108, 108, 108, 114, 113, 123, 0, 120, 121,
3739 70, 69, 23, 31, 0, 85, 86, 0, 33, 52,
3740 51, 50, 55, 0, 0, 61, 0, 133, 134, 132,
3741 184, 0, 156, 0, 163, 157, 98, 75, 0, 0,
3742 0, 96, 106, 68, 67, 0, 0, 116, 117, 115,
3743 124, 48, 47, 0, 0, 0, 0, 57, 59, 145,
3744 0, 125, 0, 185, 187, 0, 78, 77, 76, 107,
3745 95, 103, 79, 102, 105, 0, 0, 82, 84, 83,
3746 14, 139, 142, 165, 167, 0, 164, 166, 168, 173,
3747 0, 80, 136, 141, 146, 0, 0, 171, 81, 137,
3748 138, 0, 143, 0, 0, 0, 140, 172, 169, 170
3749 };
3750
3751 const short
3752 parser::yypgoto_[] =
3753 {
3754 -171, 181, -171, 204, -171, -155, 86, -171, -171, -171,
3755 -171, 117, -171, -171, -171, -171, -171, -171, -171, -171,
3756 -171, -171, -171, -171, -171, -171, -171, -171, -171, -171,
3757 -119, -130, -170, -171, -43, -100, -171, -171, -171, 174,
3758 -171, 95, 7, -171, -171, -92, -171, -171, -171, 101,
3759 104, -171, -109, -171, -171, -171, -171, -171, -171, -171,
3760 -171, -171, -171, -171, -171, -171, -171, 175, -171, -171,
3761 116, 121, -171, -171, -171, -38, -171, -171, -171, -171,
3762 -171, -171, -171, 77, -171, -171
3763 };
3764
3765 const short
3766 parser::yydefgoto_[] =
3767 {
3768 0, 9, 24, 10, 11, 124, 135, 12, 38, 13,
3769 23, 57, 119, 28, 58, 120, 121, 85, 86, 87,
3770 172, 212, 122, 84, 127, 128, 129, 88, 106, 76,
3771 154, 234, 178, 41, 107, 108, 42, 72, 73, 109,
3772 105, 110, 159, 206, 230, 160, 111, 112, 164, 113,
3773 114, 115, 116, 169, 14, 15, 89, 90, 222, 261,
3774 253, 242, 254, 186, 16, 25, 65, 66, 67, 101,
3775 68, 145, 247, 248, 257, 249, 194, 17, 18, 19,
3776 34, 35, 63, 142, 224, 92
3777 };
3778
3779 const short
3780 parser::yytable_[] =
3781 {
3782 202, 173, 77, 205, 147, 155, 168, 214, 232, 243,
3783 161, 174, 163, 125, 219, 1, 2, 20, 3, 195,
3784 3, 223, 166, 26, 148, -104, 149, 27, 220, 94,
3785 126, 197, 95, 36, 198, 244, 245, 192, 246, 150,
3786 4, 5, 4, 5, 193, 238, 239, 6, 233, 175,
3787 176, 177, 7, 190, 7, 179, 203, 204, 210, 180,
3788 151, 152, 153, 221, 193, -104, 8, 37, 8, 207,
3789 208, 209, 31, 130, 170, 171, 131, 132, 243, 157,
3790 227, 228, 148, 236, 149, 252, 137, 199, 200, 138,
3791 139, 46, 40, 133, 134, 29, 59, 150, 199, 200,
3792 264, 32, 33, 265, 244, 250, 158, 246, 64, 215,
3793 216, 133, 134, 226, 140, 102, -129, 61, 151, 152,
3794 153, 30, 75, 102, 103, 201, 60, 96, 97, 22,
3795 98, 62, 103, 43, 99, 237, 44, 45, 46, 47,
3796 48, 49, 50, 51, 52, -18, 70, -20, 53, 54,
3797 55, 69, 56, 232, 199, 200, 215, 216, 64, -87,
3798 71, 259, 260, 74, 75, 78, 235, 79, 81, 93,
3799 80, 91, 82, 83, 123, 143, 158, 182, 117, 118,
3800 183, 190, 184, 185, 136, 187, 188, 189, 211, 156,
3801 196, 217, 213, 218, 240, 241, 200, 231, 225, 232,
3802 255, 262, 216, 266, 268, 39, 21, 141, 181, 229,
3803 167, 144, 256, 165, 162, 251, 258, 263, 0, 146,
3804 191, 269, 0, 0, 0, 0, 0, 0, 0, 0,
3805 0, 0, 0, 0, 0, 267, 0, 0, 0, 0,
3806 0, 0, 100, 0, 0, 104
3807 };
3808
3809 const short
3810 parser::yycheck_[] =
3811 {
3812 155, 120, 45, 1, 1, 105, 115, 177, 23, 19,
3813 110, 19, 112, 19, 1, 0, 1, 0, 3, 42,
3814 3, 22, 114, 0, 21, 23, 23, 13, 15, 63,
3815 36, 150, 66, 14, 153, 45, 46, 40, 48, 36,
3816 25, 26, 25, 26, 67, 215, 216, 32, 63, 57,
3817 58, 59, 37, 54, 37, 19, 156, 157, 167, 23,
3818 57, 58, 59, 50, 67, 63, 51, 19, 51, 161,
3819 162, 163, 23, 19, 117, 118, 22, 23, 19, 35,
3820 199, 200, 21, 213, 23, 240, 1, 34, 35, 4,
3821 5, 6, 62, 57, 58, 1, 50, 36, 34, 35,
3822 44, 52, 53, 47, 45, 235, 62, 48, 19, 34,
3823 35, 57, 58, 60, 29, 24, 31, 49, 57, 58,
3824 59, 27, 23, 24, 33, 61, 28, 38, 39, 1,
3825 41, 55, 33, 1, 45, 60, 4, 5, 6, 7,
3826 8, 9, 10, 11, 12, 13, 1, 19, 16, 17,
3827 18, 14, 20, 23, 34, 35, 34, 35, 19, 14,
3828 15, 64, 65, 23, 23, 23, 36, 21, 19, 67,
3829 23, 23, 22, 22, 22, 56, 62, 19, 35, 35,
3830 23, 54, 23, 23, 31, 23, 23, 23, 22, 35,
3831 61, 23, 59, 23, 23, 30, 35, 63, 67, 23,
3832 62, 23, 35, 23, 19, 24, 2, 90, 122, 202,
3833 115, 95, 43, 112, 110, 60, 60, 255, -1, 98,
3834 143, 48, -1, -1, -1, -1, -1, -1, -1, -1,
3835 -1, -1, -1, -1, -1, 63, -1, -1, -1, -1,
3836 -1, -1, 67, -1, -1, 71
3837 };
3838
3839 const unsigned char
3840 parser::yystos_[] =
3841 {
3842 0, 0, 1, 3, 25, 26, 32, 37, 51, 69,
3843 71, 72, 75, 77, 122, 123, 132, 145, 146, 147,
3844 0, 71, 1, 78, 70, 133, 0, 13, 81, 1,
3845 27, 23, 52, 53, 148, 149, 14, 19, 76, 69,
3846 62, 101, 104, 1, 4, 5, 6, 7, 8, 9,
3847 10, 11, 12, 16, 17, 18, 20, 79, 82, 50,
3848 28, 49, 55, 150, 19, 134, 135, 136, 138, 14,
3849 1, 15, 105, 106, 23, 23, 97, 102, 23, 21,
3850 23, 19, 22, 22, 91, 85, 86, 87, 95, 124,
3851 125, 23, 153, 67, 63, 66, 38, 39, 41, 45,
3852 135, 137, 24, 33, 107, 108, 96, 102, 103, 107,
3853 109, 114, 115, 117, 118, 119, 120, 35, 35, 80,
3854 83, 84, 90, 22, 73, 19, 36, 92, 93, 94,
3855 19, 22, 23, 57, 58, 74, 31, 1, 4, 5,
3856 29, 79, 151, 56, 138, 139, 139, 1, 21, 23,
3857 36, 57, 58, 59, 98, 103, 35, 35, 62, 110,
3858 113, 103, 118, 103, 116, 117, 113, 109, 120, 121,
3859 102, 102, 88, 98, 19, 57, 58, 59, 100, 19,
3860 23, 74, 19, 23, 23, 23, 131, 23, 23, 23,
3861 54, 151, 40, 67, 144, 42, 61, 98, 98, 34,
3862 35, 61, 73, 103, 103, 1, 111, 113, 113, 113,
3863 120, 22, 89, 59, 100, 34, 35, 23, 23, 1,
3864 15, 50, 126, 22, 152, 67, 60, 98, 98, 110,
3865 112, 63, 23, 63, 99, 36, 99, 60, 100, 100,
3866 23, 30, 129, 19, 45, 46, 48, 140, 141, 143,
3867 99, 60, 73, 128, 130, 62, 43, 142, 60, 64,
3868 65, 127, 23, 143, 44, 47, 23, 63, 19, 48
3869 };
3870
3871 const unsigned char
3872 parser::yyr1_[] =
3873 {
3874 0, 68, 69, 70, 69, 69, 69, 69, 71, 71,
3875 71, 71, 72, 72, 73, 73, 74, 74, 75, 76,
3876 78, 77, 80, 79, 81, 81, 82, 82, 82, 82,
3877 83, 82, 84, 82, 82, 82, 82, 82, 85, 82,
3878 86, 82, 87, 82, 82, 82, 88, 88, 89, 90,
3879 90, 90, 90, 91, 91, 91, 92, 92, 93, 93,
3880 94, 94, 95, 95, 95, 95, 95, 96, 96, 97,
3881 97, 98, 98, 98, 98, 98, 98, 98, 98, 99,
3882 100, 100, 100, 100, 100, 100, 100, 101, 102, 103,
3883 104, 104, 105, 105, 105, 106, 107, 107, 107, 108,
3884 108, 109, 110, 110, 111, 111, 112, 112, 113, 113,
3885 114, 114, 115, 115, 115, 116, 117, 117, 118, 119,
3886 119, 119, 120, 120, 121, 122, 122, 123, 123, 124,
3887 125, 125, 125, 125, 125, 125, 126, 127, 127, 128,
3888 128, 129, 130, 130, 131, 131, 131, 133, 132, 134,
3889 134, 134, 134, 135, 136, 136, 137, 137, 138, 138,
3890 138, 138, 139, 139, 140, 140, 141, 141, 142, 142,
3891 142, 143, 144, 144, 145, 145, 146, 147, 147, 148,
3892 149, 149, 150, 151, 151, 152, 153, 153
3893 };
3894
3895 const signed char
3896 parser::yyr2_[] =
3897 {
3898 0, 2, 1, 0, 3, 1, 2, 2, 1, 1,
3899 1, 1, 4, 3, 0, 1, 1, 1, 2, 1,
3900 0, 3, 0, 4, 0, 2, 2, 2, 2, 1,
3901 0, 4, 0, 4, 3, 3, 2, 2, 0, 3,
3902 0, 3, 0, 3, 2, 1, 0, 2, 1, 0,
3903 2, 2, 2, 0, 2, 3, 0, 3, 0, 3,
3904 0, 2, 0, 2, 2, 2, 2, 3, 3, 3,
3905 3, 1, 1, 1, 1, 2, 3, 3, 3, 1,
3906 4, 5, 3, 3, 3, 1, 1, 1, 1, 1,
3907 0, 2, 2, 2, 1, 5, 3, 1, 3, 0,
3908 1, 1, 3, 3, 0, 2, 0, 1, 0, 1,
3909 0, 1, 1, 2, 2, 2, 3, 3, 1, 1,
3910 2, 2, 2, 2, 2, 7, 3, 1, 1, 1,
3911 0, 2, 3, 3, 3, 2, 3, 1, 1, 0,
3912 3, 2, 0, 2, 0, 2, 4, 0, 5, 0,
3913 1, 3, 2, 2, 1, 2, 3, 3, 2, 1,
3914 2, 2, 0, 2, 1, 1, 1, 1, 0, 3,
3915 3, 2, 6, 3, 3, 2, 1, 2, 2, 1,
3916 0, 3, 3, 0, 2, 1, 0, 4
3917 };
3918
3919
3920 #if HOAYYDEBUG || 1
3921 // YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
3922 // First, the terminals, then, starting at \a YYNTOKENS, nonterminals.
3923 const char*
3924 const parser::yytname_[] =
3925 {
3926 "\"end of file\"", "error", "\"invalid token\"", "\"HOA:\"",
3927 "\"States:\"", "\"Start:\"", "\"AP:\"", "\"Alias:\"", "\"Acceptance:\"",
3928 "\"acc-name:\"", "\"tool:\"", "\"name:\"", "\"properties:\"",
3929 "\"--BODY--\"", "\"--END--\"", "\"State:\"", "\"spot.highlight.edges:\"",
3930 "\"spot.highlight.states:\"", "\"spot.state-player:\"", "\"identifier\"",
3931 "\"header name\"", "\"alias name\"", "\"string\"", "\"integer\"", "'['",
3932 "\"DRA\"", "\"DSA\"", "\"v2\"", "\"explicit\"", "\"Acceptance-Pairs:\"",
3933 "\"Acc-Sig:\"", "\"---\"", "\"#line\"", "BDD", "'|'", "'&'", "'!'",
3934 "\"never\"", "\"skip\"", "\"if\"", "\"fi\"", "\"do\"", "\"od\"",
3935 "\"->\"", "\"goto\"", "\"false\"", "\"atomic\"", "\"assert\"",
3936 "\"boolean formula\"", "\"-1\"", "\"end of DSTAR automaton\"",
3937 "\"LBTT header\"", "\"state acceptance\"",
3938 "\"acceptance sets for empty automaton\"", "\"acceptance set\"",
3939 "\"state number\"", "\"destination number\"", "'t'", "'f'", "'('", "')'",
3940 "']'", "'{'", "'}'", "'+'", "'-'", "';'", "':'", "$accept", "aut", "$@1",
3941 "aut-1", "hoa", "string_opt", "BOOLEAN", "header", "version",
3942 "format-version", "$@2", "aps", "$@3", "header-items", "header-item",
3943 "$@4", "$@5", "$@6", "$@7", "$@8", "ap-names", "ap-name", "acc-spec",
3944 "properties", "highlight-edges", "highlight-states", "state-player",
3945 "header-spec", "state-conj-2", "init-state-conj-2", "label-expr",
3946 "acc-set", "acceptance-cond", "body", "state-num", "checked-state-num",
3947 "states", "state", "state-name", "label", "state-label_opt",
3948 "trans-label", "acc-sig", "acc-sets", "state-acc_opt", "trans-acc_opt",
3949 "labeled-edges", "some-labeled-edges", "incorrectly-unlabeled-edge",
3950 "labeled-edge", "state-conj-checked", "unlabeled-edges",
3951 "unlabeled-edge", "incorrectly-labeled-edge", "dstar", "dstar_type",
3952 "dstar_header", "dstar_sizes", "dstar_state_id", "sign", "dstar_accsigs",
3953 "dstar_state_accsig", "dstar_transitions", "dstar_states", "never",
3954 "$@9", "nc-states", "nc-one-ident", "nc-ident-list",
3955 "nc-transition-block", "nc-state", "nc-transitions",
3956 "nc-formula-or-ident", "nc-formula", "nc-opt-dest", "nc-src-dest",
3957 "nc-transition", "lbtt", "lbtt-header-states", "lbtt-header",
3958 "lbtt-body", "lbtt-states", "lbtt-state", "lbtt-acc", "lbtt-guard",
3959 "lbtt-transitions", YY_NULLPTR
3960 };
3961 #endif
3962
3963
3964 #if HOAYYDEBUG
3965 const short
3966 parser::yyrline_[] =
3967 {
3968 0, 343, 343, 347, 347, 348, 349, 350, 357, 358,
3969 359, 360, 366, 367, 369, 370, 371, 371, 373, 677,
3970 684, 684, 687, 686, 739, 740, 741, 759, 764, 768,
3971 769, 769, 782, 781, 815, 819, 824, 828, 830, 829,
3972 833, 832, 836, 835, 844, 853, 855, 856, 857, 885,
3973 886, 887, 888, 892, 893, 914, 929, 930, 934, 935,
3974 940, 941, 948, 949, 950, 951, 955, 960, 964, 972,
3975 976, 982, 986, 990, 1019, 1034, 1040, 1047, 1054, 1060,
3976 1078, 1106, 1124, 1128, 1134, 1140, 1144, 1153, 1237, 1247,
3977 1290, 1291, 1330, 1331, 1355, 1365, 1395, 1403, 1404, 1410,
3978 1411, 1433, 1460, 1471, 1475, 1479, 1487, 1491, 1502, 1506,
3979 1520, 1521, 1522, 1523, 1524, 1525, 1543, 1554, 1567, 1582,
3980 1583, 1584, 1585, 1616, 1647, 1658, 1659, 1664, 1676, 1689,
3981 1713, 1714, 1715, 1733, 1746, 1750, 1752, 1792, 1793, 1796,
3982 1800, 1825, 1827, 1828, 1837, 1838, 1839, 1850, 1849, 1880,
3983 1881, 1882, 1883, 1885, 1896, 1906, 1924, 1928, 1934, 1944,
3984 1945, 1946, 1962, 1963, 1973, 1973, 1975, 2005, 2011, 2015,
3985 2019, 2026, 2045, 2049, 2058, 2099, 2105, 2118, 2123, 2128,
3986 2129, 2130, 2132, 2151, 2152, 2161, 2201, 2202
3987 };
3988
3989 void
yy_stack_print_() const3990 parser::yy_stack_print_ () const
3991 {
3992 *yycdebug_ << "Stack now";
3993 for (stack_type::const_iterator
3994 i = yystack_.begin (),
3995 i_end = yystack_.end ();
3996 i != i_end; ++i)
3997 *yycdebug_ << ' ' << int (i->state);
3998 *yycdebug_ << '\n';
3999 }
4000
4001 void
yy_reduce_print_(int yyrule) const4002 parser::yy_reduce_print_ (int yyrule) const
4003 {
4004 int yylno = yyrline_[yyrule];
4005 int yynrhs = yyr2_[yyrule];
4006 // Print the symbols being reduced, and their result.
4007 *yycdebug_ << "Reducing stack by rule " << yyrule - 1
4008 << " (line " << yylno << "):\n";
4009 // The symbols being reduced.
4010 for (int yyi = 0; yyi < yynrhs; yyi++)
4011 YY_SYMBOL_PRINT (" $" << yyi + 1 << " =",
4012 yystack_[(yynrhs) - (yyi + 1)]);
4013 }
4014 #endif // HOAYYDEBUG
4015
4016 parser::symbol_kind_type
yytranslate_(int t)4017 parser::yytranslate_ (int t)
4018 {
4019 // YYTRANSLATE[TOKEN-NUM] -- Symbol number corresponding to
4020 // TOKEN-NUM as returned by yylex.
4021 static
4022 const signed char
4023 translate_table[] =
4024 {
4025 0, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4026 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4027 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4028 2, 2, 2, 36, 2, 2, 2, 2, 35, 2,
4029 59, 60, 2, 64, 2, 65, 2, 2, 2, 2,
4030 2, 2, 2, 2, 2, 2, 2, 2, 67, 66,
4031 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4032 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4033 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4034 2, 24, 2, 61, 2, 2, 2, 2, 2, 2,
4035 2, 2, 58, 2, 2, 2, 2, 2, 2, 2,
4036 2, 2, 2, 2, 2, 2, 57, 2, 2, 2,
4037 2, 2, 2, 62, 34, 63, 2, 2, 2, 2,
4038 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4039 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4040 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4041 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4042 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4043 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4044 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4045 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4046 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4047 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4048 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4049 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
4050 2, 2, 2, 2, 2, 2, 1, 2, 3, 4,
4051 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
4052 15, 16, 17, 18, 19, 20, 21, 22, 23, 25,
4053 26, 27, 28, 29, 30, 31, 32, 33, 37, 38,
4054 39, 40, 41, 42, 43, 44, 45, 46, 47, 48,
4055 49, 50, 51, 52, 53, 54, 55, 56
4056 };
4057 // Last valid token kind.
4058 const int code_max = 307;
4059
4060 if (t <= 0)
4061 return symbol_kind::S_YYEOF;
4062 else if (t <= code_max)
4063 return YY_CAST (symbol_kind_type, translate_table[t]);
4064 else
4065 return symbol_kind::S_YYUNDEF;
4066 }
4067
4068 } // hoayy
4069 #line 4070 "parseaut.cc"
4070
4071 #line 2221 "parseaut.yy"
4072
4073
fill_guards(result_ & r)4074 static void fill_guards(result_& r)
4075 {
4076 unsigned nap = r.ap.size();
4077
4078 int* vars = new int[nap];
4079 for (unsigned i = 0; i < nap; ++i)
4080 vars[i] = r.ap[nap - 1 - i];
4081
4082 // build the 2^nap possible guards
4083 r.guards.reserve(1U << nap);
4084 for (size_t i = 0; i < (1U << nap); ++i)
4085 r.guards.push_back(bdd_ibuildcube(i, nap, vars));
4086 r.cur_guard = r.guards.begin();
4087
4088 delete[] vars;
4089 }
4090
4091 void
error(const location_type & location,const std::string & message)4092 hoayy::parser::error(const location_type& location,
4093 const std::string& message)
4094 {
4095 res.h->errors.emplace_back(location, message);
4096 }
4097
4098 static spot::acc_cond::acc_code
fix_acceptance_aux(spot::acc_cond & acc,spot::acc_cond::acc_code in,unsigned pos,spot::acc_cond::mark_t onlyneg,spot::acc_cond::mark_t both,unsigned base)4099 fix_acceptance_aux(spot::acc_cond& acc,
4100 spot::acc_cond::acc_code in, unsigned pos,
4101 spot::acc_cond::mark_t onlyneg,
4102 spot::acc_cond::mark_t both,
4103 unsigned base)
4104 {
4105 auto& w = in[pos];
4106 switch (w.sub.op)
4107 {
4108 case spot::acc_cond::acc_op::And:
4109 {
4110 unsigned sub = pos - w.sub.size;
4111 --pos;
4112 auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
4113 pos -= in[pos].sub.size;
4114 while (sub < pos)
4115 {
4116 --pos;
4117 c &= fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
4118 pos -= in[pos].sub.size;
4119 }
4120 return c;
4121 }
4122 case spot::acc_cond::acc_op::Or:
4123 {
4124 unsigned sub = pos - w.sub.size;
4125 --pos;
4126 auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
4127 pos -= in[pos].sub.size;
4128 while (sub < pos)
4129 {
4130 --pos;
4131 c |= fix_acceptance_aux(acc, in, pos, onlyneg, both, base);
4132 pos -= in[pos].sub.size;
4133 }
4134 return c;
4135 }
4136 case spot::acc_cond::acc_op::Inf:
4137 return acc.inf(in[pos - 1].mark);
4138 case spot::acc_cond::acc_op::Fin:
4139 return acc.fin(in[pos - 1].mark);
4140 case spot::acc_cond::acc_op::FinNeg:
4141 {
4142 auto m = in[pos - 1].mark;
4143 auto c = acc.fin(onlyneg & m);
4144 spot::acc_cond::mark_t tmp = {};
4145 for (auto i: both.sets())
4146 {
4147 if (m.has(i))
4148 tmp.set(base);
4149 ++base;
4150 }
4151 if (tmp)
4152 c |= acc.fin(tmp);
4153 return c;
4154 }
4155 case spot::acc_cond::acc_op::InfNeg:
4156 {
4157 auto m = in[pos - 1].mark;
4158 auto c = acc.inf(onlyneg & m);
4159 spot::acc_cond::mark_t tmp = {};
4160 for (auto i: both.sets())
4161 {
4162 if (m.has(i))
4163 tmp.set(base);
4164 ++base;
4165 }
4166 if (tmp)
4167 c &= acc.inf(tmp);
4168 return c;
4169 }
4170 }
4171 SPOT_UNREACHABLE();
4172 return {};
4173 }
4174
fix_acceptance(result_ & r)4175 static void fix_acceptance(result_& r)
4176 {
4177 if (r.opts.want_kripke)
4178 return;
4179 auto& acc = r.h->aut->acc();
4180
4181 // If a set x appears only as Inf(!x), we can complement it so that
4182 // we work with Inf(x) instead.
4183 auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
4184 if (onlyneg)
4185 {
4186 for (auto& t: r.h->aut->edge_vector())
4187 t.acc ^= onlyneg;
4188 }
4189
4190 // However if set x is used elsewhere, for instance in
4191 // Inf(!x) & Inf(x)
4192 // complementing x would be wrong. We need to create a
4193 // new set, y, that is the complement of x, and rewrite
4194 // this as Inf(y) & Inf(x).
4195 auto both = r.neg_acc_sets & r.pos_acc_sets;
4196 unsigned base = 0;
4197 if (both)
4198 {
4199 base = acc.add_sets(both.count());
4200 for (auto& t: r.h->aut->edge_vector())
4201 {
4202 unsigned i = 0;
4203 if ((t.acc & both) != both)
4204 for (unsigned v : both.sets())
4205 {
4206 if (!t.acc.has(v))
4207 t.acc |= acc.mark(base + i);
4208 i++;
4209 }
4210 }
4211 }
4212
4213 if (onlyneg || both)
4214 {
4215 auto& acc = r.h->aut->acc();
4216 auto code = acc.get_acceptance();
4217 r.h->aut->set_acceptance(acc.num_sets(),
4218 fix_acceptance_aux(acc, code, code.size() - 1,
4219 onlyneg, both, base));
4220 }
4221 }
4222
4223 // Spot only supports a single initial state.
4224 //
4225 // If the input file does not declare any initial state (this is valid
4226 // in the HOA format) add one nonetheless.
4227 //
4228 // If the input file has multiple initial states we have to merge
4229 // them.
4230 //
4231 // 1) In the non-alternating case, this is as simple as making a new
4232 // initial state using the union of all the outgoing transitions of
4233 // the declared initial states. Note that if one of the original
4234 // initial state has no incoming transition, then we can use it as
4235 // initial state, avoiding the creation of a new state.
4236 //
4237 // 2) In the alternating case, the input may have several initial
4238 // states that are conjuncts. We have to reduce the conjuncts to a
4239 // single state first.
4240
fix_initial_state(result_ & r)4241 static void fix_initial_state(result_& r)
4242 {
4243 std::vector<std::vector<unsigned>> start;
4244 start.reserve(r.start.size());
4245 unsigned ssz = r.info_states.size();
4246 for (auto& p : r.start)
4247 {
4248 std::vector<unsigned> v;
4249 v.reserve(p.second.size());
4250 for (unsigned s: p.second)
4251 // Ignore initial states without declaration
4252 // (They have been diagnosed already.)
4253 if (s < ssz && r.info_states[s].declared)
4254 v.emplace_back(s);
4255 if (!v.empty())
4256 start.push_back(v);
4257 }
4258
4259 // If no initial state has been declared, add one.
4260 if (start.empty())
4261 {
4262 if (r.opts.want_kripke)
4263 r.h->ks->set_init_state(r.h->ks->new_state(bddfalse));
4264 else
4265 r.h->aut->set_init_state(r.h->aut->new_state());
4266 return;
4267 }
4268
4269 // Remove any duplicate initial state.
4270 std::sort(start.begin(), start.end());
4271 auto res = std::unique(start.begin(), start.end());
4272 start.resize(std::distance(start.begin(), res));
4273
4274 assert(start.size() >= 1);
4275 if (start.size() == 1)
4276 {
4277 if (r.opts.want_kripke)
4278 r.h->ks->set_init_state(start.front().front());
4279 else
4280 r.h->aut->set_univ_init_state(start.front().begin(),
4281 start.front().end());
4282 }
4283 else
4284 {
4285 if (r.opts.want_kripke)
4286 {
4287 r.h->errors.emplace_front(r.start.front().first,
4288 "Kripke structure only support "
4289 "a single initial state");
4290 return;
4291 }
4292 // Fiddling with initial state may turn an incomplete automaton
4293 // into a complete one.
4294 if (r.complete.is_false())
4295 r.complete = spot::trival::maybe();
4296 // Multiple initial states. We might need to add a fake one,
4297 // unless one of the actual initial state has no incoming edge.
4298 auto& aut = r.h->aut;
4299 std::vector<unsigned char> has_incoming(aut->num_states(), 0);
4300 for (auto& t: aut->edges())
4301 for (unsigned ud: aut->univ_dests(t))
4302 has_incoming[ud] = 1;
4303
4304 bool found = false;
4305 unsigned init = 0;
4306 bool init_alternation = false;
4307 for (auto& pp: start)
4308 if (pp.size() == 1)
4309 {
4310 unsigned p = pp.front();
4311 if (!has_incoming[p])
4312 {
4313 init = p;
4314 found = true;
4315 }
4316 }
4317 else
4318 {
4319 init_alternation = true;
4320 break;
4321 }
4322
4323 if (!found || init_alternation)
4324 // We do need a fake initial state
4325 init = aut->new_state();
4326 aut->set_init_state(init);
4327
4328 // The non-alternating case is the easiest, we simply declare
4329 // the outgoing transitions of all "original initial states"
4330 // into the only one initial state.
4331 if (!init_alternation)
4332 {
4333 for (auto& pp: start)
4334 {
4335 unsigned p = pp.front();
4336 if (p != init)
4337 for (auto& t: aut->out(p))
4338 aut->new_edge(init, t.dst, t.cond);
4339 }
4340 }
4341 else
4342 {
4343 // In the alternating case, we merge outgoing transition of
4344 // the universal destination of conjunct initial states.
4345 // (Note that this loop would work for the non-alternating
4346 // case too, but it is more expansive, so we avoid it if we
4347 // can.)
4348 spot::outedge_combiner combiner(aut);
4349 bdd comb_or = bddfalse;
4350 for (auto& pp: start)
4351 {
4352 bdd comb_and = bddtrue;
4353 for (unsigned d: pp)
4354 comb_and &= combiner(d);
4355 comb_or |= comb_and;
4356 }
4357 combiner.new_dests(init, comb_or);
4358 }
4359 }
4360 }
4361
fix_properties(result_ & r)4362 static void fix_properties(result_& r)
4363 {
4364 r.aut_or_ks->prop_universal(r.universal);
4365 r.aut_or_ks->prop_complete(r.complete);
4366 if (r.acc_style == State_Acc ||
4367 (r.acc_style == Mixed_Acc && !r.trans_acc_seen))
4368 r.aut_or_ks->prop_state_acc(true);
4369 }
4370
check_version(const result_ & r)4371 static void check_version(const result_& r)
4372 {
4373 if (r.h->type != spot::parsed_aut_type::HOA)
4374 return;
4375 auto& v = r.format_version;
4376 if (v.size() < 2 || v[0] != 'v' || v[1] < '1' || v[1] > '9')
4377 {
4378 r.h->errors.emplace_front(r.format_version_loc, "unknown HOA version");
4379 return;
4380 }
4381 const char* beg = &v[1];
4382 char* end = nullptr;
4383 long int vers = strtol(beg, &end, 10);
4384 if (vers != 1)
4385 {
4386 r.h->errors.emplace_front(r.format_version_loc,
4387 "unsupported HOA version");
4388 return;
4389 }
4390 constexpr const char supported[] = "1";
4391 if (strverscmp(supported, beg) < 0 && !r.h->errors.empty())
4392 {
4393 std::ostringstream s;
4394 s << "we can read HOA v" << supported
4395 << " but this file uses " << v << "; this might "
4396 "cause the following errors";
4397 r.h->errors.emplace_front(r.format_version_loc, s.str());
4398 return;
4399 }
4400 }
4401
4402 namespace spot
4403 {
automaton_stream_parser(const std::string & name,automaton_parser_options opt)4404 automaton_stream_parser::automaton_stream_parser(const std::string& name,
4405 automaton_parser_options opt)
4406 try
4407 : filename_(name), opts_(opt)
4408 {
4409 if (hoayyopen(name, &scanner_))
4410 throw std::runtime_error("Cannot open file "s + name);
4411 }
4412 catch (...)
4413 {
4414 hoayyclose(scanner_);
4415 throw;
4416 }
4417
automaton_stream_parser(int fd,const std::string & name,automaton_parser_options opt)4418 automaton_stream_parser::automaton_stream_parser(int fd,
4419 const std::string& name,
4420 automaton_parser_options opt)
4421 try
4422 : filename_(name), opts_(opt)
4423 {
4424 if (hoayyopen(fd, &scanner_))
4425 throw std::runtime_error("Cannot open file "s + name);
4426 }
4427 catch (...)
4428 {
4429 hoayyclose(scanner_);
4430 throw;
4431 }
4432
automaton_stream_parser(const char * data,const std::string & filename,automaton_parser_options opt)4433 automaton_stream_parser::automaton_stream_parser(const char* data,
4434 const std::string& filename,
4435 automaton_parser_options opt)
4436 try
4437 : filename_(filename), opts_(opt)
4438 {
4439 hoayystring(data, &scanner_);
4440 }
4441 catch (...)
4442 {
4443 hoayyclose(scanner_);
4444 throw;
4445 }
4446
~automaton_stream_parser()4447 automaton_stream_parser::~automaton_stream_parser()
4448 {
4449 hoayyclose(scanner_);
4450 }
4451
raise_parse_error(const parsed_aut_ptr & pa)4452 static void raise_parse_error(const parsed_aut_ptr& pa)
4453 {
4454 if (pa->aborted)
4455 pa->errors.emplace_back(pa->loc, "parsing aborted");
4456 if (!pa->errors.empty())
4457 {
4458 std::ostringstream s;
4459 if (pa->format_errors(s))
4460 throw parse_error(s.str());
4461 }
4462 // It is possible that pa->aut == nullptr if we reach the end of a
4463 // stream. It is not necessarily an error.
4464 }
4465
4466 parsed_aut_ptr
parse(const bdd_dict_ptr & dict,environment & env)4467 automaton_stream_parser::parse(const bdd_dict_ptr& dict,
4468 environment& env)
4469 {
4470 restart:
4471 result_ r;
4472 r.opts = opts_;
4473 r.h = std::make_shared<spot::parsed_aut>(filename_);
4474 if (opts_.want_kripke)
4475 r.aut_or_ks = r.h->ks = make_kripke_graph(dict);
4476 else
4477 r.aut_or_ks = r.h->aut = make_twa_graph(dict);
4478 r.env = &env;
4479 hoayy::parser parser(scanner_, r, last_loc);
4480 static bool env_debug = !!getenv("SPOT_DEBUG_PARSER");
4481 parser.set_debug_level(opts_.debug || env_debug);
4482 hoayyreset(scanner_);
4483 try
4484 {
4485 if (parser.parse())
4486 {
4487 r.h->aut = nullptr;
4488 r.h->ks = nullptr;
4489 r.aut_or_ks = nullptr;
4490 }
4491 }
4492 catch (const spot::hoa_abort& e)
4493 {
4494 r.h->aborted = true;
4495 // Bison 3.0.2 lacks a += operator for locations.
4496 r.h->loc = r.h->loc + e.pos;
4497 }
4498 check_version(r);
4499 last_loc = r.h->loc;
4500 last_loc.step();
4501 filename_ = r.h->filename; // in case it was changed
4502 if (r.h->aborted)
4503 {
4504 if (opts_.ignore_abort)
4505 goto restart;
4506 return r.h;
4507 }
4508 if (opts_.raise_errors)
4509 raise_parse_error(r.h);
4510 if (!r.aut_or_ks)
4511 return r.h;
4512 if (r.state_names)
4513 r.aut_or_ks->set_named_prop("state-names", r.state_names);
4514 if (r.highlight_edges)
4515 r.aut_or_ks->set_named_prop("highlight-edges", r.highlight_edges);
4516 if (r.highlight_states)
4517 r.aut_or_ks->set_named_prop("highlight-states", r.highlight_states);
4518 if (r.state_player)
4519 r.aut_or_ks->set_named_prop("state-player", r.state_player);
4520 fix_acceptance(r);
4521 fix_initial_state(r);
4522 fix_properties(r);
4523 if (r.h->aut && !r.h->aut->is_existential())
4524 r.h->aut->merge_univ_dests();
4525 return r.h;
4526 }
4527
4528 parsed_aut_ptr
parse_aut(const std::string & filename,const bdd_dict_ptr & dict,environment & env,automaton_parser_options opts)4529 parse_aut(const std::string& filename, const bdd_dict_ptr& dict,
4530 environment& env, automaton_parser_options opts)
4531 {
4532 auto localopts = opts;
4533 localopts.raise_errors = false;
4534 parsed_aut_ptr pa;
4535 try
4536 {
4537 automaton_stream_parser p(filename, localopts);
4538 pa = p.parse(dict, env);
4539 }
4540 catch (const std::runtime_error& e)
4541 {
4542 if (opts.raise_errors)
4543 throw;
4544 parsed_aut_ptr pa = std::make_shared<spot::parsed_aut>(filename);
4545 pa->errors.emplace_back(spot::location(), e.what());
4546 return pa;
4547 }
4548 if (!pa->aut && !pa->ks && pa->errors.empty())
4549 pa->errors.emplace_back(pa->loc, "no automaton read (empty input?)");
4550 if (opts.raise_errors)
4551 raise_parse_error(pa);
4552 return pa;
4553 }
4554
4555
4556 }
4557
4558 // Local Variables:
4559 // mode: c++
4560 // End:
4561