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

ltlcross, ltldo: Add support for ltl3hoa.

Browse source 
* bin/common_trans.cc: Add shorthand for ltl3hoa.
* NEWS, doc/org/ltlcross.org, doc/org/ltldo.org: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-13 21:26:53 +01:00
parent 43520a3e87
commit 01838a2456
4 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -56,6 +56,9 @@ New in spot 2.2.2.dev (Not yet released)
atomic propositions it supports, and the output automaton will atomic propositions it supports, and the output automaton will
then be fixed to use the original atomic propositions. then be fixed to use the original atomic propositions.
* ltldo and ltlcross have learned how to call ltl3hoa, so
'ltl3hoa -f %f>%O' can be abbreviated to just 'ltl3hoa'.
Library: Library:
* A twa is required to have at least one state, the initial state. * A twa is required to have at least one state, the initial state.

1
bin/common_trans.cc
View file

@ -47,6 +47,7 @@ static struct shorthands_t
{ "ltl2tgba", " -H %f>%O" }, { "ltl2tgba", " -H %f>%O" },
{ "ltl3ba", " -f %s>%O" }, { "ltl3ba", " -f %s>%O" },
{ "ltl3dra", " -f %s>%O" }, { "ltl3dra", " -f %s>%O" },
{ "ltl3hoa", " -f %f>%O" },
{ "modella", " %[MWei^]L %O" }, { "modella", " %[MWei^]L %O" },
{ "spin", " -f %s>%O" }, { "spin", " -f %s>%O" },
}; };

6
doc/org/ltlcross.org
View file

@ -163,9 +163,10 @@ tools:
- '=java -jar Rabinizer.jar -ltl2dstar %[MW]F %O; mv %O.dst %O=' (Rabinizer - '=java -jar Rabinizer.jar -ltl2dstar %[MW]F %O; mv %O.dst %O=' (Rabinizer
uses the last =%O= argument as a prefix to which it always append =.dst=, uses the last =%O= argument as a prefix to which it always append =.dst=,
so we have to rename =%O.dst= as =%O= so that =ltlcross= can find the file) so we have to rename =%O.dst= as =%O= so that =ltlcross= can find the file)
- '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %[MWR]f >%O~' - '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %[MWRei^]f >%O~'
(rabinizer 3.1 can output automata in the HOA format) (rabinizer 3.1 can output automata in the HOA format)
- '=ltl3dra -f %s >%O=' (The HOA format is the default for =ltl2dra=.) - '=ltl3dra -f %s >%O=' (The HOA format is the default for =ltl3dra=.)
- '=ltl3hoa -f %s >%O=' (The HOA format is the default for =ltl3hoa=.)
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
shorthands are available. Those can be listed with the shorthands are available. Those can be listed with the
@ -185,6 +186,7 @@ the following words, then the string on the right is appended.
ltl2tgba -H %f>%O ltl2tgba -H %f>%O
ltl3ba -f %s>%O ltl3ba -f %s>%O
ltl3dra -f %s>%O ltl3dra -f %s>%O
ltl3hoa -f %f>%O
modella %[MWei^]L %O modella %[MWei^]L %O
spin -f %s>%O spin -f %s>%O

7
doc/org/ltldo.org
View file

@ -304,18 +304,19 @@ the following words, then the string on the right is appended.
lbt <%L>%O lbt <%L>%O
ltl2ba -f %s>%O ltl2ba -f %s>%O
ltl2dstar --output-format=hoa %L %O ltl2dstar --output-format=hoa %[MW]L %O
ltl2tgba -H %f>%O ltl2tgba -H %f>%O
ltl3ba -f %s>%O ltl3ba -f %s>%O
ltl3dra -f %s>%O ltl3dra -f %s>%O
modella %L %O ltl3hoa -f %f>%O
modella %[MWei^]L %O
spin -f %s>%O spin -f %s>%O
Any {name} and directory component is skipped for the purpose of Any {name} and directory component is skipped for the purpose of
matching those prefixes. So for instance matching those prefixes. So for instance
'{DRA} ~/mytools/ltl2dstar-0.5.2' '{DRA} ~/mytools/ltl2dstar-0.5.2'
will changed into will changed into
'{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O' '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'
#+end_example #+end_example
Therefore you can type just Therefore you can type just