diff --git a/doc/org/index.org b/doc/org/index.org index 0a1a69a9f..6ee957a47 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Spot #+SETUPFILE: setup.org diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index 30385484f..563aa6627 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: =ltl2tgta= #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/randltl.org b/doc/org/randltl.org index 11554315b..839dc066b 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: =randltl= #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 2bb7a792c..edc239fb2 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: SAT-based Minimization of Deterministic ω-Automata #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/tut.org b/doc/org/tut.org index 64cbee878..d90530bb7 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Code Examples #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 53687e6f6..e84efacd5 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Parsing and Printing LTL Formulas #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut02.org b/doc/org/tut02.org index 06584971d..b983d08a8 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Relabeling Formulas #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html @@ -20,7 +21,7 @@ ltlfilt -ps --relabel=pnn --define -f '"Proc@Here" U ("var > 10" | "var < 4")' : (p0) U ((p1) || (p2)) When is this output interesting, you may ask? It is useful for -instance if you want to call =ltl2ba= (or any other LTL-to-Büchi +instance if you want to call =ltl2ba= (or any other LTL-to-Büchi translator) using a formula with complex atomic propositions it cannot parse. Then you can pass the rewritten formula to =ltl2ba=, and prepend all those =#define= to its output. For instance: diff --git a/doc/org/tut10.org b/doc/org/tut10.org index b3d8ccd48..4f7c8c4ab 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Translating an LTL formula into a never claim #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut20.org b/doc/org/tut20.org index 5623dd87c..097aaa718 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Converting a never claim into HOA #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 7cc5f85fa..e98ecbbaa 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Custom print of an automaton #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut22.org b/doc/org/tut22.org index 573df4222..b8b499993 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: Creating an automaton in C++ #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html