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 _gen
14else:
15    import _gen
16
17try:
18    import builtins as __builtin__
19except ImportError:
20    import __builtin__
21
22_swig_new_instance_method = _gen.SWIG_PyInstanceMethod_New
23_swig_new_static_method = _gen.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
67SHARED_PTR_DISOWN = _gen.SHARED_PTR_DISOWN
68import spot.impl
69AUT_BEGIN = _gen.AUT_BEGIN
70AUT_KS_NCA = _gen.AUT_KS_NCA
71AUT_L_NBA = _gen.AUT_L_NBA
72AUT_L_DSA = _gen.AUT_L_DSA
73AUT_M_NBA = _gen.AUT_M_NBA
74AUT_END = _gen.AUT_END
75aut_pattern = _gen.aut_pattern
76aut_pattern_name = _gen.aut_pattern_name
77LTL_BEGIN = _gen.LTL_BEGIN
78LTL_AND_F = _gen.LTL_AND_F
79LTL_AND_FG = _gen.LTL_AND_FG
80LTL_AND_GF = _gen.LTL_AND_GF
81LTL_CCJ_ALPHA = _gen.LTL_CCJ_ALPHA
82LTL_CCJ_BETA = _gen.LTL_CCJ_BETA
83LTL_CCJ_BETA_PRIME = _gen.LTL_CCJ_BETA_PRIME
84LTL_DAC_PATTERNS = _gen.LTL_DAC_PATTERNS
85LTL_EH_PATTERNS = _gen.LTL_EH_PATTERNS
86LTL_FXG_OR = _gen.LTL_FXG_OR
87LTL_GF_EQUIV = _gen.LTL_GF_EQUIV
88LTL_GF_EQUIV_XN = _gen.LTL_GF_EQUIV_XN
89LTL_GF_IMPLIES = _gen.LTL_GF_IMPLIES
90LTL_GF_IMPLIES_XN = _gen.LTL_GF_IMPLIES_XN
91LTL_GH_Q = _gen.LTL_GH_Q
92LTL_GH_R = _gen.LTL_GH_R
93LTL_GO_THETA = _gen.LTL_GO_THETA
94LTL_GXF_AND = _gen.LTL_GXF_AND
95LTL_HKRSS_PATTERNS = _gen.LTL_HKRSS_PATTERNS
96LTL_KR_N = _gen.LTL_KR_N
97LTL_KR_NLOGN = _gen.LTL_KR_NLOGN
98LTL_KV_PSI = _gen.LTL_KV_PSI
99LTL_MS_EXAMPLE = _gen.LTL_MS_EXAMPLE
100LTL_MS_PHI_H = _gen.LTL_MS_PHI_H
101LTL_MS_PHI_R = _gen.LTL_MS_PHI_R
102LTL_MS_PHI_S = _gen.LTL_MS_PHI_S
103LTL_OR_FG = _gen.LTL_OR_FG
104LTL_OR_G = _gen.LTL_OR_G
105LTL_OR_GF = _gen.LTL_OR_GF
106LTL_P_PATTERNS = _gen.LTL_P_PATTERNS
107LTL_PPS_ARBITER_STANDARD = _gen.LTL_PPS_ARBITER_STANDARD
108LTL_PPS_ARBITER_STRICT = _gen.LTL_PPS_ARBITER_STRICT
109LTL_R_LEFT = _gen.LTL_R_LEFT
110LTL_R_RIGHT = _gen.LTL_R_RIGHT
111LTL_RV_COUNTER = _gen.LTL_RV_COUNTER
112LTL_RV_COUNTER_CARRY = _gen.LTL_RV_COUNTER_CARRY
113LTL_RV_COUNTER_CARRY_LINEAR = _gen.LTL_RV_COUNTER_CARRY_LINEAR
114LTL_RV_COUNTER_LINEAR = _gen.LTL_RV_COUNTER_LINEAR
115LTL_SB_PATTERNS = _gen.LTL_SB_PATTERNS
116LTL_SEJK_F = _gen.LTL_SEJK_F
117LTL_SEJK_J = _gen.LTL_SEJK_J
118LTL_SEJK_K = _gen.LTL_SEJK_K
119LTL_SEJK_PATTERNS = _gen.LTL_SEJK_PATTERNS
120LTL_TV_F1 = _gen.LTL_TV_F1
121LTL_TV_F2 = _gen.LTL_TV_F2
122LTL_TV_G1 = _gen.LTL_TV_G1
123LTL_TV_G2 = _gen.LTL_TV_G2
124LTL_TV_UU = _gen.LTL_TV_UU
125LTL_U_LEFT = _gen.LTL_U_LEFT
126LTL_U_RIGHT = _gen.LTL_U_RIGHT
127LTL_END = _gen.LTL_END
128ltl_pattern = _gen.ltl_pattern
129ltl_pattern_name = _gen.ltl_pattern_name
130ltl_pattern_max = _gen.ltl_pattern_max
131ltl_pattern_argc = _gen.ltl_pattern_argc
132
133def ltl_patterns(*args):
134  """
135  Generate LTL patterns.
136
137  Each argument should specify a pattern with a
138  range for its parameter(s).
139
140  For single-parameter patterns, arguments of
141  ltl_patterns() should be have one of these three forms:
142    - (id, n)
143    - (id, min, max)
144    - id
145  In the first case, the pattern id=n is generated.  In the second
146  case, all pattern id=n for min<=n<=max are generated.  The
147  third case is a shorthand for (id, 1, 10), except when
148  id denotes one of the hard-coded list of LTL formulas (like,
149  DAC_PATTERNS, EH_PATTERNS, etc.) where all formulas from that
150  list are output.
151
152  For two-parameter patterns, arguments of
153  ltl_patterns() should be have one of these four forms:
154    - (id, n1)
155    - (id, n1, n2)
156    - (id, min1, max1, min2, max2)
157    - id
158  In the first case, n2 is assumed to be equal to n1.  In
159  the third case, all combination of n1 and n2 such that
160  min1<=n1<=max1 and min2<=n2<=max2 are generated.  The
161  last case is a shorthand for (id, 1, 3, 1, 3).
162  """
163  for spec in args:
164    min2 = -1
165    max2 = -1
166    if type(spec) is int:
167      pat = spec
168      min = 1
169      argc = ltl_pattern_argc(spec)
170      if argc == 1:
171        max = ltl_pattern_max(spec) or 10
172      else:
173        min2 = 1
174        max = max2 = 3
175    else:
176      argc = ltl_pattern_argc(spec[0])
177      ls = len(spec)
178      if argc == 1:
179        if ls == 2:
180          pat, min, max = spec[0], spec[1], spec[1]
181        elif ls == 3:
182          pat, min, max = spec
183        else:
184          raise RuntimeError("invalid pattern specification " + str(spec))
185      else:
186        if ls == 2:
187          pat, min, max, min2, max2 = \
188            spec[0], spec[1], spec[1], spec[1], spec[1]
189        elif ls == 3:
190          pat, min, max, min2, max2 = \
191            spec[0], spec[1], spec[1], spec[2], spec[2]
192        elif ls == 5:
193          pat, min, max, min2, max2 = spec
194        else:
195          raise RuntimeError("invalid pattern specification " + str(spec))
196    for n in range(min, max + 1):
197      for m in range(min2, max2 + 1):
198        yield ltl_pattern(pat, n, m)
199
200
201# Override aut_pattern now(), because %feature("shadow") does not
202# seem to work correctly.  See https://github.com/swig/swig/issues/980
203def aut_pattern(pattern: 'spot::gen::aut_pattern_id', n: 'int',
204                dict: 'spot::bdd_dict_ptr' = None) -> "spot::twa_graph_ptr":
205  return _gen.aut_pattern(pattern, n, dict or spot._bdd_dict)
206
207
208def aut_patterns(*args):
209  """
210  Generate automata patterns.
211
212  The arguments should be have one of these three forms:
213    - (id, n)
214    - (id, min, max)
215    - id
216  In the first case, the pattern id=n is generated.  In the second
217  case, all pattern id=n for min<=n<=max are generated.  The
218  third case is a shorthand for (id, 1, 10).
219  """
220  for spec in args:
221    if type(spec) is int:
222      pat = spec
223      min = 1
224      max = 10
225    else:
226      ls = len(spec)
227      if ls == 2:
228        pat, min, max = spec[0], spec[1], spec[1]
229      elif ls == 3:
230        pat, min, max = spec
231      else:
232        raise RuntimeError("invalid pattern specification")
233    for n in range(min, max + 1):
234      yield aut_pattern(pat, n)
235
236
237
238