diff --git a/doc/org/spot.css b/doc/org/spot.css index 49f4af0c9..ef1dfe6de 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -19,6 +19,7 @@ body a{color:#008181} 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.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-python:before{content:'Python'} pre.src-C\+\+:before{content:'C++'} diff --git a/doc/org/tut24.org b/doc/org/tut24.org index 1ee5fee77..fd61617d2 100644 --- a/doc/org/tut24.org +++ b/doc/org/tut24.org @@ -54,7 +54,7 @@ and that we run the following code, similar to what we did in the [[file:tut21.org][custom automaton printer]]. #+NAME: nonalt-body -#+BEGIN_SRC C++ :exports code :noweb strip-export +#+BEGIN_SRC C++ std::cout << "Initial state: " << aut->get_init_state_number() << '\n'; const spot::bdd_dict_ptr& dict = aut->get_dict(); @@ -72,7 +72,7 @@ for (unsigned s = 0; s < n; ++s) #+END_SRC #+NAME: nonalt-main -#+BEGIN_SRC C++ :exports none :noweb strip-export +#+BEGIN_SRC C++ :exports none #include #include #include @@ -98,7 +98,7 @@ for (unsigned s = 0; s < n; ++s) #+END_SRC #+NAME: nonalt-one -#+BEGIN_SRC C++ :exports results :noweb strip-export :results verbatim +#+BEGIN_SRC C++ :exports none :noweb strip-export :results verbatim <> void custom_print(spot::twa_graph_ptr& aut) { @@ -106,28 +106,11 @@ for (unsigned s = 0; s < n; ++s) } #+END_SRC -#+RESULTS: nonalt-one -#+begin_example -Initial state: 4294967295 -State 0: - edge(0 -> 0) - 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 +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC 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), @@ -153,7 +136,7 @@ unconditionally. In this example, we simply call =is_univ_dest()= to decide whether to enclose the destinations in braces. #+NAME: nonalt-body2 -#+BEGIN_SRC C++ :exports code :noweb strip-export +#+BEGIN_SRC C++ unsigned init = aut->get_init_state_number(); std::cout << "Initial state:"; if (aut->is_univ_dest(init)) @@ -186,7 +169,7 @@ decide whether to enclose the destinations in braces. #+END_SRC #+NAME: nonalt-two -#+BEGIN_SRC C++ :exports results :noweb strip-export :results verbatim +#+BEGIN_SRC C++ :exports none :noweb strip-export :results verbatim <> void custom_print(spot::twa_graph_ptr& aut) { @@ -194,28 +177,11 @@ decide whether to enclose the destinations in braces. } #+END_SRC -#+RESULTS: nonalt-two -#+begin_example -Initial state: { 0 1 } -State 0: - edge(0 -> 0) - 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 +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC * Python diff --git a/doc/org/tut51.org b/doc/org/tut51.org index b630a0cea..884cd3272 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -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 counterexample: -#+NAME: demo-2-aux -#+BEGIN_SRC C++ :exports none :noweb strip-export - <> - <> - <> - <> - <> +#+NAME: demo-2 +#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim +#include +#include +#include +#include +<> +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(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 - #+NAME: demo-2 - #+BEGIN_SRC C++ :exports both :noweb strip-export :results verbatim - #include - #include - #include - #include - <> - 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(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 +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC 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