never: use state-names as comments

* src/tgbaalgos/neverclaim.cc: Here.
* src/hoaparse/hoaparse.yy: Use set_acceptance_conditions() to set
the number of acceptance sets.  Otherwise, the single_acc_set property
is not set.
* src/tgbaalgos/postproc.cc: When expecting a BA or a monitor, do not do
anything if the input is already a BA or a monitor.
* src/tgbatest/hoaparse.test: Add a test case.
* src/tgbatest/readsave.test: Adjust.

src/hoaparse/hoaparse.yy

@@ -482,7 +482,7 @@ header-item: "States:" INT
 		  }
 		else
 		  {
-		    res.h->aut->acc().add_sets($2);
+		    res.h->aut->set_acceptance_conditions($2);
 		    res.accset = $2;
 		    res.accset_loc = @1 + @2;
 		  }
@@ -1200,7 +1200,7 @@ nc-transition:
 lbtt: lbtt-header lbtt-body ENDAUT
     | lbtt-header-states LBTT_EMPTY
       {
-        res.h->aut->acc().add_sets($2);
+        res.h->aut->set_acceptance_conditions($2);
       }
 
 lbtt-header-states: LBTT
@@ -1403,6 +1403,9 @@ static void fix_properties(result_& r)
 {
   r.h->aut->prop_deterministic(r.deterministic);
   //r.h->aut->prop_complete(r.complete);
+  if (r.acc_style == State_Acc ||
+      (r.acc_style == Mixed_Acc && !r.trans_acc_seen))
+    r.h->aut->prop_state_based_acc();
 }
 
 namespace spot
@@ -1454,9 +1457,6 @@ namespace spot
       r.h->aut->set_named_prop("state-names", r.state_names);
     if (r.neg_acc_sets)
       fix_acceptance(r);
-    if (r.acc_style == State_Acc ||
-	(r.acc_style == Mixed_Acc && !r.trans_acc_seen))
-      r.h->aut->prop_state_based_acc();
     fix_initial_state(r);
     fix_properties(r);
     return r.h;

src/tgbaalgos/neverclaim.cc

@@ -38,6 +38,7 @@ namespace spot
     public:
       std::ostream& os_;
       bool opt_comments_ = false;
+      std::vector<std::string>* sn_ = nullptr;
       bool opt_624_ = false;
       const_tgba_digraph_ptr aut_;
       bool fi_needed_ = false;
@@ -97,8 +98,9 @@ namespace spot
       void
       print_comment(unsigned n) const
       {
-	if (opt_comments_)
+	if (sn_)
-	  os_ << " /* " << aut_->format_state(n) << " */";
+	  if (n < sn_->size() && !(*sn_)[n].empty())
+	    os_ << " /* " << (*sn_)[n] << " */";
       }
 
       void
@@ -184,6 +186,8 @@ namespace spot
       void print(const const_tgba_digraph_ptr& aut)
       {
 	aut_ = aut;
+	if (opt_comments_)
+	  sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
 	start();
 	unsigned init = aut_->get_init_state_number();
 	unsigned ns = aut_->num_states();

src/tgbaalgos/postproc.cc

@@ -124,12 +124,15 @@ namespace spot
   tgba_digraph_ptr
   postprocessor::run(tgba_digraph_ptr a, const ltl::formula* f)
   {
-    if (type_ == TGBA && PREF_ == Any && level_ == Low)
+    if (PREF_ == Any && level_ == Low)
-      {
+      if (type_ == TGBA
-	if (COMP_)
+	  || (type_ == BA && a->is_sba())
-	  a = tgba_complete(a);
+	  || (type_ == Monitor && a->acc().num_sets() == 0))
-	return a;
+	{
-      }
+	  if (COMP_)
+	    a = tgba_complete(a);
+	  return a;
+	}
 
     if (simul_ < 0)
       simul_ = (level_ == Low) ? 1 : 3;

src/tgbatest/hoaparse.test

@@ -1283,3 +1283,34 @@ State: 2 "G((F(a) && F((b) && (c))) && F((d) || (e)))"
 [0&1&2&3 | 0&1&2&4] 2 {0 1 2}
 --END--
 EOF
+
+
+# name states can be output as comments in never claim
+cat >input <<EOF
+HOA: v1
+name: "a U b"
+States: 2
+Start: 1
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 "s0" {0}
+[t] 0
+State: 1 "s1"
+[1] 0
+[0&!1] 1
+--END--
+EOF
+expectok input --spin=c <<EOF
+never { /* a U b */
+T0_init: /* s1 */
+  if
+  :: ((b)) -> goto accept_all
+  :: ((a) && (!(b))) -> goto T0_init
+  fi;
+accept_all: /* s0 */
+  skip
+}
+EOF

src/tgbatest/readsave.test

@@ -315,18 +315,18 @@ digraph G {
   I -> 3
   subgraph cluster_0 {
   label=""
-  1 [label="s1"]
+  1 [label="s1", peripheries=2]
   }
   subgraph cluster_1 {
   label=""
-  0 [label="s0"]
+  0 [label="s0", peripheries=2]
   }
   subgraph cluster_2 {
   label=""
   3 [label="s3"]
   }
-  0 -> 0 [label="b\n{0}"]
+  0 -> 0 [label="b"]
-  1 -> 1 [label="a\n{0}"]
+  1 -> 1 [label="a"]
   2 [label="s2"]
   2 -> 0 [label="b"]
   3 -> 1 [label="a"]