eltlparse.yy 13.3 KB
Newer Older
1
2
/* Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
** et Dveloppement de l'Epita (LRDE).
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
**
** 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 2 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 Spot; see the file COPYING.  If not, write to the Free
** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
** 02111-1307, USA.
*/
%language "C++"
%locations
%defines
%name-prefix "eltlyy"
%debug
%error-verbose

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

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

46
47
48
49
50
    /// 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).
51
    typedef std::map<std::string, formula_tree::node_ptr> aliasmap;
52
53

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

63
64
65
66
%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}
67
%parse-param {const spot::ltl::formula* &result}
68
69
70
71
72
73
74
75
76
%lex-param {spot::eltl::parse_error_list_t &pe}
%expect 0
%pure-parser
%union
{
  int ival;
  std::string* sval;
  spot::ltl::nfa* nval;
  spot::ltl::automatop::vec* aval;
77
  const spot::ltl::formula* fval;
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

  /// 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
  {
96
    using namespace spot::ltl::formula_tree;
97

98
99
100
101
102
    /// 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.
103
104
    static node_ptr
    realias(const node_ptr ap, std::vector<node_ptr> v)
105
    {
106
107
108
109
110
      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()))
111
      {
112
113
114
115
    	node_unop* res = new node_unop;
	res->op = a->op;
    	res->child = realias(a->child, v);
    	return node_ptr(res);
116
      }
117
      if (node_nfa* a = dynamic_cast<node_nfa*>(ap.get()))
118
      {
119
120
121
122
123
124
    	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);
125
      }
126
      if (node_binop* a = dynamic_cast<node_binop*>(ap.get()))
127
      {
128
129
130
131
132
    	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);
133
      }
134
      if (node_multop* a = dynamic_cast<node_multop*>(ap.get()))
135
      {
136
137
138
139
140
    	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);
141
142
143
144
      }

      /* Unreachable code.  */
      assert(0);
145
      return node_ptr(static_cast<node_unop*>(0));
146
    }
147
148
149
  }
}

150
151
#define PARSE_ERROR(Loc, Msg)				\
  pe.list_.push_back					\
152
    (parse_error(Loc, spair(pe.file_, Msg)))
153
154
155

#define CHECK_EXISTING_NMAP(Loc, Ident)			\
  {							\
156
    nfamap::const_iterator i = nmap.find(*Ident);	\
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
184
185
186
187
    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;						\
    }							\
  }

188
189
190
191
192
193
194
195
196
#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;						\
  }

197
198
199
200
}

/* All tokens.  */

201
202
203
204
205
206
207
208
209
210
211
212
213
214
%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 "="
215
		FIN "finish"
216
217
218
219
220
221
		LPAREN "("
		RPAREN ")"
		COMMA ","
		END_OF_FILE "end of file"
		CONST_TRUE "constant true"
		CONST_FALSE "constant false"
222
223
224
225
226
227
228
229

/* Priorities.  */

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

230
231
%left ATOMIC_PROP

232
233
234
235
236
%nonassoc OP_NOT

%type <nval> nfa_def
%type <fval> subformula
%type <aval> arg_list
237
238
%type <pval> nfa_arg
%type <bval> nfa_arg_list
239

240
241
%destructor { delete $$; } <sval>
%destructor { $$->destroy(); } <fval>
242

243
%printer { debug_stream() << *$$; } <sval>
244
245
246
247
248
249
250
251
252
253
254
255

%%

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

/* NFA definitions. */

256
nfa_list: /* empty */
257
258
259
260
261
262
263
264
265
        | nfa_list nfa
;

nfa: IDENT "=" "(" nfa_def ")"
	{
	  $4->set_name(*$1);
          nmap[*$1] = nfa::ptr($4);
	  delete $1;
        }
266
   | IDENT "=" nfa_arg
267
        {
268
269
270
271
272
273
274
275
276
277
278
	  /// 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;
	  }
279
	  amap.insert(make_pair(*$1, formula_tree::node_ptr($3)));
280
281
   	  delete $1;
   	}
282
283
;

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

300
nfa_arg_list: nfa_arg
301
	{
302
303
304
305
306
307
308
309
310
	  $$ = 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;
	}
;
311

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

	    // Hack to return the right type without screwing with the
	    // boost::shared_ptr memory handling by using get for
	    // example. FIXME: Wait for the next version of boost and
	    // modify the %union to handle formula_tree::node_ptr.
	    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;
390
	  }
391
392
393
394
	  else
	  {
	    CHECK_EXISTING_NMAP(@1, $1);
	    nfa::ptr np = nmap[*$1];
395

396
397
398
399
400
401
	    CHECK_ARITY(@1, $1, $3->children.size(), np->arity());
	    $3->nfa = np;
	    $$ = $3;
	  }
	  delete $1;
	}
402

403
404
405
406
/* Formulae. */

subformula: ATOMIC_PROP
	{
407
408
409
410
411
412
413
414
415
416
417
418
419
420
	  $$ = 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;
421
	}
422
	  | subformula ATOMIC_PROP subformula
423
	{
424
425
	  aliasmap::iterator i = amap.find(*$2);
	  if (i != amap.end())
426
	  {
427
428
429
430
431
	    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);
432
433
	    $1->destroy();
	    $3->destroy();
434
	  }
435
436
437
438
439
440
441
442
	  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);
443
	    $$ = automatop::instance(np, v, false);
444
445
446
447
448
449
450
	  }
	  delete $2;
	}
	  | ATOMIC_PROP "(" arg_list ")"
	{
	  aliasmap::iterator i = amap.find(*$1);
	  if (i != amap.end())
451
	  {
452
453
	    CHECK_ARITY(@1, $1, $3->size(), formula_tree::arity(i->second));
	    $$ = instanciate(i->second, *$3);
454
455
	    automatop::vec::iterator it = $3->begin();
	    while (it != $3->end())
456
	      (*it++)->destroy();
457
	    delete $3;
458
459
460
461
462
463
	  }
	  else
	  {
	    CHECK_EXISTING_NMAP(@1, $1);
	    nfa::ptr np = nmap[*$1];

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

	    CHECK_ARITY(@1, $1, i, np->arity());
475
	    $$ = automatop::instance(np, $3, false);
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
519
520
521
522
	  }
	  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
  {
523
    const formula*
524
525
526
527
528
529
530
531
532
533
534
535
    parse_file(const std::string& name,
	       parse_error_list& error_list,
	       environment& env,
	       bool debug)
    {
      if (flex_open(name))
      {
	error_list.push_back
	  (parse_error(eltlyy::location(),
		       spair("-", std::string("Cannot open file ") + name)));
	return 0;
      }
536
      const formula* result = 0;
537
      nfamap nmap;
538
      aliasmap amap;
539
540
      parse_error_list_t pe;
      pe.file_ = name;
541
      eltlyy::parser parser(nmap, amap, pe, env, result);
542
543
544
545
546
547
548
      parser.set_debug_level(debug);
      parser.parse();
      error_list = pe.list_;
      flex_close();
      return result;
    }

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

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