diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 831d65453..0555f2fe6 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -25,7 +25,7 @@ Additionally we use =ltlfilt= to convert our formula to the prefix format used by =ltl2dstar=. #+BEGIN_SRC sh :results verbatim :exports node -ltlfilt -f 'Fa & GFb' -l | ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - fagfb +ltlfilt -f 'Fa & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-sD - fagfb #+END_SRC By looking at the file =fagfb= you can see the =ltl2dsar= actually @@ -350,7 +350,7 @@ head -n 10 | while read f; do echo "$f" ltlfilt -l -f "$f" | - ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | + ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d; complete? %p' done #+END_SRC diff --git a/doc/org/satmin.org b/doc/org/satmin.org index e1902596e..e3ad94822 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -683,16 +683,16 @@ its iterations in this file. rm -f stats.csv export SPOT_SATLOG=stats.csv 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)' cat stats.csv #+END_SRC #+RESULTS: : input(states=11) output(states=5, acc-sets=2, det=1) -: 9,8,35,64,44064,9043076,978,26,277,21 -: 7,7,33,56,14504,2191905,237,7,113,4 -: 6,6,28,48,10512,1358243,145,4,45,2 -: 5,,,,7200,782342,82,3,31,2 +: 9,9,36,72,44064,9043076,616,18,258,24 +: 8,7,29,56,19712,3493822,236,9,135,6 +: 6,6,25,48,10512,1362749,97,4,42,2 +: 5,,,,7200,784142,65,2,40,2 The generated CSV file use the following columns: - the n passed to the SAT-based minimization algorithm