1# This file was automatically generated by SWIG (http://www.swig.org).
2# Version 4.0.2
3#
4# Do not make changes to this file unless you know what you are doing--modify
5# the SWIG interface file instead.
6
7from sys import version_info as _swig_python_version_info
8if _swig_python_version_info < (2, 7, 0):
9    raise RuntimeError("Python 2.7 or later required")
10
11# Import the low-level C/C++ module
12if __package__ or "." in __name__:
13    from . import _ltsmin
14else:
15    import _ltsmin
16
17try:
18    import builtins as __builtin__
19except ImportError:
20    import __builtin__
21
22_swig_new_instance_method = _ltsmin.SWIG_PyInstanceMethod_New
23_swig_new_static_method = _ltsmin.SWIG_PyStaticMethod_New
24
25def _swig_repr(self):
26    try:
27        strthis = "proxy of " + self.this.__repr__()
28    except __builtin__.Exception:
29        strthis = ""
30    return "<%s.%s; %s >" % (self.__class__.__module__, self.__class__.__name__, strthis,)
31
32
33def _swig_setattr_nondynamic_instance_variable(set):
34    def set_instance_attr(self, name, value):
35        if name == "thisown":
36            self.this.own(value)
37        elif name == "this":
38            set(self, name, value)
39        elif hasattr(self, name) and isinstance(getattr(type(self), name), property):
40            set(self, name, value)
41        else:
42            raise AttributeError("You cannot add instance attributes to %s" % self)
43    return set_instance_attr
44
45
46def _swig_setattr_nondynamic_class_variable(set):
47    def set_class_attr(cls, name, value):
48        if hasattr(cls, name) and not isinstance(getattr(cls, name), property):
49            set(cls, name, value)
50        else:
51            raise AttributeError("You cannot add class attributes to %s" % cls)
52    return set_class_attr
53
54
55def _swig_add_metaclass(metaclass):
56    """Class decorator for adding a metaclass to a SWIG wrapped class - a slimmed down version of six.add_metaclass"""
57    def wrapper(cls):
58        return metaclass(cls.__name__, cls.__bases__, cls.__dict__.copy())
59    return wrapper
60
61
62class _SwigNonDynamicMeta(type):
63    """Meta class to enforce nondynamic attributes (no new attributes) for a class"""
64    __setattr__ = _swig_setattr_nondynamic_class_variable(type.__setattr__)
65
66
67import spot.impl
68SHARED_PTR_DISOWN = _ltsmin.SHARED_PTR_DISOWN
69class model(object):
70    thisown = property(lambda x: x.this.own(), lambda x, v: x.this.own(v), doc="The membership flag")
71
72    def __init__(self, *args, **kwargs):
73        raise AttributeError("No constructor defined")
74    __repr__ = _swig_repr
75    __swig_destroy__ = _ltsmin.delete_model
76    load = _swig_new_static_method(_ltsmin.model_load)
77    kripke_raw = _swig_new_instance_method(_ltsmin.model_kripke_raw)
78    kripkecube = _swig_new_instance_method(_ltsmin.model_kripkecube)
79    state_size = _swig_new_instance_method(_ltsmin.model_state_size)
80    state_variable_name = _swig_new_instance_method(_ltsmin.model_state_variable_name)
81    state_variable_type = _swig_new_instance_method(_ltsmin.model_state_variable_type)
82    type_count = _swig_new_instance_method(_ltsmin.model_type_count)
83    type_name = _swig_new_instance_method(_ltsmin.model_type_name)
84    type_value_count = _swig_new_instance_method(_ltsmin.model_type_value_count)
85    type_value_name = _swig_new_instance_method(_ltsmin.model_type_value_name)
86
87# Register model in _ltsmin:
88_ltsmin.model_swigregister(model)
89model_load = _ltsmin.model_load
90
91
92import spot
93import spot.aux
94import sys
95import subprocess
96import os.path
97import re
98
99def load(filename):
100# Compile promela model with Spins by end, even if it would be done in model.load,
101# so we can capture the output of the compilation regardless of the Jupyter version.
102# (Older Jupyter version to not send the output to the notebook, and newer versions
103# do it asynchronously in a way that make testing quite hard.)
104  if filename.endswith('.pm') or filename.endswith('.pml') or filename.endswith('.prom'):
105    dst = os.path.basename(filename) + '.spins'
106    if not os.path.exists(dst) or (os.path.getmtime(dst) < os.path.getmtime(filename)):
107      p = subprocess.run(['spins', filename], stdout=subprocess.PIPE,
108                         stderr=subprocess.STDOUT,
109                         universal_newlines=True)
110      if p.stdout: print(re.sub('^\s*\[\.*\s*\]\n', '', p.stdout,
111                                flags=re.MULTILINE), file=sys.stderr)
112      if p.stderr: print(p.stderr, file=sys.stderr)
113      p.check_returncode()
114      filename = dst
115  return model.load(filename)
116
117@spot._extend(model)
118class model:
119  def kripke(self, ap_set, dict=spot._bdd_dict,
120	      dead=spot.formula_ap('dead'),
121	      compress=2):
122    s = spot.atomic_prop_set()
123    for ap in ap_set:
124      s.insert(spot.formula_ap(ap))
125    return self.kripke_raw(s, dict, dead, compress)
126
127  def info(self):
128    res = {}
129    ss = self.state_size()
130    res['state_size'] = ss
131    res['variables'] = [(self.state_variable_name(i),
132			 self.state_variable_type(i)) for i in range(ss)]
133    tc = self.type_count()
134    res['types'] = [(self.type_name(i),
135		     [self.type_value_name(i, j)
136		      for j in range(self.type_value_count(i))])
137		     for i in range(tc)]
138    return res
139
140  def __repr__(self):
141    res = "ltsmin model with the following variables:\n";
142    info = self.info()
143    for (var, t) in info['variables']:
144      res += '  ' + var + ': ';
145      type, vals = info['types'][t]
146      if vals:
147        res += str(vals)
148      else:
149        res += type
150      res += '\n';
151    return res
152
153def require(*tools):
154    """
155    Exit with status code 77 if the required tool is not installed.
156
157    This function is mostly useful in Spot test suite, where 77 is a
158    code used to indicate that some test should be skipped.
159    """
160    import shutil
161    for tool in tools:
162        if tool == "divine":
163            if shutil.which("divine") == None:
164                print("divine not available", file=sys.stderr)
165                sys.exit(77)
166            try:
167                out = subprocess.check_output(['divine', 'compile', '--help'],
168                                              stderr=subprocess.STDOUT)
169            except (subprocess.CalledProcessError):
170                print("divine does not understand 'compile --help'",
171                       file=sys.stderr)
172                sys.exit(77)
173            if b'LTSmin' not in out:
174                print("divine available but no support for LTSmin",
175                       file=sys.stderr)
176                sys.exit(77)
177        elif tool == "spins":
178            if shutil.which("spins") == None:
179                print("spins not available", file=sys.stderr)
180                sys.exit(77)
181        else:
182            raise ValueError("unsupported argument for require(): " + tool)
183
184
185# Load IPython specific support if we can.
186try:
187# Load only if we are running IPython.
188    __IPYTHON__
189
190    from IPython.core.magic import Magics, magics_class, cell_magic
191    import os
192    import tempfile
193
194    @magics_class
195    class EditDVE(Magics):
196
197        @cell_magic
198        def dve(self, line, cell):
199            if not line:
200               raise ValueError("missing variable name for %%dve")
201            with spot.aux.tmpdir():
202               with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as t:
203                   t.write(cell.encode('utf-8'))
204                   t.flush()
205
206                   try:
207                       p = subprocess.run(['divine', 'compile',
208                                             '--ltsmin', t.name],
209                                            capture_output=True,
210                                            universal_newlines=True)
211                       if p.stdout: print(p.stdout)
212                       if p.stderr: print(p.stderr, file=sys.stderr)
213                       p.check_returncode()
214                       self.shell.user_ns[line] = load(t.name + '2C')
215                   finally:
216                       spot.aux.rm_f(t.name + '.cpp')
217                       spot.aux.rm_f(t.name + '2C')
218
219    @magics_class
220    class EditPML(Magics):
221
222        @cell_magic
223        def pml(self, line, cell):
224            if not line:
225               raise ValueError("missing variable name for %%pml")
226            with spot.aux.tmpdir():
227               with tempfile.NamedTemporaryFile(dir='.', suffix='.pml') as t:
228                   t.write(cell.encode('utf-8'))
229                   t.flush()
230                   try:
231                       self.shell.user_ns[line] = load(t.name)
232                   finally:
233                       spot.aux.rm_f(t.name + '.spins.c')
234                       spot.aux.rm_f(t.name + '.spins')
235
236    ip = get_ipython()
237    ip.register_magics(EditDVE)
238    ip.register_magics(EditPML)
239
240except (ImportError, NameError):
241    pass
242
243
244
245