Commit cfcfb6d4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks.

parent 25dc63d1
2004-05-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks.
* src/tgbaalgos/neverclaim.cc: Fix them.
* sanity/style.test: Diagnose semicolons with leading spaces.
......
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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 <cassert>
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. */
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment