spot_impl.i 10.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015  Laboratoire de
3
// Recherche et Développement de l'Epita (LRDE).
4
// Copyright (C) 2003, 2004, 2005, 2006  Laboratoire d'Informatique
5
6
// de 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
%{
  // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef.
  // It matters with g++ 4.6.
#include <cstddef>
%}

29
%module(directors="1") spot_impl
30

31
%include "std_shared_ptr.i"
32
33
%include "std_string.i"
%include "std_list.i"
34
%include "std_set.i"
35
%include "exception.i"
36

37
38
 // git grep 'typedef.*std::shared_ptr' | grep -v const |
 //   sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g'
39
%shared_ptr(spot::dstar_aut)
40
41
42
43
%shared_ptr(spot::hoa_aut)
%shared_ptr(spot::fair_kripke)
%shared_ptr(spot::kripke)
%shared_ptr(spot::kripke_explicit)
44
45
46
47
%shared_ptr(spot::kripke)
%shared_ptr(spot::ta)
%shared_ptr(spot::ta_explicit)
%shared_ptr(spot::ta_product)
48
49
50
%shared_ptr(spot::tgta)
%shared_ptr(spot::tgta_explicit)
%shared_ptr(spot::bdd_dict)
51
52
53
54
%shared_ptr(spot::tgba)
%shared_ptr(spot::tgba_digraph)
%shared_ptr(spot::tgba_product)
%shared_ptr(spot::tgba_product_init)
55
56
57
%shared_ptr(spot::taa_tgba)
%shared_ptr(spot::taa_tgba_string)
%shared_ptr(spot::taa_tgba_formula)
58
%shared_ptr(spot::tgba_safra_complement)
59
60
%shared_ptr(spot::tgba_run)
%shared_ptr(spot::emptiness_check_result)
61
%shared_ptr(spot::emptiness_check)
62
%shared_ptr(spot::emptiness_check_instantiator)
63
%shared_ptr(spot::tgbasl)
64

65
66
67
68
namespace std {
   %template(liststr) list<string>;
};

69
70
%import "buddy.i"

71
%{
72
73
#include <iostream>
#include <fstream>
74
#include <sstream>
75
#include <signal.h>
76

77
#include "misc/common.hh"
78
#include "misc/version.hh"
79
#include "misc/minato.hh"
80
#include "misc/optionmap.hh"
81
#include "misc/random.hh"
82

83
#include "ltlast/formula.hh"
84
85
86
87
88
89
#include "ltlast/atomic_prop.hh"
#include "ltlast/binop.hh"
#include "ltlast/constant.hh"
#include "ltlast/multop.hh"
#include "ltlast/unop.hh"
#include "ltlast/visitor.hh"
90

91
92
#include "ltlenv/environment.hh"
#include "ltlenv/defaultenv.hh"
93

94
95
#include "ltlparse/public.hh"

96
97
#include "tgba/bdddict.hh"

98
#include "ltlvisit/apcollect.hh"
99
100
101
102
#include "ltlvisit/dotty.hh"
#include "ltlvisit/dump.hh"
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/nenoform.hh"
103
#include "ltlvisit/simplify.hh"
104
#include "ltlvisit/tostring.hh"
105
#include "ltlvisit/tunabbrev.hh"
106
#include "ltlvisit/lbt.hh"
107
108
109
110
#include "ltlvisit/randomltl.hh"
#include "ltlvisit/length.hh"
#include "ltlvisit/remove_x.hh"
#include "ltlvisit/relabel.hh"
111

112
#include "tgba/bddprint.hh"
113
#include "tgba/fwd.hh"
114
#include "tgba/acc.hh"
115
#include "tgba/tgba.hh"
116
#include "tgba/taatgba.hh"
117
118
#include "tgba/tgbaproduct.hh"

119
#include "tgbaalgos/cleanacc.hh"
120
#include "tgbaalgos/dotty.hh"
121
#include "tgbaalgos/degen.hh"
122
#include "tgbaalgos/dupexp.hh"
123
124
#include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/gtec/gtec.hh"
125
126
127
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
128
#include "tgbaalgos/compsusp.hh"
129
#include "tgbaalgos/magic.hh"
130
#include "tgbaalgos/minimize.hh"
131
#include "tgbaalgos/neverclaim.hh"
132
#include "tgbaalgos/safety.hh"
133
#include "tgbaalgos/sccfilter.hh"
134
#include "tgbaalgos/stats.hh"
135
#include "tgbaalgos/isdet.hh"
136
#include "tgbaalgos/simulation.hh"
137
#include "tgbaalgos/postproc.hh"
138
#include "tgbaalgos/product.hh"
139
#include "tgbaalgos/stutter.hh"
140
#include "tgbaalgos/translate.hh"
141
#include "tgbaalgos/hoa.hh"
142

143
#include "hoaparse/public.hh"
144

145
146
147
148
149
150
151
152
153
#include "ta/ta.hh"
#include "ta/tgta.hh"
#include "ta/taexplicit.hh"
#include "ta/tgtaexplicit.hh"
#include "taalgos/tgba2ta.hh"
#include "taalgos/dotty.hh"
#include "taalgos/stats.hh"
#include "taalgos/minimize.hh"

154
using namespace spot::ltl;
155
using namespace spot;
156
157
%}

158
159
160
161
// For spot::emptiness_check_instantiator::construct and any other
// function that return errors via a "char **err" argument.
%typemap(in, numinputs=0) char** OUTPUT (char* temp)
  "$1 = &temp;";
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
%typemap(argout) char** OUTPUT {
  PyObject *obj = SWIG_FromCharPtr(*$1);
  if (!$result) {
    $result = obj;
  //# If the function returns null_ptr (i.e. Py_None), we
  //# don't want to override it with OUTPUT as in the
  //# default implementation of t_output_helper.
  // } else if ($result == Py_None) {
  //   Py_DECREF($result);
  //   $result = obj;
  } else {
    if (!PyList_Check($result)) {
      PyObject *o2 = $result;
      $result = PyList_New(1);
      PyList_SetItem($result, 0, o2);
    }
    PyList_Append($result,obj);
    Py_DECREF(obj);
  }
181

182
 };
183
184
%apply char** OUTPUT { char** err };

185
186
187
188
%exception {
  try {
    $action
  }
189
  catch (const spot::parse_error& e)
190
191
192
193
194
  {
    std::string er("\n");
    er += e.what();
    SWIG_exception(SWIG_SyntaxError, er.c_str());
  }
195
196
  catch (const std::invalid_argument& e)
  {
197
198
199
200
201
    SWIG_exception(SWIG_ValueError, e.what());
  }
  catch (const std::runtime_error& e)
  {
    SWIG_exception(SWIG_RuntimeError, e.what());
202
  }
203
204
}

205
206
207
208
209
// False and True cannot be redefined in Python3, even in a class.
// Spot uses these in an enum of the constant class.
%rename(FalseVal) False;
%rename(TrueVal) True;

210
%include "misc/common.hh"
211
%include "misc/version.hh"
212
%include "misc/minato.hh"
213
%include "misc/optionmap.hh"
214
%include "misc/random.hh"
215

216
%include "ltlast/formula.hh"
217
218
219
220
221
222
%include "ltlast/atomic_prop.hh"
%include "ltlast/binop.hh"
%include "ltlast/constant.hh"
%include "ltlast/multop.hh"
%include "ltlast/unop.hh"
%include "ltlast/visitor.hh"
223

224
225
%include "ltlenv/environment.hh"
%include "ltlenv/defaultenv.hh"
226

227
228
%include "ltlparse/public.hh"

229
 /* these must come before apcollect.hh */
230
%include "tgba/bdddict.hh"
231
232
233
234
235
236
%include "tgba/bddprint.hh"
%include "tgba/fwd.hh"
%feature("flatnested") spot::acc_cond::mark_t;
%feature("flatnested") spot::acc_cond::acc_code;
%include "tgba/acc.hh"
%include "tgba/tgba.hh"
237

238
%include "ltlvisit/apcollect.hh"
239
240
241
242
%include "ltlvisit/dotty.hh"
%include "ltlvisit/dump.hh"
%include "ltlvisit/lunabbrev.hh"
%include "ltlvisit/nenoform.hh"
243
%include "ltlvisit/simplify.hh"
244
%include "ltlvisit/tostring.hh"
245
%include "ltlvisit/tunabbrev.hh"
246
%include "ltlvisit/lbt.hh"
247
248
249
250
%include "ltlvisit/randomltl.hh"
%include "ltlvisit/length.hh"
%include "ltlvisit/remove_x.hh"
%include "ltlvisit/relabel.hh"
251

252
253
// Help SWIG with namespace lookups.
#define ltl spot::ltl
254
%include "tgba/taatgba.hh"
255
%include "tgba/tgbaproduct.hh"
256
%include "tgba/tgbagraph.hh"
257

258
259
// Should come after the definition of tgba_digraph

260
%include "tgbaalgos/cleanacc.hh"
261
%include "tgbaalgos/degen.hh"
262
%include "tgbaalgos/dotty.hh"
263
%include "tgbaalgos/dupexp.hh"
264
265
%include "tgbaalgos/emptiness.hh"
%include "tgbaalgos/gtec/gtec.hh"
266
267
268
%include "tgbaalgos/lbtt.hh"
%include "tgbaalgos/ltl2taa.hh"
%include "tgbaalgos/ltl2tgba_fm.hh"
269
%include "tgbaalgos/compsusp.hh"
270
%include "tgbaalgos/magic.hh"
271
%include "tgbaalgos/minimize.hh"
272
%include "tgbaalgos/neverclaim.hh"
273
%include "tgbaalgos/safety.hh"
274
%include "tgbaalgos/sccfilter.hh"
275
%include "tgbaalgos/stats.hh"
276
%include "tgbaalgos/isdet.hh"
277
%include "tgbaalgos/simulation.hh"
278
%include "tgbaalgos/postproc.hh"
279
%include "tgbaalgos/product.hh"
280
%include "tgbaalgos/stutter.hh"
281
%include "tgbaalgos/translate.hh"
282
%include "tgbaalgos/hoa.hh"
283

284
%include "hoaparse/public.hh"
285

286
287
288
289
290
291
292
293
294
295
%include "ta/ta.hh"
%include "ta/tgta.hh"
%include "ta/taexplicit.hh"
%include "ta/tgtaexplicit.hh"
%include "taalgos/tgba2ta.hh"
%include "taalgos/dotty.hh"
%include "taalgos/stats.hh"
%include "taalgos/minimize.hh"


296
#undef ltl
297

298
299
300
301
302
303
304
305
306
307
308
309
310
311
312

namespace std {
  %template(atomic_prop_set)    set<const spot::ltl::atomic_prop*,
spot::ltl::formula_ptr_less_than>;
}

%{
  namespace swig {
    template <>  struct traits<atomic_prop> {
      typedef pointer_category category;
      static const char* type_name() { return"atomic_prop const *"; }
    };
  }
%}

313
314
315
316
%extend spot::ltl::formula {

  // When comparing formula, make sure Python compare our
  // pointers, not the pointers to its wrappers.
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333

  // __cmp__ is for Python 2.0
  int __cmp__(const spot::ltl::formula* b) { return self - b; }
  // These are for Python 2.1+ or 3.x.  They more closely match
  // the logic in Spot.
  bool __lt__(const spot::ltl::formula* b)
  { spot::ltl::formula_ptr_less_than lt; return lt(self, b); }
  bool __le__(const spot::ltl::formula* b)
  { spot::ltl::formula_ptr_less_than lt; return !lt(b, self); }
  bool __eq__(const spot::ltl::formula* b) { return self == b; }
  bool __ne__(const spot::ltl::formula* b) { return self != b; }
  bool __gt__(const spot::ltl::formula* b)
  { spot::ltl::formula_ptr_less_than lt; return lt(b, self); }
  bool __ge__(const spot::ltl::formula* b)
  { spot::ltl::formula_ptr_less_than lt; return !lt(self, b); }

  size_t __hash__() { return self->hash(); }
334

335
336
  std::string __repr__() { return spot::ltl::to_string(self); }
  std::string _repr_latex_()
337
  {
338
    return std::string("$") + spot::ltl::to_sclatex_string(self) + '$';
339
  }
340
  std::string __str__() { return spot::ltl::to_string(self); }
341
}
342

343
%nodefaultctor std::ostream;
344
345
346
347
348
349
350
351
namespace std {
  class ostream {};
  class ofstream : public ostream
  {
  public:
     ofstream(const char *fn);
     ~ofstream();
  };
352
353
354
355
356
  class ostringstream : public ostream
  {
  public:
     ostringstream();
     std::string str() const;
357
     ~ostringstream();
358
  };
359
360
}

361
%inline %{
362
spot::ltl::parse_error_list
363
364
365
366
367
368
empty_parse_error_list()
{
  parse_error_list l;
  return l;
}

369
370
spot::hoa_parse_error_list
empty_hoa_parse_error_list()
371
{
372
  hoa_parse_error_list l;
373
374
375
  return l;
}

376
377
378
379
380
381
spot::tgba_digraph_ptr
ensure_digraph(const spot::tgba_ptr& a)
{
  auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
  if (aa)
    return aa;
382
  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
383
384
}

385
std::ostream&
386
387
388
389
390
get_cout()
{
  return std::cout;
}

391
392
393
394
395
396
void
nl_cout()
{
  std::cout << std::endl;
}

397
std::ostream&
398
399
400
401
402
get_cerr()
{
  return std::cerr;
}

403
404
405
406
407
408
void
nl_cerr()
{
  std::cerr << std::endl;
}

409
void
410
411
412
413
print_on(std::ostream& on, const std::string& what)
{
  on << what;
}
414

415
416
417
418
419
420
421
422
423
int
unblock_signal(int signum)
{
  sigset_t set;
  sigemptyset(&set);
  sigaddset(&set, signum);
  return sigprocmask(SIG_UNBLOCK, &set, 0);
}

424
%}
425
426
427
428
429
430
431
432
433

%extend spot::ltl::parse_error_list {

bool
__nonzero__()
{
  return !self->empty();
}

434
435
436
437
438
439
bool
__bool__()
{
  return !self->empty();
}

440
}
441

442
%extend spot::hoa_parse_error_list {
443
444
445
446
447
448
449

bool
__nonzero__()
{
  return !self->empty();
}

450
451
452
453
454
455
bool
__bool__()
{
  return !self->empty();
}

456
}