neverclaimparse.yy 5.7 KB
Newer Older
1
/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Dveloppement
Felix Abecassis's avatar
Felix Abecassis committed
2
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
** de l'Epita (LRDE).
**
** 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>
33
34
#include <cstring>
#include "ltlast/constant.hh"
Felix Abecassis's avatar
Felix Abecassis committed
35
#include "public.hh"
36
37

  typedef std::pair<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
60
61
62
63
64
65
66
67
68
69
70
}

%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"
71
72
73
%token FALSE "false"
%token <str> FORMULA "boolean formula"
%token <str> IDENT "identifier"
74
%type <str> formula opt_dest
Felix Abecassis's avatar
Felix Abecassis committed
75
76
%type <p> transition
%type <list> transitions
77
78
%type <str> ident_list

Felix Abecassis's avatar
Felix Abecassis committed
79
80

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

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

Felix Abecassis's avatar
Felix Abecassis committed
101
102
103

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

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

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

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

Felix Abecassis's avatar
Felix Abecassis committed
154
155
156

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

167
168

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

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

Felix Abecassis's avatar
Felix Abecassis committed
180
transition:
181
  ':' ':' formula opt_dest
Felix Abecassis's avatar
Felix Abecassis committed
182
    {
183
184
185
186
187
188
      // If there is no destination, do ignore the transition.
      // This happens for instance with
      //   if
      //   :: false
      //   fi
      if (!$4)
189
	{
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
	  delete $3;
	  $$ = 0;
	}
      else
	{
	  spot::ltl::parse_error_list pel;
	  spot::ltl::formula* f = spot::ltl::parse(*$3, pel);
	  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);
210
	}
Felix Abecassis's avatar
Felix Abecassis committed
211
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
    }
%%

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

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