From c06e15e085fe0e696a043679d19d11f073cd4774 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Feb 2021 12:20:42 +0100 Subject: [PATCH] fix eventual/universal properties for ->/<->/xor * spot/tl/formula.cc: Correctly set eventual and universal properties for ->, <->, and xor. This wasn't really relevant before, but there are now situation where those are not rewritten. * tests/core/kind.test: Adjust expected output. * tests/core/ltl2tgba2.test: New test case, reported by Florian Renkin. * NEWS: Mention the bug. --- NEWS | 3 +++ spot/tl/formula.cc | 14 ++++++++------ tests/core/kind.test | 8 ++++---- tests/core/ltl2tgba2.test | 9 +++++++++ 4 files changed, 24 insertions(+), 10 deletions(-) diff --git a/NEWS b/NEWS index e187230d7..03dd5bd3a 100644 --- a/NEWS +++ b/NEWS @@ -186,6 +186,9 @@ New in spot 2.9.6.dev (not yet released) - tgba_determinize() could create parity automata using more colors than necessary. (Related to issue #298) + - Some formulas using ->, <->, or xor were not properly detected as + purely universal or pure eventualities. + New in spot 2.9.6 (2021-01-18) Build: diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 05b295708..346d77fce 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -1283,8 +1283,8 @@ namespace spot case op::Xor: case op::Equiv: props = children[0]->props & children[1]->props; - is_.eventual = false; - is_.universal = false; + // Preserve suspendable property + is_.eventual = is_.universal = is_.eventual && is_.universal; is_.sere_formula = is_.boolean; is_.sugar_free_boolean = false; is_.in_nenoform = false; @@ -1310,8 +1310,10 @@ namespace spot break; case op::Implies: props = children[0]->props & children[1]->props; - is_.eventual = false; - is_.universal = false; + is_.eventual = + children[0]->is_universal() && children[1]->is_eventual(); + is_.universal = + children[0]->is_eventual() && children[1]->is_universal(); is_.sere_formula = (children[0]->is_boolean() && children[1]->is_sere_formula()); is_.sugar_free_boolean = false; diff --git a/tests/core/kind.test b/tests/core/kind.test index db04fc6d2..d6413211a 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010-2012, 2015, 2017, 2019 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2010-2012, 2015, 2017, 2019, 2021 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -47,8 +47,8 @@ a U (b U (c U d)),&!xfLPgopra a W (b W (c W d)),&!xfLPsopra a M (b M (c M d)),&!xfLPgopra Fa -> Fb,xLPopra -Ga -> Fb,xLPgopra -Fa -> Gb,xLPsopra +Ga -> Fb,xLPegopra +Fa -> Gb,xLPusopra (Ga|Fc) -> Fb,xLPopra (Ga|Fa) -> Gb,xLPopra {a;c*;b}|->!Xb,&fPsopra diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 7e512c17a..79a07a17a 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -507,3 +507,12 @@ med.hoa:4,14 high.hoa:4,14 EOF diff exp out + +# This used to fail because ltl-split would not detect +# the (GFa <-> (GFb & GFc & GFd & GFe & GFf & GFg & GFh)) part +# as suspendable. +f='G((a -> X((!a U b) | G!a)) & (a -> X(G!a | (!a U c))) & (a -> X(G!a +| (!a U d))) & (a -> X(G!a | (!a U e))) & (a -> X(G!a | (!a U f))) & +(a -> X(G!a | (!a U g))) & (a -> X(G!a | (!a U h)))) & (GFa <-> (GFb & +GFc & GFd & GFe & GFf & GFg & GFh))' +test 128 = `ltl2tgba -G -D "$f" --stats=%s`