never: add an option to output in Spin's 6.2.4 style

Fixes #46.

* src/tgbaalgos/neverclaim.cc: Add option '6'.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Make it
possible to use the option.
* NEWS, doc/org/oaut.org: Document it.
* src/tgbatest/ltlcross2.test: Test it.

NEWS

@@ -65,17 +65,24 @@ New in spot 1.99a (not yet released)
 
     - LTL formulas can include /* comments */.
 
+    - GraphViz output now uses an horizontal layout by default.
+      The --dot option of the various command-line tools takes an
+      optional parameter to fine-tune the GraphViz output (including
+      vertical layout, round states, and named automata).
+
+    - Never claims can now be output in the style usd by Spin since
+      version 6.2.4 (i.e., using do..od instead of if..fi, and with
+      atomic statements for terminal acceptance).  The default output
+      is still the old one for compatibility with existing tools.  The
+      new style can be requested from command-line tools using option
+      --spin=6 (or -s6 for short).
+
     - Spot is now compiling in C++11 mode.  The set of features we use
       requires GCC >= 4.6 or Clang >= 3.1.  These minimum versions
       are old enough that it should not be an issue to most people.
 
     - Boost is not used anymore.
 
-    - GraphViz output now uses an horizontal layout by default.
-      The --dot option of the various command-line tools takes an
-      optional parameter to fine-tune the GraphViz output (including
-      vertical layout, round states, and named automata).
-
     - The tgba_succ_iterator interface has changed.  Methods next(),
       and first() should now return a bool indicating whether the
       current iteration is valid.

doc/org/oaut.org

@@ -416,7 +416,7 @@ ltl2tgba -s 'a U b'
 #+END_SRC
 
 #+RESULTS:
-: never {
+: never { /* a U b */
 : T0_init:
 :   if
 :   :: ((b)) -> goto accept_all
@@ -426,6 +426,29 @@ ltl2tgba -s 'a U b'
 :   skip
 : }
 
+Recent versions of Spin (starting with Spin 6.2.4) output never claims
+in a slightly different style that can be requested using either
+=-s6= or =--spin=6=:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+ltl2tgba -s6 'a U b'
+#+END_SRC
+
+#+RESULTS:
+: never { /* a U b */
+: T0_init:
+:   do
+:   :: atomic { ((b)) -> assert(!((b))) }
+:   :: ((a) && (!(b))) -> goto T0_init
+:   od;
+: accept_all:
+:   skip
+: }
+
+(Note that while Spot is able to read never claims that follow any of
+these two styles, it is not capable of interpreting an arbitrary piece
+of Promela syntax.)
+
 * Dot output
 
 The =--dot= option (which usually is the default) causes automata to be

src/bin/common_aoutput.cc

@@ -34,6 +34,7 @@
 
 automaton_format_t automaton_format = Dot;
 static const char* opt_dot = nullptr;
+static const char* opt_never = nullptr;
 static const char* hoa_opt = nullptr;
 const char* opt_name = nullptr;
 static const char* stats = "";
@@ -63,7 +64,9 @@ static const argp_option options[] =
     { "name", OPT_NAME, "FORMAT", 0,
       "set the name of the output automaton", 0 },
     { "quiet", 'q', 0, 0, "suppress all normal output", 0 },
-    { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
+    { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)."
+      "  Add letters to select (6) Spin's 6.2.4 style, (c) comments on states",
+      0 },
     { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
     { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
       "(ignored with --lbtt or --spin)", 0 },
@@ -161,6 +164,8 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
       automaton_format = Spin;
       if (type != spot::postprocessor::Monitor)
 	type = spot::postprocessor::BA;
+      if (arg)
+	opt_never = arg;
       break;
     case OPT_DOT:
       automaton_format = Dot;
@@ -249,7 +254,7 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut,
       spot::tgba_save_reachable(std::cout, aut);
       break;
     case Spin:
-      spot::never_claim_reachable(std::cout, aut);
+      spot::never_claim_reachable(std::cout, aut, opt_never);
       break;
     case Stats:
       statistics.print(haut, aut, f, filename, loc, time) << '\n';

src/bin/dstar2tgba.cc

@@ -85,7 +85,9 @@ static const argp_option options[] =
       " on Büchi automata)", 0 },
     { "name", OPT_NAME, "FORMAT", 0,
       "set the name of the output automaton", 0 },
-    { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
+    { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)."
+      "  Add letters to select (6) Spin's 6.2.4 style, (c) comments on states",
+      0 },
     { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
     { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
       "(ignored with --lbtt or --spin)", 0 },
@@ -137,6 +139,7 @@ static output_format format = Dot;
 static const char* opt_dot = nullptr;
 static const char* stats = "";
 static const char* hoa_opt = nullptr;
+static const char* opt_never = nullptr;
 static const char* opt_name = nullptr;
 static spot::option_map extra_options;
 
@@ -166,6 +169,8 @@ parse_opt(int key, char* arg, struct argp_state*)
       format = Spin;
       if (type != spot::postprocessor::Monitor)
 	type = spot::postprocessor::BA;
+      if (arg)
+	opt_never = arg;
       break;
     case 'x':
       {
@@ -366,7 +371,7 @@ namespace
 	  spot::tgba_save_reachable(std::cout, aut);
 	  break;
 	case Spin:
-	  spot::never_claim_reachable(std::cout, aut);
+	  spot::never_claim_reachable(std::cout, aut, opt_never);
 	  break;
 	case Stats:
 	  statistics.print(daut, aut, filename, conversion_time) << '\n';

src/tgbaalgos/neverclaim.cc

@@ -38,9 +38,11 @@ namespace spot
     public:
       std::ostream& os_;
       bool opt_comments_ = false;
+      bool opt_624_ = false;
       const_tgba_digraph_ptr aut_;
       bool fi_needed_ = false;
       bool need_accept_all_ = false;
+      unsigned accept_all_ = 0;
 
     public:
       never_claim_output(std::ostream& os, const char* options)
@@ -50,6 +52,9 @@ namespace spot
 	  while (char c = *options++)
 	    switch (c)
 	      {
+	      case '6':
+		opt_624_ = true;
+		break;
 	      case 'c':
 		opt_comments_ = true;
 		break;
@@ -73,7 +78,11 @@ namespace spot
       end() const
       {
 	if (need_accept_all_)
-	  os_ << "accept_all:\n  skip\n";
+	  {
+	    os_ << "accept_all:";
+	    print_comment(accept_all_);
+	    os_ << "\n  skip\n";
+	  }
 	os_ << '}' << std::endl;
       }
 
@@ -85,6 +94,13 @@ namespace spot
 	return (it->cond == bddtrue) && (it->dst == n) && (++it == ts.end());
       }
 
+      void
+      print_comment(unsigned n) const
+      {
+	if (opt_comments_)
+	  os_ << " /* " << aut_->format_state(n) << " */";
+      }
+
       void
       print_state(unsigned n) const
       {
@@ -114,33 +130,54 @@ namespace spot
 	  {
 	    // We want the accept_all state at the end of the never claim.
 	    need_accept_all_ = true;
+	    accept_all_ = n;
 	    return;
 	  }
 
 	print_state(n);
 	os_ << ':';
-	if (opt_comments_)
+	print_comment(n);
-	  os_ << " /* " << aut_->format_state(n) << " */";
+	os_ << (opt_624_ ? "\n  do\n" : "\n  if\n");
-	os_ << "\n  if\n";
 	bool did_output = false;
-	for (auto&t : aut_->out(n))
+	for (auto& t: aut_->out(n))
 	  {
 	    did_output = true;
+	    bool atom =
+	      opt_624_ && aut_->state_is_accepting(t.dst) && is_sink(t.dst);
+	    if (atom)
+	      os_ << "  :: atomic { (";
+	    else
 	      os_ << "  :: (";
 	    const ltl::formula* f = bdd_to_formula(t.cond, aut_->get_dict());
 	    to_spin_string(f, os_, true);
-	    f->destroy();
+	    if (atom)
+	      {
+		os_ << ") -> assert(!(";
+		to_spin_string(f, os_, true);
+		os_ << ")) }";
+	      }
+	    else
+	      {
 		os_ << ") -> goto ";
 		print_state(t.dst);
+	      }
+	    f->destroy();
 	    os_ << '\n';
 	  }
 	if (!did_output)
+	  {
+	    if (opt_624_)
+	      {
+		os_ << "  :: atomic { (false) -> assert(!(false)) }";
+	      }
+	    else
 	      {
 		os_ << "  :: (false) -> goto ";
 		print_state(n);
+	      }
 	    os_ << '\n';
 	  }
-	os_ << "  fi;\n";
+	os_ << (opt_624_ ? "  od;\n" : "  fi;\n");
       }
 
       void print(const const_tgba_digraph_ptr& aut)

src/tgbatest/ltlcross2.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-# de l'Epita (LRDE).
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -40,6 +40,7 @@ ltl2tgba=../../bin/ltl2tgba
 "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \
 "$ltl2tgba --spin --ba -x degen-skip=0 %f >%N" \
 "$ltl2tgba --lbtt --ba --high %f > %T" \
+"$ltl2tgba --spin=6 --ba --medium %f > %N" \
 "$ltl2tgba --hoa  -BDC %f > %H" \
 "$ltl2tgba --lbtt -BC %f > %T" \
 --json=output.json --csv=output.csv