NEWS 120 KB
Newer Older
1
2
3
4
New in spot 1.99.9a (not yet released)

  Nothing yet.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
5
New in spot 1.99.9 (2016-03-14)
6

7
8
  Command-line tools:

9
10
11
  * autfilt has two new options: --accept-word=WORD and
    --reject-word=WORD for filtering automata that accept or reject
    some word.  The option may be used multiple times.
12

13
14
  Library:

15
16
17
  * The parse_word() function can be used to parse a lasso-shaped
    word and build a twa_word.  The twa_word::as_automaton()
    method can be used to create an automaton out of that.
18
  * twa::ap_var() renamed to twa::ap_vars().
19
20
21
22
  * emptiness_check_instantiator::min_acceptance_conditions() and
    emptiness_check_instantiator::max_acceptance_conditions() renamed
    to emptiness_check_instantiator::min_sets() and
    emptiness_check_instantiator::max_sets().
23
24
  * tgba_reachable_iterator (and subclasses) was renamed to
    twa_reachable_iterator for consistency.
25

26
27
28
29
  Documentation:

  * The page https://spot.lrde.epita.fr/upgrade2.html should help
    people migrating old C++ code written for Spot 1.2.x, and update
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
    it for (the upcoming) Spot 2.0.
31

32
33
34
35
  Bug fixes:

  * spot/twaalgos/gtec/gtec.hh was incorrectly installed as
  spot/tgbaalgos/gtec/gtec.hh.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
36
  * The shared libraries should now compile again on Darwin.
37

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
New in spot 1.99.8 (2016-02-18)
39

40
41
  Command-line tools:

42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
  * ltl2tgba now also support the --generic option (already supported
    by ltldo and autfilt) to lift any restriction on the acceptance
    condition produced.  This option now has a short version: -G.

  * ltl2tgba and autfilt have learnt how to determinize automata.
    For this to work, --generic acceptance should be enabled (this
    is the default for autfilt, but not for ltl2tgba).

    "ltl2tgba -G -D" will now always outpout a deterministic automaton.
    It can be an automaton with transition-based parity acceptance in
    case Spot could not find a deterministic automaton with (maybe
    generalized) Büchi acceptance.

    "ltl2tgba -D" is unchanged (the --tgba acceptance is the default),
    and will output a deterministic automaton with (generalized) Büchi
    acceptance only if one could be found.  Otherwise a
    non-deterministic automaton is output, but this does NOT mean that
    no deterministic Büchi automaton exist for this formula.  It only
    means Spot could not find it.

    "autfilt -D" will determinize any automaton, because --generic
    acceptance is the default for autfilt.

    "autfilt -D --tgba" will behave like "ltl2tgba -D", i.e., it may
    fail to find a deterministic automaton (even if one exists) and
    return a nondeterministic automaton.

69
70
71
72
73
  * "autfilt --complement" now also works for non-deterministic
    automata but will output a deterministic automaton.
    "autfilt --complement --tgba" will likely output a
    nondeterministic TGBA.

74
75
76
  * autfilt has a new option, --included-in, to filter automata whose
    language are included in the language of a given automaton.

77
78
79
  * autfilt has a new option, --equivalent-to, to filter automata
    that are equivalent (language-wise) to a given automaton.

80
81
82
83
84
85
86
  * ltlcross has a new option --determinize to instruct it to
    complement non-deterministic automata via determinization.  This
    option is not enabled by default as it can potentially be slow and
    generate large automata.  When --determinize is given, option
    --product=0 is implied, since the tests based on products with
    random state-space are pointless for deterministic automata.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87
88
89
  * ltl2tgba and ltldo now support %< and %> in the string passed
    to --stats when reading formulas from a CSV file.

90
91
92
93
94
  * ltlfilt's option --size-min=N, --size-max=N, --bsize-min=N, and
    --bsize-max=N have been reimplemented as --size=RANGE and
    --bsize=RANGE.  The old names are still supported for backward
    compatibility, but they are not documented anymore.

95
96
  * ltlfilt's option --ap=N can now take a RANGE as parameter.

97
98
99
  * autfilt now has a --ap=RANGE option to filter automata by number
    of atomic propositions.

100
101
102
103
104
  Library:

  * Building products with different dictionaries now raise an
    exception instead of using an assertion that could be disabled.

105
  * The load_ltsmin() function has been split in two.  Now you should
106
    first call ltsmin_model::load(filename) to create an ltsmin_model,
107
    and then call the ltsmin_model::kripke(...) method to create an
108
109
110
    automaton that can be iterated on the fly.  The intermediate
    object can be queried about the supported variables and their
    types.
111

112
113
114
115
116
117
118
119
120
121
122
123
  * print_dot() now accepts several new options:
    - use "<N" to specify a maximum number of states to output.
      Incomplete states are then marked appropriately.  For a quick
      example, compare
	ltl2tgba -D 'Ga | Gb | Gc' -d'<3'
      with
        ltl2tgba -D 'Ga | Gb | Gc' -d
    - use "C(color)" to specify the color to use for filling states.
    - use "#" to display the internal number of each transition
    - use "k" to use state-based labels when possible.  This is
      similar to the "k" option already supported by print_hoa(), and
      is useful when printing Kripke structures.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
124

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
125
126
  * Option "k" is automatically used by print_dot() and print_hoa()
    when printing Kripke structures.
127

128
129
130
131
  * print_dot() also honnor two new automaton properties called
    "highlight-edges" and "highlight-states".  These are used to color
    a subset of edges or transitions.

132
133
134
135
  * There is a new tgba_determinize() function.  Despite its name, it
    in facts works on transition-based Büchi automaton, and will first
    degeneralize any automaton with generalized Büchi acceptance.

136
137
138
  * The twa_safra_complement class has been removed.  Use
    tgba_determinize() and dtwa_complement() instead.

139
140
  * The twa::transition_annotation() and
    twa::compute_support_conditions() methods have been removed.
141

142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  * The interface for all functions parsing formulas (LTL, PSL, SERE,
    etc.) has been changed to use an interface similar to the one used
    for parsing automata.  These function now return a parsed_formula
    object that includes both a formula and a list of syntax errors.

    Typically a function written as

       spot::formula read(std::string input)
       {
	  spot::parse_error_list pel;
	  spot::formula f = spot::parse_infix_psl(input, pel);
	  if (spot::format_parse_errors(std::cerr, input, pel))
	    exit(2);
	  return f;
       }

    should be updated to

       spot::formula read(std::string input)
       {
	  spot::parsed_formula pf = spot::parse_infix_psl(input);
	  if (pf.format_errors(std::cerr))
	    exit(2);
	  return pf.f;
       }

168
169
  Python:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
170
171
172
  * The ltsmin interface has been binded in Python.  It also
    comes with a %%dve cell magic to edit DiVinE models in the notebook.
    See https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example.
173

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
174
175
176
177
178
  * spot.setup() sets de maximum number of states to display in
    automata to 50 by default, as more states is likely to be
    unreadable (and slow to process by GraphViz).  This can be
    overridden by calling spot.setup(max_states=N).

179
180
181
182
  * Automata now have methods to color selected states and
    transitions.  See
    https://spot.lrde.epita.fr/ipynb/highlighting.html for an example.

183
184
185
186
187
  Documentation:

  * There is a new page giving informal illustrations (and extra
    pointers) for some concepts used in Spot.
    See https://spot.lrde.epita.fr/concepts.html
188

189
  Bug fixes:
190
191
192

  * Using ltl2tgba -U would fail to output the unambiguous property
    (regression introduced in 1.99.7)
193
194
  * ltlfilt, autfilt, randltl, and randaut could easily crash when
    compiled statically (i.e., with configure --disable-shared).
195
  * "1 U (a | Fb)" was not always simplified to "F(a | b)".
196
197
  * destroying the operands of an otf_product() before the product
    itself could crash.
198

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
199
New in spot 1.99.7 (2016-01-15)
200
201
202

  Command-line tools:

203
  * BACKWARD INCOMPATIBLE CHANGE: All tools that output automata now
204
    use the HOA format by default instead of the GraphViz output.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
205
    This makes it easier to pipe several commands together.
206
207
208
209
210
211

    If you have an old script that relies on GraphViz being the default
    output and that you do not want to update it, use
       export SPOT_DEFAULT_FORMAT=dot
    to get the old behavior back.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
212
213
214
  * Tools that output automata now accept -d as a shorthand for --dot
    since requesting the GraphViz (a.k.a. dot) output by hand is now
    more frequent.
215
216
    randaut's short option for specifying edge-density used to be -d:
    it has been renamed to -e.
217

218
  * The SPOT_DEFAULT_FORMAT environment variable can be set to 'dot'
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
219
220
    or 'hoa' to force a default output format for automata.  Additional
    options may also be added, as in SPOT_DEFAULT_FORMAT='hoa=iv'.
221

222
223
  * autfilt has a new option: --is-inherently-weak.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
224
225
226
  * The --check=strength option of all tools that produce automata
    will also test if an automaton is inherently weak.

227
228
  Library:

229
230
231
232
233
234
235
236
237
  * Installed headers now assume that they will be included as
    #include <spot/subdir/header.hh>
    instead of
    #include <subdir/header.hh>

    This implies that when Spot headers are installed in
    /usr/include/spot/... (the default when using the Debian packages)
    or /usr/local/include/spot/... (the default when compiling from
    source), then it is no longuer necessary to add
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
238
239
240
    -I/usr/include/spot or -I/usr/local/include/spot when compiling,
    as /usr/include and /usr/local/include are usually searched by
    default.
241
242
243
244

    Inside the source distribution, the subdirectory src/ has been
    renamed to spot/, so that the root of the source tree can also be
    put on the preprocessor's search path to compile against a
245
246
    non-installed version of Spot.  Similarly, iface/ltsmin/ has been
    renamed to spot/ltsmin/, so that installed and non-installed
247
    directories can be used similarly.
248

249
250
251
252
  * twa::~twa() is now calling
      get_dict()->unregister_all_my_variable(this);
    so this does not need to be done in any subclass.

253
254
255
256
  * is_inherently_weak_automaton() is a new function, and
    check_strength() has been modified to also check inherently weak
    automata.

257
258
259
260
  * decompose_strength() is now extracting inherently weak SCCs
    instead of just weak SCCs.  This gets rid of some corner cases
    that used to require ad hoc handling.

261
262
263
264
  * acc_cond::acc_code's methods append_or(), append_and(), and
    shift_left() have been replaced by operators |=, &=, <<=, and for
    completeness the operators |, &, and << have been added.

265
266
267
  * Several methods have been removed from the acc_cond
    class because they were simply redundant with the methods of
    acc_cond::mark_t, and more complex to use.
268

269
       acc_cond::marks(...)      -> use acc_cond::mark_t(...)
270
       acc_cond::sets(m)         -> use m.sets()
271
       acc_cond::has(m, u)       -> use m.has(u)
272
273
274
275
       acc_cond::cup(l, r)       -> use l | r
       acc_cond::cap(l, r)       -> use l & r
       acc_cond::set_minus(l, r) -> use l - r

276
    Additionally, the following methods/functions have been renamed:
277
278
279

       acc_cond::is_tt() -> acc_cond::is_t()
       acc_cond::is_ff() -> acc_cond::is_f()
280
       parse_acc_code()  -> acc_cond::acc_code(...)
281

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
282
  * Automata property flags (those that tell whether the automaton is
283
284
285
    deterministic, weak, stutter-invariant, etc.) are now stored using
    three-valued logic: in addition to "maybe"/"yes" they can now also
    represent "no".  This is some preparation for the upcomming
286
287
288
289
290
291
292
293
    support of the HOA v1.1 format, but it also saves time in some
    algorithms (e.g, is_deterministic() can now return immediately on
    automata marked as not deterministic).

  * The automaton parser now accept negated properties as they will be
    introduced in HOA v1.1, and will check for some inconsistencies.
    These properties are stored and used when appropriate, but they
    are not yet output by the HOA printer.
294

295
296
  Python:

297
298
299
300
  * Iterating over the transitions leaving a state (the
    twa_graph::out() C++ function) is now possible in Python.  See
    https://spot.lrde.epita.fr/tut21.html for a demonstration.

301
302
303
304
  * Membership to acceptance sets can be specified using Python list
    when calling for instance the Python version of twa_graph::new_edge().
    See https://spot.lrde.epita.fr/tut22.html for a demonstration.

305
306
307
  * Automaton states can be named via the set_state_names() method.
    See https://spot.lrde.epita.fr/ipynb/product.html for an example.

308
309
310
311
312
  Documentation:

  * There is a new page explaining how to compile example programs and
    and link them with Spot.  https://spot.lrde.epita.fr/compile.html

313
314
315
316
317
  * Python bindings for manipulating acceptance conditions are
    demonstrated by https://spot.lrde.epita.fr/ipynb/acc_cond.html,
    and a Python implementation of the product of two automata is
    illustrated by https://spot.lrde.epita.fr/ipynb/product.html

318
319
320
321
322
323
324
325
326
327
328
329
  Source code reorganisation:

  * A lot of directories have been shuffled around in the
    distribution:
      src/                   ->  spot/    (see rational above)
      iface/ltsmin/  (code)  ->  spot/ltsmin/
      wrap/python/           ->  python/
      src/tests/             ->  tests/core/
      src/sanity/            ->  tests/sanity/
      iface/ltsmin/  (tests) ->  tests/ltsmin/
      wrap/python/tests      ->  tests/python/

330
331
  Bug fixes:

332
333
  * twa_graph would incorrectly replace named-states during
    purge_dead_states and purge_unreachable_states.
334
335
  * twa::ap() would contain duplicates when an atomic proposition
    was registered several times.
336
337
  * product() would incorrectly mark the product of two
    sttuter-sensitive automata as stutter-sensitive as well.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
338
339
  * complete() could incorrectly reuse an existing (but accepting!)
    state as a sink.
340

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
341
New in spot 1.99.6 (2015-12-04)
342

343
344
  Command-line tools:

345
346
347
348
  * autfilt has two new filters: --is-weak and --is-terminal.

  * autfilt has a new transformation: --decompose-strength,
    implementing the decomposition of our TACAS'13 paper.
349
350
    A demonstration of this feature via the Python bindings
    can be found at https://spot.lrde.epita.fr/ipynb/decompose.html
351

352
353
354
355
356
357
  * All tools that output HOA files accept a --check=strength option
    to request automata to be marked as "weak" or "terminal" as
    appropriate.  Without this option, these properties may only be
    set as a side-effect of running transformations that use this
    information.

358
359
360
361
362
363
364
  Library:

  * Properties of automata (like the "properties:" line of the HOA
    format) are stored as bits whose interpretation is True=yes,
    False=maybe.  Having getters like "aut->is_deterministic()" or
    "aut->is_unambiguous()" was confusing, because there are separate
    functions "is_deterministic(aut)" and "is_unambiguous(aut)" that
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
365
366
    do actually check the automaton.  The getters have been renamed to
    avoid confusion, and get names more in line with the HOA format.
367
368
369
370
371
372
373
374
375

    - twa::has_state_based_acc() -> twa::prop_state_acc()
    - twa::prop_state_based_acc(bool) -> twa::prop_state_acc(bool)
    - twa::is_inherently_weak() -> twa::prop_inherently_weak()
    - twa::is_deterministic() -> twa::prop_deterministic()
    - twa::is_unambiguous() -> twa::prop_unambiguous()
    - twa::is_stutter_invariant() -> twa::prop_stutter_invariant()
    - twa::is_stutter_sensitive() -> twa::prop_stutter_sensitive()

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
376
    The setters have the same names as the getters, except they take a
377
378
379
    Boolean argument.  This argument used to be optionnal (defaulting
    to True), but it no longer is.

380
381
382
383
384
385
386
387
388
389
  * Automata now support the "weak" and "terminal" properties in
    addition to the previously supported "inherently-weak".

  * By default the HOA printer tries not to bloat the output with
    properties that are redundant and probably useless.  The HOA
    printer now has a new option "v" (use "-Hv" from the command line)
    to output more verbose "properties:".  This currently includes
    outputing "no-univ-branch", outputting "unambiguous" even for
    automata already tagged as "deterministic", and "inherently-weak"
    or "weak" even for automata tagged "weak" or "terminal".
390