parseaut.yy 56.7 KB
Newer Older
1
/* -*- coding: utf-8 -*-
2
3
** Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
**
** This file is part of Spot, a model checking library.
**
** Spot is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by
** the Free Software Foundation; either version 3 of the License, or
** (at your option) any later version.
**
** Spot is distributed in the hope that it will be useful, but WITHOUT
** ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
** or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
** License for more details.
**
** You should have received a copy of the GNU General Public License
** along with this program.  If not, see <http://www.gnu.org/licenses/>.
*/
%language "C++"
%locations
%defines
%expect 0 // No shift/reduce
%name-prefix "hoayy"
%debug
%error-verbose
27
%lex-param { PARSE_ERROR_LIST }
28
29
30
31
%define api.location.type "spot::location"

%code requires
{
32
#include "config.h"
33
#include <spot/misc/common.hh>
34
35
36
#include <string>
#include <cstring>
#include <sstream>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37
#include <unordered_map>
38
#include <algorithm>
39
40
41
42
#include <spot/twa/formula2bdd.hh>
#include <spot/parseaut/public.hh>
#include "spot/priv/accmap.hh"
#include <spot/tl/parse.hh>
43

44
45
46
47
48
#ifndef HAVE_STRVERSCMP
// If the libc does not have this, a version is compiled in lib/.
extern "C" int strverscmp(const char *s1, const char *s2);
#endif

49
50
51
52
// Work around Bison not letting us write
//  %lex-param { res.h->errors }
#define PARSE_ERROR_LIST res.h->errors

53
  inline namespace hoayy_support
54
  {
55
56
    typedef std::map<int, bdd> map_t;

57
    /* Cache parsed formulae.  Labels on arcs are frequently identical
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
58
       and it would be a waste of time to parse them to formula
59
60
61
       over and over, and to register all their atomic_propositions in
       the bdd_dict.  Keep the bdd result around so we can reuse
       it.  */
62
63
64
    typedef std::map<std::string, bdd> formula_cache;

    typedef std::pair<int, std::string*> pair;
65
    typedef spot::twa_graph::namer<std::string> named_tgba_t;
66
67
68
69
70
71
72
73

    // Note: because this parser is meant to be used on a stream of
    // automata, it tries hard to recover from errors, so that we get a
    // chance to reach the end of the current automaton in order to
    // process the next one.  Several variables below are used to keep
    // track of various error conditions.
    enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
			 Implicit_Labels };
74
    enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
75
76

    struct result_
77
    {
78
79
      struct state_info
      {
80
81
	bool declared = false;
	bool used = false;
82
83
	spot::location used_loc;
      };
84
      spot::parsed_aut_ptr h;
85
      spot::twa_ptr aut_or_ks;
86
      spot::automaton_parser_options opts;
87
88
      std::string format_version;
      spot::location format_version_loc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
89
      spot::environment* env;
90
91
92
93
94
95
      formula_cache fcache;
      named_tgba_t* namer = nullptr;
      spot::acc_mapper_int* acc_mapper = nullptr;
      std::vector<int> ap;
      std::vector<bdd> guards;
      std::vector<bdd>::const_iterator cur_guard;
96
      map_t dest_map;
97
      std::vector<state_info> info_states; // States declared and used.
98
99
      std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
      std::unordered_map<std::string, bdd> alias;
100
101
102
103
104
105
106
107
108
109
      struct prop_info
      {
	spot::location loc;
	bool val;
	operator bool() const
	{
	  return val;
	};
      };
      std::unordered_map<std::string, prop_info> props;
110
111
112
113
114
115
116
      spot::location states_loc;
      spot::location ap_loc;
      spot::location state_label_loc;
      spot::location accset_loc;
      spot::acc_cond::mark_t acc_state;
      spot::acc_cond::mark_t neg_acc_sets = 0U;
      spot::acc_cond::mark_t pos_acc_sets = 0U;
117
118
      int plus;
      int minus;
119
      std::vector<std::string>* state_names = nullptr;
120
121
      std::map<unsigned, unsigned>* highlight_edges = nullptr;
      std::map<unsigned, unsigned>* highlight_states = nullptr;
122
      std::map<unsigned, unsigned> states_map;
123
      std::set<int> ap_set;
124
125
126
127
128
129
130
131
132
      unsigned cur_state;
      int states = -1;
      int ap_count = -1;
      int accset = -1;
      bdd state_label;
      bdd cur_label;
      bool has_state_label = false;
      bool ignore_more_ap = false; // Set to true after the first "AP:"
      // line has been read.
133
134
      bool ignore_acc = false;	// Set to true in case of missing
				// Acceptance: lines.
135
136
      bool ignore_acc_silent = false;
      bool ignore_more_acc = false; // Set to true after the first
137
				// "Acceptance:" line has been read.
138
139

      label_style_t label_style = Mixed_Labels;
140
      acc_style_t acc_style = Mixed_Acc;
141
142
143
144
145

      bool accept_all_needed = false;
      bool accept_all_seen = false;
      bool aliased_states = false;

146
      spot::trival deterministic = spot::trival::maybe();
147
      bool complete = false;
148
      bool trans_acc_seen = false;
149
150
151

      std::map<std::string, spot::location> labels;

152
153
154
155
156
157
158
159
      prop_info prop_is_true(const std::string& p)
      {
	auto i = props.find(p);
	if (i == props.end())
	  return prop_info{spot::location(), false};
	return i->second;
      }

160
161
162
163
164
165
166
      ~result_()
      {
	delete namer;
	delete acc_mapper;
      }
    };
  }
167
168
169
}

%parse-param {result_& res}
170
171
%parse-param {spot::location initial_loc}

172
%initial-action { @$ = res.h->loc = initial_loc; }
173

174
175
176
177
178
179
%union
{
  std::string* str;
  unsigned int num;
  int b;
  spot::acc_cond::mark_t mark;
180
181
  pair* p;
  std::list<pair>* list;
182
  spot::acc_cond::acc_code* code;
183
184
185
186
187
}

%code
{
#include <sstream>
188

189
  /* parseaut.hh and parsedecl.hh include each other recursively.
190
191
   We must ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
192
#include <spot/parseaut/parsedecl.hh>
193
194

  static void fill_guards(result_& res);
195
196
}

197
/**** HOA tokens ****/
198
199
200
201
202
203
204
205
206
207
208
209
210
%token HOA "HOA:"
%token STATES "States:"
%token START "Start:"
%token AP "AP:"
%token ALIAS "Alias:"
%token ACCEPTANCE "Acceptance:"
%token ACCNAME "acc-name:"
%token TOOL "tool:"
%token NAME "name:"
%token PROPERTIES "properties:"
%token BODY "--BODY--"
%token END "--END--"
%token STATE "State:";
211
212
%token SPOT_HIGHLIGHT_EDGES "spot.highlight.edges:";
%token SPOT_HIGHLIGHT_STATES "spot.highlight.states:";
213
%token <str> IDENTIFIER "identifier";  // also used by neverclaim
214
215
216
217
%token <str> HEADERNAME "header name";
%token <str> ANAME "alias name";
%token <str> STRING "string";
%token <num> INT "integer";
218
%token ENDOFFILE 0 "end of file"
219

220
221
222
223
224
225
226
227
228
%token DRA "DRA"
%token DSA "DSA"
%token V2 "v2"
%token EXPLICIT "explicit"
%token ACCPAIRS "Acceptance-Pairs:"
%token ACCSIG "Acc-Sig:";
%token ENDOFHEADER "---";


229
230
231
232
%left '|'
%left '&'
%nonassoc '!'

233
%type <num> checked-state-num state-num acc-set sign
234
%type <b> label-expr
235
%type <mark> acc-sig acc-sets trans-acc_opt state-acc_opt
236
             dstar_accsigs dstar_state_accsig
237
%type <str> string_opt
238

239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
/**** NEVERCLAIM tokens ****/

%token NEVER "never"
%token SKIP "skip"
%token IF "if"
%token FI "fi"
%token DO "do"
%token OD "od"
%token ARROW "->"
%token GOTO "goto"
%token FALSE "false"
%token ATOMIC "atomic"
%token ASSERT "assert"
%token <str> FORMULA "boolean formula"

%type <b> nc-formula
%type <str> nc-opt-dest nc-formula-or-ident
%type <p> nc-transition nc-src-dest
%type <list> nc-transitions nc-transition-block
%type <str> nc-one-ident nc-ident-list
259
%type <code> acceptance-cond
260

261
262
263
/**** LBTT tokens *****/
 // Also using INT, STRING
%token ENDAUT "-1"
264
%token ENDDSTAR "end of DSTAR automaton"
265
266
267
268
269
270
271
%token <num> LBTT "LBTT header"
%token <num> INT_S "state acceptance"
%token <num> LBTT_EMPTY "acceptance sets for empty automaton"
%token <num> ACC "acceptance set"
%token <num> STATE_NUM "state number"
%token <num> DEST_NUM "destination number"
%type <mark> lbtt-acc
272

273
274
%destructor { delete $$; } <str>
%destructor { bdd_delref($$); } <b>
275
%destructor { bdd_delref($$->first); delete $$->second; delete $$; } <p>
276
%destructor { delete $$; } <code>
277
278
279
280
281
282
283
284
285
%destructor {
  for (std::list<pair>::iterator i = $$->begin();
       i != $$->end(); ++i)
  {
    bdd_delref(i->first);
    delete i->second;
  }
  delete $$;
  } <list>
286
287
288
289
290
291
292
293
%printer {
    if ($$)
      debug_stream() << *$$;
    else
      debug_stream() << "\"\""; } <str>
%printer { debug_stream() << $$; } <num>

%%
294
295
aut: aut-1     { res.h->loc = @$; YYACCEPT; }
   | ENDOFFILE { YYABORT; }
296
   | error ENDOFFILE { YYABORT; }
297
298
299
300
301
302
   | error aut-1
     {
       error(@1, "leading garbage was ignored");
       res.h->loc = @2;
       YYACCEPT;
     }
303

304
305
306
307
aut-1: hoa   { res.h->type = spot::parsed_aut_type::HOA; }
     | never { res.h->type = spot::parsed_aut_type::NeverClaim; }
     | lbtt  { res.h->type = spot::parsed_aut_type::LBTT; }
     | dstar /* will set type as DSA or DRA while parsing first line */
308
309
310
311
312

/**********************************************************************/
/*                          Rules for HOA                             */
/**********************************************************************/

313
hoa: header "--BODY--" body "--END--"
314
   | "HOA:" error "--END--"
315

316
317
string_opt: { $$ = nullptr; }
          | STRING { $$ = $1; }
318
319
320
321
BOOLEAN: 't' | 'f'

header: format-version header-items
        {
322
	  // Preallocate the states if we know their number.
323
	  if (res.states >= 0)
324
325
	    {
	      unsigned states = res.states;
326
327
328
329
330
331
332
333
	      for (auto& p : res.start)
		if ((unsigned) res.states <= p.second)
		  {
		    error(p.first,
			  "initial state number is larger than state count...");
		    error(res.states_loc, "... declared here.");
		    states = std::max(states, p.second + 1);
		  }
334
335
336
337
	      if (res.opts.want_kripke)
		res.h->ks->new_states(states, bddfalse);
	      else
		res.h->aut->new_states(states);
338
	      res.info_states.resize(states);
339
	    }
340
341
342
	  if (res.accset < 0)
	    {
	      error(@$, "missing 'Acceptance:' header");
343
	      res.ignore_acc = true;
344
	    }
345
346
	  // Process properties.
	  {
347
348
	    auto explicit_labels = res.prop_is_true("explicit-labels");
	    auto implicit_labels = res.prop_is_true("implicit-labels");
349

350
	    if (implicit_labels)
351
	      {
352
353
354
355
356
		if (res.opts.want_kripke)
		  error(implicit_labels.loc,
			"Kripke structure may not use implicit labels");

		if (explicit_labels)
357
		  {
358
		    error(implicit_labels.loc,
359
			  "'properties: implicit-labels' is incompatible "
360
			  "with...");
361
		    error(explicit_labels.loc,
362
			  "... 'properties: explicit-labels'.");
363
		  }
364
365
366
367
		else
		  {
		    res.label_style = Implicit_Labels;
		  }
368
369
	      }

370
371
	    auto trans_labels = res.prop_is_true("trans-labels");
	    auto state_labels = res.prop_is_true("state-labels");
372

373
	    if (trans_labels)
374
	      {
375
376
377
378
379
		if (res.opts.want_kripke)
		  error(trans_labels.loc,
			"Kripke structure may not use transition labels");

		if (state_labels)
380
		  {
381
382
383
384
		    error(trans_labels.loc,
			  "'properties: trans-labels' is incompatible with...");
		    error(state_labels.loc,
			  "... 'properties: state-labels'.");
385
386
387
		  }
		else
		  {
388
389
		    if (res.label_style != Implicit_Labels)
		      res.label_style = Trans_Labels;
390
391
		  }
	      }
392
	    else if (state_labels)
393
	      {
394
395
396
397
398
399
		if (res.label_style != Implicit_Labels)
		  {
		    res.label_style = State_Labels;
		  }
		else
		  {
400
		    error(state_labels.loc,
401
			  "'properties: state-labels' is incompatible with...");
402
		    error(implicit_labels.loc,
403
			  "... 'properties: implicit-labels'.");
404
		  }
405
	      }
406

407
408
409
410
	    if (res.opts.want_kripke && res.label_style != State_Labels)
	      error(@$,
		    "Kripke structure should use 'properties: state-labels'");

411
412
413
	    auto state_acc = res.prop_is_true("state-acc");
	    auto trans_acc = res.prop_is_true("trans-acc");
	    if (trans_acc)
414
	      {
415
		if (state_acc)
416
		  {
417
418
419
420
		    error(trans_acc.loc,
			  "'properties: trans-acc' is incompatible with...");
		    error(state_acc.loc,
			  "... 'properties: state-acc'.");
421
422
423
		  }
		else
		  {
424
		    res.acc_style = Trans_Acc;
425
426
		  }
	      }
427
	    else if (state_acc)
428
429
430
	      {
		res.acc_style = State_Acc;
	      }
431
	  }
432
433
	  {
	    unsigned ss = res.start.size();
434
	    auto det = res.prop_is_true("deterministic");
435
436
	    if (ss > 1)
	      {
437
		if (det)
438
		  {
439
		    error(det.loc,
440
441
442
443
444
445
446
447
			  "deterministic automata should have at most "
			  "one initial state");
		  }
		res.deterministic = false;
	      }
	    else
	      {
		// Assume the automaton is deterministic until proven
448
449
		// wrong, or unless we are building a Kripke structure.
		res.deterministic = !res.opts.want_kripke;
450
	      }
451
	    auto complete = res.prop_is_true("complete");
452
453
	    if (ss < 1)
	      {
454
		if (complete)
455
		  {
456
		    error(complete.loc,
457
458
459
460
461
462
463
464
465
			  "complete automata should have at least "
			  "one initial state");
		  }
		res.complete = false;
	      }
	    else
	      {
		// Assume the automaton is complete until proven
		// wrong.
466
		res.complete = !res.opts.want_kripke;
467
	      }
468
469
470
	    // if ap_count == 0, then a Kripke structure could be
	    // declared complete, although that probably doesn't
	    // matter.
471
472
	    if (res.opts.want_kripke && complete && res.ap_count > 0)
	      error(complete.loc,
473
		    "Kripke structure may not be complete");
474
	  }
475
476
	  if (res.opts.trust_hoa)
	    {
477
	      auto& a = res.aut_or_ks;
478
479
	      auto& p = res.props;
	      auto e = p.end();
480
481
	      auto si = p.find("stutter-invariant");
	      if (si != e)
482
		{
483
		  a->prop_stutter_invariant(si->second.val);
484
		  auto i = p.find("stutter-sensitive");
485
486
		  if (i != e && si->second.val == i->second.val)
		    error(i->second.loc,
487
488
489
			  "automaton cannot be both stutter-invariant"
			  "and stutter-sensitive");
		}
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
	      else
		{
		  auto ss = p.find("stutter-sensitive");
		  if (ss != e)
		    a->prop_stutter_invariant(!ss->second.val);
		}
	      auto iw = p.find("inherently-weak");
	      auto w = p.find("weak");
	      auto t = p.find("terminal");
	      if (iw != e)
		{
		  a->prop_inherently_weak(iw->second.val);
		  if (w != e && !iw->second.val && w->second.val)
		    {
		      error(w->second.loc, "'properties: weak' contradicts...");
		      error(iw->second.loc,
			    "... 'properties: !inherently-weak' given here");
		    }
		  if (t != e && !iw->second.val && t->second.val)
		    {
		      error(t->second.loc,
			    "'properties: terminal' contradicts...");
		      error(iw->second.loc,
			    "... 'properties: !inherently-weak' given here");
		    }
		}
	      if (w != e)
		{
		  a->prop_weak(w->second.val);
		  if (t != e && !w->second.val && t->second.val)
		    {
		      error(t->second.loc,
			    "'properties: terminal' contradicts...");
		      error(w->second.loc,
			    "... 'properties: !weak' given here");
		    }
		}
	      if (t != e)
		a->prop_terminal(t->second.val);
	      auto u = p.find("unambiguous");
	      if (u != e)
		{
		  a->prop_unambiguous(u->second.val);
		  auto d = p.find("deterministic");
		  if (d != e && !u->second.val && d->second.val)
		    {
		      error(d->second.loc,
			    "'properties: deterministic' contradicts...");
		      error(u->second.loc,
			    "... 'properties: !unambiguous' given here");
		    }
		}
542
	    }
543
544
	}

545
546
version: IDENTIFIER
         {
547
548
	   res.format_version = *$1;
	   res.format_version_loc = @1;
549
550
551
552
	   delete $1;
	 }

format-version: "HOA:" { res.h->loc = @1; } version
553

554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
aps: "AP:" INT
     {
       if (res.ignore_more_ap)
	 {
	   error(@1, "ignoring this redeclaration of APs...");
	   error(res.ap_loc, "... previously declared here.");
	 }
       else
	 {
	   res.ap_count = $2;
	   res.ap.reserve($2);
	 }
     }
     ap-names
     {
       if (!res.ignore_more_ap)
	 {
	   res.ap_loc = @1 + @2;
	   if ((int) res.ap.size() != res.ap_count)
573
	     {
574
575
576
577
578
	       std::ostringstream out;
	       out << "found " << res.ap.size()
		   << " atomic propositions instead of the "
		   << res.ap_count << " announced";
	       error(@$, out.str());
579
	     }
580
581
582
	   res.ignore_more_ap = true;
	 }
     }
583

584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
header-items: | header-items header-item
header-item: "States:" INT
           {
	     if (res.states >= 0)
	       {
		 error(@$, "redefinition of the number of states...");
		 error(res.states_loc, "... previously defined here.");
	       }
	     else
	       {
		 res.states_loc = @$;
	       }
	     if (((int) $2) < 0)
	       {
		 error(@$, "too many states for this implementation");
		 YYABORT;
	       }
	     res.states = std::max(res.states, (int) $2);
	   }
603
           | "Start:" init-state-conj-2
604
605
606
607
608
609
	     {
	       error(@2, "alternation is not yet supported");
	       YYABORT;
	     }
           | "Start:" state-num
	     {
610
	       res.start.emplace_back(@$, $2);
611
	     }
612
           | aps
613
614
           | "Alias:" ANAME label-expr
             {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
615
616
617
618
619
620
	       if (!res.alias.emplace(*$2, bdd_from_int($3)).second)
		 {
		   std::ostringstream o;
		   o << "ignoring redefinition of alias @" << *$2;
		   error(@$, o.str());
		 }
621
622
623
624
625
	       delete $2;
	       bdd_delref($3);
	     }
           | "Acceptance:" INT
	      {
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
		if (res.ignore_more_acc)
		  {
		    error(@1 + @2, "ignoring this redefinition of the "
			  "acceptance condition...");
		    error(res.accset_loc, "... previously defined here.");
		  }
		else if ($2 > 8 * sizeof(spot::acc_cond::mark_t::value_t))
		  {
		    error(@1 + @2,
			  "this implementation cannot support such a large "
			  "number of acceptance sets");
		    YYABORT;
		  }
		else
		  {
641
		    res.aut_or_ks->acc().add_sets($2);
642
643
644
		    res.accset = $2;
		    res.accset_loc = @1 + @2;
		  }
645
646
	     }
             acceptance-cond
647
648
	     {
	       res.ignore_more_acc = true;
649
650
	       // Not setting the acceptance in case of error will
	       // force it to be true.
651
	       if (res.opts.want_kripke && (!$4->is_t() || $2 > 0))
652
653
654
655
		 error(@2 + @4,
		       "the acceptance for Kripke structure must be '0 t'");
	       else
		 res.aut_or_ks->set_acceptance($2, *$4);
656
	       delete $4;
657
	     }
658
659
660
661
662
663
664
           | "acc-name:" IDENTIFIER acc-spec
             {
	       delete $2;
	     }
           | "tool:" STRING string_opt
             {
	       delete $2;
665
	       delete $3;
666
667
668
	     }
           | "name:" STRING
             {
669
	       res.aut_or_ks->set_named_prop("automaton-name", $2);
670
671
	     }
           | "properties:" properties
672
673
674
675
676
677
	   | "spot.highlight.edges:"
	     { res.highlight_edges = new std::map<unsigned, unsigned>; }
             highlight-edges
	   | "spot.highlight.states:"
	     { res.highlight_states = new std::map<unsigned, unsigned>; }
             highlight-states
678
           | HEADERNAME header-spec
679
680
681
682
683
684
685
686
	     {
	       char c = (*$1)[0];
	       if (c >= 'A' && c <= 'Z')
		 error(@$, "ignoring unsupported header \"" + *$1 + ":\"\n\t"
		       "(but the capital indicates information that should not"
		       " be ignored)");
	       delete $1;
	     }
687
           | error
688
689
690
691

ap-names: | ap-names ap-name
ap-name: STRING
	 {
692
	   if (!res.ignore_more_ap)
693
	     {
694
	       auto f = res.env->require(*$1);
695
	       int b = 0;
696
697
698
699
700
	       if (f == nullptr)
		 {
		   std::ostringstream out;
		   out << "unknown atomic proposition \"" << *$1 << "\"";
		   error(@1, out.str());
701
		   b = res.aut_or_ks->register_ap("$unknown$");
702
703
704
		 }
	       else
		 {
705
		   b = res.aut_or_ks->register_ap(f);
706
707
708
709
710
711
		   if (!res.ap_set.emplace(b).second)
		     {
		       std::ostringstream out;
		       out << "duplicate atomic proposition \"" << *$1 << "\"";
		       error(@1, out.str());
		     }
712
713
		 }
	       res.ap.push_back(b);
714
715
716
717
718
719
720
721
722
723
724
725
	     }
	   delete $1;
	 }

acc-spec: | acc-spec BOOLEAN
	  | acc-spec INT
	  | acc-spec IDENTIFIER
            {
	      delete $2;
	    }
properties: | properties IDENTIFIER
	      {
726
727
728
729
730
731
732
733
734
735
		auto pos = res.props.emplace(*$2, result_::prop_info{@2, true});
		if (!pos.first->second.val)
		  {
		    std::ostringstream out(std::ios_base::ate);
		    error(@2, std::string("'properties: ")
			  + *$2 + "' contradicts...");
		    error(pos.first->second.loc,
			  std::string("... 'properties: !") + *$2
			  + "' previously given here.");
		  }
736
737
		delete $2;
	      }
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
            | properties '!' IDENTIFIER
	      {
		auto loc = @2 + @3;
		auto pos =
		  res.props.emplace(*$3, result_::prop_info{loc, false});
		if (pos.first->second.val)
		  {
		    std::ostringstream out(std::ios_base::ate);
		    error(loc, std::string("'properties: !")
			  + *$3 + "' contradicts...");
		    error(pos.first->second.loc,
			  std::string("... 'properties: ") + *$3
			  + "' previously given here.");
		  }
		delete $3;
	      }
754
755
756
757
758
759
760
761
762
763

highlight-edges: | highlight-edges INT INT
              {
		res.highlight_edges->emplace($2, $3);
	      }
highlight-states: | highlight-states INT INT
              {
		res.highlight_states->emplace($2, $3);
	      }

764
765
766
767
768
769
770
771
772
773
774
header-spec: | header-spec BOOLEAN
             | header-spec INT
             | header-spec STRING
	       {
		 delete $2;
	       }
             | header-spec IDENTIFIER
	       {
		 delete $2;
	       }

775
776
state-conj-2: checked-state-num '&' checked-state-num
            | state-conj-2 '&' checked-state-num
777

778
779
780
781
782
	      // Currently we do not check the number of these states
	      // since we do not support alternation.
init-state-conj-2: state-num '&' state-num
            | init-state-conj-2 '&' state-num

783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
label-expr: 't'
	    {
	      $$ = bddtrue.id();
	    }
          | 'f'
	    {
	      $$ = bddfalse.id();
	    }
	  | INT
	    {
	      if ($1 >= res.ap.size())
		{
		  error(@1, "AP number is larger than the number of APs...");
		  error(res.ap_loc, "... declared here");
		  $$ = bddtrue.id();
		}
	      else
		{
		  $$ = bdd_ithvar(res.ap[$1]).id();
		  bdd_addref($$);
		}
	    }
          | ANAME
	    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
807
808
809
810
811
812
813
814
815
816
817
	      auto i = res.alias.find(*$1);
	      if (i == res.alias.end())
		{
		  error(@$, "unknown alias @" + *$1);
		  $$ = 1;
		}
	      else
		{
		  $$ = i->second.id();
		  bdd_addref($$);
		}
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
	      delete $1;
	    }
          | '!' label-expr
	    {
              $$ = bdd_not($2);
              bdd_delref($2);
              bdd_addref($$);
            }
          | label-expr '&' label-expr
	    {
              $$ = bdd_and($1, $3);
              bdd_delref($1);
              bdd_delref($3);
              bdd_addref($$);
            }
          | label-expr '|' label-expr
	    {
              $$ = bdd_or($1, $3);
              bdd_delref($1);
              bdd_delref($3);
              bdd_addref($$);
            }
840
841
842
843
          | '(' label-expr ')'
	  {
	    $$ = $2;
	  }
844
845
846
847
848
849


acc-set: INT
            {
	      if ((int) $1 >= res.accset)
		{
850
851
852
853
854
855
856
857
858
859
860
		  if (!res.ignore_acc)
		    {
		      error(@1, "number is larger than the count "
			    "of acceptance sets...");
		      error(res.accset_loc, "... declared here.");
		    }
		  $$ = -1U;
		}
	      else
		{
		  $$ = $1;
861
862
863
864
865
		}
	    }

acceptance-cond: IDENTIFIER '(' acc-set ')'
		 {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
866
		   if ($3 != -1U)
867
		     {
868
		       res.pos_acc_sets |= res.aut_or_ks->acc().mark($3);
869
870
		       if (*$1 == "Inf")
			 $$ = new spot::acc_cond::acc_code
871
			   (res.aut_or_ks->acc().inf({$3}));
872
873
		       else
			 $$ = new spot::acc_cond::acc_code
874
			   (res.aut_or_ks->acc().fin({$3}));
875
876
877
878
879
		     }
		   else
		     {
		       $$ = new spot::acc_cond::acc_code;
		     }
880
881
882
883
		   delete $1;
		 }
               | IDENTIFIER '(' '!' acc-set ')'
		 {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
884
		   if ($4 != -1U)
885
		     {
886
		       res.neg_acc_sets |= res.aut_or_ks->acc().mark($4);
887
888
		       if (*$1 == "Inf")
			 $$ = new spot::acc_cond::acc_code
889
			   (res.aut_or_ks->acc().inf_neg({$4}));
890
891
		       else
			 $$ = new spot::acc_cond::acc_code
892
			   (res.aut_or_ks->acc().fin_neg({$4}));
893
894
895
896
897
		     }
		   else
		     {
		       $$ = new spot::acc_cond::acc_code;
		     }
898
899
900
		   delete $1;
		 }
               | '(' acceptance-cond ')'
901
902
903
	         {
		   $$ = $2;
		 }
904
               | acceptance-cond '&' acceptance-cond
905
	         {
906
		   *$3 &= std::move(*$1);
907
908
909
		   $$ = $3;
		   delete $1;
		 }
910
911
               | acceptance-cond '|' acceptance-cond
	         {
912
		   *$3 |= std::move(*$1);
913
914
		   $$ = $3;
		   delete $1;
915
		 }
916
               | 't'
917
918
919
	         {
		   $$ = new spot::acc_cond::acc_code;
		 }
920
921
	       | 'f'
	       {
922
	         {
923
924
		   $$ = new spot::acc_cond::acc_code
		     (res.aut_or_ks->acc().fin({}));
925
		 }
926
	       }
927
928
929


body: states
930
931
      {
	for (auto& p: res.start)
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
	  if (p.second >= res.info_states.size()
	      || !res.info_states[p.second].declared)
	    {
	      error(p.first,
		    "initial state " + std::to_string(p.second) +
		    " has no definition");
	      // Pretend that the state is declared so we do not
	      // mention it in the next loop.
	      if (p.second < res.info_states.size())
		res.info_states[p.second].declared = true;
	    }
	unsigned n = res.info_states.size();
	// States with number above res.states have already caused a
	// diagnostic, so let not add another one.
	if (res.states >= 0)
	  n = res.states;
	for (unsigned i = 0; i < n; ++i)
	  {
	    auto& p = res.info_states[i];
	    if (p.used && !p.declared)
	      error(p.used_loc,
		    "state " + std::to_string(i) + " has no definition");
	  }
955
      }
956
957
958
959
960
961
962
963
964
965
966

state-num: INT
	   {
	     if (((int) $1) < 0)
	       {
		 error(@1, "state number is too large for this implementation");
		 YYABORT;
	       }
	     $$ = $1;
	   }

967
968
969
970
971
972
973
974
975
976
checked-state-num: state-num
		   {
		     if ((int) $1 >= res.states)
		       {
			 if (res.states >= 0)
			   {
			     error(@1, "state number is larger than state "
				   "count...");
			     error(res.states_loc, "... declared here.");
			   }
977
			 if (res.opts.want_kripke)
978
			   {
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
			     int missing =
			       ((int) $1) - res.h->ks->num_states() + 1;
			     if (missing >= 0)
			       {
				 res.h->ks->new_states(missing, bddfalse);
				 res.info_states.resize
				   (res.info_states.size() + missing);
			       }
			   }
			 else
			   {
			     int missing =
			       ((int) $1) - res.h->aut->num_states() + 1;
			     if (missing >= 0)
			       {
				 res.h->aut->new_states(missing);
				 res.info_states.resize
				   (res.info_states.size() + missing);
			       }
998
999
			   }
		       }
1000
1001
1002
1003
1004
1005
1006
		     // Remember the first place were a state is the
		     // destination of a transition.
		     if (!res.info_states[$1].used)
		       {
			 res.info_states[$1].used = true;
			 res.info_states[$1].used_loc = @1;
		       }
1007
1008
1009
		     $$ = $1;
		   }

1010
states: | states state
1011
        {
1012
	  if ((res.deterministic || res.complete) && !res.opts.want_kripke)
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
	    {
	      bdd available = bddtrue;
	      bool det = true;
	      for (auto& t: res.h->aut->out(res.cur_state))
		{
		  if (det && !bdd_implies(t.cond, available))
		    det = false;
		  available -= t.cond;
		}
	      if (res.deterministic && !det)
		{
		  res.deterministic = false;
1025
		  if (auto p = res.prop_is_true("deterministic"))
1026
1027
		    {
		      error(@2, "automaton is not deterministic...");
1028
		      error(p.loc,
1029
			    "... despite 'properties: deterministic'");
1030
1031
1032
1033
1034
		    }
		}
	      if (res.complete && available != bddfalse)
		{
		  res.complete = false;
1035
		  if (auto p = res.prop_is_true("complete"))
1036
1037
		    {
		      error(@2, "automaton is not complete...");
1038
		      error(p.loc, "... despite 'properties: complete'");
1039
1040
1041
1042
		    }
		}
	    }
	}
1043
1044
1045
state: state-name labeled-edges
     | state-name unlabeled-edges
       {
1046
	 if (!res.has_state_label) // Implicit labels
1047
1048
1049
	   {
	     if (res.cur_guard != res.guards.end())
	       error(@$, "not enough transitions for this state");
1050
1051
1052
1053
1054

	     if (res.label_style == State_Labels)
	       {
		 error(@2, "these transitions have implicit labels but the"
		       " automaton is...");
1055
		 error(res.props["state-labels"].loc, "... declared with "
1056
		       "'properties: state-labels'");
1057
1058
1059
		 // Do not repeat this message.
		 res.label_style = Mixed_Labels;
	       }
1060
1061
	     res.cur_guard = res.guards.begin();
	   }
1062
1063
1064
1065
1066
	 else if (res.opts.want_kripke)
	   {
	     res.h->ks->state_from_number(res.cur_state)->cond(res.state_label);
	   }

1067
       }
1068
     | error
1069
       {
1070
1071
1072
	 // Assume the worse.  This skips the tests about determinism
	 // we might perform on the state.
	 res.deterministic = spot::trival::maybe();
1073
1074
	 res.complete = false;
       }
1075

1076

1077
state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt
1078
1079
	  {
	    res.cur_state = $3;
1080
	    if (res.info_states[$3].declared)
1081
1082
1083
1084
1085
	      {
		std::ostringstream o;
		o << "redeclaration of state " << $3;
		error(@1 + @3, o.str());
	      }
1086
	    res.info_states[$3].declared = true;
1087
	    res.acc_state = $5;
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
	    if ($4)
	      {
		if (!res.state_names)
		  res.state_names =
		    new std::vector<std::string>(res.states > 0 ?
						 res.states : 0);
		if (res.state_names->size() < $3 + 1)
		  res.state_names->resize($3 + 1);
		(*res.state_names)[$3] = std::move(*$4);
		delete $4;
	      }
1099
1100
	    if (res.opts.want_kripke && !res.has_state_label)
	      error(@$, "Kripke structures should have labeled states");
1101
1102
1103
1104
1105
1106
	  }
label: '[' label-expr ']'
	   {
             res.cur_label = bdd_from_int($2);
             bdd_delref($2);
	   }
1107
1108
1109
1110
1111
     | '[' error ']'
           {
	     error(@$, "ignoring this invalid label");
	     res.cur_label = bddtrue;
	   }
1112
state-label_opt:       { res.has_state_label = false; }
1113
1114
1115
1116
1117
               | label
	       {
		 res.has_state_label = true;
		 res.state_label_loc = @1;
		 res.state_label = res.cur_label;
1118
1119
		 if (res.label_style == Trans_Labels
		     || res.label_style == Implicit_Labels)
1120
1121
1122
		   {
		     error(@$,
			   "state label used although the automaton was...");
1123
		     if (res.label_style == Trans_Labels)
1124
		       error(res.props["trans-labels"].loc,
1125
1126
			     "... declared with 'properties: trans-labels'"
			     " here");
1127
		     else
1128
		       error(res.props["implicit-labels"].loc,
1129
1130
			     "... declared with 'properties: implicit-labels'"
			     " here");
1131
1132
1133
1134
		     // Do not show this error anymore.
		     res.label_style = Mixed_Labels;
		   }
	       }
1135
trans-label: label
1136
1137
1138
	         {
		   if (res.has_state_label)
		     {
1139
		       error(@1, "cannot label this edge because...");
1140
1141
		       error(res.state_label_loc,
			     "... the state is already labeled.");
1142
		       res.cur_label = res.state_label;
1143
		     }
1144
1145
		   if (res.label_style == State_Labels
		       || res.label_style == Implicit_Labels)
1146
1147
1148
		     {
		       error(@$, "transition label used although the "
			     "automaton was...");
1149
		       if (res.label_style == State_Labels)
1150
			 error(res.props["state-labels"].loc,
1151
			       "... declared with 'properties: state-labels' "
1152
1153
			       "here");
		       else
1154
			 error(res.props["implicit-labels"].loc,
1155
1156
			       "... declared with 'properties: implicit-labels'"
			       " here");
1157
1158
1159
		       // Do not show this error anymore.
		       res.label_style = Mixed_Labels;
		     }
1160
1161
		 }

1162
acc-sig: '{' acc-sets '}'
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
	     {
	       $$ = $2;
	       if (res.ignore_acc && !res.ignore_acc_silent)
		 {
		   error(@$, "ignoring acceptance sets because of "
			 "missing acceptance condition");
		   // Emit this message only once.
		   res.ignore_acc_silent = true;
		 }
	     }
1173
1174
1175
1176
           | '{' error '}'
	     {
	       error(@$, "ignoring this invalid acceptance set");
	     }
1177
1178
1179
1180
acc-sets:
          {
	    $$ = spot::acc_cond::mark_t(0U);
	  }
1181
1182
        | acc-sets acc-set
	  {
1183
1184
1185
	    if (res.ignore_acc || $2 == -1U)
	      $$ = spot::acc_cond::mark_t(0U);
	    else
1186
	      $$ = $1 | res.aut_or_ks->acc().mark($2);
1187
	  }
1188

1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
state-acc_opt:
               {
                 $$ = spot::acc_cond::mark_t(0U);
               }
             | acc-sig
               {
		 $$ = $1;
		 if (res.acc_style == Trans_Acc)
		   {
		     error(@$, "state-based acceptance used despite...");
1199
		     error(res.props["trans-acc"].loc,
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
			   "... declaration of transition-based acceptance.");
		     res.acc_style = Mixed_Acc;
		   }
	       }
trans-acc_opt:
               {
                 $$ = spot::acc_cond::mark_t(0U);
               }
             | acc-sig
               {
		 $$ = $1;
		 res.trans_acc_seen = true;
		 if (res.acc_style == State_Acc)
		   {
		     error(@$, "trans-based acceptance used despite...");
1215
		     error(res.props["state-acc"].loc,
1216
1217
1218
1219
1220
			   "... declaration of state-based acceptance.");
		     res.acc_style = Mixed_Acc;
		   }
	       }

1221
1222
1223
1224
1225
/* block of labeled-edges, with occasional (incorrect) unlabeled edge */
labeled-edges: | some-labeled-edges
some-labeled-edges: labeled-edge
                  | some-labeled-edges labeled-edge
                  | some-labeled-edges incorrectly-unlabeled-edge
1226
incorrectly-unlabeled-edge: checked-state-num trans-acc_opt
1227
1228
1229
1230
1231
1232
1233
                            {
			      bdd cond = bddtrue;
			      if (!res.has_state_label)
				error(@$, "missing label for this edge "
				      "(previous edge is labeled)");
			      else
				cond = res.state_label;
1234
1235
1236
1237
1238
1239
1240
1241
1242
			      if (cond != bddfalse)
				{
				  if (res.opts.want_kripke)
				    res.h->ks->new_edge(res.cur_state, $1);
				  else
				    res.h->aut->new_edge(res.cur_state, $1,
							 cond,
							 $2 | res.acc_state);
				}
1243
			    }
1244
labeled-edge: trans-label checked-state-num trans-acc_opt
1245
	      {
1246
		if (res.cur_label != bddfalse)
1247
1248
1249
1250
1251
1252
1253
		  {
		    if (res.opts.want_kripke)
		      res.h->ks->new_edge(res.cur_state, $2);
		    else
		      res.h->aut->new_edge(res.cur_state, $2,
					   res.cur_label, $3 | res.acc_state);
		  }
1254
	      }
1255
	    | trans-label state-conj-2 trans-acc_opt
1256
1257
1258
1259
1260
	      {
		error(@2, "alternation is not yet supported");
		YYABORT;
	      }

1261
1262
1263
1264
1265
1266
/* Block of unlabeled edge, with occasional (incorrect) labeled
   edge. We never have zero unlabeled edges, these are considered as
   zero labeled edges. */
unlabeled-edges: unlabeled-edge
               | unlabeled-edges unlabeled-edge
               | unlabeled-edges incorrectly-labeled-edge
1267
unlabeled-edge: checked-state-num trans-acc_opt
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
		{
		  bdd cond;
		  if (res.has_state_label)
		    {
		      cond = res.state_label;
		    }
		  else
		    {
		      if (res.guards.empty())
			fill_guards(res);
		      if (res.cur_guard == res.guards.end())
			{
1280
			  error(@$, "too many transitions for this state, "
1281
1282
1283
1284
1285
1286
1287
1288
				"ignoring this one");
			  cond = bddfalse;
			}
		      else
			{
			  cond = *res.cur_guard++;
			}
		    }
1289
		  if (cond != bddfalse)
1290
1291
1292
1293
1294
1295
1296
		    {
		      if (res.opts.want_kripke)
			res.h->ks->new_edge(res.cur_state, $1);
		      else
			res.h->aut->new_edge(res.cur_state, $1,
					     cond, $2 | res.acc_state);
		    }
1297
		}
1298
	      | state-conj-2 trans-acc_opt
1299
1300
1301
1302
		{
		  error(@1, "alternation is not yet supported");
		  YYABORT;
		}
1303
1304
1305
1306
1307
incorrectly-labeled-edge: trans-label unlabeled-edge
                          {
			    error(@1, "ignoring this label, because previous"
				  " edge has no label");
                          }
1308

1309
1310
1311
1312
1313

/**********************************************************************/
/*                   Rules for LTL2DSTAR's format                     */
/**********************************************************************/

1314
1315
1316
1317
1318
dstar: dstar_type "v2" "explicit" dstar_header "---" dstar_states ENDDSTAR
     | dstar_type error ENDDSTAR
       {
	 error(@$, "failed to parse this as an ltl2dstar automaton");
       }
1319
1320
1321
1322
1323
1324

dstar_type: "DRA"
       {
         res.h->type = spot::parsed_aut_type::DRA;
         res.plus = 1;
         res.minus = 0;
1325
1326
1327
1328
1329
1330
	 if (res.opts.want_kripke)
	   {
	     error(@$,
		   "cannot read a Kripke structure out of a DSTAR automaton");
	     YYABORT;
	   }
1331
1332
1333
1334
1335
1336
       }
       | "DSA"
       {
	 res.h->type = spot::parsed_aut_type::DSA;
         res.plus = 0;
         res.minus = 1;
1337
1338
1339
1340
1341
1342
	 if (res.opts.want_kripke)
	   {
	     error(@$,
		   "cannot read a Kripke structure out of a DSTAR automaton");
	     YYABORT;
	   }
1343
1344
       }

1345
dstar_header: dstar_sizes
1346
1347
  {
    if (res.states < 0)
1348
      error(@1, "missing state count");
1349
    if (!res.ignore_more_acc)
1350
      error(@1, "missing acceptance-pair count");
1351
    if (res.start.empty())
1352
      error(@1, "missing start-state number");
1353
    if (!res.ignore_more_ap)
1354
1355
1356
      error(@1, "missing atomic propositions definition");

    if (res.states > 0)
1357
      {
1358
1359
	res.h->aut->new_states(res.states);;
	res.info_states.resize(res.states);
1360
      }
1361
1362
    res.acc_style = State_Acc;
    res.deterministic = true;
1363
    // res.h->aut->prop_complete();
1364
1365
    fill_guards(res);
    res.cur_guard = res.guards.end();
1366
1367
1368
  }

dstar_sizes:
1369
  | dstar_sizes error
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
  | dstar_sizes "Acceptance-Pairs:" INT
  {
    if (res.ignore_more_acc)
      {
	error(@1 + @2, "ignoring this redefinition of the "
	      "acceptance pairs...");
	error(res.accset_loc, "... previously defined here.");
      }
    else{
      res.accset = $3;
      res.h->aut->set_acceptance(2 * $3,
				 res.h->type == spot::parsed_aut_type::DRA
				 ? spot::acc_cond::acc_code::rabin($3)
				 : spot::acc_cond::acc_code::streett($3));
      res.accset_loc = @3;
      res.ignore_more_acc = true;
    }
  }
  | dstar_sizes "States:" INT
  {
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
    if (res.states < 0)
      {
	res.states = $3;
      }
    else
      {
	error(@$, "redeclaration of state count");
	if ((unsigned) res.states < $3)
	  res.states = $3;
      }
1400
1401
1402
1403
1404
1405
1406
  }
  | dstar_sizes "Start:" INT
  {
    res.start.emplace_back(@3, $3);
  }
  | dstar_sizes aps

1407
dstar_state_id: "State:" INT string_opt
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
  {
    if (res.cur_guard != res.guards.end())
      error(@1, "not enough transitions for previous state");
    if (res.states < 0 || $2 >= (unsigned) res.states)
      {
	std::ostringstream o;
	if (res.states > 0)
	  {
	    o << "state numbers should be in the range [0.."
	      << res.states - 1 << "]";
	  }
	else
	  {
	    o << "no states have been declared";
	  }
	error(@2, o.str());
      }
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
    else
      {
	res.info_states[$2].declared = true;

	if ($3)
	  {
	    if (!res.state_names)
	      res.state_names =
		new std::vector<std::string>(res.states > 0 ?
					     res.states : 0);
	    if (res.state_names->size() < $2 + 1)
	      res.state_names->resize($2 + 1);
	    (*res.state_names)[$2] = std::move(*$3);
	    delete $3;
	  }
      }

1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
    res.cur_guard = res.guards.begin();
    res.dest_map.clear();
    res.cur_state = $2;
  }

sign: '+' { $$ = res.plus; }
  |   '-' { $$ = res.minus; }

// Membership to a pair is represented as (+NUM,-NUM)
dstar_accsigs:
  {
    $$ = 0U;
  }
  | dstar_accsigs sign INT
  {
    if (res.states < 0 || res.cur_state >= (unsigned) res.states)
      break;
    if (res.accset > 0 && $3 < (unsigned) res.accset)
      {
	$$ = $1;
	$$.set($3 * 2 + $2);
      }
    else
      {
	std::ostringstream o;
	if (res.accset > 0)
	  {
	    o << "acceptance pairs should be in the range [0.."
	      << res.accset - 1 << "]";
	  }
	else
	  {
	    o << "no acceptance pairs have been declared";
	  }
	error(@3, o.str());
      }
  }

dstar_state_accsig: "Acc-Sig:" dstar_accsigs { $$ = $2; }

dstar_transitions:
  | dstar_transitions INT
  {