neverclaimparse.yy 6.83 KB
Newer Older
1
/* -*- coding: utf-8 -*-
2
** Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
3
** 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 }
Felix Abecassis's avatar
Felix Abecassis committed
28
29
30
31

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

36
  typedef std::pair<const spot::ltl::formula*, std::string*> pair;
Felix Abecassis's avatar
Felix Abecassis committed
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
}

%parse-param {spot::neverclaim_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment}
%parse-param {spot::tgba_explicit_string*& result}
%union
{
  std::string* str;
  pair* p;
  std::list<pair>* list;
}

%code
{
#include "ltlast/constant.hh"
  /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */
#undef BISON_POSITION_HH
#undef BISON_LOCATION_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;
62
63
static bool accept_all_needed = false;
static bool accept_all_seen = false;
Felix Abecassis's avatar
Felix Abecassis committed
64
65
66
67
68
69
}

%token NEVER "never"
%token SKIP "skip"
%token IF "if"
%token FI "fi"
70
71
%token DO "do"
%token OD "od"
Felix Abecassis's avatar
Felix Abecassis committed
72
73
%token ARROW "->"
%token GOTO "goto"
74
%token FALSE "false"
75
76
%token ATOMIC "atomic"
%token ASSERT "assert"
77
78
%token <str> FORMULA "boolean formula"
%token <str> IDENT "identifier"
79
%type <str> formula opt_dest
80
81
%type <p> transition src_dest
%type <list> transitions transition_block
82
83
%type <str> ident_list

Felix Abecassis's avatar
Felix Abecassis committed
84
85

%destructor { delete $$; } <str>
86
%destructor { $$->first->destroy(); delete $$->second; delete $$; } <p>
Felix Abecassis's avatar
Felix Abecassis committed
87
88
89
90
%destructor {
  for (std::list<pair>::iterator i = $$->begin();
       i != $$->end(); ++i)
  {
91
    i->first->destroy();
Felix Abecassis's avatar
Felix Abecassis committed
92
93
94
95
    delete i->second;
  }
  delete $$;
  } <list>
96
97
98
99
100
  %printer {
    if ($$)
      debug_stream() << *$$;
    else
      debug_stream() << "\"\""; } <str>
Felix Abecassis's avatar
Felix Abecassis committed
101
102
103
104

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

Felix Abecassis's avatar
Felix Abecassis committed
106
107
108

states:
  /* empty */
109
110
111
112
  | state
  | states ';' state
  | states ';'

113
ident_list:
114
115
116
117
118
119
120
    IDENT ':'
    {
      $$ = $1;
    }
  | ident_list IDENT ':'
    {
      result->add_state_alias(*$2, *$1);
121
      // Keep any identifier that starts with accept.
122
123
124
125
126
127
128
129
130
131
      if (strncmp("accept", $1->c_str(), 6))
        {
          delete $1;
          $$ = $2;
        }
      else
        {
	  delete $2;
	  $$ = $1;
        }
132
    }
Felix Abecassis's avatar
Felix Abecassis committed
133

134
135
136
137
138
139
140
141
142
143
144

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

Felix Abecassis's avatar
Felix Abecassis committed
145
state:
146
  ident_list "skip"
Felix Abecassis's avatar
Felix Abecassis committed
147
    {
148
149
150
      if (*$1 == "accept_all")
	accept_all_seen = true;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
151
      spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1);
152
153
      bool acc = !strncmp("accept", $1->c_str(), 6);
      if (acc)
154
	result->add_acceptance_condition(t,
155
					 spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
156
157
      delete $1;
    }
158
159
  | ident_list { delete $1; }
  | ident_list "false" { delete $1; }
160
  | ident_list transition_block
Felix Abecassis's avatar
Felix Abecassis committed
161
162
    {
      std::list<pair>::iterator it;
163
      bool acc = !strncmp("accept", $1->c_str(), 6);
164
      for (it = $2->begin(); it != $2->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
165
      {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
166
	spot::state_explicit_string::transition* t =
167
	  result->create_transition(*$1, *it->second);
168

169
170
171
172
	result->add_condition(t, it->first);
	if (acc)
	  result
	    ->add_acceptance_condition(t, spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
173
174
175
      }
      // Free the list
      delete $1;
176
177
      for (std::list<pair>::iterator it = $2->begin();
	   it != $2->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
178
	delete it->second;
179
      delete $2;
Felix Abecassis's avatar
Felix Abecassis committed
180
    }
181

Felix Abecassis's avatar
Felix Abecassis committed
182
183
184

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

195
196

formula: FORMULA | "false" { $$ = new std::string("0"); }
197
198
199
200
201
202
203
204
205
206

opt_dest:
  /* empty */
    {
      $$ = 0;
    }
  | "->" "goto" IDENT
    {
      $$ = $3;
    }
207
208
209
210
211
212
  | "->" "assert" FORMULA
    {
      delete $3;
      $$ = new std::string("accept_all");
      accept_all_needed = true;
    }
213

214
src_dest: formula opt_dest
Felix Abecassis's avatar
Felix Abecassis committed
215
    {
216
217
218
219
220
      // If there is no destination, do ignore the transition.
      // This happens for instance with
      //   if
      //   :: false
      //   fi
221
      if (!$2)
222
	{
223
	  delete $1;
224
225
226
227
228
	  $$ = 0;
	}
      else
	{
	  spot::ltl::parse_error_list pel;
229
	  const spot::ltl::formula* f =
230
	    spot::ltl::parse_boolean(*$1, pel, parse_environment,
231
				     debug_level(), true);
232
	  delete $1;
233
234
235
236
	  for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
	  i != pel.end(); ++i)
	    {
	      // Adjust the diagnostic to the current position.
237
	      location here = @1;
238
239
240
241
242
243
	      here.end.line = here.begin.line + i->first.end.line - 1;
	      here.end.column = here.begin.column + i->first.end.column -1;
	      here.begin.line += i->first.begin.line - 1;
	      here.begin.column += i->first.begin.column - 1;
	      error(here, i->second);
	    }
244
	  $$ = new pair(f, $2);
245
	}
Felix Abecassis's avatar
Felix Abecassis committed
246
    }
247
248
249
250
251
252
253
254
255
256
257


transition:
  ':' ':' "atomic" '{' src_dest '}'
    {
      $$ = $5;
    }
  | ':' ':' src_dest
    {
      $$ = $3;
    }
Felix Abecassis's avatar
Felix Abecassis committed
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
%%

void
neverclaimyy::parser::error(const location_type& location,
			    const std::string& message)
{
  error_list.push_back(spot::neverclaim_parse_error(location, message));
}

namespace spot
{
  tgba_explicit_string*
  neverclaim_parse(const std::string& name,
		   neverclaim_parse_error_list& error_list,
		   bdd_dict* dict,
		   environment& env,
		   bool debug)
  {
    if (neverclaimyyopen(name))
      {
	error_list.push_back
	  (neverclaim_parse_error(neverclaimyy::location(),
				  std::string("Cannot open file ") + name));
	return 0;
      }
    tgba_explicit_string* result = new tgba_explicit_string(dict);
284
    result->declare_acceptance_condition(spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
285
286
287
288
    neverclaimyy::parser parser(error_list, env, result);
    parser.set_debug_level(debug);
    parser.parse();
    neverclaimyyclose();
289
290
291
292
293
294
295
296
297
298
299

    if (accept_all_needed && !accept_all_seen)
      {
	spot::state_explicit_string::transition* t =
	  result->create_transition("accept_all", "accept_all");
	result->add_acceptance_condition
	  (t, spot::ltl::constant::true_instance());
      }
    accept_all_needed = false;
    accept_all_seen = false;

Felix Abecassis's avatar
Felix Abecassis committed
300
301
302
303
304
305
306
    return result;
  }
}

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