[Spot] Bug Report

Alexandre Duret-Lutz adl at lrde.epita.fr
Wed Aug 5 22:13:48 CEST 2015


Hi Oscar,

On Wed, Aug 5, 2015 at 7:31 PM, Oscar Chang <oscar.chang at stcatz.ox.ac.uk> wrote:
> If you enter (FGa)||(FGb) and tick the option for the degeneralized buchi automaton, it still gives a generalised one.

Thank you for the report, but unfortunately I cannot reproduce it.

If I enter this formula I get a transition-based BA with a single
acceptance set.  When I tick the "state-based degeneralized B├╝chi
automaton" box, I get the same automaton but with state-based
acceptance (as expected).  See attached screenshots.

It might be browser related; what do you use?  I've tested with
Iceweasel 38.0.1 and Chromium 43.0.2357.65.

Best regards,
-- 
Alexandre Duret-Lutz
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TBAvsBA.png
Type: image/png
Size: 111123 bytes
Desc: not available
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20150805/ed75f897/attachment-0001.png>


More information about the Spot mailing list