ltsmin.i 5.12 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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
def require(tool):
    """
    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.
    """
    if tool != "divine":
        raise ValueError("unsupported argument for require(): " + tool)
    import shutil
    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)


130 131 132 133 134
# 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
135
    from IPython.core.magic import Magics, magics_class, cell_magic
136 137 138 139 140 141
    import os
    import tempfile

    @magics_class
    class EditDVE(Magics):

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
142 143 144 145 146 147 148 149 150 151
        @cell_magic
        def dve(self, line, cell):
            if not line:
               raise ValueError("missing variable name for %%dve")
            # DiViNe prefers when files are in the current directory
            # so write cell into local file
            with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as t:
                t.write(cell.encode('utf-8'))
                t.flush()

152
                try:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
153 154 155 156 157 158 159 160 161 162 163 164
                    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')
165
                finally:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
166 167
                    spot.aux.rm_f(t.name + '.cpp')
                    spot.aux.rm_f(t.name + '2C')
168 169 170 171 172 173

    ip = get_ipython()
    ip.register_magics(EditDVE)

except (ImportError, NameError):
    pass
174
%}