neverclaimparse.yy 6.75 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 }
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

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

%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"
#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;
60
61
static bool accept_all_needed = false;
static bool accept_all_seen = false;
Felix Abecassis's avatar
Felix Abecassis committed
62
63
64
65
66
67
}

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

Felix Abecassis's avatar
Felix Abecassis committed
82
83

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

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

Felix Abecassis's avatar
Felix Abecassis committed
104
105
106

states:
  /* empty */
107
108
109
110
  | state
  | states ';' state
  | states ';'

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

132
133
134
135
136
137
138
139
140
141
142

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

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

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

167
168
169
170
	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
171
172
173
      }
      // Free the list
      delete $1;
174
175
      for (std::list<pair>::iterator it = $2->begin();
	   it != $2->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
176
	delete it->second;
177
      delete $2;
Felix Abecassis's avatar
Felix Abecassis committed
178
    }
179

Felix Abecassis's avatar
Felix Abecassis committed
180
181
182

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

193
194

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

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

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


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

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
277
	  (neverclaim_parse_error(spot::location(),
Felix Abecassis's avatar
Felix Abecassis committed
278
279
280
281
				  std::string("Cannot open file ") + name));
	return 0;
      }
    tgba_explicit_string* result = new tgba_explicit_string(dict);
282
    result->declare_acceptance_condition(spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
283
284
285
286
    neverclaimyy::parser parser(error_list, env, result);
    parser.set_debug_level(debug);
    parser.parse();
    neverclaimyyclose();
287
288
289
290
291
292
293
294
295
296
297

    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
298
299
300
301
302
303
304
    return result;
  }
}

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