diff --git a/NEWS b/NEWS index 70b7a369d67597ea3df9b93844fcc30e09cf1ae9..25682d60cf1bee933518218c91611450460df0a7 100644 --- a/NEWS +++ b/NEWS @@ -23,6 +23,11 @@ New in spot 1.99.7a (not yet released) pointers) for some concepts used in Spot. 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) Command-line tools: diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index e4fd6014aea24bc9094ed16840539e5c63b9ff90..59290c271da29e6be98bfb07d35397ecfb70c35e 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -2193,7 +2193,7 @@ namespace spot } if (unambiguous) - a->prop_unambiguous(); + a->prop_unambiguous(true); // Set the following to true to preserve state names. a->release_formula_namer(namer, false); diff --git a/tests/core/unambig.test b/tests/core/unambig.test index 72184a3f87e96e0ce42f8ee358a5a0fb4c59e042..ea36a8912af10a2b5f16947e4b48bd71e24dbba2 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement -# de l'Epita +# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et +# Developpement de l'Epita # # This file is part of Spot, a model checking library. # @@ -187,6 +187,12 @@ State: 2 --END-- 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. run 0 $autfilt -H --is-unambiguous input >output