alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* NEWS: Update the micro benchmarks.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2018-06-22 17:42:37 +02:00
parent a325de8678
commit 0690a547a5
1 changed files with 27 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

50
NEWS
View file

@ -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 here are the size of deterministic transition-based Büchi automata
constructed from four GF(guarantee) formulas with two versions of constructed from four GF(guarantee) formulas with two versions of
Spot, and converted to other types of deterministic automata by 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 ltl2tgba -D rabinizer 4
2.5 2.6 delag ltl2dra 2.5 2.6 delag ltl2dra
------------------------- ----------- ------------- ------------------------- ----------- -------------
GF(a <-> XXa) 9 4 4 9 GF(a <-> XXa) 9(1) 4(1) 4(2) 9(4)
GF(a <-> XXXa) 27 8 8 25 GF(a <-> XXXa) 27(1) 8(1) 8(2) 25(4)
GF(((a & Xb) | XXc) & Xd) 6 4 16 5 GF(((a & Xb) | XXc) & Xd) 6(1) 4(1) 16(1) 5(2)
GF((b | Fa) & (b R Xb)) 6 2 3 3 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 - spot::product() and spot::product_or() learned to produce an
automaton with a simpler acceptance condition if one of the 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 sizes of deterministic automata produced with generic acceptance
using two versions of ltl2tgba and delag for reference. using two versions of ltl2tgba and delag for reference.
ltl2tgba -GD rabinizer 4 ltl2tgba -GD rabinizer 4
2.5 2.6 delag 2.5 2.6 delag
------------- ------------- ------------- -----------
FGa0&GFb0 5 1 1 FGa0&GFb0 2(2) 1(2) 1(2)
(FGa1&GFb1)|FGa0|GFb0 8 1 1 (FGa1&GFb1)|FGa0|GFb0 16(6) 1(4) 1(4)
(FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 497 1 1 (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 29(8) 1(6) 1(6)
FGa0|GFb0 2 1 1 FGa0|GFb0 5(4) 1(2) 1(2)
(FGa1|GFb1)&FGa0&GFb0 16 1 1 (FGa1|GFb1)&FGa0&GFb0 8(4) 1(4) 1(4)
(FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 29 1 1 (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 497(14) 1(6) 1(6)
GFa1 <-> GFz 4 1 1 GFa1 <-> GFz 4(6) 1(3) 1(4)
(GFa1 & GFa2) <-> GFz 8 1 1 (GFa1 & GFa2) <-> GFz 8(4) 1(3) 1(6)
(GFa1 & GFa2 & GFa3) <-> GFz 21 1 1 (GFa1 & GFa2 & GFa3) <-> GFz 21(4) 1(4) 1(8)
GFa1 -> GFz 5 1 1 GFa1 -> GFz 5(4) 1(2) 1(2)
(GFa1 & GFa2) -> GFz 12 1 1 (GFa1 & GFa2) -> GFz 12(4) 1(3) 1(3)
(GFa1 & GFa2 & GFa3) -> GFz 41 1 1 (GFa1 & GFa2 & GFa3) -> GFz 41(4) 1(4) 1(4)
FG(a|b)|FG(!a|Xb) 4 2 2 FG(a|b)|FG(!a|Xb) 4(2) 2(2) 2(2)
FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 4 4 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 8 8 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 - The automaton postprocessor will now simplify acceptance
conditions more aggressively, calling spot::simplify_acceptance() conditions more aggressively, calling spot::simplify_acceptance()