From 1b3054d8a8b97decc682b6f8872cfcee429f3609 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 16 Jun 2015 22:33:32 +0200 Subject: [PATCH] org: simplify calls to ltl2dstar * doc/org/satmin.org: Here. --- doc/org/satmin.org | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/doc/org/satmin.org b/doc/org/satmin.org index edc239fb2..f25952cc6 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -236,7 +236,7 @@ expresses a recurrence property. #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f "Ga R (F!b & (c U b))" -l | -ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' #+END_SRC #+RESULTS: @@ -255,7 +255,7 @@ has 6 states: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f "Ga R (F!b & (c U b))" -l | -ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' #+END_SRC #+RESULTS: @@ -275,7 +275,7 @@ with option =-x sat-acc=M=. For instance: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f "Ga R (F!b & (c U b))" -l | -ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' #+END_SRC #+RESULTS: @@ -364,12 +364,12 @@ used. By default, the procedure will try to use the same acceptance condition (or any inferior one) and produce transition-based acceptance. -For our example, let us first generate an deterministic Rabin +For our example, let us first generate a deterministic Rabin automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]]. #+BEGIN_SRC sh :results verbatim :exports code ltlfilt -f "FGa | FGb" -l | -ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds --output-format=hoa - - > output.hoa +ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa #+END_SRC #+RESULTS: @@ -382,7 +382,7 @@ autfilt output.hoa --dot=.a #+begin_example digraph G { rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> + label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> labelloc="t" node [shape="circle"] fontname="Lato" @@ -391,22 +391,22 @@ digraph G { node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 - 0 [label=<0
⓿❷>] + 0 [label=<0
⓿❷>] 0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=] 0 -> 3 [label=] - 1 [label=<1
❶❷>] + 1 [label=<1
❶❷>] 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] 1 -> 3 [label=] - 2 [label=<2
⓿❸>] + 2 [label=<2
⓿❸>] 2 -> 0 [label=] 2 -> 1 [label=] 2 -> 2 [label=] 2 -> 3 [label=] - 3 [label=<3
❶❸>] + 3 [label=<3
❶❸>] 3 -> 0 [label=] 3 -> 1 [label=] 3 -> 2 [label=] @@ -433,7 +433,7 @@ autfilt --sat-minimize output.hoa --dot=.a #+begin_example digraph G { rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> + label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> labelloc="t" node [shape="circle"] fontname="Lato" @@ -443,10 +443,10 @@ digraph G { I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 0 [label=❶>] - 0 -> 0 [label=⓿❷>] - 0 -> 0 [label=❶❷>] - 0 -> 0 [label=⓿❸>] + 0 -> 0 [label=❶>] + 0 -> 0 [label=⓿❷>] + 0 -> 0 [label=❶❷>] + 0 -> 0 [label=⓿❸>] } #+end_example @@ -467,7 +467,7 @@ autfilt -S --sat-minimize output.hoa --dot=.a #+begin_example digraph G { rankdir=LR - label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> + label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> labelloc="t" node [shape="circle"] fontname="Lato" @@ -476,10 +476,10 @@ digraph G { node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 - 0 [label=<0
❶❷>] + 0 [label=<0
❶❷>] 0 -> 0 [label=] 0 -> 1 [label=] - 1 [label=<1
⓿❸>] + 1 [label=<1
⓿❸>] 1 -> 0 [label=] 1 -> 1 [label=] }