autfilt: add a --product option

* src/bin/autfilt.cc: Implement the --product option.
* src/tgbatest/explprod.cc, src/tgbatest/tripprod.cc: Delete.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
src/tgbatest/tripprod.test: Rewrite using autfilt --product.

src/bin/autfilt.cc

@@ -34,6 +34,7 @@
 #include "tgbaalgos/lbtt.hh"
 #include "tgbaalgos/hoa.hh"
 #include "tgbaalgos/neverclaim.hh"
+#include "tgbaalgos/product.hh"
 #include "tgbaalgos/save.hh"
 #include "tgbaalgos/stats.hh"
 #include "tgba/bddprint.hh"
@@ -57,6 +58,7 @@ Convert, transform, and filter Büchi automata.\n\
 #define OPT_STATS 5
 #define OPT_RANDOMIZE 6
 #define OPT_SEED 7
+#define OPT_PRODUCT 8
 
 static const argp_option options[] =
   {
@@ -116,6 +118,8 @@ static const argp_option options[] =
       "a single %", 0 },
     /**************************************************/
     { 0, 0, 0, 0, "Transformation:", -1 },
+    { "product", OPT_PRODUCT, "FILENAME", 0,
+      "build the product with FILENAME", 0 },
     { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
       "randomize states and transitions (specify 's' or 't' to"
       "randomize only states or transitions)", 0 },
@@ -143,6 +147,8 @@ static spot::option_map extra_options;
 static bool randomize_st = false;
 static bool randomize_tr = false;
 static int opt_seed = 0;
+static auto dict = spot::make_bdd_dict();
+static spot::tgba_digraph_ptr opt_product = nullptr;
 
 static int
 to_int(const char* s)
@@ -204,6 +210,20 @@ parse_opt(int key, char* arg, struct argp_state*)
 	  format = Lbtt;
 	}
       break;
+    case OPT_PRODUCT:
+      {
+	spot::hoa_parse_error_list pel;
+	auto p = hoa_parse(arg, pel, dict);
+	if (spot::format_hoa_parse_errors(std::cerr, arg, pel)
+	    || !p || p->aborted)
+	  error(2, 0, "failed to read automaton from %s", arg);
+	if (!opt_product)
+	  opt_product = std::move(p->aut);
+	else
+	  opt_product = spot::product(std::move(opt_product),
+				      std::move(p->aut));
+      }
+      break;
     case OPT_RANDOMIZE:
       if (arg)
 	{
@@ -347,12 +367,19 @@ namespace
     {
       spot::stopwatch sw;
       sw.start();
-      auto aut = post.run(haut->aut, nullptr);
+
-      const double conversion_time = sw.stop();
+      auto aut = haut->aut;
+
+      if (opt_product)
+	aut = spot::product(std::move(aut), opt_product);
+
+      aut = post.run(aut, nullptr);
 
       if (randomize_st || randomize_tr)
 	spot::randomize(aut, randomize_st, randomize_tr);
 
+      const double conversion_time = sw.stop();
+
       switch (format)
 	{
 	case Dot:
@@ -394,7 +421,6 @@ namespace
     process_file(const char* filename)
     {
       spot::hoa_parse_error_list pel;
-      auto b = spot::make_bdd_dict();
       auto hp = spot::hoa_stream_parser(filename);
 
       int err = 0;
@@ -402,7 +428,7 @@ namespace
       for (;;)
 	{
 	  pel.clear();
-	  auto haut = hp.parse(pel, b);
+	  auto haut = hp.parse(pel, dict);
 	  if (!haut && pel.empty())
 	    break;
 	  if (spot::format_hoa_parse_errors(std::cerr, filename, pel))

src/tgbatest/Makefile.am

@@ -38,7 +38,6 @@ check_PROGRAMS = \
   checkta \
   emptchk \
   expldot \
-  explprod \
   intvcomp \
   intvcmp2 \
   ltlprod \
@@ -46,8 +45,7 @@ check_PROGRAMS = \
   powerset \
   readsat \
   taatgba \
-  tgbaread \
+  tgbaread
-  tripprod
 
 # Keep this sorted alphabetically.
 acc_SOURCES = acc.cc
@@ -58,7 +56,6 @@ complement_SOURCES = complementation.cc
 emptchk_SOURCES  = emptchk.cc
 expldot_SOURCES  = powerset.cc
 expldot_CXXFLAGS = -DDOTTY
-explprod_SOURCES = explprod.cc
 intvcomp_SOURCES = intvcomp.cc
 intvcmp2_SOURCES = intvcmp2.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
@@ -69,7 +66,6 @@ randtgba_SOURCES = randtgba.cc
 readsat_SOURCES = readsat.cc
 taatgba_SOURCES = taatgba.cc
 tgbaread_SOURCES = tgbaread.cc
-tripprod_SOURCES = tripprod.cc
 
 # Keep this sorted by STRENGTH.  Test basic things first,
 # because such failures will be easier to diagnose and fix.

src/tgbatest/explpro2.test

@@ -27,23 +27,58 @@
 set -e
 
 cat >input1 <<EOF
-acc = p1 p2;
+HOA: v1
-s1, s2, "!a", p1;
+States: 3
-s1, s3, "!b", p2;
+Start: 0
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[!0] 1 {0}
+[!1] 2 {1}
+State: 1
+State: 2
+--END--
 EOF
 
 cat >input2 <<EOF
-acc = p2 p3;
+HOA: v1
-s1, s2, "b", p2;
+States: 3
-s1, s3, "a", p3;
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 1 {0}
+[1] 2 {1}
+State: 1
+State: 2
+--END--
 EOF
 
 cat >expected <<'EOF'
-acc = "0" "1" "2" "3";
+HOA: v1
-"0 * 0", "1 * 1", "!a & b", "0" "2";
+States: 3
-"0 * 0", "2 * 2", "a & !b", "1" "3";
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 4
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0&!1] 1 {0 2}
+[!0&1] 2 {1 3}
+State: 1
+State: 2
+--END--
 EOF
 
-run 0 ../explprod input1 input2 | tee stdout
+run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout
+# FIXME: Use are-isomorphic
 diff stdout expected
+
 rm input1 input2 stdout expected

src/tgbatest/explpro3.test

@@ -27,24 +27,57 @@
 set -e
 
 cat >input1 <<EOF
-acc = ;
+HOA: v1
-s1, s2, "!a",;
+States: 3
-s1, s3, "!b",;
+Start: 0
+AP: 2 "a" "b"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[!0] 1
+[!1] 2
+State: 1
+State: 2
+--END--
 EOF
 
 cat >input2 <<EOF
-acc = p2 p3;
+HOA: v1
-s1, s2, "b", p2;
+States: 3
-s1, s3, "a", p3;
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 1 {0}
+[1] 2 {1}
+State: 1
+State: 2
+--END--
 EOF
 
 cat >expected <<EOF
-acc = "0" "1";
+HOA: v1
-"0 * 0", "1 * 1", "!a & b", "0";
+States: 3
-"0 * 0", "2 * 2", "a & !b", "1";
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0
+[0&!1] 1 {0}
+[!0&1] 2 {1}
+State: 1
+State: 2
+--END--
 EOF
 
-run 0 ../explprod input1 input2 |
+run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout
-sed 's/"p3" "p2"/"p2" "p3"/g' | tee stdout
+# FIXME: Use are-isomorphic
 diff stdout expected
 rm input1 input2 stdout expected

src/tgbatest/explpro4.test

@@ -27,24 +27,52 @@
 set -e
 
 cat >input1 <<EOF
-acc = p1;
+HOA: v1
-s1, s1, "a", p1;
+States: 1
-s1, s1, "!a", ;
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[!0] 0
+[0] 0 {0}
+--END--
 EOF
 
 cat >input2 <<EOF
-acc= p1;
+HOA: v1
-s1, s1, "a", ;
+States: 1
-s1, s1, "!a", p1;
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[0] 0
+[!0] 0 {0}
+--END--
 EOF
 
 cat >expected <<'EOF'
-acc = "0" "1";
+HOA: v1
-"0 * 0", "0 * 0", "a", "0";
+States: 1
-"0 * 0", "0 * 0", "!a", "1";
+Start: 0
+AP: 1 "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[!0] 0 {1}
+[0] 0 {0}
+--END--
 EOF
 
-run 0 ../explprod input1 input2 > stdout
+run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout
-cat stdout
+# FIXME: Use are-isomorphic
 diff stdout expected
+
 rm input1 input2 stdout expected

src/tgbatest/explprod.cc

@@ -1,66 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
-// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#include <iostream>
-#include <cassert>
-#include <cstdlib>
-#include "tgba/tgbaproduct.hh"
-#include "tgbaparse/public.hh"
-#include "tgbaalgos/save.hh"
-#include "ltlast/allnodes.hh"
-
-void
-syntax(char* prog)
-{
-  std::cerr << prog << " file1 file2" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  int exit_code = 0;
-
-  if (argc != 3)
-    syntax(argv[0]);
-
-  {
-    auto dict = spot::make_bdd_dict();
-
-    spot::ltl::environment& env(spot::ltl::default_environment::instance());
-    spot::tgba_parse_error_list pel1;
-    auto a1 = spot::tgba_parse(argv[1], pel1, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1))
-      return 2;
-    spot::tgba_parse_error_list pel2;
-    auto a2 = spot::tgba_parse(argv[2], pel2, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
-      return 2;
-
-    spot::tgba_save_reachable(std::cout, product(a1, a2));
-  }
-  assert(spot::ltl::unop::instance_count() == 0);
-  assert(spot::ltl::binop::instance_count() == 0);
-  assert(spot::ltl::multop::instance_count() == 0);
-  assert(spot::ltl::atomic_prop::instance_count() == 0);
-  return exit_code;
-}

src/tgbatest/explprod.test

@@ -27,26 +27,77 @@
 set -e
 
 cat >input1 <<EOF
-acc = p1;
+HOA: v1
-s1, s3, "a", p1;
+States: 3
-s1, s2, "b", p1;
+Start: 0
-s2, s1, "!a", p1;
+AP: 3 "a" "b" "c"
-s2, s3, "c", p1;
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0}
+[0] 1
+[1] 2
+State: 1
+State: 2 {0}
+[!0] 0
+[2] 1
+--END--
 EOF
 
 cat >input2 <<EOF
-acc=p2 p3;
+HOA: v1
-s1, s2, "b", p2;
+States: 2
-s2, s1, "a", p3;
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {0}
+[0] 1
+State: 1 {1}
+[1] 0
+--END--
 EOF
 
 cat >expected <<EOF
-acc = "0" "1" "2";
+HOA: v1
-"0 * 0", "1 * 1", "a & b", "0" "1";
+States: 4
-"0 * 0", "2 * 1", "b", "0" "1";
+Start: 0
-"2 * 1", "1 * 0", "a & c", "0" "2";
+AP: 3 "b" "a" "c"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0 1}
+[0&1] 1
+[0] 2
+State: 1
+State: 2 {0 2}
+[1&2] 3
+State: 3
+--END--
 EOF
 
-run 0 ../explprod input1 input2 | tee stdout
+run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout
 diff stdout expected
+
+cat >expected <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 0
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+--END--
+EOF
+
+run 0 ../../bin/autfilt input1 --product input2 --hoa --small | tee stdout
+# FIXME: Use are-isomorphic
+diff stdout expected
+
 rm input1 input2 stdout expected

src/tgbatest/tripprod.cc

@@ -1,70 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
-// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#include <iostream>
-#include <cassert>
-#include <cstdlib>
-#include "tgba/tgbaproduct.hh"
-#include "tgbaparse/public.hh"
-#include "tgbaalgos/save.hh"
-#include "ltlast/allnodes.hh"
-
-void
-syntax(char* prog)
-{
-  std::cerr << prog << " file1 file2 file3" << std::endl;
-  exit(2);
-}
-
-int
-main(int argc, char** argv)
-{
-  int exit_code = 0;
-
-  if (argc != 4)
-    syntax(argv[0]);
-  {
-    auto dict = spot::make_bdd_dict();
-
-    spot::ltl::environment& env(spot::ltl::default_environment::instance());
-    spot::tgba_parse_error_list pel1;
-    auto a1 = spot::tgba_parse(argv[1], pel1, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel1))
-      return 2;
-    spot::tgba_parse_error_list pel2;
-    auto a2 = spot::tgba_parse(argv[2], pel2, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2))
-      return 2;
-    spot::tgba_parse_error_list pel3;
-    auto a3 = spot::tgba_parse(argv[3], pel3, dict, env);
-    if (spot::format_tgba_parse_errors(std::cerr, argv[3], pel3))
-      return 2;
-
-    spot::tgba_save_reachable(std::cout, product(product(a1, a2), a3));
-  }
-
-  assert(spot::ltl::unop::instance_count() == 0);
-  assert(spot::ltl::binop::instance_count() == 0);
-  assert(spot::ltl::multop::instance_count() == 0);
-  assert(spot::ltl::atomic_prop::instance_count() == 0);
-  return exit_code;
-}

src/tgbatest/tripprod.test

@@ -26,37 +26,88 @@
 set -e
 
 cat >input1 <<EOF
-acc = p1;
+HOA: v1
-s1, s3, "a", p1;
+States: 3
-s1, s2, "b", p1;
+Start: 0
-s2, s1, "!a", p1;
+AP: 3 "a" "b" "c"
-s2, s3, "c",;
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc
+--BODY--
+State: 0
+[0] 1 {0}
+[1] 2 {0}
+State: 1
+State: 2
+[!0] 0 {0}
+[2] 1
+--END--
 EOF
 
 cat >input2 <<EOF
-acc = p2 p3;
+HOA: v1
-s1, s2, "b", p2;
+States: 2
-s2, s1, "a", p3;
+Start: 0
+AP: 2 "b" "a"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {0}
+[0] 1
+State: 1 {1}
+[1] 0
+--END--
 EOF
 
 cat >input3 <<EOF
-acc = p4;
+HOA: v1
-s1, s2, "a",;
+States: 3
-s1, s3, "b",;
+Start: 0
-s3, s2,, p4;
+AP: 2 "a" "b"
-s2, s3,, p4;
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[0] 1
+[1] 2
+State: 1 {0}
+[t] 2
+State: 2 {0}
+[t] 1
+--END--
 EOF
 
 cat >expected <<EOF
-acc = "0" "1" "2" "3";
+HOA: v1
-"0 * 0 * 0", "1 * 1 * 1", "a & b", "0" "1";
+States: 7
-"0 * 0 * 0", "2 * 1 * 1", "a & b", "0" "1";
+Start: 0
-"0 * 0 * 0", "1 * 1 * 2", "a & b", "0" "1";
+AP: 3 "b" "a" "c"
-"0 * 0 * 0", "2 * 1 * 2", "b", "0" "1";
+acc-name: generalized-Buchi 4
-"2 * 1 * 1", "1 * 0 * 2", "a & c", "2" "3";
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
-"2 * 1 * 2", "1 * 0 * 1", "a & c", "2" "3";
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0 1}
+[0&1] 1
+[0&1] 2
+[0&1] 3
+[0] 4
+State: 1
+State: 2
+State: 3 {2 3}
+[1&2] 5
+State: 4 {2 3}
+[1&2] 6
+State: 5
+State: 6
+--END--
 EOF
 
-run 0 ../tripprod input1 input2 input3 | tee stdout
+run 0 ../../bin/autfilt input1 --product input2 --product input3 --hoa |
+    tee stdout
+
+# FIXME: Use are-isomorphic
 diff stdout expected
+
 rm input1 input2 input3 stdout expected