postproc: add a SBAcc option

Producing state-based acceptance is now part of the postprocessing
routines.  That means we can more easily simplify automata with
state-based acceptance (using autfilt -S --small --high, for instance)
and as as side-effect, ltl2tgba can produce GBA.  However the result of
ltl2tgba -S is often larger than that of ltl2tgba -B.

* src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Implement
the SBAcc option.
* src/bin/common_post.cc, src/bin/common_post.hh: Implement -S.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
src/bin/ltl2tgta.cc, src/bin/ltldo.cc: Adjust.
* src/tests/sim3.test: Augment test case.
* NEWS, doc/org/ltl2tgba.org, doc/org/autfilt.org: Document it -S.

NEWS

@@ -80,6 +80,12 @@ New in spot 1.99b (not yet released)
       accepting run (but there might be several ways to reject a
       word).  This works for LTL and PSL formulas.
 
+    - ltl2tgba has a new option, -S to produce generalized-Büchi
+      automata with state-based acceptance.  Those are obtained by
+      converting some transition-based GBA into a state-based GBA, so
+      they are usually not as small as one would wish.  The same
+      option -S is also supported by autfilt.
+
     - ltlcross will work with translator producing automata with any
       acceptance condition, provided the output is in the HOA format.
       So it can effectively be used to validate tools producing Rabin

doc/org/autfilt.org

@@ -143,7 +143,6 @@ refer to the output automaton.  Of course this distinction makes sense
 only if =autfilt= was instructed to perform an operation on the input
 automaton.
 
-
 * Filtering automata
 
 =autfilt= supports multiple ways to filter automata based on different
@@ -192,10 +191,10 @@ autfilt --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
 #+END_SRC
 #+RESULTS:
 :   -B, --ba                   Büchi Automaton
+:       --generic              Any acceptance is allowed (default)
 :   -M, --monitor              Monitor (accepts all finite prefixes of the given
 :                              property)
 :       --tgba                 Transition-based Generalized Büchi Automaton
-:                              (default)
 
 These options specifies desired properties:
 
@@ -203,11 +202,14 @@ These options specifies desired properties:
 autfilt --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d'
 #+END_SRC
 #+RESULTS:
-:   -a, --any                  no preference (default)
+:   -a, --any                  no preference, do not bother making it small or
+:                              deterministic (default)
 :   -C, --complete             output a complete automaton (combine with other
 :                              intents)
 :   -D, --deterministic        prefer deterministic automata
 :       --small                prefer small automata
+:   -S, --state-based-acceptance, --sbacc
+:                              define the acceptance using states
 
 Finally, the following switches control the amount of effort applied
 to reach the desired properties:
@@ -252,7 +254,8 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
                              exclusive propositions.
       --instut[=1|2]         allow more stuttering (two possible algorithms)
       --keep-states=NUM[,NUM...]   only keep specified states.  The first state
-                             will be the new initial state
+                             will be the new initial state.  Implies
+                             --remove-unreachable-states.
       --mask-acc=NUM[,NUM...]   remove all transitions in specified acceptance
                              sets
       --merge-transitions    merge transitions with same destination and
@@ -263,10 +266,20 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
       --remove-ap=AP[=0|=1][,AP...]
                              remove atomic propositions either by existential
                              quantification, or by assigning them 0 or 1
-      --remove-fin           rewrite the automaton without using Fin
+      --remove-dead-states   remove states that are unreachable, or that cannot
-                             acceptance
+                             belong to an infinite path
-      --state-based-acceptance, --sbacc
+      --remove-fin           rewrite the automaton without using Fin acceptance
-                             define the acceptance using states
+
+      --remove-unreachable-states
+                             remove states that are unreachable from the
+                             initial state
+      --separate-sets        if both Inf(x) and Fin(x) appear in the acceptance
+                             condition, replace Fin(x) by a new Fin(y) and
+                             adjust the automaton
+      --simplify-exclusive-ap   if --exclusive-ap is used, assume those AP
+                             groups are actually exclusive in the system to
+                             simplify the expression of transition labels
+                             (implies --merge-transitions)
       --strip-acceptance     remove the acceptance condition and all acceptance
                              sets
 #+end_example
@@ -345,11 +358,11 @@ $txt
 #+RESULTS:
 [[file:autfilt-ex1.png]]
 
-Using =--sbacc= will "push" the acceptance membership of the transitions to the states:
+Using =-S= will "push" the acceptance membership of the transitions to the states:
 
 #+NAME: autfilt-ex2
 #+BEGIN_SRC sh :results verbatim :export code
-autfilt --sbacc aut-ex1.hoa --dot=.a
+autfilt -S aut-ex1.hoa --dot=.a
 #+END_SRC
 
 #+RESULTS: autfilt-ex2
@@ -358,6 +371,7 @@ digraph G {
   rankdir=LR
   label=<(Fin(<font color="#F17CB0">❶</font>) &amp; Fin(<font color="#B276B2">❸</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&amp;Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#F17CB0">❶</font>)>
   labelloc="t"
+  node [shape="circle"]
   fontname="Lato"
   node [fontname="Lato"]
   edge [fontname="Lato"]

doc/org/ltl2tgba.org

@@ -214,6 +214,61 @@ $txt
 #+RESULTS:
 [[file:dotex2ba-t.png]]
 
+Using option =-S= instead of option =-B= you can obtain generalized
+Büchi automata with state-based acceptance.  Here is the same formula
+as above, for comparison.
+
+#+NAME: dotex2gba
+#+BEGIN_SRC sh :results verbatim :exports code
+ltl2tgba -S 'GFa & GFb'
+#+END_SRC
+
+#+RESULTS: dotex2gba
+#+begin_example
+digraph G {
+  rankdir=LR
+  node [shape="circle"]
+  fontname="Lato"
+  node [fontname="Lato"]
+  edge [fontname="Lato"]
+  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label=<0<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
+  0 -> 0 [label=<a &amp; b>]
+  0 -> 1 [label=<!a &amp; !b>]
+  0 -> 2 [label=<!a &amp; b>]
+  0 -> 3 [label=<a &amp; !b>]
+  1 [label=<1>]
+  1 -> 0 [label=<a &amp; b>]
+  1 -> 1 [label=<!a &amp; !b>]
+  1 -> 2 [label=<!a &amp; b>]
+  1 -> 3 [label=<a &amp; !b>]
+  2 [label=<2<br/><font color="#F17CB0">❶</font>>]
+  2 -> 0 [label=<a &amp; b>]
+  2 -> 1 [label=<!a &amp; !b>]
+  2 -> 2 [label=<!a &amp; b>]
+  2 -> 3 [label=<a &amp; !b>]
+  3 [label=<3<br/><font color="#5DA5DA">⓿</font>>]
+  3 -> 0 [label=<a &amp; b>]
+  3 -> 1 [label=<!a &amp; !b>]
+  3 -> 2 [label=<!a &amp; b>]
+  3 -> 3 [label=<a &amp; !b>]
+}
+#+end_example
+
+#+BEGIN_SRC dot :file dotex2gba.png :cmdline -Tpng :var txt=dotex2gba :exports results
+$txt
+#+END_SRC
+#+RESULTS:
+[[file:dotex2gba.png]]
+
+Note that =ltl2tgba= is not very good at generating state-based
+generalized Büchi automata (GBA): all it does is generating a
+transition-based one internally, and then pushing acceptance sets onto
+states.  On this example, the resulting GBA produced by =-S= is larger
+than the BA produced by =-B=.
+
 As already discussed on the page about [[file:oaut.org][common output options]], various
 options controls the output format of =ltl2tgba=:
 

src/bin/autfilt.cc

@@ -50,7 +50,6 @@
 #include "twaalgos/are_isomorphic.hh"
 #include "twaalgos/canonicalize.hh"
 #include "twaalgos/mask.hh"
-#include "twaalgos/sbacc.hh"
 #include "twaalgos/sepsets.hh"
 #include "twaalgos/stripacc.hh"
 #include "twaalgos/remfin.hh"
@@ -92,7 +91,6 @@ enum {
   OPT_REM_DEAD,
   OPT_REM_UNREACH,
   OPT_REM_FIN,
-  OPT_SBACC,
   OPT_SEED,
   OPT_SEP_SETS,
   OPT_SIMPLIFY_EXCLUSIVE_AP,
@@ -133,9 +131,6 @@ static const argp_option options[] =
     { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 },
     { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
       "remove all transitions in specified acceptance sets", 0 },
-    { "state-based-acceptance", OPT_SBACC, 0, 0,
-      "define the acceptance using states", 0 },
-    { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
     { "strip-acceptance", OPT_STRIPACC, 0, 0,
       "remove the acceptance condition and all acceptance sets", 0 },
     { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
@@ -251,7 +246,6 @@ static int opt_max_count = -1;
 static bool opt_destut = false;
 static char opt_instut = 0;
 static bool opt_is_empty = false;
-static bool opt_sbacc = false;
 static bool opt_stripacc = false;
 static bool opt_dnf_acc = false;
 static bool opt_cnf_acc = false;
@@ -437,9 +431,6 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_REM_UNREACH:
       opt_rem_unreach = true;
       break;
-    case OPT_SBACC:
-      opt_sbacc = true;
-      break;
     case OPT_SEED:
       opt_seed = to_int(arg);
       break;
@@ -583,9 +574,6 @@ namespace
       if (opt->product)
 	aut = spot::product(std::move(aut), opt->product);
 
-      if (opt_sbacc)
-	aut = spot::sbacc(aut);
-
       aut = post.run(aut, nullptr);
 
       if (randomize_st || randomize_tr)
@@ -686,7 +674,7 @@ main(int argc, char** argv)
       spot::srand(opt_seed);
 
       spot::postprocessor post(&extra_options);
-      post.set_pref(pref | comp);
+      post.set_pref(pref | comp | sbacc);
       post.set_type(type);
       post.set_level(level);
 

src/bin/common_post.cc

@@ -24,6 +24,7 @@
 spot::postprocessor::output_type type = spot::postprocessor::TGBA;
 spot::postprocessor::output_pref pref = spot::postprocessor::Small;
 spot::postprocessor::output_pref comp = spot::postprocessor::Any;
+spot::postprocessor::output_pref sbacc = spot::postprocessor::Any;
 spot::postprocessor::optimization_level level = spot::postprocessor::High;
 
 enum {
@@ -43,6 +44,9 @@ static const argp_option options[] =
       "or deterministic", 0 },
     { "complete", 'C', 0, 0, "output a complete automaton (combine "
       "with other intents)", 0 },
+    { "state-based-acceptance", 'S', 0, 0,
+      "define the acceptance using states", 0 },
+    { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
     /**************************************************/
     { 0, 0, 0, 0, "Optimization level:", 21 },
     { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 },
@@ -62,6 +66,9 @@ static const argp_option options_disabled[] =
       "or deterministic (default)", 0 },
     { "complete", 'C', 0, 0, "output a complete automaton (combine "
       "with other intents)", 0 },
+    { "state-based-acceptance", 'S', 0, 0,
+      "define the acceptance using states", 0 },
+    { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
     /**************************************************/
     { 0, 0, 0, 0, "Optimization level:", 21 },
     { "low", OPT_LOW, 0, 0, "minimal optimizations (fast, default)", 0 },
@@ -86,6 +93,9 @@ parse_opt_post(int key, char*, struct argp_state*)
     case 'D':
       pref = spot::postprocessor::Deterministic;
       break;
+    case 'S':
+      sbacc = spot::postprocessor::SBAcc;
+      break;
     case OPT_HIGH:
       level = spot::postprocessor::High;
       simplification_level = 3;

src/bin/common_post.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -29,4 +29,5 @@ extern const struct argp post_argp_disabled; // postprocessing disabled
 extern spot::postprocessor::output_type type;
 extern spot::postprocessor::output_pref pref;
 extern spot::postprocessor::output_pref comp;
+extern spot::postprocessor::output_pref sbacc;
 extern spot::postprocessor::optimization_level level;

src/bin/dstar2tgba.cc

@@ -428,7 +428,7 @@ main(int argc, char** argv)
     jobs.emplace_back("-", true);
 
   spot::postprocessor post(&extra_options);
-  post.set_pref(pref | comp);
+  post.set_pref(pref | comp | sbacc);
   post.set_type(type);
   post.set_level(level);
 

src/bin/ltl2tgba.cc

@@ -204,7 +204,7 @@ main(int argc, char** argv)
 	  program_name);
 
   spot::translator trans(&extra_options);
-  trans.set_pref(pref | comp);
+  trans.set_pref(pref | comp | sbacc);
   trans.set_type(type);
   trans.set_level(level);
   if (unambiguous)

src/bin/ltl2tgta.cc

@@ -232,7 +232,7 @@ main(int argc, char** argv)
 	  program_name);
 
   spot::translator trans(&extra_options);
-  trans.set_pref(pref | comp);
+  trans.set_pref(pref | comp | sbacc);
   trans.set_type(type);
   trans.set_level(level);
 

src/bin/ltldo.cc

@@ -358,7 +358,7 @@ main(int argc, char** argv)
   setup_sig_handler();
 
   spot::postprocessor post;
-  post.set_pref(pref | comp);
+  post.set_pref(pref | comp | sbacc);
   post.set_type(type);
   post.set_level(level);
 

src/tests/sim3.test

@@ -47,3 +47,40 @@ State: 6 {0 3}
 EOF
 
 test "`../../bin/autfilt --small input --stats=%S,%s`" = 7,5
+
+../../bin/autfilt -S --high --small input -H > out
+cat >expected <<EOF
+HOA: v1
+States: 5
+Start: 0
+AP: 2 "b" "a"
+Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0 {0}
+[!1] 1
+[1] 3
+State: 1 {1 3}
+[0&!1] 1
+[!0&!1] 2
+[0&1] 3
+[!0&1] 4
+State: 2 {1}
+[0&!1] 1
+[!0&!1] 2
+[0&1] 3
+[!0&1] 4
+State: 3 {0 3}
+[0&!1] 1
+[!0&!1] 2
+[0&1] 3
+[!0&1] 4
+State: 4 {0}
+[0&!1] 1
+[!0&!1] 2
+[0&1] 3
+[!0&1] 4
+--END--
+EOF
+diff out expected

src/twaalgos/postproc.cc

@@ -31,6 +31,7 @@
 #include "dtgbasat.hh"
 #include "complete.hh"
 #include "totgba.hh"
+#include "sbacc.hh"
 
 namespace spot
 {
@@ -107,7 +108,7 @@ namespace spot
   }
 
   twa_graph_ptr
-  postprocessor::do_ba_simul(const twa_graph_ptr& a, int opt)
+  postprocessor::do_sba_simul(const twa_graph_ptr& a, int opt)
   {
     if (ba_simul_ <= 0)
       return a;
@@ -132,11 +133,12 @@ namespace spot
 			  degen_reset_, degen_order_,
 			  degen_cache_, degen_lskip_,
 			  degen_lowinit_);
-    return do_ba_simul(d, ba_simul_);
+    return do_sba_simul(d, ba_simul_);
   }
 
 #define PREF_ (pref_ & (Small | Deterministic))
 #define COMP_ (pref_ & Complete)
+#define SBACC_ (pref_ & SBAcc)
 
   twa_graph_ptr
   postprocessor::run(twa_graph_ptr a, const ltl::formula* f)
@@ -152,6 +154,8 @@ namespace spot
 	{
 	  if (COMP_)
 	    a = tgba_complete(a);
+	  if (SBACC_)
+	    a = sbacc(a);
 	  return a;
 	}
 
@@ -161,7 +165,7 @@ namespace spot
       ba_simul_ = (level_ == High) ? 3 : 0;
     if (scc_filter_ < 0)
       scc_filter_ = 1;
-    if (type_ == BA)
+    if (type_ == BA || SBACC_)
       state_based_ = true;
 
     int original_acc = a->acc().num_sets();
@@ -173,7 +177,7 @@ namespace spot
       a = scc_filter_states(a);
     else if (scc_filter_ > 0)
       {
-	if (type_ == BA && a->is_sba())
+	if (state_based_ && a->has_state_based_acc())
 	  a = scc_filter_states(a);
 	else
 	  a = scc_filter(a, scc_filter_ > 1);
@@ -208,8 +212,10 @@ namespace spot
       {
 	if (type_ == BA)
 	  a = do_degen(a);
-	if (COMP_ == Complete)
+	if (COMP_)
 	  a = tgba_complete(a);
+	if (SBACC_)
+	  a = sbacc(a);
 	return a;
       }
 
@@ -243,9 +249,11 @@ namespace spot
     // at hard levels if we want a small output.
     if (!dba || (level_ == High && PREF_ == Small))
       {
-	if (type_ == BA && a->is_sba() && !tba_determinisation_)
+	if (((SBACC_ && a->has_state_based_acc())
+	     || (type_ == BA && a->is_sba()))
+	    && !tba_determinisation_)
 	  {
-	    sim = do_ba_simul(a, ba_simul_);
+	    sim = do_sba_simul(a, ba_simul_);
 	  }
 	else
 	  {
@@ -254,6 +262,8 @@ namespace spot
 	    // No need to do that if tba_determinisation_ will be used.
 	    if (type_ == BA && !tba_determinisation_)
 	      sim = do_degen(sim);
+	    else if (SBACC_ && !tba_determinisation_)
+	      sim = sbacc(sim);
 	  }
       }
 
@@ -266,11 +276,19 @@ namespace spot
 	// We postponed degeneralization above i case we would need
 	// to perform TBA-determinisation, but now it is clear
 	// that we won't perform it.  So do degeneralize.
-	if (tba_determinisation_ && type_ == BA)
+	if (tba_determinisation_)
+	  {
+	    if (type_ == BA)
 	      {
 		dba = do_degen(dba);
 		assert(is_deterministic(dba));
 	      }
+	    else if (SBACC_)
+	      {
+		dba = sbacc(dba);
+		assert(is_deterministic(dba));
+	      }
+	  }
       }
 
     // If we don't have a DBA, attempt tba-determinization if requested.
@@ -412,11 +430,17 @@ namespace spot
       {
 	if (dba && !dba_is_minimal) // WDBA is already clean.
 	  {
+	    if (state_based_ && dba->has_state_based_acc())
+	      dba = scc_filter_states(dba);
+	    else
 	      dba = scc_filter(dba, true);
 	    assert(!sim);
 	  }
 	else if (sim)
 	  {
+	    if (state_based_ && sim->has_state_based_acc())
+	      sim = scc_filter_states(sim);
+	    else
 	      sim = scc_filter(sim, true);
 	    assert(!dba);
 	  }
@@ -426,6 +450,8 @@ namespace spot
 
     if (COMP_)
       sim = tgba_complete(sim);
+    if (SBACC_)
+      sim = sbacc(sim);
 
     return sim;
   }

src/twaalgos/postproc.hh

@@ -78,7 +78,9 @@ namespace spot
       Deterministic = 2,
       // 3 reserved for unambiguous
       // Combine Complete as 'Small | Complete' or 'Deterministic | Complete'
-      Complete = 4
+      Complete = 4,
+      // Likewise.  State-based acceptance.
+      SBAcc = 8,
     };
     typedef int output_pref;
 
@@ -104,7 +106,7 @@ namespace spot
 
   protected:
     twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt);
-    twa_graph_ptr do_ba_simul(const twa_graph_ptr& input, int opt);
+    twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt);
     twa_graph_ptr do_degen(const twa_graph_ptr& input);
 
     output_type type_;