diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index e65a43b28..ab9b9c686 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -68,8 +68,10 @@ namespace spot is.psl_formula = false; is.accepting_eword = false; break; - case Closure: case NegClosure: + is.not_marked = false; + // fall through + case Closure: is.boolean = false; is.ltl_formula = false; is.eltl_formula = false; diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 8ab52cad9..61c3a8dd3 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -29,103 +29,6 @@ namespace spot { namespace { - - class has_mark_visitor : public visitor - { - bool result_; - public: - has_mark_visitor() - : result_(false) - { - } - ~has_mark_visitor() - { - } - - bool - result() - { - return result_; - } - - void - visit(atomic_prop*) - { - } - - void - visit(constant*) - { - } - - void - visit(bunop*) - { - } - - void - visit(unop* uo) - { - switch (uo->op()) - { - case unop::NegClosure: - result_ = true; - return; - case unop::Finish: - case unop::Closure: - case unop::Not: - case unop::X: - case unop::F: - case unop::G: - return; - } - /* Unreachable code. */ - assert(0); - } - - void - visit(automatop*) - { - } - - void - visit(multop* mo) - { - unsigned mos = mo->size(); - for (unsigned i = 0; i < mos && !result_; ++i) - result_ = recurse(mo->nth(i)); - } - - void - visit(binop* bo) - { - switch (bo->op()) - { - case binop::EConcatMarked: - result_ = true; - return; - case binop::Xor: - case binop::Implies: - case binop::Equiv: - case binop::U: - case binop::W: - case binop::M: - case binop::R: - case binop::EConcat: - case binop::UConcat: - return; - } - /* Unreachable code. */ - assert(0); - } - - bool - recurse(const formula* f) - { - return has_mark(f); - } - }; - class simplify_mark_visitor : public visitor { formula* result_; @@ -415,15 +318,5 @@ namespace spot return v.has_mark(); } - bool - has_mark(const formula* f) - { - has_mark_visitor v; - const_cast(f)->accept(v); - return v.result(); - } - - - } } diff --git a/src/ltlvisit/mark.hh b/src/ltlvisit/mark.hh index eee6cca5a..834e14da6 100644 --- a/src/ltlvisit/mark.hh +++ b/src/ltlvisit/mark.hh @@ -35,8 +35,6 @@ namespace spot formula* mark_concat_ops(const formula* f); bool simplify_mark(formula*& f); - - bool has_mark(const formula* f); } } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 85c3107c7..b3ee310f6 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1394,7 +1394,7 @@ namespace spot *new_flag = true; // Perform the actual translation. - v_.reset(!has_mark(f)); + v_.reset(!f->is_marked()); f->accept(v_); translated t; t.symbolic = v_.result();