From 925a807f4f9b6c278783a5334bfd9dc2ca148e36 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Nov 2013 02:07:13 +0100 Subject: [PATCH] * doc/org/ltlcross.org: Show how to call ltl3dra and fix typos. --- doc/org/ltlcross.org | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 7caf57c9b..9a524f13f 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -118,7 +118,7 @@ no problem detected converted to non-deterministic TGBA, where generalized acceptance conditions are used to reduce the size of the automaton you would get by the classical conversion from Streett to Büchi. - This kind of output (Rabin or Streett) should be indicated with =%T=. + This kind of output (Rabin or Streett) should be indicated with =%D=. Of course all configured tools need not use the same =%= sequences. The following list shows some typical configurations for some existing @@ -136,17 +136,18 @@ tools: - '=ltl2tgba --lbtt %s >%T=' (smaller output, TGBA) - '=ltl2tgba --lbtt -D %s >%T=' (more deterministic output, TGBA) - '=lbt <%L >%T=' - - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L %T=' + - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L %D=' (deterministic Rabin output) - '=ltl2dstar --automata=streett --ltl2nba=spin:path/tp/ltl2tgba@-sD - %L %T=' (deterministic Streett output) + %L %D=' (deterministic Streett output) - '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L - | dstar2tgba -s >%N=' (external conversion from Rabin to Büchi done by - =dstar2tgba= for additional reduction of the Büchi automaton than + =dstar2tgba= for more reduction of the Büchi automaton than what =ltlcross= would provide) - '=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=, so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file) + - '=ltl3dra -f %s >%D=' * Getting statistics