neverclaimparse.yy 7.34 KB
Newer Older
1
/* -*- coding: utf-8 -*-
2
3
** Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
** et Développement de l'Epita (LRDE).
Felix Abecassis's avatar
Felix Abecassis committed
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
Felix Abecassis's avatar
Felix Abecassis committed
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/>.
Felix Abecassis's avatar
Felix Abecassis committed
19
20
21
22
23
24
25
26
*/
%language "C++"
%locations
%defines
%expect 0 // No shift/reduce
%name-prefix "neverclaimyy"
%debug
%error-verbose
27
%lex-param { spot::neverclaim_parse_error_list& error_list }
28
%define api.location.type "spot::location"
Felix Abecassis's avatar
Felix Abecassis committed
29
30
31
32

%code requires
{
#include <string>
33
34
#include <cstring>
#include "ltlast/constant.hh"
Felix Abecassis's avatar
Felix Abecassis committed
35
#include "public.hh"
36
#include "tgba/formula2bdd.hh"
37

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

  typedef std::pair<const bdd*, std::string*> pair;
  typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
Felix Abecassis's avatar
Felix Abecassis committed
46
47
48
49
}

%parse-param {spot::neverclaim_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment}
50
51
52
%parse-param {spot::tgba_digraph*& result}
%parse-param {named_tgba_t*& namer}
%parse-param {formula_cache& fcache}
Felix Abecassis's avatar
Felix Abecassis committed
53
54
55
56
57
%union
{
  std::string* str;
  pair* p;
  std::list<pair>* list;
58
  const bdd* b;
Felix Abecassis's avatar
Felix Abecassis committed
59
60
61
62
63
64
65
66
67
68
69
70
}

%code
{
#include "ltlast/constant.hh"
#include "ltlparse/public.hh"

/* neverclaimparse.hh and parsedecl.hh include each other recursively.
   We must ensure that YYSTYPE is declared (by the above %union)
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
using namespace spot::ltl;
71
72
static bool accept_all_needed = false;
static bool accept_all_seen = false;
Felix Abecassis's avatar
Felix Abecassis committed
73
74
75
76
77
78
}

%token NEVER "never"
%token SKIP "skip"
%token IF "if"
%token FI "fi"
79
80
%token DO "do"
%token OD "od"
Felix Abecassis's avatar
Felix Abecassis committed
81
82
%token ARROW "->"
%token GOTO "goto"
83
%token FALSE "false"
84
85
%token ATOMIC "atomic"
%token ASSERT "assert"
86
87
%token <str> FORMULA "boolean formula"
%token <str> IDENT "identifier"
88
89
%type <b> formula
%type <str> opt_dest
90
91
%type <p> transition src_dest
%type <list> transitions transition_block
92
93
%type <str> ident_list

Felix Abecassis's avatar
Felix Abecassis committed
94
95

%destructor { delete $$; } <str>
96
%destructor { delete $$->second; delete $$; } <p>
Felix Abecassis's avatar
Felix Abecassis committed
97
98
99
100
101
102
103
104
%destructor {
  for (std::list<pair>::iterator i = $$->begin();
       i != $$->end(); ++i)
  {
    delete i->second;
  }
  delete $$;
  } <list>
105
%printer {
106
107
108
109
    if ($$)
      debug_stream() << *$$;
    else
      debug_stream() << "\"\""; } <str>
Felix Abecassis's avatar
Felix Abecassis committed
110
111
112
113

%%
neverclaim:
  "never" '{' states '}'
114

Felix Abecassis's avatar
Felix Abecassis committed
115
116
117

states:
  /* empty */
118
119
120
121
  | state
  | states ';' state
  | states ';'

122
ident_list:
123
124
    IDENT ':'
    {
125
      namer->new_state(*$1);
126
127
128
129
      $$ = $1;
    }
  | ident_list IDENT ':'
    {
130
      namer->alias_state(namer->get_state(*$1), *$2);
131
      // Keep any identifier that starts with accept.
132
133
134
135
136
137
138
139
140
141
      if (strncmp("accept", $1->c_str(), 6))
        {
          delete $1;
          $$ = $2;
        }
      else
        {
	  delete $2;
	  $$ = $1;
        }
142
    }
Felix Abecassis's avatar
Felix Abecassis committed
143

144
145
146
147
148
149
150
151
152
153
154

transition_block:
  "if" transitions "fi"
    {
      $$ = $2;
    }
  | "do" transitions "od"
    {
      $$ = $2;
    }

Felix Abecassis's avatar
Felix Abecassis committed
155
state:
156
  ident_list "skip"
Felix Abecassis's avatar
Felix Abecassis committed
157
    {
158
159
160
      if (*$1 == "accept_all")
	accept_all_seen = true;

161
162
163
164
      namer->new_transition(*$1, *$1, bddtrue,
			    !strncmp("accept", $1->c_str(), 6) ?
			    result->all_acceptance_conditions() :
			    static_cast<const bdd>(bddfalse));
Felix Abecassis's avatar
Felix Abecassis committed
165
166
      delete $1;
    }
167
168
  | ident_list { delete $1; }
  | ident_list "false" { delete $1; }
169
  | ident_list transition_block
Felix Abecassis's avatar
Felix Abecassis committed
170
171
    {
      std::list<pair>::iterator it;
172
173
174
175
176
      bdd acc = !strncmp("accept", $1->c_str(), 6) ?
	result->all_acceptance_conditions() :
	static_cast<const bdd>(bddfalse);
      for (auto& p: *$2)
	namer->new_transition(*$1, *p.second, *p.first, acc);
Felix Abecassis's avatar
Felix Abecassis committed
177
178
      // Free the list
      delete $1;
179
180
      for (auto& p: *$2)
	delete p.second;
181
      delete $2;
Felix Abecassis's avatar
Felix Abecassis committed
182
    }
183

Felix Abecassis's avatar
Felix Abecassis committed
184
185
186

transitions:
  /* empty */ { $$ = new std::list<pair>; }
187
  | transitions transition
Felix Abecassis's avatar
Felix Abecassis committed
188
    {
189
190
191
192
193
194
      if ($2)
	{
	  $1->push_back(*$2);
	  delete $2;
	}
      $$ = $1;
Felix Abecassis's avatar
Felix Abecassis committed
195
196
    }

197

198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
formula: FORMULA
     {
       formula_cache::const_iterator i = fcache.find(*$1);
       if (i == fcache.end())
	 {
	   parse_error_list pel;
	   const formula* f =
	     spot::ltl::parse_boolean(*$1, pel, parse_environment,
				      debug_level(), true);
	   for (auto& j: pel)
	     {
	       // Adjust the diagnostic to the current position.
	       spot::location here = @1;
	       here.end.line = here.begin.line + j.first.end.line - 1;
	       here.end.column = here.begin.column + j.first.end.column;
	       here.begin.line += j.first.begin.line - 1;
	       here.begin.column += j.first.begin.column;
	       error_list.emplace_back(here, j.second);
	     }
           bdd cond = bddfalse;
	   if (f)
	     {
	       cond = formula_to_bdd(f, result->get_dict(), result);
	       f->destroy();
	     }
	   $$ = &(fcache[*$1] = cond);
	 }
       else
	 {
	   $$ = &i->second;
	 }
       delete $1;
     }
   | "false"
     {
       $$ = &bddfalse;
     }
235
236
237
238
239
240
241
242
243
244

opt_dest:
  /* empty */
    {
      $$ = 0;
    }
  | "->" "goto" IDENT
    {
      $$ = $3;
    }
245
246
247
248
249
250
  | "->" "assert" FORMULA
    {
      delete $3;
      $$ = new std::string("accept_all");
      accept_all_needed = true;
    }
251

252
src_dest: formula opt_dest
Felix Abecassis's avatar
Felix Abecassis committed
253
    {
254
255
256
257
258
      // If there is no destination, do ignore the transition.
      // This happens for instance with
      //   if
      //   :: false
      //   fi
259
      if (!$2)
260
	{
261
262
263
264
	  $$ = 0;
	}
      else
	{
265
266
	  $$ = new pair($1, $2);
	  namer->new_state(*$2);
267
	}
Felix Abecassis's avatar
Felix Abecassis committed
268
    }
269
270
271
272
273
274
275
276
277
278
279


transition:
  ':' ':' "atomic" '{' src_dest '}'
    {
      $$ = $5;
    }
  | ':' ':' src_dest
    {
      $$ = $3;
    }
Felix Abecassis's avatar
Felix Abecassis committed
280
281
282
283
284
285
%%

void
neverclaimyy::parser::error(const location_type& location,
			    const std::string& message)
{
286
  error_list.emplace_back(location, message);
Felix Abecassis's avatar
Felix Abecassis committed
287
288
289
290
}

namespace spot
{
291
  tgba_digraph*
Felix Abecassis's avatar
Felix Abecassis committed
292
293
294
295
296
297
298
299
  neverclaim_parse(const std::string& name,
		   neverclaim_parse_error_list& error_list,
		   bdd_dict* dict,
		   environment& env,
		   bool debug)
  {
    if (neverclaimyyopen(name))
      {
300
301
	error_list.emplace_back(spot::location(),
				std::string("Cannot open file ") + name);
Felix Abecassis's avatar
Felix Abecassis committed
302
303
	return 0;
      }
304
305
306
307
308
309
310
311
    formula_cache fcache;
    tgba_digraph* result = new tgba_digraph(dict);
    auto namer = result->create_namer<std::string>();

    const ltl::formula* t = ltl::constant::true_instance();
    bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result));
    result->set_acceptance_conditions(acc);

312
313
    result->set_bprop(tgba_digraph::SBA);

314
    neverclaimyy::parser parser(error_list, env, result, namer, fcache);
Felix Abecassis's avatar
Felix Abecassis committed
315
316
317
    parser.set_debug_level(debug);
    parser.parse();
    neverclaimyyclose();
318
319
320

    if (accept_all_needed && !accept_all_seen)
      {
321
322
	unsigned n = namer->new_state("accept_all");
	result->new_transition(n, n, bddtrue, acc);
323
324
325
326
      }
    accept_all_needed = false;
    accept_all_seen = false;

327
    delete namer;
Felix Abecassis's avatar
Felix Abecassis committed
328
329
330
331
332
333
334
    return result;
  }
}

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