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

org: fix broken links

Browse source 
* doc/org/upgrade2.org, doc/org/ioltl.org, doc/org/concepts.org: Here.
* doc/org/tut51.org: Fix example output.
This commit is contained in:
Alexandre Duret-Lutz 2018-04-06 10:59:12 +02:00
parent be9096a5cd
commit 309eb0bbaa
4 changed files with 19 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

4
doc/org/concepts.org
View file

@ -836,7 +836,7 @@ $txt
:CUSTOM_ID: hoa :CUSTOM_ID: hoa
:END: :END:
The [[http://adl.github.io/hoaf/][HOA format]] inherits several features from the [[:dstar][DSTAR format]], but The [[http://adl.github.io/hoaf/][HOA format]] inherits several features from the [[#dstar][DSTAR format]], but
extends it in many ways, including support for non-deterministic extends it in many ways, including support for non-deterministic
automata, alternating automata, and for arbitrary acceptance conditions. automata, alternating automata, and for arbitrary acceptance conditions.
@ -1107,7 +1107,7 @@ correspond to any =twa= flag.
:CUSTOM_ID: named-properties :CUSTOM_ID: named-properties
:END: :END:
In addition to [[#proeprty-flags][property flags]], automata in Spot can be tied to an In addition to [[#property-flags][property flags]], automata in Spot can be tied to an
arbitrary number of objects via a system of named properties that is arbitrary number of objects via a system of named properties that is
implemented mostly as an =std::map= between =std::string= and =void*=. implemented mostly as an =std::map= between =std::string= and =void*=.

2
doc/org/ioltl.org
View file

@ -44,7 +44,7 @@ Spot's default LTL parser is able to parse the syntaxes of many tools,
such as [[http://spinroot.com][Spin]], [[http://vlsi.colorado.edu/~rbloem/wring.html][Wring]], [[http://goal.im.ntu.edu.tw][Goal]], etc. For instance here are the preferred ways such as [[http://spinroot.com][Spin]], [[http://vlsi.colorado.edu/~rbloem/wring.html][Wring]], [[http://goal.im.ntu.edu.tw][Goal]], etc. For instance here are the preferred ways
to express the same formula for different tools. to express the same formula for different tools.
# <<tab:formula-syntaxes>> #+NAME: tab:formula-syntaxes
| Tool | Formula | | Tool | Formula |
|--------------+-------------------------| |--------------+-------------------------|
| Spot | =G(a -> (b R !c))= | | Spot | =G(a -> (b R !c))= |

26
doc/org/tut51.org
View file

@ -377,23 +377,23 @@ this reason.
<<demo-succ-iter-2>> <<demo-succ-iter-2>>
#+END_SRC #+END_SRC
#+NAME: demo-1 #+NAME: demo-1
#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim #+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
#include <spot/twaalgos/dot.hh> #include <spot/twaalgos/dot.hh>
<<demo-1-aux>> <<demo-1-aux>>
int main() int main()
{ {
auto k = std::make_shared<demo_kripke>(spot::make_bdd_dict()); auto k = std::make_shared<demo_kripke>(spot::make_bdd_dict());
spot::print_dot(std::cout, k); spot::print_dot(std::cout, k);
} }
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file kripke-1.svg :cmd circo :var txt=demo-1 :exports results #+BEGIN_SRC dot :file kripke-1.svg :cmd circo :var txt=demo-1 :exports results
$txt $txt
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
q[[file:kripke-1.svg]] [[file:kripke-1.svg]]
* Checking a property on this state space * Checking a property on this state space

2
doc/org/upgrade2.org
View file

@ -85,7 +85,7 @@ experience of updating a couple of projects that are using Spot.
* Upgrading to C++14 * Upgrading to C++14
:PROPERTIES: :PROPERTIES:
:CUSTOM_ID: cpp11 :CUSTOM_ID: cpp14
:END: :END:
Because Spot now relies on C++14 features, programs that use Spot Because Spot now relies on C++14 features, programs that use Spot