ltsmin.i 6.56 KB
Newer Older
1
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
// -*- coding: utf-8 -*-
// Copyright (C) 2016 Laboratoire de Recherche et Développement 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

%{
  // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef.
  // It matters with g++ 4.6.
#include <cstddef>
%}

%module(package="spot", director="1") ltsmin

%include "std_string.i"
%include "std_set.i"
%include "std_shared_ptr.i"

%shared_ptr(spot::bdd_dict)
%shared_ptr(spot::twa)
%shared_ptr(spot::kripke)
%shared_ptr(spot::fair_kripke)

%{
#include <spot/ltsmin/ltsmin.hh>
using namespace spot;
%}

%import(module="spot.impl") <spot/misc/common.hh>
%import(module="spot.impl") <spot/twa/bdddict.hh>
%import(module="spot.impl") <spot/twa/twa.hh>
%import(module="spot.impl") <spot/tl/formula.hh>
%import(module="spot.impl") <spot/tl/apcollect.hh>
%import(module="spot.impl") <spot/kripke/fairkripke.hh>
%import(module="spot.impl") <spot/kripke/kripke.hh>

50
51
52
53
54
55
56
57
58
59
60
61
%exception {
  try {
    $action
  }
  catch (const std::runtime_error& e)
  {
    SWIG_exception(SWIG_RuntimeError, e.what());
  }
}

%rename(model) spot::ltsmin_model;
%rename(kripke_raw) spot::ltsmin_model::kripke;
62
63
64
65
%include <spot/ltsmin/ltsmin.hh>

%pythoncode %{
import spot
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
66
67
68
import spot.aux
import sys
import subprocess
69

70
71
72
def load(filename):
  return model.load(filename)

73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
@spot._extend(model)
class model:
  def kripke(self, ap_set, dict=spot._bdd_dict,
	      dead=spot.formula_ap('dead'),
	      compress=2):
    s = spot.atomic_prop_set()
    for ap in ap_set:
      s.insert(spot.formula_ap(ap))
    return self.kripke_raw(s, dict, dead, compress)

  def info(self):
    res = {}
    ss = self.state_size()
    res['state_size'] = ss
    res['variables'] = [(self.state_variable_name(i),
			 self.state_variable_type(i)) for i in range(ss)]
    tc = self.type_count()
    res['types'] = [(self.type_name(i),
		     [self.type_value_name(i, j)
		      for j in range(self.type_value_count(i))])
		     for i in range(tc)]
    return res

  def __repr__(self):
    res = "ltsmin model with the following variables:\n";
    info = self.info()
    for (var, t) in info['variables']:
      res += '  ' + var + ': ';
      type, vals = info['types'][t]
      if vals:
        res += str(vals)
      else:
        res += type
      res += '\n';
    return res
108

109
def require(*tools):
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
110
111
112
113
114
115
116
    """
    Exit with status code 77 if the required tool is not installed.

    This function is mostly useful in Spot test suite, where 77 is a
    code used to indicate that some test should be skipped.
    """
    import shutil
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
    for tool in tools:
        if tool == "divine":
            if shutil.which("divine") == None:
                print("divine not available", file=sys.stderr)
                sys.exit(77)
            out = subprocess.check_output(['divine', 'compile', '--help'],
                                          stderr=subprocess.STDOUT)
            if b'LTSmin' not in out:
                print("divine available but no support for LTSmin",
                       file=sys.stderr)
                sys.exit(77)
        elif tool == "spins":
            if shutil.which("spins") == None:
                print("spins not available", file=sys.stderr)
                sys.exit(77)
        else:
            raise ValueError("unsupported argument for require(): " + tool)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
134
135


136
137
138
139
140
# Load IPython specific support if we can.
try:
    # Load only if we are running IPython.
    __IPYTHON__

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
141
    from IPython.core.magic import Magics, magics_class, cell_magic
142
143
144
145
146
147
    import os
    import tempfile

    @magics_class
    class EditDVE(Magics):

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
148
149
150
151
        @cell_magic
        def dve(self, line, cell):
            if not line:
               raise ValueError("missing variable name for %%dve")
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
            with spot.aux.tmpdir():
               with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as t:
                   t.write(cell.encode('utf-8'))
                   t.flush()

                   try:
                       p = subprocess.Popen(['divine', 'compile',
                                             '--ltsmin', t.name],
                                            stdout=subprocess.PIPE,
                                            stderr=subprocess.STDOUT,
                                            universal_newlines=True)
                       out = p.communicate()
                       if out[0]:
                          print(out[0], file=sys.stderr)
                       ret = p.wait()
                       if ret:
                          raise subprocess.CalledProcessError(ret, 'divine')
                       self.shell.user_ns[line] = load(t.name + '2C')
                   finally:
                       spot.aux.rm_f(t.name + '.cpp')
                       spot.aux.rm_f(t.name + '2C')
173

174
175
176
177
178
179
180
    @magics_class
    class EditPML(Magics):

        @cell_magic
        def pml(self, line, cell):
            if not line:
               raise ValueError("missing variable name for %%pml")
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
            with spot.aux.tmpdir():
               with tempfile.NamedTemporaryFile(dir='.', suffix='.pml') as t:
                   t.write(cell.encode('utf-8'))
                   t.flush()

                   try:
                       p = subprocess.Popen(['spins', t.name],
                                            stdout=subprocess.PIPE,
                                            stderr=subprocess.STDOUT,
                                            universal_newlines=True)
                       out = p.communicate()
                       if out[0]:
                          print(out[0], file=sys.stderr)
                       ret = p.wait()
                       if ret:
                          raise subprocess.CalledProcessError(ret, 'spins')
                       self.shell.user_ns[line] = load(t.name + '.spins')
                   finally:
                       spot.aux.rm_f(t.name + '.spins.c')
                       spot.aux.rm_f(t.name + '.spins')
201

202
203
    ip = get_ipython()
    ip.register_magics(EditDVE)
204
    ip.register_magics(EditPML)
205
206
207

except (ImportError, NameError):
    pass
208
%}