From 59202bd5de3b4f7f310fec9b3db65b91a304ef62 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Aug 2015 17:28:01 +0200 Subject: [PATCH] do not rewrite <-> and -> for Spin LTL output Fixes #39, reported by Joachim Klein. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Take an option to specify which of xor/equiv/implies should be rewritten. * src/ltlvisit/print.cc (print_spin): Rewrite only xor. * src/tests/ltlfilt.test: Add a test case. * NEWS: Mention this. --- NEWS | 2 ++ src/ltlvisit/lunabbrev.cc | 64 ++++++++++++++++++++++++++++++--------- src/ltlvisit/lunabbrev.hh | 15 +++++++-- src/ltlvisit/print.cc | 8 ++--- src/tests/ltlfilt.test | 53 +++++++++++++++++++++++++++++++- 5 files changed, 119 insertions(+), 23 deletions(-) diff --git a/NEWS b/NEWS index acaac7dfe..3e3703bca 100644 --- a/NEWS +++ b/NEWS @@ -26,6 +26,8 @@ New in spot 1.99.2a (not yet released) double quotes where not always properly rendered. - A spurious assertion was triggered by streett_to_generalized_buchi(), but only when compiled in DEBUG mode. + - LTL formula rewritten in Spin's syntax no longer have their -> + and <-> rewritten aways. New in spot 1.99.2 (2015-07-18) diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 0466e8860..db22e6441 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // 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. @@ -29,8 +29,25 @@ namespace spot namespace ltl { - unabbreviate_logic_visitor::unabbreviate_logic_visitor() + unabbreviate_logic_visitor::unabbreviate_logic_visitor(const char* opt) { + while (*opt) + switch (char c = *opt++) + { + case '^': + rewrite_xor = true; + break; + case 'i': + rewrite_i = true; + break; + case 'e': + rewrite_e = true; + break; + default: + throw std::runtime_error + (std::string("unknown option for unabbreviate_logic_visitor(): ") + + c); + } } unabbreviate_logic_visitor::~unabbreviate_logic_visitor() @@ -42,29 +59,44 @@ namespace spot { const formula* f1 = recurse(bo->first()); const formula* f2 = recurse(bo->second()); - binop::type op = bo->op(); switch (op) { + /* f1 ^ f2 == !(f1 <-> f2) */ /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ case binop::Xor: { - const formula* a = - multop::instance(multop::And, f1->clone(), - unop::instance(unop::Not, f2->clone())); - const formula* b = - multop::instance(multop::And, f2, - unop::instance(unop::Not, f1)); - result_ = multop::instance(multop::Or, a, b); - return; + if (!rewrite_xor) + goto no_rewrite; + if (!rewrite_e) + { + result_ = unop::instance(unop::Not, + binop::instance(binop::Equiv, f1, f2)); + return; + } + else + { + const formula* a = + multop::instance(multop::And, f1->clone(), + unop::instance(unop::Not, f2->clone())); + const formula* b = + multop::instance(multop::And, f2, + unop::instance(unop::Not, f1)); + result_ = multop::instance(multop::Or, a, b); + return; + } } /* f1 => f2 == !f1 | f2 */ case binop::Implies: + if (!rewrite_i) + goto no_rewrite; result_ = multop::instance(multop::Or, unop::instance(unop::Not, f1), f2); return; /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ case binop::Equiv: + if (!rewrite_e) + goto no_rewrite; { const formula* f1c = f1->clone(); const formula* f2c = f2->clone(); @@ -90,6 +122,7 @@ namespace spot case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: + no_rewrite: result_ = binop::instance(op, f1, f2); return; } @@ -99,15 +132,16 @@ namespace spot const formula* unabbreviate_logic_visitor::recurse(const formula* f) { - return unabbreviate_logic(f); + f->accept(*this); + return result_; } const formula* - unabbreviate_logic(const formula* f) + unabbreviate_logic(const formula* f, const char* xie) { if (f->is_sugar_free_boolean()) return f->clone(); - unabbreviate_logic_visitor v; + unabbreviate_logic_visitor v(xie); f->accept(v); return v.result(); } diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh index 278ee923c..98c5f7441 100644 --- a/src/ltlvisit/lunabbrev.hh +++ b/src/ltlvisit/lunabbrev.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -44,13 +44,17 @@ namespace spot { typedef clone_visitor super; public: - unabbreviate_logic_visitor(); + unabbreviate_logic_visitor(const char* opt = "^ie"); virtual ~unabbreviate_logic_visitor(); using super::visit; void visit(const binop* bo); virtual const formula* recurse(const formula* f); + private: + bool rewrite_xor = false; + bool rewrite_i = false; + bool rewrite_e = false; }; /// \ingroup ltl_rewriting @@ -60,7 +64,12 @@ namespace spot /// This will rewrite binary operators such as binop::Implies, /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, /// and multop::And. - SPOT_API const formula* unabbreviate_logic(const formula* f); + /// + /// The optional \a opt argument can be a string containing any + /// subset of the string "^ie" to denote the operators (xor, + /// implication, equivalence) to actually remove. + SPOT_API const formula* unabbreviate_logic(const formula* f, + const char* opt = "^ie"); } } diff --git a/src/ltlvisit/print.cc b/src/ltlvisit/print.cc index 2cf30ba53..c6162d513 100644 --- a/src/ltlvisit/print.cc +++ b/src/ltlvisit/print.cc @@ -121,8 +121,8 @@ namespace spot "true", // 1 doesn't work from the command line "[*0]", // not supported " xor ", // rewritten - " -> ", // rewritten, although supported - " <-> ", // rewritten, although supported + " -> ", + " <-> ", " U ", " V ", " W ", // rewritten @@ -985,8 +985,8 @@ namespace spot std::ostream& print_spin_ltl(std::ostream& os, const formula* f, bool full_parent) { - // Remove xor, ->, and <-> first. - const formula* fu = unabbreviate_logic(f); + // Rewrite xor. + const formula* fu = unabbreviate_logic(f, "^"); // Also remove W and M. f = unabbreviate_wm(fu); fu->destroy(); diff --git a/src/tests/ltlfilt.test b/src/tests/ltlfilt.test index 0ded87f7c..1acef4d4e 100755 --- a/src/tests/ltlfilt.test +++ b/src/tests/ltlfilt.test @@ -50,7 +50,6 @@ G(a & Xb) Xa F(a & !Xa & Xb) {a & {b|c} } - EOF checkopt --eventual < b) -> (c xor d) EOF cat >exp <out @@ -189,11 +190,55 @@ p0 && []<>p1 && <>[]p1 #define p2 (!c) #define p3 (f) p0 || []p1 || <>[](p2 || Xp3) +#define p0 ((c && !d) || (!c && d)) +#define p1 ((a && !b) || (!a && b)) +p0 || []p1 EOF run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out diff exp out +cat >exp <(p0 || p2) && <>[](p0 || p2) +#define p0 (b) +#define p1 (a) +#define p2 (c) +p0 && []<>(p1 || p2) && <>[](p1 || p2) +#define p0 (h) +#define p1 (i) +#define p2 (d) +#define p3 (e) +#define p4 (c) +#define p5 (f) +p0 || p1 || [](p2 && p3) || <>[](!p4 || Xp5) +#define p0 (b) +#define p1 (e) +#define p2 (f) +#define p3 (g) +#define p4 (c) +p0 && p1 && (p2 || p3) && !Xp4 +#define p0 (b) +#define p1 (a) +#define p2 (c) +p0 && []<>(p1 || p2) && ![]<>!(p1 || p2) +#define p0 (a) +#define p1 (b) +#define p2 (c) +#define p3 (d) +<>(p0 <-> p1) -> !(p2 <-> p3) +EOF + +run 0 $ltlfilt -s -u --relabel=pnn --define in >out +diff exp out + +toolong='((p2=0) * (p3=1))' # work around the 80-col check cat >exp <exp <out diff exp out @@ -233,6 +283,7 @@ b & GF(a | c) & FG(a | c)@ h | i | G(d & e) | FG(!c | Xf)@ b & e & (f | g) & !Xc@ b & GF(a | c) & !GF!(a | c)@ +F(a <-> b) -> (c xor d)@ EOF diff exp out