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

* doc/org/ltlcross.org: Update.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-05-25 17:56:05 +02:00
parent 7b6626d176
commit d5598a9aaa
1 changed files with 25 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

40
doc/org/ltlcross.org
View file

@ -18,8 +18,7 @@ The main differences are:
- statistics output in a format that can be more easily be post-processed, - statistics output in a format that can be more easily be post-processed,
- more precise time measurement (LBTT was only precise to - more precise time measurement (LBTT was only precise to
1/100 of a second, reporting most times as "0.00s"), 1/100 of a second, reporting most times as "0.00s"),
- support for deterministic Rabin or Streett automata written in - support for any type of acceptance condition,
[[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dstar='s format]],
- additional intersection checks with the complement of any - additional intersection checks with the complement of any
deterministic automaton produced by a translator. deterministic automaton produced by a translator.
@ -150,6 +149,8 @@ tools:
- '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer - '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer
uses the last =%D= argument as a prefix to which it always append =.dst=, uses the last =%D= argument as a prefix to which it always append =.dst=,
so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file) so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file)
- '=java -jar Rabinizer3.jar -hoa -formula %f; mv output.hoa %O=' (Rabinizer *3*
always output in =output.hoa= when the formula comes from the command line.)
- '=ltl3dra -f %s >%O=' - '=ltl3dra -f %s >%O='
To simplify the use of some of the above tools, a set of predefined To simplify the use of some of the above tools, a set of predefined
@ -408,15 +409,17 @@ such missing data with the option =--omit-missing=.)
The columns =in_type=, =in_states=, =in_edges=, =in_transitions=, The columns =in_type=, =in_states=, =in_edges=, =in_transitions=,
=in_acc=, and =in_scc= are only output if one of the translator =in_acc=, and =in_scc= are only output if one of the translator
produces Rabin or Streett automata (i.e., if =%D= is used to specify produces Rabin or Streett automata in =ltl2dstar='s format (i.e., if
one output filename for any translator). In that case these columns =%D= is used to specify one output filename for any translator). In
give the type (DRA or DSA) of the produced automaton, as well as its that case these columns give the type (DRA or DSA) of the produced
size (states, edges, transitions, number of acceptance pairs, and automaton, as well as its size (states, edges, transitions, number of
number of SCCs). This input automaton is then converted by =ltlcross= acceptance pairs, and number of SCCs). This input automaton is then
into a TGBA before being checked the result of other translators, and converted by =ltlcross= into a TGBA before being checked the result of
all the following columns are measures of that converted automaton. other translators, and all the following columns are measures of that
(Aside from parsing them and converting them to TGBA, Spot has no support converted automaton. This conversion to TGBA is historical. When the
for Rabin automata and Streett automata.) automata are produced in the HOA format (i.e., not in =ltl2dstar='s
format) then no conversion occur, and =ltlcross= works directly with
the given acceptance condition.
=states=, =edges=, =transitions=, =acc= are size measures for the =states=, =edges=, =transitions=, =acc= are size measures for the
automaton that was translated. =acc= counts the number of acceptance automaton that was translated. =acc= counts the number of acceptance
@ -492,11 +495,14 @@ showing two automata for =a U b=, the first automaton is deterministic
a nondeterministic state (state A2 has two possible successors for the a nondeterministic state (state A2 has two possible successors for the
assignment $ab$) and is therefore not deterministic. assignment $ab$) and is therefore not deterministic.
=ambiguous_aut= counts the number of ambiguous automaton. An =ambiguous_aut= is a Boolean indicating whether the automaton is
automaton is ambiguous is there exist a word that can be accepted by ambiguous, i.e., if there exists a word that can be accepted by at
at least two different runs. least two different runs.
Finally, =product_states=, =product_transitions=, and =product_scc= =complete_aut= is a Boolean indicating whether the automaton is
complete.
Columns =product_states=, =product_transitions=, and =product_scc=
count the number of state, transitions and strongly-connect components count the number of state, transitions and strongly-connect components
in the product that has been built between the translated automaton in the product that has been built between the translated automaton
and a random model. For a given formula, the same random model is of and a random model. For a given formula, the same random model is of
@ -523,6 +529,10 @@ This might be useful if you want to compute different kind of
statistic (e.g., a median instead of a mean) or if you want to build statistic (e.g., a median instead of a mean) or if you want to build
scatter plots of all these products. scatter plots of all these products.
Finally, if the =--automata= option was passed to =ltlcross=, the CSV
or JSON output will contain a column named =automaton= encoding each
produced automaton in the HOA format.
** Changing the name of the translators ** Changing the name of the translators
By default, the names used in the CSV and JSON output to designate the By default, the names used in the CSV and JSON output to designate the