ltl2tgba_fm: fix setting of unambiguous property
Report from Joachim Klein. * spot/twaalgos/ltl2tgba_fm.cc: Set the property, do not read it. * tests/core/unambig.test: Add a test. * NEWS: Mention the bug.
This commit is contained in:
parent
a3c2691632
commit
c968e7b856
3 changed files with 14 additions and 3 deletions
5
NEWS
5
NEWS
|
|
@ -23,6 +23,11 @@ New in spot 1.99.7a (not yet released)
|
||||||
pointers) for some concepts used in Spot.
|
pointers) for some concepts used in Spot.
|
||||||
See https://spot.lrde.epita.fr/concepts.html
|
See https://spot.lrde.epita.fr/concepts.html
|
||||||
|
|
||||||
|
Bugs:
|
||||||
|
|
||||||
|
* Using ltl2tgba -U would fail to output the unambiguous property
|
||||||
|
(regression introduced in 1.99.7)
|
||||||
|
|
||||||
New in spot 1.99.7 (2016-01-15)
|
New in spot 1.99.7 (2016-01-15)
|
||||||
|
|
||||||
Command-line tools:
|
Command-line tools:
|
||||||
|
|
|
||||||
|
|
@ -2193,7 +2193,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
if (unambiguous)
|
if (unambiguous)
|
||||||
a->prop_unambiguous();
|
a->prop_unambiguous(true);
|
||||||
|
|
||||||
// Set the following to true to preserve state names.
|
// Set the following to true to preserve state names.
|
||||||
a->release_formula_namer(namer, false);
|
a->release_formula_namer(namer, false);
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement
|
# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et
|
||||||
# de l'Epita
|
# Developpement de l'Epita
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
#
|
#
|
||||||
|
|
@ -187,6 +187,12 @@ State: 2
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
|
|
||||||
|
# Thus should be marked as unambiguous. Report from Joachim Klein.
|
||||||
|
ltl2tgba --lbt-input -B -U -x wdba-minimize=0 "U p0 & p1 X ! p0" |
|
||||||
|
grep 'properties:.*unambiguous'
|
||||||
|
|
||||||
|
|
||||||
# Make sure we preserve the "unambiguous" property if it is given.
|
# Make sure we preserve the "unambiguous" property if it is given.
|
||||||
run 0 $autfilt -H --is-unambiguous input >output
|
run 0 $autfilt -H --is-unambiguous input >output
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue