neverclaimparse.yy 5.3 KB
Newer Older
1
/* Copyright (C) 2010 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
74
%token FALSE "false"
%token <str> FORMULA "boolean formula"
%token <str> IDENT "identifier"
%type <str> formula
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
91
92
93
94
95
    delete i->second;
  }
  delete $$;
  } <list>
%printer { debug_stream() << *$$; } <str>

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

Felix Abecassis's avatar
Felix Abecassis committed
97
98
99

states:
  /* empty */
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
  | state
  | states ';' state
  | states ';'

ident_list: 
    IDENT ':'
    {
      $$ = $1;
    }
  | ident_list IDENT ':'
    {
      result->add_state_alias(*$2, *$1);
      delete $1;
      $$ = $2;
    }
Felix Abecassis's avatar
Felix Abecassis committed
115
116

state:
117
  ident_list "skip"
Felix Abecassis's avatar
Felix Abecassis committed
118
    {
119
120
121
122
123
      spot::tgba_explicit::transition* t = result->create_transition(*$1, *$1);
      bool acc = !strncmp("accept", $1->c_str(), 6);
      if (acc)
	result->add_acceptance_condition(t, 
					 spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
124
125
      delete $1;
    }
126
127
128
  | ident_list { delete $1; }
  | ident_list "false" { delete $1; }
  | ident_list "if" transitions "fi"
Felix Abecassis's avatar
Felix Abecassis committed
129
130
    {
      std::list<pair>::iterator it;
131
132
      bool acc = !strncmp("accept", $1->c_str(), 6);
      for (it = $3->begin(); it != $3->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
133
134
135
      {
	spot::tgba_explicit::transition* t =
	  result->create_transition(*$1,*it->second);
136
137
138
139
140
	      
	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
141
142
143
      }
      // Free the list
      delete $1;
144
145
      for (std::list<pair>::iterator it = $3->begin();
	   it != $3->end(); ++it)
Felix Abecassis's avatar
Felix Abecassis committed
146
	delete it->second;
147
      delete $3;
Felix Abecassis's avatar
Felix Abecassis committed
148
    }
149

Felix Abecassis's avatar
Felix Abecassis committed
150
151
152
153
154
155
156
157
158
159

transitions:
  /* empty */ { $$ = new std::list<pair>; }
  | transition transitions
    {
      $2->push_back(*$1);
      delete $1;
      $$ = $2;
    }

160
161
162

formula: FORMULA | "false" { $$ = new std::string("0"); }
   
Felix Abecassis's avatar
Felix Abecassis committed
163
transition:
164
  ':' ':' formula  "->" "goto" IDENT
Felix Abecassis's avatar
Felix Abecassis committed
165
    {
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
      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, $6);
Felix Abecassis's avatar
Felix Abecassis committed
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
    }
%%

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);
209
    result->declare_acceptance_condition(spot::ltl::constant::true_instance());
Felix Abecassis's avatar
Felix Abecassis committed
210
211
212
213
214
215
216
217
218
219
220
    neverclaimyy::parser parser(error_list, env, result);
    parser.set_debug_level(debug);
    parser.parse();
    neverclaimyyclose();
    return result;
  }
}

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