From 0690a547a5e283b473e0b6e2d6a9b94dc792c553 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Jun 2018 17:42:37 +0200 Subject: [PATCH] * NEWS: Update the micro benchmarks. --- NEWS | 50 +++++++++++++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 23 deletions(-) diff --git a/NEWS b/NEWS index 4276cd9c9..da8b5e88c 100644 --- a/NEWS +++ b/NEWS @@ -67,15 +67,19 @@ New in spot 2.5.3.dev (not yet released) 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. + other tools. "x(y)" means x states and y acceptance sets. ltl2tgba -D rabinizer 4 2.5 2.6 delag ltl2dra ------------------------- ----------- ------------- - GF(a <-> XXa) 9 4 4 9 - GF(a <-> XXXa) 27 8 8 25 - GF(((a & Xb) | XXc) & Xd) 6 4 16 5 - GF((b | Fa) & (b R Xb)) 6 2 3 3 + GF(a <-> XXa) 9(1) 4(1) 4(2) 9(4) + GF(a <-> XXXa) 27(1) 8(1) 8(2) 25(4) + GF(((a & Xb) | XXc) & Xd) 6(1) 4(1) 16(1) 5(2) + GF((b | Fa) & (b R Xb)) 6(2) 2(1) 3(4) 3(4) + + Note that in the above the automata produced by 'ltl2tgba -D' in + version 2.5 were not nodeterministic (because -D is only a + preference). They are deterministic in 2.6 and other tools. - spot::product() and spot::product_or() learned to produce an automaton with a simpler acceptance condition if one of the @@ -97,24 +101,24 @@ 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 - 2.5 2.6 delag - ------------- ------------- - FGa0&GFb0 5 1 1 - (FGa1&GFb1)|FGa0|GFb0 8 1 1 - (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 497 1 1 - FGa0|GFb0 2 1 1 - (FGa1|GFb1)&FGa0&GFb0 16 1 1 - (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 29 1 1 - GFa1 <-> GFz 4 1 1 - (GFa1 & GFa2) <-> GFz 8 1 1 - (GFa1 & GFa2 & GFa3) <-> GFz 21 1 1 - GFa1 -> GFz 5 1 1 - (GFa1 & GFa2) -> GFz 12 1 1 - (GFa1 & GFa2 & GFa3) -> GFz 41 1 1 - FG(a|b)|FG(!a|Xb) 4 2 2 - FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 4 4 - FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 8 8 + ltl2tgba -GD rabinizer 4 + 2.5 2.6 delag + ------------- ----------- + FGa0&GFb0 2(2) 1(2) 1(2) + (FGa1&GFb1)|FGa0|GFb0 16(6) 1(4) 1(4) + (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 29(8) 1(6) 1(6) + FGa0|GFb0 5(4) 1(2) 1(2) + (FGa1|GFb1)&FGa0&GFb0 8(4) 1(4) 1(4) + (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 497(14) 1(6) 1(6) + GFa1 <-> GFz 4(6) 1(3) 1(4) + (GFa1 & GFa2) <-> GFz 8(4) 1(3) 1(6) + (GFa1 & GFa2 & GFa3) <-> GFz 21(4) 1(4) 1(8) + GFa1 -> GFz 5(4) 1(2) 1(2) + (GFa1 & GFa2) -> GFz 12(4) 1(3) 1(3) + (GFa1 & GFa2 & GFa3) -> GFz 41(4) 1(4) 1(4) + FG(a|b)|FG(!a|Xb) 4(2) 2(2) 2(2) + 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) - The automaton postprocessor will now simplify acceptance conditions more aggressively, calling spot::simplify_acceptance()