hoaparse.yy 25.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
/* -*- coding: utf-8 -*-
** Copyright (C) 2014 Laboratoire de Recherche et Développement
** de l'Epita (LRDE).
**
** 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
%lex-param { spot::hoa_parse_error_list& error_list }
%define api.location.type "spot::location"

%code requires
{
#include <string>
#include <cstring>
#include <sstream>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
35
#include <unordered_map>
36
#include <algorithm>
37
#include "ltlast/constant.hh"
38
#include "tgba/formula2bdd.hh"
39
40
#include "public.hh"

41
42
43
44
45
46
47
48
49
  /* Cache parsed formulae.  Labels on arcs are frequently identical
   and it would be a waste of time to parse them to formula* over and
   over, and to register all their atomic_propositions in the
   bdd_dict.  Keep the bdd result around so we can reuse it.  */
  typedef std::map<std::string, bdd> formula_cache;

  typedef std::pair<int, std::string*> pair;
  typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;

50
51
52
53
54
  // 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.
55
56
57
58
  struct result_
  {
    spot::hoa_aut_ptr h;
    spot::ltl::environment* env;
59
60
    formula_cache fcache;
    named_tgba_t* namer = nullptr;
61
    std::vector<int> ap;
62
63
    std::vector<bdd> guards;
    std::vector<bdd>::const_iterator cur_guard;
64
    std::vector<bool> declared_states; // States that have been declared.
65
    std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
66
    std::unordered_map<std::string, bdd> alias;
67
68
69
70
    spot::location states_loc;
    spot::location ap_loc;
    spot::location state_label_loc;
    spot::location accset_loc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
71
72
73
    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;
74
75
76
77
78
79
80
    unsigned cur_state;
    int states = -1;
    int ap_count = -1;
    int accset = -1;
    bdd state_label;
    bdd cur_label;
    bool has_state_label = false;
81
82
83
84
85
86
87
    bool ignore_more_ap = false; // Set to true after the first "AP:"
				 // line has been read.
    bool ignore_acc = false; // Set to true in case of missing
			     // Acceptance: lines.
    bool ignore_acc_silent = false;
    bool ignore_more_acc = false; // Set to true after the first
				  // "Acceptance:" line has been read.
88
89
90

    bool accept_all_needed = false;
    bool accept_all_seen = false;
91
    bool aliased_states = false;
92
93
94
95
96
97
    std::map<std::string, spot::location> labels;

    ~result_()
    {
      delete namer;
    }
98
99
100
101
102
  };
}

%parse-param {spot::hoa_parse_error_list& error_list}
%parse-param {result_& res}
103
104
%parse-param {spot::location initial_loc}

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

107
108
109
110
111
112
%union
{
  std::string* str;
  unsigned int num;
  int b;
  spot::acc_cond::mark_t mark;
113
114
  pair* p;
  std::list<pair>* list;
115
116
117
118
119
}

%code
{
#include <sstream>
120
121
122
123
#include "ltlast/constant.hh"
#include "ltlparse/public.hh"

  /* hoaparse.hh and parsedecl.hh include each other recursively.
124
125
126
   We must ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
127
128

  static void fill_guards(result_& res);
129
130
}

131
/**** HOA tokens ****/
132
133
134
135
136
137
138
139
140
141
142
143
144
%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:";
145
%token <str> IDENTIFIER "identifier";  // also used by neverclaim
146
147
148
149
%token <str> HEADERNAME "header name";
%token <str> ANAME "alias name";
%token <str> STRING "string";
%token <num> INT "integer";
150
%token ENDOFFILE 0 "end of file"
151
152
153
154
155

%left '|'
%left '&'
%nonassoc '!'

156
%type <num> checked-state-num state-num acc-set
157
158
159
%type <b> label-expr
%type <mark> acc-sig_opt acc-sets

160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
/**** 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




184
185
%destructor { delete $$; } <str>
%destructor { bdd_delref($$); } <b>
186
187
188
189
190
191
192
193
194
195
%destructor { bdd_delref($$->first); delete $$->second; delete $$; } <p>
%destructor {
  for (std::list<pair>::iterator i = $$->begin();
       i != $$->end(); ++i)
  {
    bdd_delref(i->first);
    delete i->second;
  }
  delete $$;
  } <list>
196
197
198
199
200
201
202
203
%printer {
    if ($$)
      debug_stream() << *$$;
    else
      debug_stream() << "\"\""; } <str>
%printer { debug_stream() << $$; } <num>

%%
204
205
aut: aut-1     { res.h->loc = @$; YYACCEPT; }
   | ENDOFFILE { YYABORT; }
206
207
208
209
   | error ENDOFFILE { YYABORT; }

aut-1: hoa
     | never
210
211
212
213
214
215


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

216
hoa: header "--BODY--" body "--END--"
217
hoa: error "--END--"
218
219
220
221
222
223

string_opt: | STRING
BOOLEAN: 't' | 'f'

header: format-version header-items
        {
224
	  // Preallocate the states if we know their number.
225
	  if (res.states >= 0)
226
227
	    {
	      unsigned states = res.states;
228
229
230
231
232
233
234
235
	      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);
		  }
236
237
238
	      res.h->aut->new_states(states);
	      res.declared_states.resize(states);
	    }
239
240
241
	  if (res.accset < 0)
	    {
	      error(@$, "missing 'Acceptance:' header");
242
	      res.ignore_acc = true;
243
244
245
	    }
	}

246
247
248
249
250
251
252
253
254
255
256
257
version: IDENTIFIER
         {
	   if (*$1 != "v1")
	     error(@$, "unsupported version of the HOA format");
	   delete $1;
	 }

format-version: "HOA:" { res.h->loc = @1; } version
              | error "HOA:"
	        { error(@1, "ignoring leading garbage");
		  res.h->loc = @2; }
                version
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284

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);
	   }
           | "Start:" state-conj-2
	     {
	       error(@2, "alternation is not yet supported");
	       YYABORT;
	     }
           | "Start:" state-num
	     {
285
	       res.start.emplace_back(@$, $2);
286
287
	     }
           | "AP:" INT {
288
289
290
291
292
293
294
295
296
297
	                 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);
			   }
298
299
300
	               }
                   ap-names
	     {
301
	       if (!res.ignore_more_ap)
302
		 {
303
304
305
306
307
308
309
310
311
312
		   res.ap_loc = @1 + @2;
		   if ((int) res.ap.size() != res.ap_count)
		     {
		       std::ostringstream out;
		       out << "found " << res.ap.size()
			   << " atomic propositions instead of the "
			   << res.ap_count << " announced";
		       error(@$, out.str());
		     }
		   res.ignore_more_ap = true;
313
314
315
316
		 }
	     }
           | "Alias:" ANAME label-expr
             {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
317
318
319
320
321
322
	       if (!res.alias.emplace(*$2, bdd_from_int($3)).second)
		 {
		   std::ostringstream o;
		   o << "ignoring redefinition of alias @" << *$2;
		   error(@$, o.str());
		 }
323
324
325
326
327
	       delete $2;
	       bdd_delref($3);
	     }
           | "Acceptance:" INT
	      {
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
		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
		  {
		    res.h->aut->acc().add_sets($2);
		    res.accset = $2;
		    res.accset_loc = @1 + @2;
		  }
347
348
	     }
             acceptance-cond
349
350
351
	     {
	       res.ignore_more_acc = true;
	     }
352
353
354
355
356
357
358
359
360
361
           | "acc-name:" IDENTIFIER acc-spec
             {
	       delete $2;
	     }
           | "tool:" STRING string_opt
             {
	       delete $2;
	     }
           | "name:" STRING
             {
362
363
364
	       res.h->aut->set_named_prop("automaton-name", $2, [](void* name) {
		   delete static_cast<std::string*>(name);
		 });
365
366
367
	     }
           | "properties:" properties
           | HEADERNAME header-spec
368
369
370
371
372
373
374
375
	     {
	       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;
	     }
376
           | error
377
378
379
380

ap-names: | ap-names ap-name
ap-name: STRING
	 {
381
	   if (!res.ignore_more_ap)
382
	     {
383
384
385
386
387
388
389
390
391
392
393
394
395
396
	       auto f = res.env->require(*$1);
	       if (f == nullptr)
		 {
		   std::ostringstream out;
		   out << "unknown atomic proposition \"" << *$1 << "\"";
		   delete $1;
		   error(@1, out.str());
		   f = spot::ltl::default_environment::instance()
		     .require("$unknown$");
		 }
	       auto b =
		 res.h->aut->get_dict()->register_proposition(f, res.h->aut);
	       f->destroy();
	       res.ap.push_back(b);
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
	     }
	   delete $1;
	 }

acc-spec: | acc-spec BOOLEAN
	  | acc-spec INT
	  | acc-spec IDENTIFIER
            {
	      delete $2;
	    }
properties: | properties IDENTIFIER
	      {
		delete $2;
	      }
header-spec: | header-spec BOOLEAN
             | header-spec INT
             | header-spec STRING
	       {
		 delete $2;
	       }
             | header-spec IDENTIFIER
	       {
		 delete $2;
	       }

422
423
state-conj-2: checked-state-num '&' checked-state-num
            | state-conj-2 '&' checked-state-num
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448

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
449
450
451
452
453
454
455
456
457
458
459
	      auto i = res.alias.find(*$1);
	      if (i == res.alias.end())
		{
		  error(@$, "unknown alias @" + *$1);
		  $$ = 1;
		}
	      else
		{
		  $$ = i->second.id();
		  bdd_addref($$);
		}
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
	      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($$);
            }


acc-set: INT
            {
	      if ((int) $1 >= res.accset)
		{
488
489
490
491
492
493
494
495
496
497
498
		  if (!res.ignore_acc)
		    {
		      error(@1, "number is larger than the count "
			    "of acceptance sets...");
		      error(res.accset_loc, "... declared here.");
		    }
		  $$ = -1U;
		}
	      else
		{
		  $$ = $1;
499
500
501
502
503
		}
	    }

acceptance-cond: IDENTIFIER '(' acc-set ')'
		 {
504
		   if (!res.ignore_more_acc && *$1 != "Inf")
505
506
		     error(@1, "this implementation only supports "
			   "'Inf' acceptance");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
507
508
		   if ($3 != -1U)
		     res.pos_acc_sets |= res.h->aut->acc().mark($3);
509
510
511
512
		   delete $1;
		 }
               | IDENTIFIER '(' '!' acc-set ')'
		 {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
513
514
515
516
517
		   if (!res.ignore_more_acc && *$1 != "Inf")
		     error(@1, "this implementation only supports "
			   "'Inf' acceptance");
		   if ($4 != -1U)
		     res.neg_acc_sets |= res.h->aut->acc().mark($4);
518
519
520
521
522
523
		   delete $1;
		 }
               | '(' acceptance-cond ')'
               | acceptance-cond '&' acceptance-cond
               | acceptance-cond '|' acceptance-cond
	         {
524
525
526
		   if (!res.ignore_more_acc)
		     error(@2, "this implementation does not support "
			   "disjunction in acceptance conditions");
527
		 }
528
529
530
531
532
533
534
               | 't'
	       | 'f'
	       {
		 if (!res.ignore_more_acc)
		   error(@$, "this implementation does not support "
			 "false acceptance");
	       }
535
536
537
538
539
540
541
542
543
544
545
546
547
548


body: states

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

549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
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.");
			   }
			 int missing =
			   ((int) $1) - res.h->aut->num_states() + 1;
			 if (missing >= 0)
			   {
			     res.h->aut->new_states(missing);
			     res.declared_states.resize
			       (res.declared_states.size() + missing);
			   }
		       }
		     $$ = $1;
		   }

571
states: | states state
572
573
574
575
576
577
578
579
580
581
state: state-name labeled-edges
     | state-name unlabeled-edges
       {
	 if (!res.has_state_label)
	   {
	     if (res.cur_guard != res.guards.end())
	       error(@$, "not enough transitions for this state");
	     res.cur_guard = res.guards.begin();
	   }
       }
582
583
     | error

584
state-name: "State:" state-label_opt checked-state-num string_opt acc-sig_opt
585
586
	  {
	    res.cur_state = $3;
587
588
589
590
591
592
593
	    if (res.declared_states[$3])
	      {
		std::ostringstream o;
		o << "redeclaration of state " << $3;
		error(@1 + @3, o.str());
	      }
	    res.declared_states[$3] = true;
594
595
596
597
598
599
600
	    res.acc_state = $5;
	  }
label: '[' label-expr ']'
	   {
             res.cur_label = bdd_from_int($2);
             bdd_delref($2);
	   }
601
602
603
604
605
     | '[' error ']'
           {
	     error(@$, "ignoring this invalid label");
	     res.cur_label = bddtrue;
	   }
606
607
608
609
state-label_opt:       { res.has_state_label = false; }
               | label { res.has_state_label = true;
                         res.state_label_loc = @1;
		         res.state_label = res.cur_label; }
610
trans-label: label
611
612
613
	         {
		   if (res.has_state_label)
		     {
614
		       error(@1, "cannot label this edge because...");
615
616
		       error(res.state_label_loc,
			     "... the state is already labeled.");
617
		       res.cur_label = res.state_label;
618
619
620
		     }
		 }

621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
acc-sig_opt:
             {
               $$ = spot::acc_cond::mark_t(0U);
             }
           | '{' acc-sets '}'
	     {
	       $$ = $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;
		 }
	     }
636
637
638
639
           | '{' error '}'
	     {
	       error(@$, "ignoring this invalid acceptance set");
	     }
640
641
642
643
acc-sets:
          {
	    $$ = spot::acc_cond::mark_t(0U);
	  }
644
645
        | acc-sets acc-set
	  {
646
647
648
649
	    if (res.ignore_acc || $2 == -1U)
	      $$ = spot::acc_cond::mark_t(0U);
	    else
	      $$ = $1 | res.h->aut->acc().mark($2);
650
	  }
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668

/* 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
incorrectly-unlabeled-edge: checked-state-num acc-sig_opt
                            {
			      bdd cond = bddtrue;
			      if (!res.has_state_label)
				error(@$, "missing label for this edge "
				      "(previous edge is labeled)");
			      else
				cond = res.state_label;
			      res.h->aut->new_transition(res.cur_state, $1,
							 cond,
							 $2 | res.acc_state);
			    }
669
labeled-edge: trans-label checked-state-num acc-sig_opt
670
	      {
671
672
673
674
		if (res.cur_label != bddfalse)
		  res.h->aut->new_transition(res.cur_state, $2,
					     res.cur_label,
					     $3 | res.acc_state);
675
676
677
678
679
680
681
	      }
	    | trans-label state-conj-2 acc-sig_opt
	      {
		error(@2, "alternation is not yet supported");
		YYABORT;
	      }

682
683
684
685
686
687
/* 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
688
unlabeled-edge: checked-state-num acc-sig_opt
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
		{
		  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())
			{
			  error(@$, "too many transition for this state, "
				"ignoring this one");
			  cond = bddfalse;
			}
		      else
			{
			  cond = *res.cur_guard++;
			}
		    }
710
711
712
		  if (cond != bddfalse)
		    res.h->aut->new_transition(res.cur_state, $1,
					       cond, $2 | res.acc_state);
713
714
715
716
717
718
		}
	      | state-conj-2 acc-sig_opt
		{
		  error(@1, "alternation is not yet supported");
		  YYABORT;
		}
719
720
721
722
723
incorrectly-labeled-edge: trans-label unlabeled-edge
                          {
			    error(@1, "ignoring this label, because previous"
				  " edge has no label");
                          }
724

725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
/**********************************************************************/
/*                      Rules for neverclaims                         */
/**********************************************************************/

never: "never" { res.namer = res.h->aut->create_namer<std::string>();
	         res.h->aut->set_single_acceptance_set();
		 res.h->aut->prop_state_based_acc(); }
       '{' nc-states '}'
       {
	 // Add an accept_all state if needed.
	 if (res.accept_all_needed && !res.accept_all_seen)
	   {
	     unsigned n = res.namer->new_state("accept_all");
	     res.h->aut->new_acc_transition(n, n, bddtrue);
	   }
740
741
742
743
	 // If we aliased existing state, we have some unreachable
	 // states to remove.
	 if (res.aliased_states)
	   res.h->aut->purge_unreachable_states();
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
       }

nc-states:
  /* empty */
  | nc-state
  | nc-states ';' nc-state
  | nc-states ';'

nc-one-ident: IDENTIFIER ':'
    {
      auto r = res.labels.insert(std::make_pair(*$1, @1));
      if (!r.second)
	{
	  error(@1, std::string("redefinition of ") + *$1 + "...");
	  error(r.first->second, std::string("... ")  + *$1
		+ " previously defined here");
	}
      $$ = $1;
    }

nc-ident-list: nc-one-ident
765
766
767
768
769
770
771
772
773
    {
      unsigned n = res.namer->new_state(*$1);
      if (res.start.empty())
	{
	  // The first state is initial.
	  res.start.emplace_back(@$, n);
	}
      $$ = $1;
    }
774
775
  | nc-ident-list nc-one-ident
    {
776
777
      res.aliased_states |=
	res.namer->alias_state(res.namer->get_state(*$1), *$2);
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
      // Keep any identifier that starts with accept.
      if (strncmp("accept", $1->c_str(), 6))
        {
          delete $1;
          $$ = $2;
        }
      else
        {
	  delete $2;
	  $$ = $1;
        }
    }

nc-transition-block:
  "if" nc-transitions "fi"
    {
      $$ = $2;
    }
  | "do" nc-transitions "od"
    {
      $$ = $2;
    }

nc-state:
  nc-ident-list "skip"
    {
      if (*$1 == "accept_all")
	res.accept_all_seen = true;

807
808
809
      auto acc = !strncmp("accept", $1->c_str(), 6) ?
	res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U);
      res.namer->new_transition(*$1, *$1, bddtrue, acc);
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
      delete $1;
    }
  | nc-ident-list { delete $1; }
  | nc-ident-list "false" { delete $1; }
  | nc-ident-list nc-transition-block
    {
      auto acc = !strncmp("accept", $1->c_str(), 6) ?
	res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U);
      for (auto& p: *$2)
	{
	  bdd c = bdd_from_int(p.first);
	  bdd_delref(p.first);
	  res.namer->new_transition(*$1, *p.second, c, acc);
	  delete p.second;
	}
      delete $1;
      delete $2;
    }

nc-transitions:
  /* empty */ { $$ = new std::list<pair>; }
  | nc-transitions nc-transition
    {
      if ($2)
	{
	  $1->push_back(*$2);
	  delete $2;
	}
      $$ = $1;
    }

nc-formula-or-ident: FORMULA | IDENTIFIER

nc-formula: nc-formula-or-ident
     {
       auto i = res.fcache.find(*$1);
       if (i == res.fcache.end())
	 {
	   spot::ltl::parse_error_list pel;
	   auto f = spot::ltl::parse_boolean(*$1, pel, *res.env,
					     debug_level(), true);
	   for (auto& j: pel)
	     {
	       // Adjust the diagnostic to the current position.
	       spot::location here = @1;
	       here.end.line = here.begin.line + j.first.end.line - 1;
856
	       here.end.column = here.begin.column + j.first.end.column - 1;
857
	       here.begin.line += j.first.begin.line - 1;
858
	       here.begin.column += j.first.begin.column - 1;
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
	       error_list.emplace_back(here, j.second);
	     }
           bdd cond = bddfalse;
	   if (f)
	     {
	       cond = spot::formula_to_bdd(f, res.h->aut->get_dict(),
					   res.h->aut);
	       f->destroy();
	     }
	   $$ = (res.fcache[*$1] = cond).id();
	 }
       else
	 {
	   $$ = i->second.id();
	 }
       bdd_addref($$);
       delete $1;
     }
   | "false"
     {
       $$ = 0;
     }

nc-opt-dest:
  /* empty */
    {
      $$ = 0;
    }
  | "->" "goto" IDENTIFIER
    {
      $$ = $3;
    }
  | "->" "assert" FORMULA
    {
      delete $3;
      $$ = new std::string("accept_all");
      res.accept_all_needed = true;
    }

nc-src-dest: nc-formula nc-opt-dest
    {
      // If there is no destination, do ignore the transition.
      // This happens for instance with
      //   if
      //   :: false
      //   fi
      if (!$2)
	{
	  $$ = 0;
	}
      else
	{
	  $$ = new pair($1, $2);
	  res.namer->new_state(*$2);
	}
    }

nc-transition:
  ':' ':' "atomic" '{' nc-src-dest '}'
    {
      $$ = $5;
    }
  | ':' ':' nc-src-dest
    {
      $$ = $3;
    }

926
927
%%

928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
static void fill_guards(result_& r)
{
  spot::bdd_dict_ptr d = r.h->aut->get_dict();
  unsigned nap = r.ap.size();

  int* vars = new int[nap];
  for (unsigned i = 0; i < nap; ++i)
    vars[i] = r.ap[nap - 1 - i];

  // build the 2^nap possible guards
  r.guards.reserve(1U << nap);
  for (size_t i = 0; i < (1U << nap); ++i)
    r.guards.push_back(bdd_ibuildcube(i, nap, vars));
  r.cur_guard = r.guards.begin();

  delete[] vars;
}

946
947
948
949
950
951
952
void
hoayy::parser::error(const location_type& location,
		       const std::string& message)
{
  error_list.emplace_back(location, message);
}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
953
954
955
956
957
static void fix_acceptance(result_& r)
{
  // If a set x appears only as Inf(!x), we can complement it so that
  // we work with Inf(x) instead.
  auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
958
  for (auto& t: r.h->aut->transition_vector())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
959
960
961
962
963
964
965
966
967
968
969
970
971
972
    t.acc ^= onlyneg;

  // However if set x is used elsewhere, for instance in
  //   Inf(!x) & Inf(x)
  // complementing x would be wrong.  We need to create a
  // new set, y, that is the complement of x, and rewrite
  // this as Inf(y) & Inf(x).
  auto both = r.neg_acc_sets & r.pos_acc_sets;
  if (both)
    {
      auto& acc = r.h->aut->acc();
      auto v = acc.sets(both);
      auto vs = v.size();
      unsigned base = acc.add_sets(vs);
973
      for (auto& t: r.h->aut->transition_vector())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
974
975
976
977
978
979
980
	if ((t.acc & both) != both)
	  for (unsigned i = 0; i < vs; ++i)
	    if (!t.acc.has(i))
	      t.acc |= acc.mark(base + i);
    }
}

981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
static void fix_initial_state(result_& r)
{
  if (r.start.empty())
    {
      // If no initial state has been declared, add one, because
      // Spot will not work without one.
      r.h->aut->set_init_state(r.h->aut->new_state());
      return;
    }

  // Remove any duplicate initial state.
  std::vector<unsigned> start;
  start.reserve(r.start.size());
  for (auto& p : r.start)
    start.push_back(p.second);
  std::sort(start.begin(), start.end());
  auto res = std::unique(start.begin(), start.end());
  start.resize(std::distance(start.begin(), res));

  assert(start.size() >= 1);
  if (start.size() == 1)
    {
      r.h->aut->set_init_state(start.front());
    }
  else
    {
      // Multiple initial states.  Add a fake one.
      auto& aut = r.h->aut;
      unsigned i = aut->new_state();
      aut->set_init_state(i);
      for (auto p : start)
	for (auto& t: aut->out(p))
	  aut->new_transition(i, t.dst, t.cond);
    }
}

1017
1018
namespace spot
{
1019
  hoa_stream_parser::hoa_stream_parser(const std::string& name)
1020
1021
  {
    if (hoayyopen(name))
1022
1023
1024
1025
1026
1027
1028
1029
      throw std::runtime_error(std::string("Cannot open file ") + name);
  }

  hoa_stream_parser::~hoa_stream_parser()
  {
    hoayyclose();
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1030

1031
1032
1033
1034
1035
1036
  hoa_aut_ptr
  hoa_stream_parser::parse(hoa_parse_error_list& error_list,
			   const bdd_dict_ptr& dict,
			   ltl::environment& env,
			   bool debug)
  {
1037
1038
1039
1040
    result_ r;
    r.h = std::make_shared<spot::hoa_aut>();
    r.h->aut = make_tgba_digraph(dict);
    r.env = &env;
1041
    hoayy::parser parser(error_list, r, last_loc);
1042
    parser.set_debug_level(debug);
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
    try
      {
	if (parser.parse())
	  r.h->aut = nullptr;
      }
    catch (const spot::hoa_abort& e)
      {
	r.h->aborted = true;
	// Bison 3.0.2 lacks a += operator for locations.
	r.h->loc = r.h->loc + e.pos;
      }
    last_loc = r.h->loc;
    last_loc.step();
    if (r.h->aborted)
      return r.h;
1058
1059
    if (!r.h->aut)
      return nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1060
1061
    if (r.neg_acc_sets)
      fix_acceptance(r);
1062
    fix_initial_state(r);
1063
    return r.h;
1064
  };
1065
1066
1067
1068
1069
}

// Local Variables:
// mode: c++
// End: