neverclaimparse.yy 5.75 KB
Newer Older
1
2
3
/* -*- coding: utf-8 -*-
** Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
Felix Abecassis's avatar
Felix Abecassis committed
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
%expect 0 // No shift/reduce
%expect-rr 0 // No reduce/reduce
%name-prefix "neverclaimyy"
%debug
%error-verbose

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

38
  typedef std::pair<const spot::ltl::formula*, std::string*> pair;
Felix Abecassis's avatar
Felix Abecassis committed
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
}

%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;
}

%token NEVER "never"
%token SKIP "skip"
%token IF "if"
%token FI "fi"
%token ARROW "->"
%token GOTO "goto"
72
73
74
%token FALSE "false"
%token <str> FORMULA "boolean formula"
%token <str> IDENT "identifier"
75
%type <str> formula opt_dest
Felix Abecassis's avatar
Felix Abecassis committed
76
77
%type <p> transition
%type <list> transitions
78
79
%type <str> ident_list

Felix Abecassis's avatar
Felix Abecassis committed
80
81

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

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

Felix Abecassis's avatar
Felix Abecassis committed
102
103
104

states:
  /* empty */
105
106
107
108
  | state
  | states ';' state
  | states ';'

109
ident_list:
110
111
112
113
114
115
116
117
118
119
    IDENT ':'
    {
      $$ = $1;
    }
  | ident_list IDENT ':'
    {
      result->add_state_alias(*$2, *$1);
      delete $1;
      $$ = $2;
    }
Felix Abecassis's avatar
Felix Abecassis committed
120
121

state:
122
  ident_list "skip"
Felix Abecassis's avatar
Felix Abecassis committed
123
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
124
      spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1);
125
126
      bool acc = !strncmp("accept", $1->c_str(), 6);
      if (acc)
127
	result->add_acceptance_condition(t,
128
					 spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
129
130
      delete $1;
    }
131
132
133
  | ident_list { delete $1; }
  | ident_list "false" { delete $1; }
  | ident_list "if" transitions "fi"
Felix Abecassis's avatar
Felix Abecassis committed
134
135
    {
      std::list<pair>::iterator it;
136
137
      bool acc = !strncmp("accept", $1->c_str(), 6);
      for (it = $3->begin(); it != $3->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
138
      {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
139
	spot::state_explicit_string::transition* t =
Felix Abecassis's avatar
Felix Abecassis committed
140
	  result->create_transition(*$1,*it->second);
141

142
143
144
145
	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
146
147
148
      }
      // Free the list
      delete $1;
149
150
      for (std::list<pair>::iterator it = $3->begin();
	   it != $3->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
151
	delete it->second;
152
      delete $3;
Felix Abecassis's avatar
Felix Abecassis committed
153
    }
154

Felix Abecassis's avatar
Felix Abecassis committed
155
156
157

transitions:
  /* empty */ { $$ = new std::list<pair>; }
158
  | transitions transition
Felix Abecassis's avatar
Felix Abecassis committed
159
    {
160
161
162
163
164
165
      if ($2)
	{
	  $1->push_back(*$2);
	  delete $2;
	}
      $$ = $1;
Felix Abecassis's avatar
Felix Abecassis committed
166
167
    }

168
169

formula: FORMULA | "false" { $$ = new std::string("0"); }
170
171
172
173
174
175
176
177
178
179
180

opt_dest:
  /* empty */
    {
      $$ = 0;
    }
  | "->" "goto" IDENT
    {
      $$ = $3;
    }

Felix Abecassis's avatar
Felix Abecassis committed
181
transition:
182
  ':' ':' formula opt_dest
Felix Abecassis's avatar
Felix Abecassis committed
183
    {
184
185
186
187
188
189
      // If there is no destination, do ignore the transition.
      // This happens for instance with
      //   if
      //   :: false
      //   fi
      if (!$4)
190
	{
191
192
193
194
195
196
	  delete $3;
	  $$ = 0;
	}
      else
	{
	  spot::ltl::parse_error_list pel;
197
	  const spot::ltl::formula* f = spot::ltl::parse(*$3, pel);
198
199
200
201
202
203
204
205
206
207
208
209
210
	  delete $3;
	  for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
	  i != pel.end(); ++i)
	    {
	      // Adjust the diagnostic to the current position.
	      location here = @3;
	      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);
	    }
	  $$ = new pair(f, $4);
211
	}
Felix Abecassis's avatar
Felix Abecassis committed
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
    }
%%

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);
239
    result->declare_acceptance_condition(spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
240
241
242
243
244
245
246
247
248
249
250
    neverclaimyy::parser parser(error_list, env, result);
    parser.set_debug_level(debug);
    parser.parse();
    neverclaimyyclose();
    return result;
  }
}

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