diff --git a/ChangeLog b/ChangeLog index a38b7f759..b42f1a8fe 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,7 @@ 2004-05-17 Alexandre Duret-Lutz + * src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks. + * src/tgbaalgos/neverclaim.cc: Fix them. * sanity/style.test: Diagnose semicolons with leading spaces. diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index e075bb020..cc6b7013f 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -22,7 +22,6 @@ #include "ltlast/allnodes.hh" #include "ltlvisit/clone.hh" #include "lunabbrev.hh" -#include "reducform.hh" #include namespace spot @@ -72,25 +71,19 @@ namespace spot unop::instance(unop::Not, f2))); return; - /* true U f2 == F(f2) */ case binop::U: - if ( node_type(f1) == node_type_form_visitor::Const ) - if ( ((constant*)f1)->val() == constant::True ) { - result_ = unop::instance(unop::F,f2); - return; - } - result_ = binop::instance(bo->op(), f1, f2); + if (f1 == constant::true_instance()) + result_ = unop::instance(unop::F, f2); + else + result_ = binop::instance(bo->op(), f1, f2); return; - /* false R f2 == G(f2) */ case binop::R: - if ( node_type(f1) == node_type_form_visitor::Const ) - if ( ((constant*)f1)->val() == constant::False ) { - result_ = unop::instance(unop::G,f2); - return; - } - result_ = binop::instance(bo->op(), f1, f2); + if (f1 == constant::false_instance()) + result_ = unop::instance(unop::G, f2); + else + result_ = binop::instance(bo->op(), f1, f2); return; } /* Unreachable code. */