Fix many dead links.
Also change http:// to https:// for url that would automatically redirect to the later. * doc/mainpage.dox, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/satmin.org, doc/org/tools.org, src/ltlvisit/dot.hh, src/misc/hashfunc.hh, wrap/python/ajax/trans.html: Here.
This commit is contained in:
Alexandre Duret-Lutz
parent
44bc1d7e39
commit
750d352fb6
9 changed files with 12 additions and 12 deletions
|
|
@ -6,7 +6,7 @@
|
||||||
/// structures to manipulate omega-automata, and implement the
|
/// structures to manipulate omega-automata, and implement the
|
||||||
/// automata-theoretic approach to model-checking.
|
/// automata-theoretic approach to model-checking.
|
||||||
///
|
///
|
||||||
/// See <a href="http://spot.lrde.epita.fr/">spot.lrde.epita.fr</a>
|
/// See <a href="https://spot.lrde.epita.fr/">spot.lrde.epita.fr</a>
|
||||||
/// for more information about this project.
|
/// for more information about this project.
|
||||||
///
|
///
|
||||||
/// \section thisdoc This Document
|
/// \section thisdoc This Document
|
||||||
|
|
|
||||||
|
|
@ -94,7 +94,7 @@ digraph G {
|
||||||
#+end_example
|
#+end_example
|
||||||
|
|
||||||
Which can be rendered as (note that in this documentation
|
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):
|
output by default):
|
||||||
|
|
||||||
#+NAME: fagfb2ba
|
#+NAME: fagfb2ba
|
||||||
|
|
@ -293,7 +293,7 @@ For instance using =-a --low= will skip any optional post-processing,
|
||||||
should you find =dstar2tgba= too slow.
|
should you find =dstar2tgba= too slow.
|
||||||
|
|
||||||
Finally, the output format can be changed with the following
|
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
|
#+BEGIN_SRC sh :results verbatim :exports results
|
||||||
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
|
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
|
||||||
|
|
@ -51,7 +51,7 @@ ltl2tgba "Fa & GFb" | dot -Tpdf > tgba.pdf
|
||||||
#+RESULTS:
|
#+RESULTS:
|
||||||
|
|
||||||
The result would look like this (note that in this documentation
|
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)
|
output by default)
|
||||||
#+NAME: dotex
|
#+NAME: dotex
|
||||||
#+BEGIN_SRC sh :results verbatim :exports none
|
#+BEGIN_SRC sh :results verbatim :exports none
|
||||||
|
|
|
||||||
|
|
@ -131,7 +131,7 @@ tools:
|
||||||
- '=ltl3ba -M0 -f %s >%O=' (less deterministic output, can be smaller)
|
- '=ltl3ba -M0 -f %s >%O=' (less deterministic output, can be smaller)
|
||||||
- '=ltl3ba -M1 -f %s >%O=' (more deterministic output)
|
- '=ltl3ba -M1 -f %s >%O=' (more deterministic output)
|
||||||
- '=modella -r12 -g -e %L %O='
|
- '=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)
|
its interface with LBTT)
|
||||||
- '=ltl2tgba -s %s >%O=' (smaller output, Büchi automaton)
|
- '=ltl2tgba -s %s >%O=' (smaller output, Büchi automaton)
|
||||||
- '=ltl2tgba -s -D %s >%O=' (more deterministic output, Büchi automaton)
|
- '=ltl2tgba -s -D %s >%O=' (more deterministic output, Büchi automaton)
|
||||||
|
|
|
||||||
|
|
@ -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
|
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
|
killed by a signal. [[file:autfilt.org][=autfilt --sat-minimize=]] will only output an
|
||||||
automaton if the SAT-based minimization was successful.
|
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
|
of deterministic BA and TGBA. Since then, the technique used in
|
||||||
the SAT encoding for deterministic TGBA has been generalized to
|
the SAT encoding for deterministic TGBA has been generalized to
|
||||||
deal with any deterministic TωA.
|
deal with any deterministic TωA.
|
||||||
|
|
@ -292,7 +292,7 @@ degeneralized in the meantime for the purpose of determinization.
|
||||||
|
|
||||||
* Low-level details
|
* 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
|
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
|
minimal DBA/DTBA/DTGBA. The blue area at the top describes =ltl2tgba
|
||||||
-D -x sat-minimize=, while the purple area at the bottom corresponds
|
-D -x sat-minimize=, while the purple area at the bottom corresponds
|
||||||
|
|
|
||||||
|
|
@ -65,7 +65,7 @@ the following articles:
|
||||||
|
|
||||||
- *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/.
|
- *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/.
|
||||||
In Proc. of ATVA'13, LNCS 8172, pp. 442--445. Hanoi, Vietnam,
|
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=.
|
This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -35,7 +35,7 @@ namespace spot
|
||||||
/// \param f The formula to translate.
|
/// \param f The formula to translate.
|
||||||
///
|
///
|
||||||
/// \c dot is part of the GraphViz package
|
/// \c dot is part of the GraphViz package
|
||||||
/// http://www.research.att.com/sw/tools/graphviz/
|
/// http://www.graphviz.org/
|
||||||
SPOT_API
|
SPOT_API
|
||||||
std::ostream& print_dot_psl(std::ostream& os, const formula* f);
|
std::ostream& print_dot_psl(std::ostream& os, const formula* f);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -35,7 +35,7 @@ namespace spot
|
||||||
/// \brief Thomas Wang's 32 bit hash function.
|
/// \brief Thomas Wang's 32 bit hash function.
|
||||||
///
|
///
|
||||||
/// Hash an integer amongst the integers.
|
/// 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
|
inline size_t
|
||||||
wang32_hash(size_t key)
|
wang32_hash(size_t key)
|
||||||
{
|
{
|
||||||
|
|
@ -54,7 +54,7 @@ namespace spot
|
||||||
/// This function is suitable for hashing values whose
|
/// This function is suitable for hashing values whose
|
||||||
/// high order bits do not vary much (ex. addresses of
|
/// high order bits do not vary much (ex. addresses of
|
||||||
/// memory objects). Prefer spot::wang32_hash() otherwise.
|
/// 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
|
inline size_t
|
||||||
knuth32_hash(size_t key)
|
knuth32_hash(size_t key)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -325,7 +325,7 @@
|
||||||
<div id="mailicon">
|
<div id="mailicon">
|
||||||
<a href="mailto:spot@lrde.epita.fr"><img border=0 src="logos/mail.png" alt="Spot Logo" class="rtip" title="A bug? A question? Please e-mail us at <b>spot@lrde.epita.fr</b>."></a></div>
|
<a href="mailto:spot@lrde.epita.fr"><img border=0 src="logos/mail.png" alt="Spot Logo" class="rtip" title="A bug? A question? Please e-mail us at <b>spot@lrde.epita.fr</b>."></a></div>
|
||||||
<div id="lrdelogo">
|
<div id="lrdelogo">
|
||||||
<a href="http://www.lrde.epita.fr/"><img border=0 src="logos/lrde64.png" alt="LRDE Logo"></a></div>
|
<a href="https://www.lrde.epita.fr/"><img border=0 src="logos/lrde64.png" alt="LRDE Logo"></a></div>
|
||||||
<div id="lip6logo">
|
<div id="lip6logo">
|
||||||
<a href="http://www.lip6.fr/"><img border=0 src="logos/lip6sys64.png" alt="LIP6 Logo"></a></div>
|
<a href="http://www.lip6.fr/"><img border=0 src="logos/lip6sys64.png" alt="LIP6 Logo"></a></div>
|
||||||
<div class="ltl2tgba">
|
<div class="ltl2tgba">
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue