tgbaparse.yy 5.96 KB
Newer Older
1
/* -*- coding: utf-8 -*-
2 3
** Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
** et Développement de l'Epita (LRDE).
4
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
5 6
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
** Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7 8 9 10 11
**
** 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
12
** the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13 14 15 16 17 18 19 20
** (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
21
** along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22
*/
23 24 25 26 27 28
%language "C++"
%locations
%defines
%name-prefix "tgbayy"
%debug
%error-verbose
29
%define api.location.type "spot::location"
30 31 32

%code requires
{
33 34
#include <string>
#include "public.hh"
35 36
#include "priv/accmap.hh"
#include "tgba/formula2bdd.hh"
37 38 39 40 41

/* Cache parsed formulae.  Labels on arcs are frequently identical and
   it would be a waste of time to parse them to formula* over and
   over, and to register all their atomic_propositions in the
   bdd_dict.  Keep the bdd result around so we can reuse it.  */
42 43
  typedef std::map<std::string, bdd> formula_cache;
  typedef typename spot::tgba_digraph::namer<std::string>::type named_tgba_t;
44
}
45

46 47
%parse-param {spot::tgba_parse_error_list& error_list}
%parse-param {spot::ltl::environment& parse_environment}
48 49 50
%parse-param {spot::acc_mapper& acc_map}
%parse-param {spot::tgba_digraph*& result}
%parse-param {named_tgba_t*& namer}
51
%parse-param {formula_cache& fcache}
52 53 54 55
%union
{
  int token;
  std::string* str;
56
  const spot::ltl::formula* f;
57
  bdd* acc;
58 59
}

60 61
%code
{
62
#include "ltlast/constant.hh"
63
#include "ltlparse/public.hh"
64
#include <map>
65

66
/* tgbaparse.hh and parsedecl.hh include each other recursively.
67
   We must ensure that YYSTYPE is declared (by the above %union)
68 69 70 71 72
   before parsedecl.hh uses it. */
#include "parsedecl.hh"
using namespace spot::ltl;

typedef std::pair<bool, spot::ltl::formula*> pair;
73
}
74

75
%token <str> STRING UNTERMINATED_STRING
76
%token <str> IDENT
77
%type <str> strident string
78
%type <str> condition
79
%type <acc> acc_list
80
%token ACC_DEF
81

82
%destructor { delete $$; } <str>
83
%destructor { delete $$; } <acc>
84

85
%printer { debug_stream() << *$$; } <str>
86
%printer { debug_stream() << *$$; } <acc>
87

88
%%
89 90
tgba: acceptance_decl lines
      | acceptance_decl
91
      { namer->new_state("0"); }
92 93
      | lines
      |
94
      { namer->new_state("0"); };
95

96
acceptance_decl: ACC_DEF acc_decl ';'
97
      { acc_map.commit(); }
98

99 100
/* At least one line.  */
lines: line
101 102 103
       | lines line
       ;

104
line: strident ',' strident ',' condition ',' acc_list ';'
105
       {
106
	 bdd cond = bddtrue;
107 108 109 110 111 112
	 if ($5)
	   {
	     formula_cache::const_iterator i = fcache.find(*$5);
	     if (i == fcache.end())
	       {
		 parse_error_list pel;
113
		 const formula* f =
114 115
		   spot::ltl::parse_boolean(*$5, pel, parse_environment,
					    debug_level());
116
		 for (auto& j: pel)
117 118
		   {
		     // Adjust the diagnostic to the current position.
119
		     spot::location here = @5;
120 121 122 123 124
		     here.end.line = here.begin.line + j.first.end.line - 1;
		     here.end.column = here.begin.column + j.first.end.column;
		     here.begin.line += j.first.begin.line - 1;
		     here.begin.column += j.first.begin.column;
		     error_list.emplace_back(here, j.second);
125 126
		   }
		 if (f)
127 128 129 130 131
		   {
		     cond = formula_to_bdd(f, result->get_dict(), result);
		     f->destroy();
		   }
		 fcache[*$5] = cond;
132 133 134
	       }
	     else
	       {
135
		 cond = i->second;
136 137
	       }
	   }
138 139 140
	 unsigned s = namer->new_state(*$1);
	 unsigned d = namer->new_state(*$3);
	 namer->graph().new_transition(s, d, cond, *$7);
141 142
	 delete $1;
	 delete $3;
143
	 delete $5;
144 145 146 147
	 delete $7;
       }
       ;

148 149 150
string: STRING
       | UNTERMINATED_STRING
       {
151
	 $$ = $1;
152
	 error_list.emplace_back(@1, "unterminated string");
153 154 155
       }

strident: string | IDENT
156

157
condition:
158
       {
159
	 $$ = 0;
160
       }
161
       | string
162
       {
163
	 $$ = $1;
164 165 166
       }
       ;

167 168
acc_list:
       {
169
	 $$ = new bdd(bddfalse);
170 171 172
       }
       | acc_list strident
       {
173
	 if (*$2 != "" && *$2 != "false")
174
	   {
175 176
	     auto p = acc_map.lookup(*$2);
	     if (! p.first)
177
	       {
178 179
		 error_list.emplace_back(@2,
			 "undeclared acceptance condition `" + *$2 + "'");
180
		 // $2 will be destroyed on error recovery.
181 182
		 YYERROR;
	       }
183
	     *$1 |= p.second;
184 185 186 187 188 189 190 191 192 193
	   }
	 delete $2;
	 $$ = $1;
       }
       ;


acc_decl:
       | acc_decl strident
       {
194
	 if (! acc_map.declare(*$2))
195 196 197 198
	   {
	     std::string s = "acceptance condition `";
	     s += *$2;
	     s += "' unknown in environment `";
199
	     s += acc_map.get_env().name();
200
	     s += "'";
201
	     error_list.emplace_back(@2, s);
202 203
	     YYERROR;
	   }
204 205 206
	 delete $2;
       }
       ;
207 208 209 210

%%

void
211
tgbayy::parser::error(const location_type& location,
212
		      const std::string& message)
213
{
214
  error_list.emplace_back(location, message);
215 216 217 218
}

namespace spot
{
219
  tgba_digraph*
220 221
  tgba_parse(const std::string& name,
	     tgba_parse_error_list& error_list,
222
	     bdd_dict* dict,
223
	     environment& env,
224
	     environment& envacc,
225 226 227
	     bool debug)
  {
    if (tgbayyopen(name))
228
      {
229 230
	error_list.emplace_back(spot::location(),
				std::string("Cannot open file ") + name);
231 232
	return 0;
      }
233
    formula_cache fcache;
234 235 236 237
    tgba_digraph* result = new tgba_digraph(dict);
    auto* namer = result->create_namer<std::string>();
    spot::acc_mapper acc_map(result, envacc);
    tgbayy::parser parser(error_list, env, acc_map, result, namer, fcache);
238
    parser.set_debug_level(debug);
239 240
    parser.parse();
    tgbayyclose();
241 242 243 244 245 246 247 248 249 250 251

    if (namer)			// No fatal error
      {
	delete namer;
	return result;
      }
    else			// Fatal error
      {
	delete result;
	return nullptr;
      }
252
  }
253 254 255 256 257
}

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