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

%code requires
{
32 33
#include "config.h"
#include "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
#include "twa/formula2bdd.hh"
40
#include "public.hh"
41
#include "priv/accmap.hh"
42
#include "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
  inline namespace hoayy_support
50
  {
51 52
    typedef std::map<int, bdd> map_t;

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

    typedef std::pair<int, std::string*> pair;
61
    typedef spot::twa_graph::namer<std::string> named_tgba_t;
62 63 64 65 66 67 68 69

    // 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 };
70
    enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
71 72

    struct result_
73
    {
74 75
      struct state_info
      {
76 77
	bool declared = false;
	bool used = false;
78 79
	spot::location used_loc;
      };
80
      spot::parsed_aut_ptr h;
81
      spot::automaton_parser_options opts;
82 83
      std::string format_version;
      spot::location format_version_loc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
84
      spot::environment* env;
85 86 87 88 89 90
      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;
91
      map_t dest_map;
92
      std::vector<state_info> info_states; // States declared and used.
93 94 95 96 97 98 99 100 101 102
      std::vector<std::pair<spot::location, unsigned>> start; // Initial states;
      std::unordered_map<std::string, bdd> alias;
      std::unordered_map<std::string, spot::location> props;
      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;
103 104
      int plus;
      int minus;
105
      std::vector<std::string>* state_names = nullptr;
106
      std::map<unsigned, unsigned> states_map;
107
      std::set<int> ap_set;
108 109 110 111 112 113 114 115 116
      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.
117 118
      bool ignore_acc = false;	// Set to true in case of missing
				// Acceptance: lines.
119 120
      bool ignore_acc_silent = false;
      bool ignore_more_acc = false; // Set to true after the first
121
				// "Acceptance:" line has been read.
122 123

      label_style_t label_style = Mixed_Labels;
124
      acc_style_t acc_style = Mixed_Acc;
125 126 127 128 129 130 131

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

      bool deterministic = false;
      bool complete = false;
132
      bool trans_acc_seen = false;
133 134 135 136 137 138 139 140 141 142

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

      ~result_()
      {
	delete namer;
	delete acc_mapper;
      }
    };
  }
143 144
}

145
%parse-param {spot::parse_aut_error_list& error_list}
146
%parse-param {result_& res}
147 148
%parse-param {spot::location initial_loc}

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

151 152 153 154 155 156
%union
{
  std::string* str;
  unsigned int num;
  int b;
  spot::acc_cond::mark_t mark;
157 158
  pair* p;
  std::list<pair>* list;
159
  spot::acc_cond::acc_code* code;
160 161 162 163 164
}

%code
{
#include <sstream>
165

166
  /* parseaut.hh and parsedecl.hh include each other recursively.
167 168 169
   We must ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
170 171

  static void fill_guards(result_& res);
172 173
}

174
/**** HOA tokens ****/
175 176 177 178 179 180 181 182 183 184 185 186 187
%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:";
188
%token <str> IDENTIFIER "identifier";  // also used by neverclaim
189 190 191 192
%token <str> HEADERNAME "header name";
%token <str> ANAME "alias name";
%token <str> STRING "string";
%token <num> INT "integer";
193
%token ENDOFFILE 0 "end of file"
194

195 196 197 198 199 200 201 202 203
%token DRA "DRA"
%token DSA "DSA"
%token V2 "v2"
%token EXPLICIT "explicit"
%token ACCPAIRS "Acceptance-Pairs:"
%token ACCSIG "Acc-Sig:";
%token ENDOFHEADER "---";


204 205 206 207
%left '|'
%left '&'
%nonassoc '!'

208
%type <num> checked-state-num state-num acc-set sign
209
%type <b> label-expr
210
%type <mark> acc-sig acc-sets trans-acc_opt state-acc_opt
211
             dstar_accsigs dstar_state_accsig
212
%type <str> string_opt
213

214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233
/**** 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
234
%type <code> acceptance-cond
235

236 237 238
/**** LBTT tokens *****/
 // Also using INT, STRING
%token ENDAUT "-1"
239
%token ENDDSTAR "end of DSTAR automaton"
240 241 242 243 244 245 246
%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
247

248 249
%destructor { delete $$; } <str>
%destructor { bdd_delref($$); } <b>
250
%destructor { bdd_delref($$->first); delete $$->second; delete $$; } <p>
251
%destructor { delete $$; } <code>
252 253 254 255 256 257 258 259 260
%destructor {
  for (std::list<pair>::iterator i = $$->begin();
       i != $$->end(); ++i)
  {
    bdd_delref(i->first);
    delete i->second;
  }
  delete $$;
  } <list>
261 262 263 264 265 266 267 268
%printer {
    if ($$)
      debug_stream() << *$$;
    else
      debug_stream() << "\"\""; } <str>
%printer { debug_stream() << $$; } <num>

%%
269 270
aut: aut-1     { res.h->loc = @$; YYACCEPT; }
   | ENDOFFILE { YYABORT; }
271
   | error ENDOFFILE { YYABORT; }
272 273 274 275 276 277
   | error aut-1
     {
       error(@1, "leading garbage was ignored");
       res.h->loc = @2;
       YYACCEPT;
     }
278

279 280 281 282
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 */
283 284 285 286 287

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

288
hoa: header "--BODY--" body "--END--"
289
   | "HOA:" error "--END--"
290

291 292
string_opt: { $$ = nullptr; }
          | STRING { $$ = $1; }
293 294 295 296
BOOLEAN: 't' | 'f'

header: format-version header-items
        {
297
	  // Preallocate the states if we know their number.
298
	  if (res.states >= 0)
299 300
	    {
	      unsigned states = res.states;
301 302 303 304 305 306 307 308
	      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);
		  }
309
	      res.h->aut->new_states(states);
310
	      res.info_states.resize(states);
311
	    }
312 313 314
	  if (res.accset < 0)
	    {
	      error(@$, "missing 'Acceptance:' header");
315
	      res.ignore_acc = true;
316
	    }
317 318
	  // Process properties.
	  {
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
	    auto explicit_labels = res.props.find("explicit-labels");
	    auto implicit_labels = res.props.find("implicit-labels");
	    if (implicit_labels != res.props.end())
	      {
		if (explicit_labels == res.props.end())
		  {
		    res.label_style = Implicit_Labels;
		  }
		else
		  {
		    error(implicit_labels->second,
			  "'property: implicit-labels' is incompatible "
			  "with...");
		    error(explicit_labels->second,
			  "... 'property: explicit-labels'.");
		  }
	      }

337 338 339 340 341 342
	    auto trans_labels = res.props.find("trans-labels");
	    auto state_labels = res.props.find("state-labels");
	    if (trans_labels != res.props.end())
	      {
		if (state_labels == res.props.end())
		  {
343 344
		    if (res.label_style != Implicit_Labels)
		      res.label_style = Trans_Labels;
345 346 347 348 349 350 351 352 353 354 355
		  }
		else
		  {
		    error(trans_labels->second,
			  "'property: trans-labels' is incompatible with...");
		    error(state_labels->second,
			  "... 'property: state-labels'.");
		  }
	      }
	    else if (state_labels != res.props.end())
	      {
356 357 358 359 360 361 362 363 364 365 366
		if (res.label_style != Implicit_Labels)
		  {
		    res.label_style = State_Labels;
		  }
		else
		  {
		    error(state_labels->second,
			  "'property: state-labels' is incompatible with...");
		    error(implicit_labels->second,
			  "... 'property: implicit-labels'.");
		  }
367
	      }
368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388

	    auto state_acc = res.props.find("state-acc");
	    auto trans_acc = res.props.find("trans-acc");
	    if (trans_acc != res.props.end())
	      {
		if (state_acc == res.props.end())
		  {
		    res.acc_style = Trans_Acc;
		  }
		else
		  {
		    error(trans_acc->second,
			  "'property: trans-acc' is incompatible with...");
		    error(state_acc->second,
			  "... 'property: state-acc'.");
		  }
	      }
	    else if (state_acc != res.props.end())
	      {
		res.acc_style = State_Acc;
	      }
389
	  }
390 391 392 393 394 395 396 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 422 423 424 425 426
	  {
	    unsigned ss = res.start.size();
	    if (ss > 1)
	      {
		auto det = res.props.find("deterministic");
		if (det != res.props.end())
		  {
		    error(det->second,
			  "deterministic automata should have at most "
			  "one initial state");
		  }
		res.deterministic = false;
	      }
	    else
	      {
		// Assume the automaton is deterministic until proven
		// wrong.
		res.deterministic = true;
	      }
	    if (ss < 1)
	      {
		auto complete = res.props.find("complete");
		if (complete != res.props.end())
		  {
		    error(complete->second,
			  "complete automata should have at least "
			  "one initial state");
		  }
		res.complete = false;
	      }
	    else
	      {
		// Assume the automaton is complete until proven
		// wrong.
		res.complete = true;
	      }
	  }
427 428 429 430 431 432 433 434 435 436
	  if (res.opts.trust_hoa)
	    {
	      auto e = res.props.end();
	      bool si = res.props.find("stutter-invariant") != e;
	      res.h->aut->prop_stutter_invariant(si);
	      bool ss = res.props.find("stutter-sensitive") != e;
	      res.h->aut->prop_stutter_sensitive(ss);
	      bool iw = res.props.find("inherently-weak") != e;
	      res.h->aut->prop_inherently_weak(iw);
	    }
437 438
	}

439 440
version: IDENTIFIER
         {
441 442
	   res.format_version = *$1;
	   res.format_version_loc = @1;
443 444 445 446
	   delete $1;
	 }

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

448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476
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)
		     {
		       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;
		 }
	     }

477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
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);
	   }
496
           | "Start:" init-state-conj-2
497 498 499 500 501 502
	     {
	       error(@2, "alternation is not yet supported");
	       YYABORT;
	     }
           | "Start:" state-num
	     {
503
	       res.start.emplace_back(@$, $2);
504
	     }
505
           | aps
506 507
           | "Alias:" ANAME label-expr
             {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
508 509 510 511 512 513
	       if (!res.alias.emplace(*$2, bdd_from_int($3)).second)
		 {
		   std::ostringstream o;
		   o << "ignoring redefinition of alias @" << *$2;
		   error(@$, o.str());
		 }
514 515 516 517 518
	       delete $2;
	       bdd_delref($3);
	     }
           | "Acceptance:" INT
	      {
519 520 521 522 523 524 525 526 527 528 529 530 531 532 533
		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
		  {
534
		    res.h->aut->acc().add_sets($2);
535 536 537
		    res.accset = $2;
		    res.accset_loc = @1 + @2;
		  }
538 539
	     }
             acceptance-cond
540 541
	     {
	       res.ignore_more_acc = true;
542 543
	       res.h->aut->set_acceptance($2, *$4);
	       delete $4;
544
	     }
545 546 547 548 549 550 551
           | "acc-name:" IDENTIFIER acc-spec
             {
	       delete $2;
	     }
           | "tool:" STRING string_opt
             {
	       delete $2;
552
	       delete $3;
553 554 555
	     }
           | "name:" STRING
             {
556
	       res.h->aut->set_named_prop("automaton-name", $2);
557 558 559
	     }
           | "properties:" properties
           | HEADERNAME header-spec
560 561 562 563 564 565 566 567
	     {
	       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;
	     }
568
           | error
569 570 571 572

ap-names: | ap-names ap-name
ap-name: STRING
	 {
573
	   if (!res.ignore_more_ap)
574
	     {
575
	       auto f = res.env->require(*$1);
576
	       int b = 0;
577 578 579 580 581
	       if (f == nullptr)
		 {
		   std::ostringstream out;
		   out << "unknown atomic proposition \"" << *$1 << "\"";
		   error(@1, out.str());
582
		   b = res.h->aut->register_ap("$unknown$");
583 584 585
		 }
	       else
		 {
586
		   b = res.h->aut->register_ap(f);
587 588 589 590 591 592
		   if (!res.ap_set.emplace(b).second)
		     {
		       std::ostringstream out;
		       out << "duplicate atomic proposition \"" << *$1 << "\"";
		       error(@1, out.str());
		     }
593 594
		 }
	       res.ap.push_back(b);
595 596 597 598 599 600 601 602 603 604 605 606
	     }
	   delete $1;
	 }

acc-spec: | acc-spec BOOLEAN
	  | acc-spec INT
	  | acc-spec IDENTIFIER
            {
	      delete $2;
	    }
properties: | properties IDENTIFIER
	      {
607
		res.props.emplace(*$2, @2);
608 609 610 611 612 613 614 615 616 617 618 619 620
		delete $2;
	      }
header-spec: | header-spec BOOLEAN
             | header-spec INT
             | header-spec STRING
	       {
		 delete $2;
	       }
             | header-spec IDENTIFIER
	       {
		 delete $2;
	       }

621 622
state-conj-2: checked-state-num '&' checked-state-num
            | state-conj-2 '&' checked-state-num
623

624 625 626 627 628
	      // 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

629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652
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
653 654 655 656 657 658 659 660 661 662 663
	      auto i = res.alias.find(*$1);
	      if (i == res.alias.end())
		{
		  error(@$, "unknown alias @" + *$1);
		  $$ = 1;
		}
	      else
		{
		  $$ = i->second.id();
		  bdd_addref($$);
		}
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685
	      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($$);
            }
686 687 688 689
          | '(' label-expr ')'
	  {
	    $$ = $2;
	  }
690 691 692 693 694 695


acc-set: INT
            {
	      if ((int) $1 >= res.accset)
		{
696 697 698 699 700 701 702 703 704 705 706
		  if (!res.ignore_acc)
		    {
		      error(@1, "number is larger than the count "
			    "of acceptance sets...");
		      error(res.accset_loc, "... declared here.");
		    }
		  $$ = -1U;
		}
	      else
		{
		  $$ = $1;
707 708 709 710 711
		}
	    }

acceptance-cond: IDENTIFIER '(' acc-set ')'
		 {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
712
		   if ($3 != -1U)
713 714 715 716 717 718 719 720 721 722 723 724 725
		     {
		       res.pos_acc_sets |= res.h->aut->acc().mark($3);
		       if (*$1 == "Inf")
			 $$ = new spot::acc_cond::acc_code
			   (res.h->aut->acc().inf({$3}));
		       else
			 $$ = new spot::acc_cond::acc_code
			   (res.h->aut->acc().fin({$3}));
		     }
		   else
		     {
		       $$ = new spot::acc_cond::acc_code;
		     }
726 727 728 729
		   delete $1;
		 }
               | IDENTIFIER '(' '!' acc-set ')'
		 {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
730
		   if ($4 != -1U)
731 732 733 734 735 736 737 738 739 740 741 742 743
		     {
		       res.neg_acc_sets |= res.h->aut->acc().mark($4);
		       if (*$1 == "Inf")
			 $$ = new spot::acc_cond::acc_code
			   (res.h->aut->acc().inf_neg({$4}));
		       else
			 $$ = new spot::acc_cond::acc_code
			   (res.h->aut->acc().fin_neg({$4}));
		     }
		   else
		     {
		       $$ = new spot::acc_cond::acc_code;
		     }
744 745 746
		   delete $1;
		 }
               | '(' acceptance-cond ')'
747 748 749
	         {
		   $$ = $2;
		 }
750
               | acceptance-cond '&' acceptance-cond
751 752 753 754 755
	         {
		   $3->append_and(std::move(*$1));
		   $$ = $3;
		   delete $1;
		 }
756 757
               | acceptance-cond '|' acceptance-cond
	         {
758 759 760
		   $3->append_or(std::move(*$1));
		   $$ = $3;
		   delete $1;
761
		 }
762
               | 't'
763 764 765
	         {
		   $$ = new spot::acc_cond::acc_code;
		 }
766 767
	       | 'f'
	       {
768 769 770
	         {
		   $$ = new spot::acc_cond::acc_code(res.h->aut->acc().fin({}));
		 }
771
	       }
772 773 774


body: states
775 776
      {
	for (auto& p: res.start)
777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799
	  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");
	  }
800
      }
801 802 803 804 805 806 807 808 809 810 811

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

812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
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);
827 828
			     res.info_states.resize
			       (res.info_states.size() + missing);
829 830
			   }
		       }
831 832 833 834 835 836 837
		     // 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;
		       }
838 839 840
		     $$ = $1;
		   }

841
states: | states state
842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874
        {
	  if (res.deterministic || res.complete)
	    {
	      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;
		  auto p = res.props.find("deterministic");
		  if (p != res.props.end())
		    {
		      error(@2, "automaton is not deterministic...");
		      error(p->second, "... despite 'property: deterministic'");
		    }
		}
	      if (res.complete && available != bddfalse)
		{
		  res.complete = false;
		  auto p = res.props.find("complete");
		  if (p != res.props.end())
		    {
		      error(@2, "automaton is not complete...");
		      error(p->second, "... despite 'property: complete'");
		    }
		}
	    }
	}
875 876 877
state: state-name labeled-edges
     | state-name unlabeled-edges
       {
878
	 if (!res.has_state_label) // Implicit labels
879 880 881
	   {
	     if (res.cur_guard != res.guards.end())
	       error(@$, "not enough transitions for this state");
882 883 884 885 886 887 888 889 890 891 892

	     if (res.label_style == State_Labels)
	       {
		 error(@2, "these transitions have implicit labels but the"
		       " automaton is...");
		 error(res.props["state-labels"], "... declared with "
		       "'property: state-labels'");
		 // Do not repeat this message.
		 res.label_style = Mixed_Labels;
	       }

893 894 895
	     res.cur_guard = res.guards.begin();
	   }
       }
896
     | error
897 898 899 900 901
       {
	 // Assume the worse.
	 res.deterministic = false;
	 res.complete = false;
       }
902

903

904
state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt
905 906
	  {
	    res.cur_state = $3;
907
	    if (res.info_states[$3].declared)
908 909 910 911 912
	      {
		std::ostringstream o;
		o << "redeclaration of state " << $3;
		error(@1 + @3, o.str());
	      }
913
	    res.info_states[$3].declared = true;
914
	    res.acc_state = $5;
915 916 917 918 919 920 921 922 923 924 925
	    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;
	      }
926 927 928 929 930 931
	  }
label: '[' label-expr ']'
	   {
             res.cur_label = bdd_from_int($2);
             bdd_delref($2);
	   }
932 933 934 935 936
     | '[' error ']'
           {
	     error(@$, "ignoring this invalid label");
	     res.cur_label = bddtrue;
	   }
937
state-label_opt:       { res.has_state_label = false; }
938 939 940 941 942
               | label
	       {
		 res.has_state_label = true;
		 res.state_label_loc = @1;
		 res.state_label = res.cur_label;
943 944
		 if (res.label_style == Trans_Labels
		     || res.label_style == Implicit_Labels)
945 946 947
		   {
		     error(@$,
			   "state label used although the automaton was...");
948 949 950 951 952 953 954
		     if (res.label_style == Trans_Labels)
		       error(res.props["trans-labels"],
			     "... declared with 'property: trans-labels' here");
		     else
		       error(res.props["implicit-labels"],
			     "... declared with 'property: implicit-labels' "
			     "here");
955 956 957 958
		     // Do not show this error anymore.
		     res.label_style = Mixed_Labels;
		   }
	       }
959
trans-label: label
960 961 962
	         {
		   if (res.has_state_label)
		     {
963
		       error(@1, "cannot label this edge because...");
964 965
		       error(res.state_label_loc,
			     "... the state is already labeled.");
966
		       res.cur_label = res.state_label;
967
		     }
968 969
		   if (res.label_style == State_Labels
		       || res.label_style == Implicit_Labels)
970 971 972
		     {
		       error(@$, "transition label used although the "
			     "automaton was...");
973 974 975 976 977 978 979 980
		       if (res.label_style == State_Labels)
			 error(res.props["state-labels"],
			       "... declared with 'property: state-labels' "
			       "here");
		       else
			 error(res.props["implicit-labels"],
			       "... declared with 'property: implicit-labels' "
			       "here");
981 982 983
		       // Do not show this error anymore.
		       res.label_style = Mixed_Labels;
		     }
984 985
		 }

986
acc-sig: '{' acc-sets '}'
987 988 989 990 991 992 993 994 995 996
	     {
	       $$ = $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;
		 }
	     }
997 998 999 1000
           | '{' error '}'
	     {
	       error(@$, "ignoring this invalid acceptance set");
	     }
1001 1002 1003 1004
acc-sets:
          {
	    $$ = spot::acc_cond::mark_t(0U);
	  }
1005 1006
        | acc-sets acc-set
	  {
1007 1008 1009 1010
	    if (res.ignore_acc || $2 == -1U)
	      $$ = spot::acc_cond::mark_t(0U);
	    else
	      $$ = $1 | res.h->aut->acc().mark($2);
1011
	  }
1012

1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044
state-acc_opt:
               {
                 $$ = spot::acc_cond::mark_t(0U);
               }
             | acc-sig
               {
		 $$ = $1;
		 if (res.acc_style == Trans_Acc)
		   {
		     error(@$, "state-based acceptance used despite...");
		     error(res.props["trans-acc"],
			   "... 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...");
		     error(res.props["state-acc"],
			   "... declaration of state-based acceptance.");
		     res.acc_style = Mixed_Acc;
		   }
	       }

1045 1046 1047 1048 1049
/* 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
1050
incorrectly-unlabeled-edge: checked-state-num trans-acc_opt
1051 1052 1053 1054 1055 1056 1057
                            {
			      bdd cond = bddtrue;
			      if (!res.has_state_label)
				error(@$, "missing label for this edge "
				      "(previous edge is labeled)");
			      else
				cond = res.state_label;
1058 1059
			      res.h->aut->new_edge(res.cur_state, $1,
						   cond, $2 | res.acc_state);
1060
			    }
1061
labeled-edge: trans-label checked-state-num trans-acc_opt
1062
	      {
1063
		if (res.cur_label != bddfalse)
1064 1065
		  res.h->aut->new_edge(res.cur_state, $2,
				       res.cur_label, $3 | res.acc_state);
1066
	      }
1067
	    | trans-label state-conj-2 trans-acc_opt
1068 1069 1070 1071 1072
	      {
		error(@2, "alternation is not yet supported");
		YYABORT;
	      }

1073 1074 1075 1076 1077 1078
/* 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
1079
unlabeled-edge: checked-state-num trans-acc_opt
1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091
		{
		  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())
			{
1092
			  error(@$, "too many transitions for this state, "
1093 1094 1095 1096 1097 1098 1099 1100
				"ignoring this one");
			  cond = bddfalse;
			}
		      else
			{
			  cond = *res.cur_guard++;
			}
		    }
1101
		  if (cond != bddfalse)
1102 1103
		    res.h->aut->new_edge(res.cur_state, $1,
					 cond, $2 | res.acc_state);
1104
		}
1105
	      | state-conj-2 trans-acc_opt
1106 1107 1108 1109
		{
		  error(@1, "alternation is not yet supported");
		  YYABORT;
		}
1110 1111 1112 1113 1114
incorrectly-labeled-edge: trans-label unlabeled-edge
                          {
			    error(@1, "ignoring this label, because previous"
				  " edge has no label");
                          }
1115

1116 1117 1118 1119 1120

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

1121 1122 1123 1124 1125
dstar: dstar_type "v2" "explicit" dstar_header "---" dstar_states ENDDSTAR
     | dstar_type error ENDDSTAR
       {
	 error(@$, "failed to parse this as an ltl2dstar automaton");
       }
1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139

dstar_type: "DRA"
       {
         res.h->type = spot::parsed_aut_type::DRA;
         res.plus = 1;
         res.minus = 0;
       }
       | "DSA"
       {
	 res.h->type = spot::parsed_aut_type::DSA;
         res.plus = 0;
         res.minus = 1;
       }

1140
dstar_header: dstar_sizes
1141 1142
  {
    if (res.states < 0)
1143
      error(@1, "missing state count");
1144
    if (!res.ignore_more_acc)
1145
      error(@1, "missing acceptance-pair count");
1146
    if (res.start.empty())
1147
      error(@1, "missing start-state number");
1148
    if (!res.ignore_more_ap)
1149 1150 1151
      error(@1, "missing atomic propositions definition");

    if (res.states > 0)
1152
      {
1153 1154
	res.h->aut->new_states(res.states);;
	res.info_states.resize(res.states);
1155 1156 1157 1158
      }
    res.h->aut->prop_state_based_acc();
    res.h->aut->prop_deterministic();
    // res.h->aut->prop_complete();
1159 1160
    fill_guards(res);
    res.cur_guard = res.guards.end();
1161 1162 1163
  }

dstar_sizes:
1164
  | dstar_sizes error
1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184
  | 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
  {
1185 1186 1187 1188 1189 1190 1191 1192 1193 1194
    if (res.states < 0)
      {
	res.states = $3;
      }
    else
      {
	error(@$, "redeclaration of state count");
	if ((unsigned) res.states < $3)
	  res.states = $3;
      }
1195 1196 1197 1198 1199 1200 1201
  }
  | dstar_sizes "Start:" INT
  {
    res.start.emplace_back(@3, $3);
  }
  | dstar_sizes aps

1202
dstar_state_id: "State:" INT string_opt
1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219
  {
    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());
      }
1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236
    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;
	  }
      }

1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287
    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
  {
    std::pair<map_t::iterator, bool> i =
      res.dest_map.emplace($2, *res.cur_guard);
    if (!i.second)
      i.first->second |= *res.cur_guard;
    ++res.cur_guard;
  }

dstar_states:
1288
  | dstar_states error
1289 1290 1291 1292 1293 1294
  | dstar_states dstar_state_id dstar_state_accsig dstar_transitions
  {
    for (auto i: res.dest_map)
      res.h->aut->new_edge(res.cur_state, i.first, i.second, $3);
  }

1295 1296 1297 1298 1299
/**********************************************************************/
/*                      Rules for neverclaims                         */
/**********************************************************************/

never: "never" { res.namer = res.h->aut->create_namer<std::string>();
1300
	         res.h->aut->set_buchi();
1301
		 res.h->aut->prop_state_based_acc();
1302 1303 1304
		 res.acc_state = State_Acc;
		 res.pos_acc_sets = res.h->aut->acc().all_sets();
	       }
1305 1306 1307 1308 1309 1310
       '{' 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");
1311
	     res.h->aut->new_acc_edge(n, n, bddtrue);
1312
	   }
1313 1314 1315 1316
	 // If we aliased existing state, we have some unreachable
	 // states to remove.
	 if (res.aliased_states)
	   res.h->aut->purge_unreachable_states();
1317 1318 1319 1320
	 res.info_states.resize(res.h->aut->num_states());
	 // Pretend that we have declared all states.
	 for (auto& p: res.info_states)
	   p.declared = true;
1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341
       }

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
1342 1343 1344 1345 1346 1347 1348 1349 1350
    {
      unsigned n = res.namer->new_state(*$1);
      if (res.start.empty())
	{
	  // The first state is initial.
	  res.start.emplace_back(@$, n);
	}
      $$ = $1;
    }
1351 1352
  | nc-ident-list nc-one-ident
    {
1353 1354
      res.aliased_states |=
	res.namer->alias_state(res.namer->get_state(*$1), *$2);
1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383
      // 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;

1384 1385
      auto acc = !strncmp("accept", $1->c_str(), 6) ?
	res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U);
1386
      res.namer->new_edge(*$1, *$1, bddtrue, acc);
1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398
      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);
1399
	  res.namer->new_edge(*$1, *p.second, c, acc);
1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414