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