import spot
from spot.jupyter import display_inline
from ltlcross_wrapper import Modulizer, ResAnalyzer
spot.setup()
Let's create some file with formulas that we can play with
formula_file = "random.ltl"
name = "random"
tools = {
"small" : "ltl2tgba",
"det-TGBA" : "ltl2tgba -H -D %f>%O",
"det-EL" : "ltl2tgba -H -D -G %f>%O",
}
randltl = spot.randltl(4, 500)
with open(formula_file, "w") as file:
for f in randltl:
print(f, file=file)
Let's run modulizer on these formulas using up to 6 processes
m = Modulizer(tools, formula_file, name=name, processes=6)
m.run()
ResAnalyzer
¶By specifying cols
we say the analyzer which columns from the results it should gather.
cols = ["states", "transitions", "acc", "nondet_states"]
a = ResAnalyzer(f"{name}.csv", cols=cols)
a.cumulative(col=cols)
acc | nondet_states | states | transitions | |
---|---|---|---|---|
tool | ||||
det-EL | 566 | 0 | 2280 | 14633 |
det-TGBA | 520 | 359 | 2155 | 13014 |
small | 505 | 408 | 2081 | 12433 |
cumulative
takes tool_subset
as an arguments, which restricts the computation to the given subset of tools. Only formulas with timeouts within the given tool subset are removed from the sum. Run the following command to obtain results where all formulas with some timeout are removed.
analyzer.cumulative().loc[tool_subset]
a.cross_compare(highlight=True)
det-EL | det-TGBA | small | V | |
---|---|---|---|---|
det-EL | nan | 78 | 78 | 156 |
det-TGBA | 76 | nan | 0 | 76 |
small | 108 | 32 | nan | 140 |
Let's see the cases where the fully deterministic automaton with EL acceptance produces smaller automaton than small
a.better_than("det-EL","small",compare_on=["states"])
column | states | ||
---|---|---|---|
tool | det-EL | small | |
form_id | formula | ||
3 | F(p0 R p1) | 2 | 3 |
4 | G(p1 | Fp1) W (FGp2 R !p2) | 4 | 5 |
10 | X((Fp2 W Xp0) <-> (p2 <-> (p1 U Fp3))) | 21 | 29 |
34 | F(!p1 | GXp2) | 2 | 3 |
39 | Xp3 R (p2 <-> (1 U Xp1)) | 6 | 8 |
... | ... | ... | ... |
458 | !(Xp1 xor ((!p1 R Xp3) R (p1 M 1))) | 12 | 13 |
478 | FG(XFp1 | (Fp3 -> !p3)) | 1 | 3 |
484 | F!(!p0 M Fp0) | 2 | 3 |
488 | G(Xp0 M 1) -> p0 | 3 | 4 |
499 | F((Xp0 W Gp1) | F!(!p1 xor p3)) | 3 | 4 |
69 rows × 2 columns
There is also an equivalent for the above. Use
reverse=True
to swap the tools
a.smaller_than("det-EL","small",reverse=True)
column | states | ||
---|---|---|---|
tool | det-EL | small | |
form_id | formula | ||
0 | Xp1 R ((Gp1 R p2) W p3) | 11 | 10 |
8 | XXG((Xp1 R (p0 W p3)) -> (p2 R GXp0)) | 10 | 6 |
13 | (X!p0 -> G(Gp1 | Xp2)) W p2 | 7 | 5 |
16 | (p0 U (0 R p2)) R (p0 R Xp1) | 8 | 5 |
24 | F(!p2 <-> F(Fp1 R p3)) | 15 | 7 |
... | ... | ... | ... |
476 | Fp2 M (Xp2 | (p1 <-> ((p2 | p3) W p1))) | 7 | 6 |
481 | (Gp0 R p3) <-> (!p2 U p0) | 9 | 8 |
489 | ((p3 | (p1 U p0)) -> p3) M Xp1 | 7 | 6 |
492 | (!Fp1 R (Fp3 xor Gp2)) M Fp2 | 14 | 8 |
498 | (p2 -> Xp2) -> Gp0 | 5 | 4 |
82 rows × 2 columns
For better feel about the size differences, we can use a scatter plot. By default, the color of the marks represent the number of cases with the same automata sizes. By clicking one of the dots, we can get a command for displaying exactly the cases represented by the dot (see the cell bellow the scatter plot and try yourself).
display_inline(a.aut_for_id(47, "det-EL"),a.aut_for_id(47, "small"))
We can also add marks for cases when tool1
and tool2
deliver automaton of the same size.
a.bokeh_scatter_plot("det-EL","small",include_equal=True)
If you don't like colors, you can choose to use a single mark for a single formula (with transparency). You can tweek the transparency using the alpha argument. Click on a dot to see all the formulas hiden there.
a.bokeh_scatter_plot("det-EL","small",merge_same=False, alpha=.1)
a.get_error_counts(drop_zeros=False, error_types=["timeout", "crash"])
timeout | crash | |
---|---|---|
tool | ||
det-EL | 0 | 0 |
det-TGBA | 0 | 0 |
small | 0 | 0 |