diff --git a/doc/org/.dir-locals.el b/doc/org/.dir-locals.el index a30bf9806..e94e0784a 100644 --- a/doc/org/.dir-locals.el +++ b/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 "." diff --git a/doc/org/genltl.org b/doc/org/genltl.org index d5e995b36..909058e9e 100644 --- a/doc/org/genltl.org +++ b/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 diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 564ac2415..b6ad3a55a 100644 --- a/doc/org/init.el.in +++ b/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/" diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 4c6caef5b..e48cac66b 100644 --- a/doc/org/ltl2tgba.org +++ b/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 diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index 1c4863070..6190232c3 100644 --- a/doc/org/ltl2tgta.org +++ b/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 diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index ebfffc59f..5af5e53bd 100644 --- a/doc/org/ltlcross.org +++ b/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 diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index c642aa273..43df9c605 100644 --- a/doc/org/ltlfilt.org +++ b/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 diff --git a/doc/org/randltl.org b/doc/org/randltl.org index b16fdaaed..85da5e8db 100644 --- a/doc/org/randltl.org +++ b/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 diff --git a/doc/org/tools.org b/doc/org/tools.org index 17671c2a6..8e56a2dba 100644 --- a/doc/org/tools.org +++ b/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