From 0a8c6479b737163f1edcbc60e34abd87052c1535 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Jun 2018 15:36:05 +0200 Subject: [PATCH] translate: extract obligations terms when translating LTL to Parity * spot/twaalgos/translate.cc: Here. * NEWS: Mention the change. * tests/core/genltl.test: Add parity automata sizes for a set of formulas. * tests/core/parity2.test: Add another formula to the tests. --- NEWS | 26 +- spot/twaalgos/translate.cc | 70 ++-- tests/core/genltl.test | 110 ++--- tests/core/parity2.test | 836 ++++++++++++++++++++++++++++++++++++- 4 files changed, 948 insertions(+), 94 deletions(-) diff --git a/NEWS b/NEWS index da8b5e88c..ecaa126db 100644 --- a/NEWS +++ b/NEWS @@ -64,10 +64,11 @@ New in spot 2.5.3.dev (not yet released) These are now used by the main translation routine, and can be disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, - here are the size of deterministic transition-based Büchi automata - constructed from four GF(guarantee) formulas with two versions of - Spot, and converted to other types of deterministic automata by - other tools. "x(y)" means x states and y acceptance sets. + here are the size of deterministic transition-based generalized + Büchi automata constructed from four GF(guarantee) formulas with + two versions of Spot, and converted to other types of + deterministic automata by other tools. "x(y)" means x states and + y acceptance sets. ltl2tgba -D rabinizer 4 2.5 2.6 delag ltl2dra @@ -101,7 +102,7 @@ New in spot 2.5.3.dev (not yet released) sizes of deterministic automata produced with generic acceptance using two versions of ltl2tgba and delag for reference. - ltl2tgba -GD rabinizer 4 + ltl2tgba -DG rabinizer 4 2.5 2.6 delag ------------- ----------- FGa0&GFb0 2(2) 1(2) 1(2) @@ -120,9 +121,22 @@ New in spot 2.5.3.dev (not yet released) FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21(2) 4(3) 4(3) FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170(2) 8(4) 8(4) + - For 'parity' output, the 'ltl-split' optimization just separate + obligation subformulas from the rest, where a determinization is + still performed. + ltl2tgba -DP ltl3dra rabinizer 4 + 2.5 2.6 0.2.3 ltl2dpa + -------------- ------- ----------- + FGp0 & (Gp1 | XFp2) 6(2) 4(1) 4(1) 4(2) + G!p0 | F(p0 & (!p1 W p2)) 5(2) 4(2) n/a 5(2) + (p0 W XXGp0) & GFp1 & FGp2 6(2) 5(2) n/a 6(3) + + (The above just show a few cases that were improved. There are + many cases where ltl2dpa still produces smaller automata.) + - The automaton postprocessor will now simplify acceptance conditions more aggressively, calling spot::simplify_acceptance() - or spot::cleanup_acceptance() depanding on the optimization level. + or spot::cleanup_acceptance() depending on the optimization level. - print_dot(), used to print automata in GraphViz's format, underwent several changes: diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 7fb429414..0e054c912 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -168,7 +168,8 @@ namespace spot twa_graph_ptr aut; twa_graph_ptr aut2 = nullptr; - if (ltl_split_ && type_ == Generic && !r.is_syntactic_obligation()) + if (ltl_split_ && (type_ == Generic + || (type_ & Parity)) && !r.is_syntactic_obligation()) { formula r2 = r; unsigned leading_x = 0; @@ -177,28 +178,31 @@ namespace spot r2 = r2[0]; ++leading_x; } - // F(q|u|f) = q|F(u)|F(f) - // G(q&e&f) = q&G(e)&G(f) - bool want_u = r2.is({op::F, op::Or}); - if (want_u || r2.is({op::G, op::And})) + if (type_ == Generic) { - std::vector susp; - std::vector rest; - auto op1 = r2.kind(); - auto op2 = r2[0].kind(); - for (formula child: r2[0]) + // F(q|u|f) = q|F(u)|F(f) + // G(q&e&f) = q&G(e)&G(f) + bool want_u = r2.is({op::F, op::Or}); + if (want_u || r2.is({op::G, op::And})) { - bool u = child.is_universal(); - bool e = child.is_eventual(); - if (u && e) - susp.push_back(child); - else if ((want_u && u) || (!want_u && e)) - susp.push_back(formula::unop(op1, child)); - else - rest.push_back(child); + std::vector susp; + std::vector rest; + auto op1 = r2.kind(); + auto op2 = r2[0].kind(); + for (formula child: r2[0]) + { + bool u = child.is_universal(); + bool e = child.is_eventual(); + if (u && e) + susp.push_back(child); + else if ((want_u && u) || (!want_u && e)) + susp.push_back(formula::unop(op1, child)); + else + rest.push_back(child); + } + susp.push_back(formula::unop(op1, formula::multop(op2, rest))); + r2 = formula::multop(op2, susp); } - susp.push_back(formula::unop(op1, formula::multop(op2, rest))); - r2 = formula::multop(op2, susp); } if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or)) goto nosplit; @@ -212,7 +216,8 @@ namespace spot { if (child.is_syntactic_obligation()) oblg.push_back(child); - else if (child.is_eventual() && child.is_universal()) + else if (child.is_eventual() && child.is_universal() + && (type_ == Generic)) susp.push_back(child); else rest.push_back(child); @@ -243,13 +248,24 @@ namespace spot if (!rest.empty()) { formula rest_f = formula::multop(r2.kind(), rest); - twa_graph_ptr rest_aut = transrun(rest_f); - if (aut == nullptr) - aut = rest_aut; - else if (is_and) - aut = product(aut, rest_aut); + // In case type_ is Parity, all suspendable formulas have + // been put into rest_f. But if the entire rest_f is + // suspendable, we want to handle it like so. + if (rest_f.is_eventual() && rest_f.is_universal()) + { + assert(susp.empty()); + susp.push_back(rest_f); + } else - aut = product_or(aut, rest_aut); + { + twa_graph_ptr rest_aut = transrun(rest_f); + if (aut == nullptr) + aut = rest_aut; + else if (is_and) + aut = product(aut, rest_aut); + else + aut = product_or(aut, rest_aut); + } } if (!susp.empty()) { diff --git a/tests/core/genltl.test b/tests/core/genltl.test index c157da3b9..b73a40236 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -156,60 +156,61 @@ test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16 genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \ --gf-equiv=0..5 --gf-implies=0..5 --gf-equiv-xn=1..3 --gf-implies-xn=3 \ --format='"%F=%L",%f' | - ltl2tgba -G -D -F-/2 --stats='%<,%s' > out + ltl2tgba -G -D -F-/2 --stats='%f,%<,%s' | + ltl2tgba -P -D -F-/1 --stats='%>,%s' > out cat >exp< out + ltldo 'ltl2tgba -DG' -F-/2 --stats='%f,%<,%s' | + ltldo 'ltl2tgba -DP' -F-/1 --stats='%>,%s' > out diff out exp # Test out-of-range conditions diff --git a/tests/core/parity2.test b/tests/core/parity2.test index 6d40b7414..f9ba01c77 100755 --- a/tests/core/parity2.test +++ b/tests/core/parity2.test @@ -21,13 +21,13 @@ . ./defs set -e -rm -rf res res2 - for x in P 'Pmin odd' 'Pmax even' p 'pmin odd' 'pmax even'; do - ltl2tgba "-$x" FGa 'GFa & GFb' >>res - ltl2tgba FGa 'GFa & GFb' | autfilt --name=%M --high "-$x" >>res2 - ltl2tgba -D "-$x" FGa 'GFa & GFb' >>res3 - ltl2tgba FGa 'GFa & GFb' | autfilt -D --name=%M --high "-$x" >>res4 + ltl2tgba "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res + ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' | + autfilt --name=%M --high "-$x" >>res2 + ltl2tgba -D "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res3 + ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' | + autfilt -D --name=%M --high "-$x" >>res4 done cat >expected< XXXb)' + -f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'