org: work around issue with Org 9.2
See the following email http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html * doc/org/tut24.org, doc/org/tut51.org: Export the output of noweb-based block without ':export results' or ':export both'. * doc/org/spot.css: Add style for src-text.
This commit is contained in:
parent
3908cc1bca
commit
476a874c71
3 changed files with 48 additions and 105 deletions
|
|
@ -19,6 +19,7 @@ body a{color:#008181}
|
||||||
pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto}
|
pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto}
|
||||||
pre.src-hoa{padding-top:8px;border-left-style:solid;border-color:#d70079;overflow:auto}
|
pre.src-hoa{padding-top:8px;border-left-style:solid;border-color:#d70079;overflow:auto}
|
||||||
pre.example{border-left-style:solid;border-color:#d70079}
|
pre.example{border-left-style:solid;border-color:#d70079}
|
||||||
|
pre.src-text{border-left-style:solid;border-color:#d70079}
|
||||||
pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;}
|
pre.src:before{border:none;border-bottom-style:solid;border-color:#00adad;top:0px;}
|
||||||
pre.src-python:before{content:'Python'}
|
pre.src-python:before{content:'Python'}
|
||||||
pre.src-C\+\+:before{content:'C++'}
|
pre.src-C\+\+:before{content:'C++'}
|
||||||
|
|
|
||||||
|
|
@ -54,7 +54,7 @@ and that we run the following code, similar to what we did in the
|
||||||
[[file:tut21.org][custom automaton printer]].
|
[[file:tut21.org][custom automaton printer]].
|
||||||
|
|
||||||
#+NAME: nonalt-body
|
#+NAME: nonalt-body
|
||||||
#+BEGIN_SRC C++ :exports code :noweb strip-export
|
#+BEGIN_SRC C++
|
||||||
std::cout << "Initial state: " << aut->get_init_state_number() << '\n';
|
std::cout << "Initial state: " << aut->get_init_state_number() << '\n';
|
||||||
|
|
||||||
const spot::bdd_dict_ptr& dict = aut->get_dict();
|
const spot::bdd_dict_ptr& dict = aut->get_dict();
|
||||||
|
|
@ -72,7 +72,7 @@ for (unsigned s = 0; s < n; ++s)
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+NAME: nonalt-main
|
#+NAME: nonalt-main
|
||||||
#+BEGIN_SRC C++ :exports none :noweb strip-export
|
#+BEGIN_SRC C++ :exports none
|
||||||
#include <string>
|
#include <string>
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
#include <spot/parseaut/public.hh>
|
#include <spot/parseaut/public.hh>
|
||||||
|
|
@ -98,7 +98,7 @@ for (unsigned s = 0; s < n; ++s)
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+NAME: nonalt-one
|
#+NAME: nonalt-one
|
||||||
#+BEGIN_SRC C++ :exports results :noweb strip-export :results verbatim
|
#+BEGIN_SRC C++ :exports none :noweb strip-export :results verbatim
|
||||||
<<nonalt-main>>
|
<<nonalt-main>>
|
||||||
void custom_print(spot::twa_graph_ptr& aut)
|
void custom_print(spot::twa_graph_ptr& aut)
|
||||||
{
|
{
|
||||||
|
|
@ -106,28 +106,11 @@ for (unsigned s = 0; s < n; ++s)
|
||||||
}
|
}
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: nonalt-one
|
# temporary fix for an issue in Org 9.2, see
|
||||||
#+begin_example
|
# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html
|
||||||
Initial state: 4294967295
|
#+BEGIN_SRC text :noweb yes
|
||||||
State 0:
|
<<nonalt-one()>>
|
||||||
edge(0 -> 0)
|
#+END_SRC
|
||||||
label = a
|
|
||||||
acc sets = {}
|
|
||||||
edge(0 -> 4294967295)
|
|
||||||
label = !a
|
|
||||||
acc sets = {}
|
|
||||||
State 1:
|
|
||||||
edge(1 -> 1)
|
|
||||||
label = !a
|
|
||||||
acc sets = {0}
|
|
||||||
edge(1 -> 2)
|
|
||||||
label = a
|
|
||||||
acc sets = {}
|
|
||||||
State 2:
|
|
||||||
edge(2 -> 2)
|
|
||||||
label = 1
|
|
||||||
acc sets = {}
|
|
||||||
#+end_example
|
|
||||||
|
|
||||||
This output seems correct only for non-universal edges. The reason is
|
This output seems correct only for non-universal edges. The reason is
|
||||||
that Spot always store all edges as a tuple (src,dst,label,acc sets),
|
that Spot always store all edges as a tuple (src,dst,label,acc sets),
|
||||||
|
|
@ -153,7 +136,7 @@ unconditionally. In this example, we simply call =is_univ_dest()= to
|
||||||
decide whether to enclose the destinations in braces.
|
decide whether to enclose the destinations in braces.
|
||||||
|
|
||||||
#+NAME: nonalt-body2
|
#+NAME: nonalt-body2
|
||||||
#+BEGIN_SRC C++ :exports code :noweb strip-export
|
#+BEGIN_SRC C++
|
||||||
unsigned init = aut->get_init_state_number();
|
unsigned init = aut->get_init_state_number();
|
||||||
std::cout << "Initial state:";
|
std::cout << "Initial state:";
|
||||||
if (aut->is_univ_dest(init))
|
if (aut->is_univ_dest(init))
|
||||||
|
|
@ -186,7 +169,7 @@ decide whether to enclose the destinations in braces.
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+NAME: nonalt-two
|
#+NAME: nonalt-two
|
||||||
#+BEGIN_SRC C++ :exports results :noweb strip-export :results verbatim
|
#+BEGIN_SRC C++ :exports none :noweb strip-export :results verbatim
|
||||||
<<nonalt-main>>
|
<<nonalt-main>>
|
||||||
void custom_print(spot::twa_graph_ptr& aut)
|
void custom_print(spot::twa_graph_ptr& aut)
|
||||||
{
|
{
|
||||||
|
|
@ -194,28 +177,11 @@ decide whether to enclose the destinations in braces.
|
||||||
}
|
}
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+RESULTS: nonalt-two
|
# temporary fix for an issue in Org 9.2, see
|
||||||
#+begin_example
|
# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html
|
||||||
Initial state: { 0 1 }
|
#+BEGIN_SRC text :noweb yes
|
||||||
State 0:
|
<<nonalt-two()>>
|
||||||
edge(0 -> 0)
|
#+END_SRC
|
||||||
label = a
|
|
||||||
acc sets = {}
|
|
||||||
edge(0 -> { 0 1 })
|
|
||||||
label = !a
|
|
||||||
acc sets = {}
|
|
||||||
State 1:
|
|
||||||
edge(1 -> 1)
|
|
||||||
label = !a
|
|
||||||
acc sets = {0}
|
|
||||||
edge(1 -> 2)
|
|
||||||
label = a
|
|
||||||
acc sets = {}
|
|
||||||
State 2:
|
|
||||||
edge(2 -> 2)
|
|
||||||
label = 1
|
|
||||||
acc sets = {}
|
|
||||||
#+end_example
|
|
||||||
|
|
||||||
* Python
|
* Python
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -408,64 +408,40 @@ check whether the output is empty. If it is not, that means we have
|
||||||
found a counterexample. Here is some code that would show this
|
found a counterexample. Here is some code that would show this
|
||||||
counterexample:
|
counterexample:
|
||||||
|
|
||||||
#+NAME: demo-2-aux
|
#+NAME: demo-2
|
||||||
#+BEGIN_SRC C++ :exports none :noweb strip-export
|
#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim
|
||||||
<<headers>>
|
#include <spot/tl/parse.hh>
|
||||||
<<demo-state>>
|
#include <spot/twaalgos/translate.hh>
|
||||||
<<demo-iterator>>
|
#include <spot/twa/twaproduct.hh>
|
||||||
<<demo-kripke>>
|
#include <spot/twaalgos/emptiness.hh>
|
||||||
<<demo-succ-iter-2>>
|
<<demo-1-aux>>
|
||||||
|
int main()
|
||||||
|
{
|
||||||
|
auto d = spot::make_bdd_dict();
|
||||||
|
|
||||||
|
// Parse the input formula.
|
||||||
|
spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
|
||||||
|
if (pf.format_errors(std::cerr))
|
||||||
|
return 1;
|
||||||
|
|
||||||
|
// Translate its negation.
|
||||||
|
spot::formula f = spot::formula::Not(pf.f);
|
||||||
|
spot::twa_graph_ptr af = spot::translator(d).run(f);
|
||||||
|
|
||||||
|
// Find a run of or demo_kripke that intersects af.
|
||||||
|
auto k = std::make_shared<demo_kripke>(d);
|
||||||
|
if (auto run = k->intersecting_run(af))
|
||||||
|
std::cout << "formula is violated by the following run:\n" << *run;
|
||||||
|
else
|
||||||
|
std::cout << "formula is verified\n";
|
||||||
|
}
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
#+NAME: demo-2
|
# temporary fix for an issue in Org 9.2, see
|
||||||
#+BEGIN_SRC C++ :exports both :noweb strip-export :results verbatim
|
# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html
|
||||||
#include <spot/tl/parse.hh>
|
#+BEGIN_SRC text :noweb yes
|
||||||
#include <spot/twaalgos/translate.hh>
|
<<demo-2()>>
|
||||||
#include <spot/twa/twaproduct.hh>
|
#+END_SRC
|
||||||
#include <spot/twaalgos/emptiness.hh>
|
|
||||||
<<demo-2-aux>>
|
|
||||||
int main()
|
|
||||||
{
|
|
||||||
auto d = spot::make_bdd_dict();
|
|
||||||
|
|
||||||
// Parse the input formula.
|
|
||||||
spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
|
|
||||||
if (pf.format_errors(std::cerr))
|
|
||||||
return 1;
|
|
||||||
|
|
||||||
// Translate its negation.
|
|
||||||
spot::formula f = spot::formula::Not(pf.f);
|
|
||||||
spot::twa_graph_ptr af = spot::translator(d).run(f);
|
|
||||||
|
|
||||||
// Find a run of or demo_kripke that intersects af.
|
|
||||||
auto k = std::make_shared<demo_kripke>(d);
|
|
||||||
if (auto run = k->intersecting_run(af))
|
|
||||||
std::cout << "formula is violated by the following run:\n" << *run;
|
|
||||||
else
|
|
||||||
std::cout << "formula is verified\n";
|
|
||||||
}
|
|
||||||
#+END_SRC
|
|
||||||
|
|
||||||
#+RESULTS: demo-2
|
|
||||||
#+begin_example
|
|
||||||
formula is violated by the following run:
|
|
||||||
Prefix:
|
|
||||||
(x = 0, y = 0)
|
|
||||||
| !odd_x & !odd_y
|
|
||||||
(x = 1, y = 0)
|
|
||||||
| odd_x & !odd_y
|
|
||||||
(x = 1, y = 1)
|
|
||||||
| odd_x & odd_y
|
|
||||||
(x = 1, y = 2)
|
|
||||||
| odd_x & !odd_y
|
|
||||||
Cycle:
|
|
||||||
(x = 2, y = 2)
|
|
||||||
| !odd_x & !odd_y
|
|
||||||
(x = 0, y = 2)
|
|
||||||
| !odd_x & !odd_y
|
|
||||||
(x = 1, y = 2)
|
|
||||||
| odd_x & !odd_y
|
|
||||||
#+end_example
|
|
||||||
|
|
||||||
With a small variant of the above code, we could also display the
|
With a small variant of the above code, we could also display the
|
||||||
counterexample on the state space, but only because our state space is
|
counterexample on the state space, but only because our state space is
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue