From 54fd973a90f7c551779e8e9bcd4a965d12e99aeb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 6 Feb 2012 13:18:52 +0100 Subject: [PATCH] Fix computation of syntactic classes for Implies. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * src/ltlast/binop.cc (binop::binop): Fix computation of syntactic guarantee and syntactic obligation for the Implies operator. Reported by Étienne Renault. * src/ltltest/kind.test: Add more tests. --- src/ltlast/binop.cc | 6 +++--- src/ltltest/kind.test | 7 ++++++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index c2866d4c3..e69c47f68 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -95,9 +95,9 @@ namespace spot is.sugar_free_boolean = false; is.in_nenoform = false; is.syntactic_safety = - first->is_syntactic_obligation() && second->is_syntactic_safety(); - is.syntactic_obligation = - first->is_syntactic_safety() && second->is_syntactic_obligation(); + first->is_syntactic_guarantee() && second->is_syntactic_safety(); + is.syntactic_guarantee = + first->is_syntactic_safety() && second->is_syntactic_guarantee(); // is.syntactic_obligation inherited is.syntactic_persistence = first->is_syntactic_recurrence() && second->is_syntactic_persistence(); diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 1211033e0..122364d95 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement to +# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Developement to # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -53,6 +53,11 @@ check 'a R (b R (c R d))' '&!xfLPsopr' check 'a U (b U (c U d))' '&!xfLPgopr' check 'a W (b W (c W d))' '&!xfLPsopr' check 'a M (b M (c M d))' '&!xfLPgopr' +check 'Fa -> Fb' 'xLPopr' +check 'Ga -> Fb' 'xLPgopr' +check 'Fa -> Gb' 'xLPsopr' +check '(Ga|Fc) -> Fb' 'xLPopr' +check '(Ga|Fa) -> Gb' 'xLPopr' check '{a;c*;b}|->!Xb' '&fPsopr' check '{a;c*;b}|->X!b' '&!fPsopr' check '{a;c*;b}|->!Fb' '&xPsopr'