org: Make sure ../../src/bin is searched first.

We used to set PATH in emacs, but because babel executes "sh" via
shell-command, the configuration of the main shell may supersedes ours.

* doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org,
doc/org/genltl.org: Move all local-file variable to...
* doc/org/.dir-locals.el: ... here.  And also set the PATH
in org-babel-sh-command.
* doc/org/init.el.in: Set the PATH in org-babel-sh-command.

doc/org/.dir-locals.el

@@ -3,6 +3,17 @@
 	 (require-final-newline . t)
 	 (mode . whitespace)))
  (org-mode . ((whitespace-style face empty trailing)
+	      (eval .
+		    (progn
+		      (setq org-babel-sh-command (concat "PATH=../../src/bin"
+							 path-separator
+							 "$PATH sh"))
+		      (org-babel-do-load-languages 'org-babel-load-languages
+						   '((sh . t)
+						     (python . t)
+						     (dot . t)))))
+	      (org-confirm-babel-evaluate . nil)
+	      (org-babel-python-command . "/usr/bin/python3")
 	      (org-publish-project-alist
 	       . (("spot-html"
 		   :base-directory "."

doc/org/genltl.org

@@ -73,12 +73,5 @@ Note that for the =--lbt= output, each formula is relabeled using
 =p0=, =p1=, ...  before it is output, when the pattern (like
 =--ccj-alpha=) use different names.
 
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# End:
-
-
 #  LocalWords:  genltl num toc LTL scalable SRC sed gh pn fg FG gf qn
 #  LocalWords:  ccj Xp XXp Xq XXq rv GFp lbt

doc/org/init.el.in

@@ -13,6 +13,9 @@
    (python . t)))
 (setq org-confirm-babel-evaluate nil)
 
+(setq org-babel-sh-command
+      (concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh"))
+
 (setq org-publish-project-alist
       '(("spot-html"
 	:base-directory "@abs_top_srcdir@/doc/org/"

doc/org/ltl2tgba.org

@@ -700,13 +700,6 @@ Because they accept all finite executions that could be extended to
 match the formula, monitor cannot be used to check for eventualities
 such as =F(a)=.  Any finite execution can be extended to match =F(a)=.
 
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# End:
-
-
 #  LocalWords:  ltl tgba num toc PSL Büchi automata SRC GFb invis Acc
 #  LocalWords:  ltlfilt filenames GraphViz vectorial pdf Tpdf dotex
 #  LocalWords:  sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb

doc/org/ltl2tgta.org

@@ -328,13 +328,6 @@ Ala Eddine BEN SALEM's PhD work, and should appear in a future edition
 of ToPNoC (LNCS 7400).
 
 
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# End:
-
-
 #  LocalWords:  ltl tgta num toc Automata automata GraphViz UTF Gb na
 #  LocalWords:  Geldenhuys tgba SRC init invis nb Acc augb sed png fn
 #  LocalWords:  cmdline Tpng txt Büchi livelock gba gta GFa GFb TGTAs

doc/org/ltlcross.org

@@ -358,13 +358,6 @@ When checks are enabled, the negated formulas are intermixed with the
 positives ones in the results.  Therefore the =--no-check= option can
 be used to gather statistics about a specific set of formulas.
 
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t) (python . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# eval: (setq org-babel-python-command "/usr/bin/python3")
-# End:
-
 #  LocalWords:  ltlcross num toc LTL Büchi LBTT Testbench PSL SRC sed
 #  LocalWords:  automata LBT LBTT's ltl tgba GFa lck iDGV sA FYp BYY
 #  LocalWords:  ClVQg wyErP UNE dQ coM tH eHPoQy goto ba lbt modella

doc/org/ltlfilt.org

@@ -127,6 +127,8 @@ ltlfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
       --safety               match safety formulas (even pathological)
       --size-max=INT         match formulas with size <= INT
       --size-min=INT         match formulas with size >= INT
+      --stutter-insensitive, --stutter-invariant
+                             match stutter-insensitive LTL formulas
       --syntactic-guarantee  match syntactic-guarantee formulas
       --syntactic-obligation match syntactic-obligation formulas
       --syntactic-persistence   match syntactic-persistence formulas
@@ -218,15 +220,6 @@ The commands prints the formula and returns an exit status of 0 if the
 two formulas are equivalent.  It would print nothing and set the exit
 status to 1, were the two formulas not equivalent.
 
-
-
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# End:
-
-
 #  LocalWords:  ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck
 #  LocalWords:  ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc
 #  LocalWords:  pnn Xb Fc XFb XXd sed boolean bsize nox Gb Fb Xa XGb

doc/org/randltl.org

@@ -313,13 +313,6 @@ Boolean formula (generated using the priorities set by
 =star_b= is the bounded version, and =andNLM= is the
 non-length-matching variant of the =and= operator.
 
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# End:
-
-
 #  LocalWords:  randltl num toc LTL PSL SRC Gb sed utf UTF lbt LBT's
 #  LocalWords:  Xc GFb Gc Xb Fb XFb Xa dups ltlfilt Fc XXc GX GFc XG
 #  LocalWords:  rewritings ltl ap GF ANDed GFa boolean EConcat eword

doc/org/tools.org

@@ -42,14 +42,6 @@ corresponding commands are hidden.
 - [[file:ltl2tgta.org][=ltl2tgta=]] Translate LTL/PSL formulas into Testing automata.
 - [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-Büchi translators.
 
-
-# Local variables:
-# eval: (setenv "PATH" (concat "../../src/bin" path-separator (getenv "PATH")))
-# eval: (org-babel-do-load-languages 'org-babel-load-languages '((sh . t) (dot . t)))
-# eval: (setq org-confirm-babel-evaluate nil)
-# End:
-
-
 #  LocalWords:  num toc helloworld SRC LTL PSL randltl ltlfilt genltl
 #  LocalWords:  scalable ltl tgba Büchi automata tgta ltlcross eval
 #  LocalWords:  setenv concat getenv setq