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 8add81824a
commit e2a71cba38
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
: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
automata, alternating automata, and for arbitrary acceptance conditions.
@ -1107,7 +1107,7 @@ correspond to any =twa= flag.
:CUSTOM_ID: named-properties
: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
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
to express the same formula for different tools.
# <<tab:formula-syntaxes>>
#+NAME: tab:formula-syntaxes
| Tool | Formula |
|--------------+-------------------------|
| Spot | =G(a -> (b R !c))= |

30
doc/org/tut51.org
View file

@ -377,23 +377,23 @@ this reason.
<<demo-succ-iter-2>>
#+END_SRC
#+NAME: demo-1
#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
#include <spot/twaalgos/dot.hh>
<<demo-1-aux>>
int main()
{
auto k = std::make_shared<demo_kripke>(spot::make_bdd_dict());
spot::print_dot(std::cout, k);
}
#+END_SRC
#+NAME: demo-1
#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
#include <spot/twaalgos/dot.hh>
<<demo-1-aux>>
int main()
{
auto k = std::make_shared<demo_kripke>(spot::make_bdd_dict());
spot::print_dot(std::cout, k);
}
#+END_SRC
#+BEGIN_SRC dot :file kripke-1.svg :cmd circo :var txt=demo-1 :exports results
$txt
#+END_SRC
#+BEGIN_SRC dot :file kripke-1.svg :cmd circo :var txt=demo-1 :exports results
$txt
#+END_SRC
#+RESULTS:
q[[file:kripke-1.svg]]
#+RESULTS:
[[file:kripke-1.svg]]
* 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
:PROPERTIES:
:CUSTOM_ID: cpp11
:CUSTOM_ID: cpp14
:END:
Because Spot now relies on C++14 features, programs that use Spot