parsetl.yy 32.3 KB
Newer Older
1
/* -*- coding: utf-8 -*-
2
3
** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
** de Recherche et Développement de l'Epita (LRDE).
4
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
5
6
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
** Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
**
** 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
12
** the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
** (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
21
** along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22
*/
23
24
25
%language "C++"
%locations
%defines
26
%name-prefix "tlyy"
27
28
%debug
%error-verbose
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29
%expect 0
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
%lex-param { spot::parse_error_list& error_list }
31
%define api.location.type "spot::location"
32
33
34

%code requires
{
35
#include <string>
36
#include <sstream>
37
#include "tl/parse.hh"
38
39
#include "tl/formula.hh"
#include "tl/print.hh"
40
41

  struct minmax_t { unsigned min, max; };
42
}
43

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
44
45
46
%parse-param {spot::parse_error_list &error_list}
%parse-param {spot::environment &parse_environment}
%parse-param {spot::formula &result}
47
48
49
%union
{
  std::string* str;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
50
  const spot::fnode* ltl;
51
52
  unsigned num;
  minmax_t minmax;
53
54
}

55
%code {
56
/* parsetl.hh and parsedecl.hh include each other recursively.
57
58
59
   We mut ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
60
using namespace spot;
61

62
#define missing_right_op_msg(op, str)		\
63
64
  error_list.emplace_back(op,			\
    "missing right operand for \"" str "\"");
65
66
67
68
69

#define missing_right_op(res, op, str)		\
  do						\
    {						\
      missing_right_op_msg(op, str);		\
70
      res = fnode::ff();		\
71
    }						\
72
73
  while (0);

74
// right is missing, so complain and use left.
75
76
77
#define missing_right_binop(res, left, op, str)	\
  do						\
    {						\
78
79
      missing_right_op_msg(op, str);		\
      res = left;				\
80
81
82
    }						\
  while (0);

83
84
85
86
87
88
89
90
91
// right is missing, so complain and use false.
#define missing_right_binop_hard(res, left, op, str)	\
  do							\
    {							\
      left->destroy();					\
      missing_right_op(res, op, str);			\
    }							\
  while (0);

92
93
  enum parser_type { parser_ltl, parser_bool, parser_sere };

94
  static formula
95
  try_recursive_parse(const std::string& str,
96
		      const spot::location& location,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
97
		      spot::environment& env,
98
		      bool debug,
99
		      parser_type type,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
100
		      spot::parse_error_list& error_list)
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
    {
      // We want to parse a U (b U c) as two until operators applied
      // to the atomic propositions a, b, and c.  We also want to
      // parse a U (b == c) as one until operator applied to the
      // atomic propositions "a" and "b == c".  The only problem is
      // that we do not know anything about "==" or in general about
      // the syntax of atomic proposition of our users.
      //
      // To support that, the lexer will return "b U c" and "b == c"
      // as PAR_BLOCK tokens.  We then try to parse such tokens
      // recursively.  If, as in the case of "b U c", the block is
      // successfully parsed as a formula, we return this formula.
      // Otherwise, we convert the string into an atomic proposition
      // (it's up to the environment to check the syntax of this
      // proposition, and maybe reject it).
116
117
118

      if (str.empty())
	{
119
	  error_list.emplace_back(location, "unexpected empty block");
120
	  return nullptr;
121
122
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
123
      spot::parse_error_list suberror;
124
      formula f;
125
126
127
      switch (type)
	{
	case parser_sere:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128
	  f = spot::parse_infix_sere(str, suberror, env, debug, true);
129
130
	  break;
	case parser_bool:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
131
	  f = spot::parse_infix_boolean(str, suberror, env, debug, true);
132
133
	  break;
	case parser_ltl:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
134
	  f = spot::parse_infix_psl(str, suberror, env, debug, true);
135
136
	  break;
	}
137
138
139
140
141
142
143
144
145
146
147
148

      if (suberror.empty())
	return f;

      f = env.require(str);
      if (!f)
	{
	  std::string s = "atomic proposition `";
	  s += str;
	  s += "' rejected by environment `";
	  s += env.name();
	  s += "'";
149
	  error_list.emplace_back(location, s);
150
151
152
	}
      return f;
    }
153
}
154
155


156
/* All tokens.  */
157

158
%token START_LTL "LTL start marker"
159
%token START_LBT "LBT start marker"
160
%token START_SERE "SERE start marker"
161
%token START_BOOL "BOOLEAN start marker"
162
%token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
163
164
165
%token <str> PAR_BLOCK "(...) block"
%token <str> BRA_BLOCK "{...} block"
%token <str> BRA_BANG_BLOCK "{...}! block"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
166
%token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace"
167
%token BRACE_BANG_CLOSE "closing brace-bang"
168
169
%token OP_OR "or operator" OP_XOR "xor operator"
%token OP_AND "and operator" OP_SHORT_AND "short and operator"
170
171
%token OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator"
%token OP_U "until operator" OP_R "release operator"
172
%token OP_W "weak until operator" OP_M "strong release operator"
173
%token OP_F "sometimes operator" OP_G "always operator"
174
175
%token OP_X "next operator" OP_NOT "not operator"
%token OP_STAR "star operator" OP_BSTAR "bracket star operator"
176
%token OP_BFSTAR "bracket fusion-star operator"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
%token OP_PLUS "plus operator"
178
%token OP_FPLUS "fusion-plus operator"
179
%token OP_STAR_OPEN "opening bracket for star operator"
180
%token OP_FSTAR_OPEN "opening bracket for fusion-star operator"
181
%token OP_EQUAL_OPEN "opening bracket for equal operator"
182
%token OP_GOTO_OPEN "opening bracket for goto operator"
183
184
%token OP_SQBKT_CLOSE "closing bracket"
%token <num> OP_SQBKT_NUM "number for square bracket operator"
185
%token OP_UNBOUNDED "unbounded mark"
186
%token OP_SQBKT_SEP "separator for square bracket operator"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
187
188
%token OP_UCONCAT "universal concat operator"
%token OP_ECONCAT "existential concat operator"
189
190
%token OP_UCONCAT_NONO "universal non-overlapping concat operator"
%token OP_ECONCAT_NONO "existential non-overlapping concat operator"
191
%token <str> ATOMIC_PROP "atomic proposition"
192
%token OP_CONCAT "concat operator" OP_FUSION "fusion operator"
193
%token CONST_TRUE "constant true" CONST_FALSE "constant false"
194
%token END_OF_INPUT "end of formula"
195
%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
196

197
/* Priorities.  */
198

199
/* Low priority SERE-LTL binding operator. */
200
%nonassoc OP_UCONCAT OP_ECONCAT OP_UCONCAT_NONO OP_ECONCAT_NONO
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
201

202
203
%left OP_CONCAT
%left OP_FUSION
204

205
/* Logical operators.  */
206
%right OP_IMPLIES OP_EQUIV
207
208
%left OP_OR
%left OP_XOR
209
%left OP_AND OP_SHORT_AND
210

211
212
213
214
215
216
/* OP_STAR can be used as an AND when occurring in some LTL formula in
   Wring's syntax (so it has to be close to OP_AND), and as a Kleen
   Star in SERE (so it has to be close to OP_BSTAR -- luckily
   U/R/M/W/F/G/X are not used in SERE). */
%left OP_STAR

217
/* LTL operators.  */
218
%right OP_U OP_R OP_M OP_W
219
220
221
%nonassoc OP_F OP_G
%nonassoc OP_X

222
/* High priority regex operator. */
223
224
225
%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS
          OP_BFSTAR OP_FSTAR_OPEN OP_FPLUS
          OP_EQUAL_OPEN OP_GOTO_OPEN
226

227
228
229
/* Not has the most important priority (after Wring's `=0' and `=1',
   but as those can only attach to atomic proposition, they do not
   need any precedence).  */
230
%nonassoc OP_NOT
231

232
%type <ltl> subformula booleanatom sere lbtformula boolformula
233
%type <ltl> bracedsere parenthesedsubformula
234
%type <minmax> starargs fstarargs equalargs sqbracketargs gotoargs
235

236
237
%destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl>
238

239
%printer { debug_stream() << *$$; } <str>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240
241
%printer { print_psl(debug_stream(), formula($$)); } <ltl>
%printer { print_sere(debug_stream(), formula($$)); } sere bracedsere
242
243
%printer { debug_stream() << $$; } <num>
%printer { debug_stream() << $$.min << ".." << $$.max; } <minmax>
244

245
%%
246
result:       START_LTL subformula END_OF_INPUT
247
248
              {
		result = formula($2);
249
250
		YYACCEPT;
	      }
251
252
	    | START_LTL enderror
	      {
253
		result = nullptr;
254
255
		YYABORT;
	      }
256
257
	    | START_LTL subformula enderror
	      {
258
		result = formula($2);
259
260
261
262
		YYACCEPT;
	      }
	    | START_LTL emptyinput
              { YYABORT; }
263
            | START_BOOL boolformula END_OF_INPUT
264
265
	      {
		result = formula($2);
266
267
268
269
		YYACCEPT;
	      }
	    | START_BOOL enderror
	      {
270
		result = nullptr;
271
272
273
274
		YYABORT;
	      }
	    | START_BOOL boolformula enderror
	      {
275
		result = formula($2);
276
277
278
279
		YYACCEPT;
	      }
	    | START_BOOL emptyinput
              { YYABORT; }
280
            | START_SERE sere END_OF_INPUT
281
282
	      {
		result = formula($2);
283
284
		YYACCEPT;
	      }
285
	    | START_SERE enderror
286
	      {
287
		result = nullptr;
288
289
		YYABORT;
	      }
290
	    | START_SERE sere enderror
291
	      {
292
		result = formula($2);
293
294
		YYACCEPT;
	      }
295
	    | START_SERE emptyinput
296
              { YYABORT; }
297
            | START_LBT lbtformula END_OF_INPUT
298
299
	      {
		result = formula($2);
300
301
302
303
		YYACCEPT;
	      }
	    | START_LBT enderror
	      {
304
		result = nullptr;
305
306
307
308
		YYABORT;
	      }
	    | START_LBT lbtformula enderror
	      {
309
		result = formula($2);
310
311
312
313
		YYACCEPT;
	      }
	    | START_LBT emptyinput
              { YYABORT; }
314
315
316

emptyinput: END_OF_INPUT
              {
317
		error_list.emplace_back(@$, "empty input");
318
		result = nullptr;
319
320
321
322
	      }

enderror: error END_OF_INPUT
              {
323
		error_list.emplace_back(@1, "ignoring trailing garbage");
324
	      }
325

326

327
328
OP_SQBKT_SEP_unbounded: OP_SQBKT_SEP | OP_SQBKT_SEP OP_UNBOUNDED
OP_SQBKT_SEP_opt: | OP_SQBKT_SEP_unbounded
329
330
error_opt: | error

331
/* for [*i..j] and [=i..j] */
332
333
sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
              { $$.min = $1; $$.max = $3; }
334
	     | OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
335
              { $$.min = $1; $$.max = fnode::unbounded(); }
336
337
338
	     | OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
              { $$.min = 0U; $$.max = $2; }
	     | OP_SQBKT_SEP_opt OP_SQBKT_CLOSE
339
              { $$.min = 0U; $$.max = fnode::unbounded(); }
340
341
342
	     | OP_SQBKT_NUM OP_SQBKT_CLOSE
              { $$.min = $$.max = $1; }

343
344
345
/* [->i..j] has default values that are different than [*] and [=]. */
gotoargs: OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
           { $$.min = $2; $$.max = $4; }
346
	  | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
347
           { $$.min = $2; $$.max = fnode::unbounded(); }
348
349
	  | OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
           { $$.min = 1U; $$.max = $3; }
350
	  | OP_GOTO_OPEN OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
351
           { $$.min = 1U; $$.max = fnode::unbounded(); }
352
353
354
355
356
	  | OP_GOTO_OPEN OP_SQBKT_CLOSE
           { $$.min = $$.max = 1U; }
	  | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_CLOSE
           { $$.min = $$.max = $2; }
	  | OP_GOTO_OPEN error OP_SQBKT_CLOSE
357
           { error_list.emplace_back(@$, "treating this goto block as [->]");
358
359
             $$.min = $$.max = 1U; }
          | OP_GOTO_OPEN error_opt END_OF_INPUT
360
361
	   { error_list.
	       emplace_back(@$, "missing closing bracket for goto operator");
362
363
	     $$.min = $$.max = 0U; }

364
365
366
kleen_star: OP_STAR | OP_BSTAR

starargs: kleen_star
367
            { $$.min = 0U; $$.max = fnode::unbounded(); }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
        | OP_PLUS
369
	    { $$.min = 1U; $$.max = fnode::unbounded(); }
370
371
372
	| OP_STAR_OPEN sqbracketargs
	    { $$ = $2; }
	| OP_STAR_OPEN error OP_SQBKT_CLOSE
373
            { error_list.emplace_back(@$, "treating this star block as [*]");
374
              $$.min = 0U; $$.max = fnode::unbounded(); }
375
        | OP_STAR_OPEN error_opt END_OF_INPUT
376
	    { error_list.emplace_back(@$, "missing closing bracket for star");
377
378
	      $$.min = $$.max = 0U; }

379
fstarargs: OP_BFSTAR
380
            { $$.min = 0U; $$.max = fnode::unbounded(); }
381
        | OP_FPLUS
382
	    { $$.min = 1U; $$.max = fnode::unbounded(); }
383
384
385
386
387
	| OP_FSTAR_OPEN sqbracketargs
	    { $$ = $2; }
	| OP_FSTAR_OPEN error OP_SQBKT_CLOSE
            { error_list.emplace_back
		(@$, "treating this fusion-star block as [:*]");
388
              $$.min = 0U; $$.max = fnode::unbounded(); }
389
390
391
392
393
        | OP_FSTAR_OPEN error_opt END_OF_INPUT
	    { error_list.emplace_back
		(@$, "missing closing bracket for fusion-star");
	      $$.min = $$.max = 0U; }

394
395
396
equalargs: OP_EQUAL_OPEN sqbracketargs
	    { $$ = $2; }
	| OP_EQUAL_OPEN error OP_SQBKT_CLOSE
397
            { error_list.emplace_back(@$, "treating this equal block as [*]");
398
              $$.min = 0U; $$.max = fnode::unbounded(); }
399
        | OP_EQUAL_OPEN error_opt END_OF_INPUT
400
401
	    { error_list.
		emplace_back(@$, "missing closing bracket for equal operator");
402
403
	      $$.min = $$.max = 0U; }

404

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
405
booleanatom: ATOMIC_PROP
406
	      {
407
		$$ = parse_environment.require(*$1).to_node_();
408
409
410
411
412
		if (! $$)
		  {
		    std::string s = "unknown atomic proposition `";
		    s += *$1;
		    s += "' in environment `";
413
		    s += parse_environment.name();
414
		    s += "'";
415
		    error_list.emplace_back(@1, s);
416
		    delete $1;
417
418
419
		    YYERROR;
		  }
		else
420
		  delete $1;
421
	      }
422
423
	    | ATOMIC_PROP OP_POST_POS
	      {
424
		$$ = parse_environment.require(*$1).to_node_();
425
426
427
428
429
430
431
		if (! $$)
		  {
		    std::string s = "unknown atomic proposition `";
		    s += *$1;
		    s += "' in environment `";
		    s += parse_environment.name();
		    s += "'";
432
		    error_list.emplace_back(@1, s);
433
434
435
436
437
438
439
440
		    delete $1;
		    YYERROR;
		  }
		else
		  delete $1;
	      }
	    | ATOMIC_PROP OP_POST_NEG
	      {
441
		$$ = parse_environment.require(*$1).to_node_();
442
443
444
445
446
447
448
		if (! $$)
		  {
		    std::string s = "unknown atomic proposition `";
		    s += *$1;
		    s += "' in environment `";
		    s += parse_environment.name();
		    s += "'";
449
		    error_list.emplace_back(@1, s);
450
451
452
453
454
		    delete $1;
		    YYERROR;
		  }
		else
		  delete $1;
455
		$$ = fnode::unop(op::Not, $$);
456
	      }
457
	    | CONST_TRUE
458
	      { $$ = fnode::tt(); }
459
	    | CONST_FALSE
460
	      { $$ = fnode::ff(); }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
461

462
463
sere: booleanatom
            | OP_NOT sere
464
465
466
	      {
		if ($2->is_boolean())
		  {
467
		    $$ = fnode::unop(op::Not, $2);
468
469
470
		  }
		else
		  {
471
		    error_list.emplace_back(@2,
472
                       "not a boolean expression: inside a SERE `!' can only "
473
474
                       "be applied to a Boolean expression");
		    error_list.emplace_back(@$, "treating this block as false");
475
		    $2->destroy();
476
		    $$ = fnode::ff();
477
478
		  }
	      }
479
            | bracedsere
480
481
	    | PAR_BLOCK
              {
482
483
484
485
		$$ =
		  try_recursive_parse(*$1, @1, parse_environment,
				      debug_level(), parser_sere, error_list)
		  .to_node_();
486
487
488
489
		delete $1;
		if (!$$)
		  YYERROR;
	      }
490
	    | PAR_OPEN sere PAR_CLOSE
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
491
492
	      { $$ = $2; }
	    | PAR_OPEN error PAR_CLOSE
493
494
495
	      { error_list.
		  emplace_back(@$,
			       "treating this parenthetical block as false");
496
		$$ = fnode::ff();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
497
	      }
498
	    | PAR_OPEN sere END_OF_INPUT
499
	      { error_list.emplace_back(@1 + @2, "missing closing parenthesis");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
500
501
502
		$$ = $2;
	      }
	    | PAR_OPEN error END_OF_INPUT
503
	      { error_list.emplace_back(@$,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
504
                    "missing closing parenthesis, "
505
		    "treating this parenthetical block as false");
506
		$$ = fnode::ff();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
507
	      }
508
	    | sere OP_AND sere
509
	      { $$ = fnode::multop(op::AndRat, {$1, $3}); }
510
	    | sere OP_AND error
511
512
	      { missing_right_binop($$, $1, @2,
				    "length-matching and operator"); }
513
	    | sere OP_SHORT_AND sere
514
	      { $$ = fnode::multop(op::AndNLM, {$1, $3}); }
515
	    | sere OP_SHORT_AND error
516
517
              { missing_right_binop($$, $1, @2,
                                    "non-length-matching and operator"); }
518
	    | sere OP_OR sere
519
	      { $$ = fnode::multop(op::OrRat, {$1, $3}); }
520
	    | sere OP_OR error
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
521
              { missing_right_binop($$, $1, @2, "or operator"); }
522
	    | sere OP_CONCAT sere
523
	      { $$ = fnode::multop(op::Concat, {$1, $3}); }
524
	    | sere OP_CONCAT error
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
525
              { missing_right_binop($$, $1, @2, "concat operator"); }
526
	    | sere OP_FUSION sere
527
	      { $$ = fnode::multop(op::Fusion, {$1, $3}); }
528
	    | sere OP_FUSION error
529
              { missing_right_binop($$, $1, @2, "fusion operator"); }
530
531
532
533
534
535
536
	    | starargs
	      {
		if ($1.max < $1.min)
		  {
		    error_list.emplace_back(@1, "reversed range");
		    std::swap($1.max, $1.min);
		  }
537
		$$ = fnode::bunop(op::Star, fnode::tt(), $1.min, $1.max);
538
	      }
539
	    | sere starargs
540
541
542
	      {
		if ($2.max < $2.min)
		  {
543
		    error_list.emplace_back(@2, "reversed range");
544
545
		    std::swap($2.max, $2.min);
		  }
546
		$$ = fnode::bunop(op::Star, $1, $2.min, $2.max);
547
	      }
548
	    | sere fstarargs
549
	      {
550
		if ($2.max < $2.min)
551
		  {
552
553
		    error_list.emplace_back(@2, "reversed range");
		    std::swap($2.max, $2.min);
554
		  }
555
		$$ = fnode::bunop(op::FStar, $1, $2.min, $2.max);
556
	      }
557
	    | sere equalargs
558
	      {
559
560
		if ($2.max < $2.min)
		  {
561
		    error_list.emplace_back(@2, "reversed range");
562
563
		    std::swap($2.max, $2.min);
		  }
564
		if ($1->is_boolean())
565
		  {
566
567
		    $$ = formula::sugar_equal(formula($1),
					      $2.min, $2.max).to_node_();
568
569
570
		  }
		else
		  {
571
		    error_list.emplace_back(@1,
572
				"not a boolean expression: [=...] can only "
573
574
575
				"be applied to a Boolean expression");
		    error_list.emplace_back(@$,
				"treating this block as false");
576
		    $1->destroy();
577
		    $$ = fnode::ff();
578
579
		  }
	      }
580
	    | sere gotoargs
581
	      {
582
583
		if ($2.max < $2.min)
		  {
584
		    error_list.emplace_back(@2, "reversed range");
585
586
		    std::swap($2.max, $2.min);
		  }
587
		if ($1->is_boolean())
588
		  {
589
590
		    $$ = formula::sugar_goto(formula($1),
					     $2.min, $2.max).to_node_();
591
592
593
		  }
		else
		  {
594
		    error_list.emplace_back(@1,
595
				"not a boolean expression: [->...] can only "
596
597
598
				"be applied to a Boolean expression");
		    error_list.emplace_back(@$,
				"treating this block as false");
599
		    $1->destroy();
600
		    $$ = fnode::ff();
601
602
		  }
	      }
603
	    | sere OP_XOR sere
604
605
606
	      {
		if ($1->is_boolean() && $3->is_boolean())
		  {
607
		    $$ = fnode::binop(op::Xor, $1, $3);
608
609
610
611
612
		  }
		else
		  {
		    if (!$1->is_boolean())
		      {
613
			error_list.emplace_back(@1,
614
                         "not a boolean expression: inside SERE `<->' can only "
615
                         "be applied to Boolean expressions");
616
617
618
                      }
		    if (!$3->is_boolean())
		      {
619
			error_list.emplace_back(@3,
620
                         "not a boolean expression: inside SERE `<->' can only "
621
                         "be applied to Boolean expressions");
622
                      }
623
		    error_list.emplace_back(@$, "treating this block as false");
624
625
		    $1->destroy();
		    $3->destroy();
626
		    $$ = fnode::ff();
627
628
		  }
	      }
629
	    | sere OP_XOR error
630
	      { missing_right_binop($$, $1, @2, "xor operator"); }
631
	    | sere OP_IMPLIES sere
632
633
634
	      {
		if ($1->is_boolean())
		  {
635
		    $$ = fnode::binop(op::Implies, $1, $3);
636
637
638
639
640
		  }
		else
		  {
		    if (!$1->is_boolean())
		      {
641
			error_list.emplace_back(@1,
642
                         "not a boolean expression: inside SERE `->' can only "
643
                         "be applied to a Boolean expression");
644
                      }
645
		    error_list.emplace_back(@$, "treating this block as false");
646
647
		    $1->destroy();
		    $3->destroy();
648
		    $$ = fnode::ff();
649
650
		  }
	      }
651
	    | sere OP_IMPLIES error
652
	      { missing_right_binop($$, $1, @2, "implication operator"); }
653
	    | sere OP_EQUIV sere
654
655
656
	      {
		if ($1->is_boolean() && $3->is_boolean())
		  {
657
		    $$ = fnode::binop(op::Equiv, $1, $3);
658
659
660
661
662
		  }
		else
		  {
		    if (!$1->is_boolean())
		      {
663
			error_list.emplace_back(@1,
664
                         "not a boolean expression: inside SERE `<->' can only "
665
                         "be applied to Boolean expressions");
666
667
668
                      }
		    if (!$3->is_boolean())
		      {
669
			error_list.emplace_back(@3,
670
                         "not a boolean expression: inside SERE `<->' can only "
671
                         "be applied to Boolean expressions");
672
                      }
673
		    error_list.emplace_back(@$, "treating this block as false");
674
		    $1->destroy();
675
		    $3->destroy();
676
		    $$ = fnode::ff();
677
678
		  }
	      }
679
	    | sere OP_EQUIV error
680
	      { missing_right_binop($$, $1, @2, "equivalent operator"); }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
681

682
bracedsere: BRACE_OPEN sere BRACE_CLOSE
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
683
              { $$ = $2; }
684
            | BRACE_OPEN sere error BRACE_CLOSE
685
	      { error_list.emplace_back(@3, "ignoring this");
686
687
		$$ = $2;
	      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
688
            | BRACE_OPEN error BRACE_CLOSE
689
690
	      { error_list.emplace_back(@$,
					"treating this brace block as false");
691
		$$ = fnode::ff();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
692
	      }
693
            | BRACE_OPEN sere END_OF_INPUT
694
695
	      { error_list.emplace_back(@1 + @2,
					"missing closing brace");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
696
697
		$$ = $2;
	      }
698
	    | BRACE_OPEN sere error END_OF_INPUT
699
700
	      { error_list. emplace_back(@3,
                  "ignoring trailing garbage and missing closing brace");
701
702
		$$ = $2;
	      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
703
	    | BRACE_OPEN error END_OF_INPUT
704
	      { error_list.emplace_back(@$,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
705
                    "missing closing brace, "
706
		    "treating this brace block as false");
707
		$$ = fnode::ff();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
708
	      }
709
710
711
            | BRA_BLOCK
              {
		$$ = try_recursive_parse(*$1, @1, parse_environment,
712
					 debug_level(),
713
					 parser_sere, error_list).to_node_();
714
715
716
717
		delete $1;
		if (!$$)
		  YYERROR;
	      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
718

719
720
721
parenthesedsubformula: PAR_BLOCK
              {
		$$ = try_recursive_parse(*$1, @1, parse_environment,
722
723
					 debug_level(), parser_ltl, error_list)
		  .to_node_();
724
725
726
727
728
		delete $1;
		if (!$$)
		  YYERROR;
	      }
            | PAR_OPEN subformula PAR_CLOSE
729
	      { $$ = $2; }
730
	    | PAR_OPEN subformula error PAR_CLOSE
731
	      { error_list.emplace_back(@3, "ignoring this");
732
733
		$$ = $2;
	      }
734
	    | PAR_OPEN error PAR_CLOSE
735
736
	      { error_list.emplace_back(@$,
		 "treating this parenthetical block as false");
737
		$$ = fnode::ff();
738
	      }
739
	    | PAR_OPEN subformula END_OF_INPUT
740
	      { error_list.emplace_back(@1 + @2, "missing closing parenthesis");
741
		$$ = $2;
742
	      }
743
	    | PAR_OPEN subformula error END_OF_INPUT
744
745
	      { error_list.emplace_back(@3,
                "ignoring trailing garbage and missing closing parenthesis");
746
747
		$$ = $2;
	      }
748
	    | PAR_OPEN error END_OF_INPUT
749
	      { error_list.emplace_back(@$,
750
                    "missing closing parenthesis, "
751
		    "treating this parenthetical block as false");
752
		$$ = fnode::ff();
753
	      }
754
755


756
757
758
759
boolformula: booleanatom
            | PAR_BLOCK
              {
		$$ = try_recursive_parse(*$1, @1, parse_environment,
760
761
					 debug_level(), parser_bool, error_list)
		  .to_node_();
762
763
764
765
766
767
768
		delete $1;
		if (!$$)
		  YYERROR;
	      }
            | PAR_OPEN boolformula PAR_CLOSE
	      { $$ = $2; }
	    | PAR_OPEN boolformula error PAR_CLOSE
769
	      { error_list.emplace_back(@3, "ignoring this");
770
771
772
		$$ = $2;
	      }
	    | PAR_OPEN error PAR_CLOSE
773
774
	      { error_list.emplace_back(@$,
		 "treating this parenthetical block as false");
775
		$$ = fnode::ff();
776
777
	      }
	    | PAR_OPEN boolformula END_OF_INPUT
778
779
	      { error_list.emplace_back(@1 + @2,
					"missing closing parenthesis");
780
781
782
		$$ = $2;
	      }
	    | PAR_OPEN boolformula error END_OF_INPUT
783
784
	      { error_list.emplace_back(@3,
                "ignoring trailing garbage and missing closing parenthesis");
785
786
787
		$$ = $2;
	      }
	    | PAR_OPEN error END_OF_INPUT
788
	      { error_list.emplace_back(@$,
789
                    "missing closing parenthesis, "
790
		    "treating this parenthetical block as false");
791
		$$ = fnode::ff();
792
793
	      }
	    | boolformula OP_AND boolformula
794
	      { $$ = fnode::multop(op::And, {$1, $3}); }
795
796
797
	    | boolformula OP_AND error
              { missing_right_binop($$, $1, @2, "and operator"); }
	    | boolformula OP_SHORT_AND boolformula
798
	      { $$ = fnode::multop(op::And, {$1, $3}); }
799
800
801
	    | boolformula OP_SHORT_AND error
              { missing_right_binop($$, $1, @2, "and operator"); }
	    | boolformula OP_STAR boolformula
802
	      { $$ = fnode::multop(op::And, {$1, $3}); }
803
804
805
	    | boolformula OP_STAR error
              { missing_right_binop($$, $1, @2, "and operator"); }
	    | boolformula OP_OR boolformula
806
	      { $$ = fnode::multop(op::Or, {$1, $3}); }
807
808
809
	    | boolformula OP_OR error
              { missing_right_binop($$, $1, @2, "or operator"); }
	    | boolformula OP_XOR boolformula
810
	      { $$ = fnode::binop(op::Xor, $1, $3); }
811
812
813
	    | boolformula OP_XOR error
	      { missing_right_binop($$, $1, @2, "xor operator"); }
	    | boolformula OP_IMPLIES boolformula
814
	      { $$ = fnode::binop(op::Implies, $1, $3); }
815
816
817
	    | boolformula OP_IMPLIES error
	      { missing_right_binop($$, $1, @2, "implication operator"); }
	    | boolformula OP_EQUIV boolformula
818
	      { $$ = fnode::binop(op::Equiv, $1, $3); }
819
820
821
	    | boolformula OP_EQUIV error
	      { missing_right_binop($$, $1, @2, "equivalent operator"); }
	    | OP_NOT boolformula
822
	      { $$ = fnode::unop(op::Not, $2); }
823
824
825
	    | OP_NOT error
	      { missing_right_op($$, @1, "not operator"); }

826
827
subformula: booleanatom
            | parenthesedsubformula
828
	    | subformula OP_AND subformula
829
              { $$ = fnode::multop(op::And, {$1, $3}); }
830
	    | subformula OP_AND error
831
              { missing_right_binop($$, $1, @2, "and operator"); }
832
	    | subformula OP_SHORT_AND subformula
833
	      { $$ = fnode::multop(op::And, {$1, $3}); }
834
835
	    | subformula OP_SHORT_AND error
              { missing_right_binop($$, $1, @2, "and operator"); }
836
	    | subformula OP_STAR subformula
837
	      { $$ = fnode::multop(op::And, {$1, $3}); }
838
839
	    | subformula OP_STAR error
              { missing_right_binop($$, $1, @2, "and operator"); }
840
	    | subformula OP_OR subformula
841
	      { $$ = fnode::multop(op::Or, {$1, $3}); }
842
	    | subformula OP_OR error
843
              { missing_right_binop($$, $1, @2, "or operator"); }
844
	    | subformula OP_XOR subformula
845
 	      { $$ = fnode::binop(op::Xor, $1, $3); }
846
	    | subformula OP_XOR error
847
	      { missing_right_binop($$, $1, @2, "xor operator"); }
848
	    | subformula OP_IMPLIES subformula
849
	      { $$ = fnode::binop(op::Implies, $1, $3); }
850
	    | subformula OP_IMPLIES error
851
	      { missing_right_binop($$, $1, @2, "implication operator"); }
852
	    | subformula OP_EQUIV subformula
853
	      { $$ = fnode::binop(op::Equiv, $1, $3); }
854
	    | subformula OP_EQUIV error
855
	      { missing_right_binop($$, $1, @2, "equivalent operator"); }
856
	    | subformula OP_U subformula
857
	      { $$ = fnode::binop(op::U, $1, $3); }
858
	    | subformula OP_U error
859
	      { missing_right_binop($$, $1, @2, "until operator"); }
860
	    | subformula OP_R subformula
861
	      { $$ = fnode::binop(op::R, $1, $3); }
862
	    | subformula OP_R error
863
	      { missing_right_binop($$, $1, @2, "release operator"); }
864
	    | subformula OP_W subformula
865
	      { $$ = fnode::binop(op::W, $1, $3); }
866
867
868
	    | subformula OP_W error
	      { missing_right_binop($$, $1, @2, "weak until operator"); }
	    | subformula OP_M subformula
869
	      { $$ = fnode::binop(op::M, $1, $3); }
870
871
	    | subformula OP_M error
	      { missing_right_binop($$, $1, @2, "strong release operator"); }
872
	    | OP_F subformula
873
	      { $$ = fnode::unop(op::F, $2); }