diff --git a/NEWS b/NEWS index a78117cb4..0ec0b0afc 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,12 @@ New in spot 2.9.0.dev (not yet released) + Command-line tools: + + - 'ltl2tgba -G -D' is now better at handling formulas that use + '<->' and 'xor' operators at the top level. For instance + ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe' + now produces a 16-state automaton (instead of 31 in Spot 2.9). + Library: - product_xor() and product_xnor() are two new versions of the @@ -8,6 +15,11 @@ New in spot 2.9.0.dev (not yet released) respectively the symmetric difference of the operands, and the complement of that. + - tl_simplifier_options::keep_top_xor is a new option to keep Xor + and Equiv operator that appear at the top of LTL formulas (maybe + below other Boolean or X operators). This is used by the + spot::translator class when creating deterministic automata with + generic acceptance. New in spot 2.9 (2020-04-30) diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 22f48edd4..8b1340aaa 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -186,18 +186,27 @@ namespace spot std::string kindstr() const; /// \see formula::is + /// @{ bool is(op o) const { return op_ == o; } - /// \see formula::is bool is(op o1, op o2) const { return op_ == o1 || op_ == o2; } - /// \see formula::is + bool is(op o1, op o2, op o3) const + { + return op_ == o1 || op_ == o2 || op_ == o3; + } + + bool is(op o1, op o2, op o3, op o4) const + { + return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4; + } + bool is(std::initializer_list l) const { const fnode* n = this; @@ -209,6 +218,7 @@ namespace spot } return true; } + /// @} /// \see formula::get_child_of const fnode* get_child_of(op o) const @@ -1333,6 +1343,19 @@ namespace spot return ptr_->is(o1, o2); } + /// Return true if the formula is of kind \a o1 or \a o2 or \a o3 + bool is(op o1, op o2, op o3) const + { + return ptr_->is(o1, o2, o3); + } + + /// Return true if the formula is of kind \a o1 or \a o2 or \a o3 + /// or \a a4. + bool is(op o1, op o2, op o3, op o4) const + { + return ptr_->is(o1, o2, o3, o4); + } + /// Return true if the formulas nests all the operators in \a l. bool is(std::initializer_list l) const { diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 0f4c34218..00fac4c9e 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011-2019 Laboratoire de Recherche et Developpement +// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -417,22 +417,25 @@ namespace spot ////////////////////////////////////////////////////////////////////// formula - nenoform_rec(formula f, bool negated, tl_simplifier_cache* c); + nenoform_rec(formula f, bool negated, tl_simplifier_cache* c, + bool deep); formula equiv_or_xor(bool equiv, formula f1, formula f2, - tl_simplifier_cache* c) + tl_simplifier_cache* c, bool deep) { - auto rec = [c](formula f, bool negated) + auto rec = [c, deep](formula f, bool negated) { - return nenoform_rec(f, negated, c); + return nenoform_rec(f, negated, c, deep); }; if (equiv) { // Rewrite a<=>b as (a&b)|(!a&!b) auto recurse_f1_true = rec(f1, true); - auto recurse_f1_false = rec(f1, false); auto recurse_f2_true = rec(f2, true); + if (!deep && c->options.keep_top_xor) + return formula::Equiv(recurse_f1_true, recurse_f2_true); + auto recurse_f1_false = rec(f1, false); auto recurse_f2_false = rec(f2, false); auto left = formula::And({recurse_f1_false, recurse_f2_false}); auto right = formula::And({recurse_f1_true, recurse_f2_true}); @@ -442,8 +445,10 @@ namespace spot { // Rewrite a^b as (a&!b)|(!a&b) auto recurse_f1_true = rec(f1, true); - auto recurse_f1_false = rec(f1, false); auto recurse_f2_true = rec(f2, true); + if (!deep && c->options.keep_top_xor) + return formula::Xor(recurse_f1_true, recurse_f2_true); + auto recurse_f1_false = rec(f1, false); auto recurse_f2_false = rec(f2, false); auto left = formula::And({recurse_f1_false, recurse_f2_true}); auto right = formula::And({recurse_f1_true, recurse_f2_false}); @@ -451,8 +456,11 @@ namespace spot } } + // The deep argument indicate whether we are under a temporal + // operator (except X). formula - nenoform_rec(formula f, bool negated, tl_simplifier_cache* c) + nenoform_rec(formula f, bool negated, tl_simplifier_cache* c, + bool deep) { if (f.is(op::Not)) { @@ -474,9 +482,9 @@ namespace spot } else { - auto rec = [c](formula f, bool neg) + auto rec = [c, &deep](formula f, bool neg) { - return nenoform_rec(f, neg, c); + return nenoform_rec(f, neg, c, deep); }; switch (op o = f.kind()) @@ -504,21 +512,25 @@ namespace spot break; case op::F: // !Fa == G!a + deep = true; result = formula::unop(negated ? op::G : op::F, rec(f[0], negated)); break; case op::G: // !Ga == F!a + deep = true; result = formula::unop(negated ? op::F : op::G, rec(f[0], negated)); break; case op::Closure: + deep = true; result = formula::unop(negated ? op::NegClosure : op::Closure, rec(f[0], false)); break; case op::NegClosure: case op::NegClosureMarked: + deep = true; result = formula::unop(negated ? op::Closure : o, rec(f[0], false)); break; @@ -539,17 +551,18 @@ namespace spot case op::Xor: { // !(a ^ b) == a <=> b - result = equiv_or_xor(negated, f[0], f[1], c); + result = equiv_or_xor(negated, f[0], f[1], c, deep); break; } case op::Equiv: { // !(a <=> b) == a ^ b - result = equiv_or_xor(!negated, f[0], f[1], c); + result = equiv_or_xor(!negated, f[0], f[1], c, deep); break; } case op::U: { + deep = true; // !(a U b) == !a R !b auto f1 = rec(f[0], negated); auto f2 = rec(f[1], negated); @@ -558,6 +571,7 @@ namespace spot } case op::R: { + deep = true; // !(a R b) == !a U !b auto f1 = rec(f[0], negated); auto f2 = rec(f[1], negated); @@ -566,6 +580,7 @@ namespace spot } case op::W: { + deep = true; // !(a W b) == !a M !b auto f1 = rec(f[0], negated); auto f2 = rec(f[1], negated); @@ -574,6 +589,7 @@ namespace spot } case op::M: { + deep = true; // !(a M b) == !a W !b auto f1 = rec(f[0], negated); auto f2 = rec(f[1], negated); @@ -604,15 +620,16 @@ namespace spot // !(a*) etc. should never occur. { assert(!negated); - result = f.map([c](formula f) + result = f.map([c, deep](formula f) { - return nenoform_rec(f, false, c); + return nenoform_rec(f, false, c, deep); }); break; } case op::EConcat: case op::EConcatMarked: { + deep = true; // !(a <>-> b) == a[]-> !b auto f1 = f[0]; auto f2 = f[1]; @@ -622,6 +639,7 @@ namespace spot } case op::UConcat: { + deep = true; // !(a []-> b) == a<>-> !b auto f1 = f[0]; auto f2 = f[1]; @@ -4048,9 +4066,9 @@ namespace spot if (f2.is_sere_formula() && !f2.is_boolean()) return false; if (right) - f2 = nenoform_rec(f2, true, this); + f2 = nenoform_rec(f2, true, this, false); else - f1 = nenoform_rec(f1, true, this); + f1 = nenoform_rec(f1, true, this, false); return syntactic_implication(f1, f2); } @@ -4085,7 +4103,7 @@ namespace spot formula tl_simplifier::negative_normal_form(formula f, bool negated) { - return nenoform_rec(f, negated, cache_); + return nenoform_rec(f, negated, cache_, false); } bool diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh index 725255745..34377ff62 100644 --- a/spot/tl/simplify.hh +++ b/spot/tl/simplify.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011-2017, 2019 Laboratoire de Recherche et Developpement +// Copyright (C) 2011-2017, 2019, 2020 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -30,14 +30,15 @@ namespace spot { public: tl_simplifier_options(bool basics = true, - bool synt_impl = true, - bool event_univ = true, - bool containment_checks = false, - bool containment_checks_stronger = false, - bool nenoform_stop_on_boolean = false, - bool reduce_size_strictly = false, - bool boolean_to_isop = false, - bool favor_event_univ = false) + bool synt_impl = true, + bool event_univ = true, + bool containment_checks = false, + bool containment_checks_stronger = false, + bool nenoform_stop_on_boolean = false, + bool reduce_size_strictly = false, + bool boolean_to_isop = false, + bool favor_event_univ = false, + bool keep_top_xor = false) : reduce_basics(basics), synt_impl(synt_impl), event_univ(event_univ), @@ -46,7 +47,8 @@ namespace spot nenoform_stop_on_boolean(nenoform_stop_on_boolean), reduce_size_strictly(reduce_size_strictly), boolean_to_isop(boolean_to_isop), - favor_event_univ(favor_event_univ) + favor_event_univ(favor_event_univ), + keep_top_xor(keep_top_xor) { } @@ -87,6 +89,10 @@ namespace spot bool boolean_to_isop; // Try to isolate subformulae that are eventual and universal. bool favor_event_univ; + // Keep Xor and Equiv at the top of the formula, possibly under + // &,|, and X operators. Only rewrite Xor and Equiv under + // temporal operators. + bool keep_top_xor; }; // fwd declaration to hide technical details. diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 7ef799662..878bcaa43 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -108,6 +108,8 @@ namespace spot } if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic)) options.favor_event_univ = true; + if (type_ == Generic && ltl_split_ && (pref_ & Deterministic)) + options.keep_top_xor = true; simpl_owned_ = simpl_ = new tl_simplifier(options, dict); } @@ -167,15 +169,16 @@ namespace spot r2 = formula::multop(op2, susp); } } - if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or) || + if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or, + op::Xor, op::Equiv) || // For TGBA/BA we only do conjunction. There is nothing wrong // with disjunction, but it seems to generate larger automata // in many cases and it needs to be further investigated. Maybe // this could be relaxed in the case of deterministic output. - (r2.is(op::Or) && (type_ == TGBA || type_ == BA))) + (!r2.is(op::And) && (type_ == TGBA || type_ == BA))) goto nosplit; - bool is_and = r2.is(op::And); + op topop = r2.kind(); // Let's classify subformulas. std::vector oblg; std::vector susp; @@ -270,10 +273,16 @@ namespace spot twa_graph_ptr rest_aut = transrun(rest_f); if (aut == nullptr) aut = rest_aut; - else if (is_and) + else if (topop == op::And) aut = product(aut, rest_aut); - else + else if (topop == op::Or) aut = product_or(aut, rest_aut); + else if (topop == op::Xor) + aut = product_xor(aut, rest_aut); + else if (topop == op::Equiv) + aut = product_xnor(aut, rest_aut); + else + SPOT_UNREACHABLE(); } if (!susp.empty()) { @@ -285,10 +294,16 @@ namespace spot twa_graph_ptr one = transrun(f); if (!susp_aut) susp_aut = one; - else if (is_and) + else if (topop == op::And) susp_aut = product(susp_aut, one); - else + else if (topop == op::Or) susp_aut = product_or(susp_aut, one); + else if (topop == op::Xor) + susp_aut = product_xor(susp_aut, one); + else if (topop == op::Equiv) + susp_aut = product_xnor(susp_aut, one); + else + SPOT_UNREACHABLE(); } if (susp_aut->prop_universal().is_true()) { @@ -311,10 +326,14 @@ namespace spot } if (aut == nullptr) aut = susp_aut; - else if (is_and) + else if (topop == op::And) aut = product_susp(aut, susp_aut); - else + else if (topop == op::Or) aut = product_or_susp(aut, susp_aut); + else if (topop == op::Xor) // No suspension here + aut = product_xor(aut, susp_aut); + else if (topop == op::Equiv) // No suspension here + aut = product_xnor(aut, susp_aut); //if (aut && susp_aut) // { // print_hoa(std::cerr << "AUT\n", aut) << '\n'; diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 22c005146..3e50df480 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -451,4 +451,11 @@ f='(GFp0 | FGp1) & (GF!p1 | FGp2) & (GF!p2 | FG!p0)' test 1,8,3 = `ltl2tgba -G -D "$f" --stats=%s,%e,%a` test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a` +# Handling of Xor and <-> by ltl-split and -D -G. +res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) <-> GFe)' --stats='%s %g'` +test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))" +res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'` +test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))" +ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe' + : diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 8e5e1c712..1be3d9a94 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -178,13 +178,13 @@ b.copy_state_names_from(a) assert b.to_str() == """HOA: v1 States: 1 Start: 0 -AP: 2 "p0" "p1" +AP: 2 "p1" "p0" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 "[1,7]" -[!1] 0 {0} -[1] 0 +[!0] 0 {0} +[0] 0 --END--"""