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'