From a0d9268fda6997d1bc84ff1cbef1007e81f45476 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Dec 2014 17:48:42 +0100 Subject: [PATCH] ltl: remove the useless Finish operator * src/ltlast/unop.cc, src/ltlast/unop.hh src/ltlvisit/lbt.cc, src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc: Remove Finish. * src/tgbaalgos/ltl2taa.cc: Remove Finish, and simply use an empty destination to code the sink. --- src/ltlast/unop.cc | 20 -------------------- src/ltlast/unop.hh | 2 -- src/ltlvisit/lbt.cc | 1 - src/ltlvisit/mark.cc | 2 -- src/ltlvisit/simplify.cc | 9 --------- src/ltlvisit/tostring.cc | 4 ---- src/ltlvisit/tunabbrev.cc | 8 ++++---- src/tgba/formula2bdd.cc | 1 - src/tgbaalgos/ltl2taa.cc | 23 ++++++----------------- src/tgbaalgos/ltl2tgba_fm.cc | 4 ---- 10 files changed, 10 insertions(+), 64 deletions(-) diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index d96f989b3..f2b46e877 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -98,20 +98,6 @@ namespace spot is.syntactic_persistence = is.syntactic_safety; is.accepting_eword = false; break; - case Finish: - is.not_marked = true; - is.boolean = false; - is.ltl_formula = false; - is.psl_formula = false; - is.sere_formula = false; - is.finite = false; - is.syntactic_safety = false; - is.syntactic_guarantee = false; - is.syntactic_obligation = false; - is.syntactic_recurrence = false; - is.syntactic_persistence = false; - is.accepting_eword = false; - break; case NegClosure: case NegClosureMarked: is.not_marked = (op == NegClosure); @@ -181,8 +167,6 @@ namespace spot return "F"; case G: return "G"; - case Finish: - return "Finish"; case Closure: return "Closure"; case NegClosure: @@ -272,10 +256,6 @@ namespace spot assert(child != constant::empty_word_instance()); break; - case Finish: - // No simplifications for Finish. - break; - case Closure: // {0} = 0, {1} = 1, {b} = b if (child->is_boolean()) diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index d8b51a918..993ab0fe9 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -42,8 +42,6 @@ namespace spot enum type { // LTL Not, X, F, G, - // ELTL - Finish, // Closure Closure, NegClosure, NegClosureMarked }; diff --git a/src/ltlvisit/lbt.cc b/src/ltlvisit/lbt.cc index 5c54a4dc1..31fe9eef5 100644 --- a/src/ltlvisit/lbt.cc +++ b/src/ltlvisit/lbt.cc @@ -160,7 +160,6 @@ namespace spot case unop::G: os_ << 'G'; break; - case unop::Finish: case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index a3d60648a..6553e12bb 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -142,7 +142,6 @@ namespace spot case unop::X: case unop::F: case unop::G: - case unop::Finish: case unop::Closure: res->push_back(recurse(f)); break; @@ -236,7 +235,6 @@ namespace spot case unop::X: case unop::F: case unop::G: - case unop::Finish: case unop::Closure: case unop::NegClosureMarked: result_ = uo->clone(); diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index fd33b639c..bc8257a29 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -516,12 +516,6 @@ namespace spot unop::Closure : op, recurse_(f, false)); return; - /* !Finish(x), is not simplified */ - case unop::Finish: - result_ = unop::instance(uo->op(), recurse_(f, false)); - if (negated_) - result_ = unop::instance(unop::Not, result_); - return; } SPOT_UNREACHABLE(); } @@ -1737,9 +1731,6 @@ namespace spot } } break; - case unop::Finish: - // No simplification - break; } result_ = unop::instance(op, result_); } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 6fe648cdc..c5eb56ca1 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -712,10 +712,6 @@ namespace spot case unop::G: emit(KG); break; - case unop::Finish: - os_ << "finish"; - need_parent = true; - break; case unop::Closure: os_ << '{'; in_ratexp_ = true; diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index baf4021d3..973566fd3 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -39,7 +40,6 @@ namespace spot { switch (uo->op()) { - case unop::Finish: case unop::X: case unop::Not: case unop::Closure: diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 78779fb04..87eaffa9e 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -79,7 +79,6 @@ namespace spot { switch (node->op()) { - case unop::Finish: case unop::F: case unop::G: case unop::X: diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 4ad63e169..01ce00ac4 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -70,15 +70,10 @@ namespace spot to_free_.push_back(f); } init_ = f; - std::vector dst; - std::vector a; - - // A little hack to define a sink - dst.push_back(unop::instance(unop::Finish, constant::true_instance())); - to_free_.push_back(dst[0]); - taa_tgba::transition* t = res_->create_transition(init_, dst); + std::vector empty; + taa_tgba::transition* t = res_->create_transition(init_, empty); res_->add_condition(t, f->clone()); - succ_state ss = { dst, f, a }; + succ_state ss = { empty, f, empty }; succ_.push_back(ss); } @@ -90,15 +85,10 @@ namespace spot { case constant::True: { - std::vector dst; - std::vector a; - // A little hack to define a sink - dst.push_back(unop::instance(unop::Finish, - constant::true_instance())); - res_->create_transition(init_, dst); - succ_state ss = { dst, node, a }; + std::vector empty; + res_->create_transition(init_, empty); + succ_state ss = { empty, node, empty }; succ_.push_back(ss); - to_free_.push_back(dst[0]); return; } case constant::False: @@ -139,7 +129,6 @@ namespace spot // Done in recurse succ_ = v.succ_; return; - case unop::Finish: case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 842a459e9..148b55f1c 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -682,7 +682,6 @@ namespace spot case unop::F: case unop::G: case unop::X: - case unop::Finish: case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: @@ -1484,9 +1483,6 @@ namespace spot //trace_ltl_bdd(dict_, res_); } break; - - case unop::Finish: - SPOT_UNIMPLEMENTED(); } }