eltlparse.yy 13.2 KB
Newer Older
1
/* -*- coding: utf-8 -*-
2
3
** Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
** de Recherche et Développement de l'Epita (LRDE).
4
5
6
7
8
**
** 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
9
** the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
** (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
18
** along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
20
21
22
23
24
25
*/
%language "C++"
%locations
%defines
%name-prefix "eltlyy"
%debug
%error-verbose
26
%define api.location.type "spot::location"
27
28
29
30
31
32
33

%code requires
{
#include <string>
#include <sstream>
#include <limits>
#include <cerrno>
34
#include <algorithm>
35
36
#include "public.hh"
#include "ltlast/allnodes.hh"
37
#include "ltlast/formula_tree.hh"
38
39
40
41
42

namespace spot
{
  namespace eltl
  {
43
44
    typedef std::map<std::string, nfa::ptr> nfamap;

45
46
47
48
49
    /// The following parser allows one to define aliases of automaton
    /// operators such as: F=U(true,$0). Internally it's handled by
    /// creating a small AST associated with each alias in order to
    /// instanciate the right automatop after: U(constant(1), AP(f))
    /// for the formula F(f).
50
    typedef std::map<std::string, formula_tree::node_ptr> aliasmap;
51
52

    /// Implementation details for error handling.
53
54
55
56
57
    struct parse_error_list_t
    {
      parse_error_list list_;
      std::string file_;
    };
58
59
60
  }
}
}
61

62
63
64
65
%parse-param {spot::eltl::nfamap& nmap}
%parse-param {spot::eltl::aliasmap& amap}
%parse-param {spot::eltl::parse_error_list_t &pe}
%parse-param {spot::ltl::environment &parse_environment}
66
%parse-param {const spot::ltl::formula* &result}
67
68
%lex-param {spot::eltl::parse_error_list_t &pe}
%expect 0
69

70
71
72
73
74
75
%union
{
  int ival;
  std::string* sval;
  spot::ltl::nfa* nval;
  spot::ltl::automatop::vec* aval;
76
  const spot::ltl::formula* fval;
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

  /// To handle aliases.
  spot::ltl::formula_tree::node* pval;
  spot::ltl::formula_tree::node_nfa* bval;
}

%code {
/* ltlparse.hh and parsedecl.hh include each other recursively.
   We mut ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
using namespace spot::eltl;
using namespace spot::ltl;

namespace spot
{
  namespace eltl
  {
95
    using namespace spot::ltl::formula_tree;
96

97
98
99
100
101
    /// Alias an existing alias, as in Strong=G(F($0))->G(F($1)),
    /// where F is an alias.
    ///
    /// \param ap The original alias.
    /// \param v The arguments of the new alias.
102
103
    static node_ptr
    realias(const node_ptr ap, std::vector<node_ptr> v)
104
    {
105
106
107
108
109
      if (node_atomic* a = dynamic_cast<node_atomic*>(ap.get())) // Do it.
    	return a->i < 0 ? ap : v.at(a->i);

      // Traverse the tree.
      if (node_unop* a = dynamic_cast<node_unop*>(ap.get()))
110
      {
111
112
113
114
    	node_unop* res = new node_unop;
	res->op = a->op;
    	res->child = realias(a->child, v);
    	return node_ptr(res);
115
      }
116
      if (node_nfa* a = dynamic_cast<node_nfa*>(ap.get()))
117
      {
118
119
120
121
122
123
    	node_nfa* res = new node_nfa;
    	std::vector<node_ptr>::const_iterator i = a->children.begin();
    	while (i != a->children.end())
    	  res->children.push_back(realias(*i++, v));
    	res->nfa = a->nfa;
    	return node_ptr(res);
124
      }
125
      if (node_binop* a = dynamic_cast<node_binop*>(ap.get()))
126
      {
127
128
129
130
131
    	node_binop* res = new node_binop;
    	res->op = a->op;
    	res->lhs = realias(a->lhs, v);
    	res->rhs = realias(a->rhs, v);
    	return node_ptr(res);
132
      }
133
      if (node_multop* a = dynamic_cast<node_multop*>(ap.get()))
134
      {
135
136
137
138
139
    	node_multop* res = new node_multop;
    	res->op = a->op;
    	res->lhs = realias(a->lhs, v);
    	res->rhs = realias(a->rhs, v);
    	return node_ptr(res);
140
      }
141
      SPOT_UNREACHABLE();
142
    }
143
144
145
  }
}

146
147
#define PARSE_ERROR(Loc, Msg)				\
  pe.list_.push_back					\
148
    (parse_error(Loc, spair(pe.file_, Msg)))
149
150
151

#define CHECK_EXISTING_NMAP(Loc, Ident)			\
  {							\
152
    nfamap::const_iterator i = nmap.find(*Ident);	\
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
    if (i == nmap.end())				\
    {							\
      std::string s = "unknown automaton operator `";	\
      s += *Ident;					\
      s += "'";						\
      PARSE_ERROR(Loc, s);				\
      delete Ident;					\
      YYERROR;						\
    }							\
  }

#define CHECK_ARITY(Loc, Ident, A1, A2)			\
  {							\
    if (A1 != A2)					\
    {							\
      std::ostringstream oss1;				\
      oss1 << A1;					\
      std::ostringstream oss2;				\
      oss2 << A2;					\
							\
      std::string s(*Ident);				\
      s += " is used with ";				\
      s += oss1.str();					\
      s += " arguments, but has an arity of ";		\
      s += oss2.str();					\
      PARSE_ERROR(Loc, s);				\
      delete Ident;					\
      YYERROR;						\
    }							\
  }

184
185
186
187
188
189
190
191
192
#define INSTANCIATE_OP(Name, TypeNode, TypeOp, L, R)	\
  {							\
    TypeNode* res = new TypeNode;			\
    res->op = TypeOp;					\
    res->lhs = formula_tree::node_ptr(L);		\
    res->rhs = formula_tree::node_ptr(R);		\
    Name = res;						\
  }

193
194
195
196
}

/* All tokens.  */

197
198
199
200
201
202
203
204
205
206
207
208
209
210
%token <sval>	ATOMIC_PROP "atomic proposition"
		IDENT "identifier"

%token <ival>	ARG "argument"
		STATE "state"
		OP_OR "or operator"
		OP_XOR "xor operator"
		OP_AND "and operator"
		OP_IMPLIES "implication operator"
		OP_EQUIV "equivalent operator"
		OP_NOT "not operator"

%token		ACC "accept"
		EQ "="
211
		FIN "finish"
212
213
214
215
216
217
		LPAREN "("
		RPAREN ")"
		COMMA ","
		END_OF_FILE "end of file"
		CONST_TRUE "constant true"
		CONST_FALSE "constant false"
218
219
220
221
222
223
224
225

/* Priorities.  */

%left OP_OR
%left OP_XOR
%left OP_AND
%left OP_IMPLIES OP_EQUIV

226
227
%left ATOMIC_PROP

228
229
230
231
232
%nonassoc OP_NOT

%type <nval> nfa_def
%type <fval> subformula
%type <aval> arg_list
233
234
%type <pval> nfa_arg
%type <bval> nfa_arg_list
235

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

239
%printer { debug_stream() << *$$; } <sval>
240
241
242
243
244
245
246
247
248
249
250
251

%%

result: nfa_list subformula
	{
	  result = $2;
	  YYACCEPT;
	}
;

/* NFA definitions. */

252
nfa_list: /* empty */
253
254
255
256
257
258
259
260
261
        | nfa_list nfa
;

nfa: IDENT "=" "(" nfa_def ")"
	{
	  $4->set_name(*$1);
          nmap[*$1] = nfa::ptr($4);
	  delete $1;
        }
262
   | IDENT "=" nfa_arg
263
        {
264
265
266
267
268
269
270
271
272
273
274
	  /// Recursivity issues of aliases are handled by a parse error.
	  aliasmap::iterator i = amap.find(*$1);
	  if (i != amap.end())
	  {
	    std::string s = "`";
	    s += *$1;
	    s += "' is already aliased";
	    PARSE_ERROR(@1, s);
	    delete $1;
	    YYERROR;
	  }
275
	  amap.insert(make_pair(*$1, formula_tree::node_ptr($3)));
276
277
   	  delete $1;
   	}
278
279
;

280
nfa_def: /* empty */
281
        {
282
	  $$ = new nfa;
283
        }
284
        | nfa_def STATE STATE nfa_arg
285
        {
286
	  $1->add_transition($2, $3, formula_tree::node_ptr($4));
287
288
289
290
291
292
293
294
295
	  $$ = $1;
        }
        | nfa_def ACC STATE
        {
 	  $1->set_final($3);
	  $$ = $1;
        }
;

296
nfa_arg_list: nfa_arg
297
	{
298
299
300
301
302
303
304
305
306
	  $$ = new formula_tree::node_nfa;
	  $$->children.push_back(formula_tree::node_ptr($1));
	}
	| nfa_arg_list "," nfa_arg
	{
	  $1->children.push_back(formula_tree::node_ptr($3));
	  $$ = $1;
	}
;
307

308
309
310
nfa_arg: ARG
	{
	  if ($1 == -1)
311
	  {
312
313
314
	    std::string s = "out of range integer";
	    PARSE_ERROR(@1, s);
	    YYERROR;
315
	  }
316
317
318
	  formula_tree::node_atomic* res = new formula_tree::node_atomic;
	  res->i = $1;
	  $$ = res;
319
	}
320
	| CONST_TRUE
321
	{
322
323
	  formula_tree::node_atomic* res = new formula_tree::node_atomic;
	  res->i = formula_tree::True;
324
	  $$ = res;
325
	}
326
        | CONST_FALSE
327
	{
328
329
	  formula_tree::node_atomic* res = new formula_tree::node_atomic;
	  res->i = formula_tree::False;
330
331
	  $$ = res;
	}
332
	| OP_NOT nfa_arg
333
	{
334
335
336
	  formula_tree::node_unop* res = new formula_tree::node_unop;
	  res->op = unop::Not;
	  res->child = formula_tree::node_ptr($2);
337
	  $$ = res;
338
	}
339
	| FIN "(" nfa_arg ")"
340
	{
341
342
343
	  formula_tree::node_unop* res = new formula_tree::node_unop;
	  res->op = unop::Finish;
	  res->child = formula_tree::node_ptr($3);
344
	  $$ = res;
345
	}
346
	| nfa_arg OP_AND nfa_arg
347
	{
348
	  INSTANCIATE_OP($$, formula_tree::node_multop, multop::And, $1, $3);
349
	}
350
	| nfa_arg OP_OR nfa_arg
351
	{
352
	  INSTANCIATE_OP($$, formula_tree::node_multop, multop::Or, $1, $3);
353
	}
354
	| nfa_arg OP_XOR nfa_arg
355
	{
356
	  INSTANCIATE_OP($$, formula_tree::node_binop, binop::Xor, $1, $3);
357
	}
358
	| nfa_arg OP_IMPLIES nfa_arg
359
	{
360
	  INSTANCIATE_OP($$, formula_tree::node_binop, binop::Implies, $1, $3);
361
	}
362
	| nfa_arg OP_EQUIV nfa_arg
363
	{
364
365
366
367
368
369
	  INSTANCIATE_OP($$, formula_tree::node_binop, binop::Equiv, $1, $3);
	}
        | IDENT "(" nfa_arg_list ")"
	{
	  aliasmap::const_iterator i = amap.find(*$1);
	  if (i != amap.end())
370
	  {
371
            unsigned arity = formula_tree::arity(i->second);
372
373
374
	    CHECK_ARITY(@1, $1, $3->children.size(), arity);

	    // Hack to return the right type without screwing with the
375
376
377
	    // std::shared_ptr memory handling by using get for
	    // example. FIXME: modify the %union to handle
	    // formula_tree::node_ptr.
378
379
380
381
382
383
384
385
	    formula_tree::node_unop* tmp1 = new formula_tree::node_unop;
	    tmp1->op = unop::Not;
	    tmp1->child = realias(i->second, $3->children);
	    formula_tree::node_unop* tmp2 = new formula_tree::node_unop;
	    tmp2->op = unop::Not;
	    tmp2->child = formula_tree::node_ptr(tmp1);
	    $$ = tmp2;
	    delete $3;
386
	  }
387
388
389
390
	  else
	  {
	    CHECK_EXISTING_NMAP(@1, $1);
	    nfa::ptr np = nmap[*$1];
391

392
393
394
395
396
397
	    CHECK_ARITY(@1, $1, $3->children.size(), np->arity());
	    $3->nfa = np;
	    $$ = $3;
	  }
	  delete $1;
	}
398

399
400
401
402
/* Formulae. */

subformula: ATOMIC_PROP
	{
403
404
405
406
407
408
409
410
411
412
413
414
415
416
	  $$ = parse_environment.require(*$1);
	  if (!$$)
	  {
	    std::string s = "unknown atomic proposition `";
	    s += *$1;
	    s += "' in environment `";
	    s += parse_environment.name();
	    s += "'";
	    PARSE_ERROR(@1, s);
	    delete $1;
	    YYERROR;
	  }
	  else
	    delete $1;
417
	}
418
	  | subformula ATOMIC_PROP subformula
419
	{
420
421
	  aliasmap::iterator i = amap.find(*$2);
	  if (i != amap.end())
422
	  {
423
424
425
426
427
	    CHECK_ARITY(@1, $2, 2, formula_tree::arity(i->second));
	    automatop::vec v;
	    v.push_back($1);
	    v.push_back($3);
	    $$ = instanciate(i->second, v);
428
429
	    $1->destroy();
	    $3->destroy();
430
	  }
431
432
433
434
435
436
437
438
	  else
	  {
	    CHECK_EXISTING_NMAP(@1, $2);
	    nfa::ptr np = nmap[*$2];
	    CHECK_ARITY(@1, $2, 2, np->arity());
	    automatop::vec* v = new automatop::vec;
	    v->push_back($1);
	    v->push_back($3);
439
	    $$ = automatop::instance(np, v, false);
440
441
442
443
444
445
446
	  }
	  delete $2;
	}
	  | ATOMIC_PROP "(" arg_list ")"
	{
	  aliasmap::iterator i = amap.find(*$1);
	  if (i != amap.end())
447
	  {
448
449
	    CHECK_ARITY(@1, $1, $3->size(), formula_tree::arity(i->second));
	    $$ = instanciate(i->second, *$3);
450
451
	    automatop::vec::iterator it = $3->begin();
	    while (it != $3->end())
452
	      (*it++)->destroy();
453
	    delete $3;
454
455
456
457
458
459
	  }
	  else
	  {
	    CHECK_EXISTING_NMAP(@1, $1);
	    nfa::ptr np = nmap[*$1];

Damien Lefortier's avatar
Damien Lefortier committed
460
	    /// Easily handle deletion of $3 when CHECK_ARITY fails.
461
	    unsigned i = $3->size();
Damien Lefortier's avatar
Damien Lefortier committed
462
463
464
465
	    if ($3->size() != np->arity())
	    {
	      automatop::vec::iterator it = $3->begin();
	      while (it != $3->end())
466
		(*it++)->destroy();
Damien Lefortier's avatar
Damien Lefortier committed
467
468
469
470
	      delete $3;
	    }

	    CHECK_ARITY(@1, $1, i, np->arity());
471
	    $$ = automatop::instance(np, $3, false);
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
	  }
	  delete $1;
	}
	  | CONST_TRUE
	{ $$ = constant::true_instance(); }
	  | CONST_FALSE
	{ $$ = constant::false_instance(); }
          | "(" subformula ")"
	{ $$ = $2; }
          | subformula OP_AND subformula
	{ $$ = multop::instance(multop::And, $1, $3); }
          | subformula OP_OR subformula
	{ $$ = multop::instance(multop::Or, $1, $3); }
	  | subformula OP_XOR subformula
	{ $$ = binop::instance(binop::Xor, $1, $3); }
	  | subformula OP_IMPLIES subformula
        { $$ = binop::instance(binop::Implies, $1, $3); }
	  | subformula OP_EQUIV subformula
	{ $$ = binop::instance(binop::Equiv, $1, $3); }
          | OP_NOT subformula
	{ $$ = unop::instance(unop::Not, $2); }
;

arg_list: subformula
	{
	  $$ = new automatop::vec;
	  $$->push_back($1);
	}
	| arg_list "," subformula
	{
	  $1->push_back($3);
	  $$ = $1;
	}
;

%%

void
eltlyy::parser::error(const location_type& loc, const std::string& s)
{
  PARSE_ERROR(loc, s);
}

namespace spot
{
  namespace eltl
  {
519
    const formula*
520
521
522
523
524
525
526
527
    parse_file(const std::string& name,
	       parse_error_list& error_list,
	       environment& env,
	       bool debug)
    {
      if (flex_open(name))
      {
	error_list.push_back
528
	  (parse_error(spot::location(),
529
530
531
		       spair("-", std::string("Cannot open file ") + name)));
	return 0;
      }
532
      const formula* result = 0;
533
      nfamap nmap;
534
      aliasmap amap;
535
536
      parse_error_list_t pe;
      pe.file_ = name;
537
      eltlyy::parser parser(nmap, amap, pe, env, result);
538
539
540
541
542
543
544
      parser.set_debug_level(debug);
      parser.parse();
      error_list = pe.list_;
      flex_close();
      return result;
    }

545
    const formula*
546
547
548
549
550
    parse_string(const std::string& eltl_string,
		 parse_error_list& error_list,
		 environment& env,
		 bool debug)
    {
551
      flex_set_buffer(eltl_string);
552
      const formula* result = 0;
553
      nfamap nmap;
554
      aliasmap amap;
555
      parse_error_list_t pe;
556
      eltlyy::parser parser(nmap, amap, pe, env, result);
557
558
559
      parser.set_debug_level(debug);
      parser.parse();
      error_list = pe.list_;
560
      flex_unset_buffer();
561
562
563
564
565
566
567
568
      return result;
    }
  }
}

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