diff --git a/doc/mainpage.dox b/doc/mainpage.dox index 7f576ed19..f125bdade 100644 --- a/doc/mainpage.dox +++ b/doc/mainpage.dox @@ -6,7 +6,7 @@ /// structures to manipulate omega-automata, and implement the /// automata-theoretic approach to model-checking. /// -/// See spot.lrde.epita.fr +/// See spot.lrde.epita.fr /// for more information about this project. /// /// \section thisdoc This Document diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index e4e57e8bb..831d65453 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -94,7 +94,7 @@ digraph G { #+end_example Which can be rendered as (note that in this documentation -we use some [[file:aout.org][environement variables]] to produce a more colorful +we use some [[file:oaut.org][environment variables]] to produce a more colorful output by default): #+NAME: fagfb2ba @@ -293,7 +293,7 @@ For instance using =-a --low= will skip any optional post-processing, should you find =dstar2tgba= too slow. Finally, the output format can be changed with the following -[[file:oaout.org][common ouput options]]: +[[file:oaut.org][common ouput options]]: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 5ceec39fb..9300cbe07 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -51,7 +51,7 @@ ltl2tgba "Fa & GFb" | dot -Tpdf > tgba.pdf #+RESULTS: The result would look like this (note that in this documentation -we use some [[file:aout.org][environment variables]] to produce a more colorful +we use some [[file:oaut.org][environment variables]] to produce a more colorful output by default) #+NAME: dotex #+BEGIN_SRC sh :results verbatim :exports none diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index ec45d01c9..1536b6b32 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -131,7 +131,7 @@ tools: - '=ltl3ba -M0 -f %s >%O=' (less deterministic output, can be smaller) - '=ltl3ba -M1 -f %s >%O=' (more deterministic output) - '=modella -r12 -g -e %L %O=' - - '=/path/to/script4lbtt.py %L %O=' (script supplied by [[http://www.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for + - '=/path/to/script4lbtt.py %L %O=' (script supplied by [[http://web.archive.org/web/20070214050826/http://estragon.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for its interface with LBTT) - '=ltl2tgba -s %s >%O=' (smaller output, Büchi automaton) - '=ltl2tgba -s -D %s >%O=' (more deterministic output, Büchi automaton) diff --git a/doc/org/satmin.org b/doc/org/satmin.org index f549b3a03..e1902596e 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -35,7 +35,7 @@ Let us first state a few facts about this minimization procedure. to the SAT solver) exceeds $2^{31}$, or when the SAT-solver was killed by a signal. [[file:autfilt.org][=autfilt --sat-minimize=]] will only output an automaton if the SAT-based minimization was successful. -6) Our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]] describes the SAT encoding for the minimization +6) Our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf%0A][FORTE'14 paper]] describes the SAT encoding for the minimization of deterministic BA and TGBA. Since then, the technique used in the SAT encoding for deterministic TGBA has been generalized to deal with any deterministic TωA. @@ -292,7 +292,7 @@ degeneralized in the meantime for the purpose of determinization. * Low-level details -The following figure (from our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]]) gives an overview of +The following figure (from our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]]) gives an overview of the processing chains that can be used to turn an LTL formula into a minimal DBA/DTBA/DTGBA. The blue area at the top describes =ltl2tgba -D -x sat-minimize=, while the purple area at the bottom corresponds diff --git a/doc/org/tools.org b/doc/org/tools.org index 9dbdf91a6..89ed8e73c 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -65,7 +65,7 @@ the following articles: - *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/. In Proc. of ATVA'13, LNCS 8172, pp. 442--445. Hanoi, Vietnam, - Oct. 2013. ([[http://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]]) + Oct. 2013. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]]) This focuses on =ltlfilt=, =randltl=, and =ltlcross=. diff --git a/src/ltlvisit/dot.hh b/src/ltlvisit/dot.hh index 418970a73..095e13cbd 100644 --- a/src/ltlvisit/dot.hh +++ b/src/ltlvisit/dot.hh @@ -35,7 +35,7 @@ namespace spot /// \param f The formula to translate. /// /// \c dot is part of the GraphViz package - /// http://www.research.att.com/sw/tools/graphviz/ + /// http://www.graphviz.org/ SPOT_API std::ostream& print_dot_psl(std::ostream& os, const formula* f); } diff --git a/src/misc/hashfunc.hh b/src/misc/hashfunc.hh index c431304b6..bf52451e9 100644 --- a/src/misc/hashfunc.hh +++ b/src/misc/hashfunc.hh @@ -35,7 +35,7 @@ namespace spot /// \brief Thomas Wang's 32 bit hash function. /// /// Hash an integer amongst the integers. - /// http://www.concentric.net/~Ttwang/tech/inthash.htm + /// http://web.archive.org/web/2011/concentric.net/~Ttwang/tech/inthash.htm inline size_t wang32_hash(size_t key) { @@ -54,7 +54,7 @@ namespace spot /// This function is suitable for hashing values whose /// high order bits do not vary much (ex. addresses of /// memory objects). Prefer spot::wang32_hash() otherwise. - /// http://www.concentric.net/~Ttwang/tech/addrhash.htm + /// http://web.archive.org/web/2011/concentric.net/~Ttwang/tech/addrhash.htm inline size_t knuth32_hash(size_t key) { diff --git a/wrap/python/ajax/trans.html b/wrap/python/ajax/trans.html index b56f68a2d..a3f156947 100644 --- a/wrap/python/ajax/trans.html +++ b/wrap/python/ajax/trans.html @@ -325,7 +325,7 @@
Spot Logo
+ LRDE Logo