diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index c2b1651e9..e4e57e8bb 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -66,7 +66,7 @@ Acc-Sig: =dstar2tgba= can now be used to convert this DRA into a TGBA, a BA, or a Monitor, using the same options as [[file:ltl2tgba.org][=ltl2tgba=]]. -For instance here is the conversion to a Büchi automaton (=-B=) in [[http://http://www.graphviz.org/][GraphViz]]'s format: +For instance here is the conversion to a Büchi automaton (=-B=) in [[http://www.graphviz.org/][GraphViz]]'s format: #+BEGIN_SRC sh :results verbatim :exports code dstar2tgba -B fagfb diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 3d946f23f..5ceec39fb 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -42,7 +42,7 @@ assumed to be a formula to translate (this differs from [[file:ltlfilt.org][=ltl where such parameters are assumed to be filenames). =ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]]. -The default output format, as shown above, is [[http://http://www.graphviz.org/][GraphViz]]'s format. This +The default output format, as shown above, is [[http://www.graphviz.org/][GraphViz]]'s format. This can converted into a picture, or into vectorial format using =dot= or =dotty=. Typically, you could get a =pdf= of this TGBA using #+BEGIN_SRC sh :results verbatim :exports code diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index 563aa6627..f850de106 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -7,7 +7,7 @@ This tool generates various form of Testing Automata, i.e., automata that observe the /changes/ of atomic propositions, not their values. Three types of automata can be output. The only output format -supported currently is [[http://http://www.graphviz.org/][GraphViz]]'s format, with option =-8= to enable +supported currently is [[http://www.graphviz.org/][GraphViz]]'s format, with option =-8= to enable UTF-8 characters as in other tools. The =--ta= option will translate a formula into Testing Automaton, as