nix: provide package in release tarballs

* flake.nix, flake.lock: here

.gitignore

@@ -81,3 +81,4 @@ GTAGS
 *.dsc
 *.gcov
 spot.spec
+default.nix

HACKING

@@ -290,8 +290,8 @@ would understand with:
   make check LOG_DRIVER=$PWD/tools/test-driver-teamcity
 
 
-Coding conventions
-==================
+C++ Coding conventions
+======================
 
 Here some of the conventions we follow in Spot, so that the code looks
 homogeneous.  Please follow these strictly.  Since this is free
@@ -682,3 +682,43 @@ Other style recommandations
 
   * Always code as if the person who ends up maintaining your code is
     a violent psychopath who knows where you live.
+
+
+Coding conventions for Python Tests
+===================================
+
+Unless you have some specific reason to write test cases in C++ (for
+instance do test some specific C++ constructions, or to use valgrind),
+prefer writing test cases in Python.  Writing test cases in C++
+requires some compilation, which slows down the test suite.  Doing the
+same test in Python is therefore faster, and it has the added benefit
+of ensuring that the Python bindings works.
+
+We have two types of Python tests: Python scripts or jupyter
+notebooks.  Jupyter notebooks are usually used for a sequence of
+examples and comments that can also serve as part of the
+documentation.  Such jupyter notebooks should be added to the list of
+code examples in doc/org/tut.org.  Testing a notebook is done by the
+tests/python/ipnbdoctest.py scripts, which evaluate each cells, and
+checks that the obtainted result is equivalent to the result saved in
+the notebook.  The process is a bit slow, so plain Python scripts
+should be prefered for most tests.
+
+If you do need a notebook to tests Jupyter-specific code but this
+notebook should not be shown in the documentation, use a filename
+starting with '_'.
+
+Tests written as Python scripts should follow the same convention as
+shell scripts: exit 0 for PASS, exit 77 for SKIP, and any other exit
+code for FAIL.
+
+Do not use assert() in those scripts, as (1) asserts can be disabled,
+and (2) they provide poor insights in case of failures.  Instead do
+
+   from unittest import TestCase
+   tc = TestCase()
+
+and then use tc.assertTrue(...), tc.assertEqual(..., ...),
+tc.assertIn(..., ...), etc.  In case of failures, those will print
+useful messages in the trace of the tests.  For instance multiline
+strings that should have been equal will be presented with a diff.

Makefile.am

@@ -68,7 +68,8 @@ EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog	\
 	     tools/help2man tools/man2html.pl			\
 	     tools/test-driver-teamcity $(UTF8) $(DEBIAN)	\
 	     m4/gnulib-cache.m4 .dir-locals.el			\
-	     spot.spec spot.spec.in
+	     spot.spec spot.spec.in \
+	     default.nix default.nix.in
 
 dist-hook: gen-ChangeLog
 
@@ -114,3 +115,6 @@ deb: dist
 
 spot.spec: configure.ac spot.spec.in
 	sed 's/[@]VERSION[@]/$(VERSION)/;s/[@]GITPATCH[@]/@@@$(GITPATCH)/;s/@@@\.//' spot.spec.in > $@.tmp && mv $@.tmp $@
+
+default.nix: configure.ac default.nix.in
+	sed 's/[@]VERSION[@]/$(VERSION)/' default.nix.in > $@.tmp && mv $@.tmp $@

NEWS

@@ -9,8 +9,17 @@ New in spot 2.10.4.dev  (net yet released)
   - autfilt has a new --to-finite option, illustrated on
     https://spot.lrde.epita.fr/tut12.html
 
+  - ltlfilt has a new --sonf option to produce a formula's Suffix
+    Operator Normal Form, described in [cimatti.06.fmcad].  The
+    associated option --sonf-aps allows listing the newly introduced
+    atomic propositions.
+
   Library:
 
+  - The new function suffix_operator_normal_form() implements
+    transformation of formulas to Suffix Operator Normal Form,
+    described in [cimatti.06.fmcad].
+
   - "original-classes" is a new named property similar to
     "original-states".  It maps an each state to an unsigned integer
     such that if two classes are in the same class, they are expected
@@ -65,6 +74,12 @@ New in spot 2.10.4.dev  (net yet released)
   - work around a portability issue in Flex 2.6.4 preventing
     compilation on OpenBSD.
 
+  - Do not use the seq command in test cases, it is not available
+    everywhere.
+
+  - Do not erase the previous contents of the PYTHONPATH environment
+    variable when running tests, prepend to it instead.
+
 New in spot 2.10.4  (2022-02-01)
 
   Bug fixed:

bin/ltlfilt.cc

@@ -38,6 +38,7 @@
 #include <spot/misc/hash.hh>
 #include <spot/misc/timer.hh>
 #include <spot/tl/simplify.hh>
+#include <spot/tl/sonf.hh>
 #include <spot/tl/length.hh>
 #include <spot/tl/relabel.hh>
 #include <spot/tl/unabbrev.hh>
@@ -100,6 +101,8 @@ enum {
   OPT_SIZE_MAX,
   OPT_SIZE_MIN,
   OPT_SKIP_ERRORS,
+  OPT_SONF,
+  OPT_SONF_APS,
   OPT_STUTTER_INSENSITIVE,
   OPT_SUSPENDABLE,
   OPT_SYNTACTIC_GUARANTEE,
@@ -127,6 +130,11 @@ static const argp_option options[] =
     { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 0 },
     { "nnf", OPT_NNF, nullptr, 0,
       "rewrite formulas in negative normal form", 0 },
+    { "sonf", OPT_SONF, "PREFIX", OPTION_ARG_OPTIONAL,
+      "rewrite formulas in suffix operator normal form", 0 },
+    { "sonf-aps", OPT_SONF_APS, "FILENAME", OPTION_ARG_OPTIONAL,
+      "when used with --sonf, output the newly introduced atomic "
+      "propositions", 0 },
     { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL,
       "relabel all atomic propositions, alphabetically unless " \
       "specified otherwise", 0 },
@@ -316,6 +324,7 @@ static range opt_nth = { 0, std::numeric_limits<int>::max() };
 static int opt_max_count = -1;
 static long int match_count = 0;
 static const char* from_ltlf = nullptr;
+static const char* sonf = nullptr;
 
 
 // We want all these variables to be destroyed when we exit main, to
@@ -327,6 +336,7 @@ static struct opt_t
   spot::bdd_dict_ptr dict = spot::make_bdd_dict();
   spot::exclusive_ap excl_ap;
   std::unique_ptr<output_file> output_define = nullptr;
+  std::unique_ptr<output_file> output_sonf = nullptr;
   spot::formula implied_by = nullptr;
   spot::formula imply = nullptr;
   spot::formula equivalent_to = nullptr;
@@ -460,6 +470,12 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_NNF:
       nnf = true;
       break;
+    case OPT_SONF:
+      sonf = arg ? arg : "sonf_";
+      break;
+    case OPT_SONF_APS:
+      opt->output_sonf.reset(new output_file(arg ? arg : "-"));
+      break;
     case OPT_OBLIGATION:
       obligation = true;
       break;
@@ -650,6 +666,25 @@ namespace
       if (nnf)
         f = simpl.negative_normal_form(f);
 
+      if (sonf != nullptr)
+        {
+          std::vector<std::string> new_aps;
+          std::tie(f, new_aps) = suffix_operator_normal_form(f, sonf);
+
+          if (opt->output_sonf
+              && output_format != count_output
+              && output_format != quiet_output)
+            {
+              for (size_t i = 0; i < new_aps.size(); ++i)
+                {
+                  if (i > 0)
+                    opt->output_sonf->ostream() << ' ';
+                  opt->output_sonf->ostream() << new_aps[i];
+                }
+              opt->output_sonf->ostream() << '\n';
+            }
+        }
+
       switch (relabeling)
         {
         case ApRelabeling:

default.nix.in

@@ -0,0 +1,35 @@
+# -*- mode: nix; coding: utf-8 -*-
+# Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita
+# (LRDE).
+#
+# 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/>.
+
+{ pkgs ? import <nixpkgs> {} }:
+let
+  version = "@VERSION@";
+in
+pkgs.stdenv.mkDerivation {
+  inherit version;
+  pname = "spot";
+
+  buildInputs = [
+    pkgs.python3
+  ];
+
+  src = ./.;
+
+  enableParallelBuilding = true;
+}

doc/spot.bib

@@ -214,6 +214,18 @@
   doi		= {10.1109/DepCoS-RELCOMEX.2009.31}
 }
 
+@InProceedings{	cimatti.06.fmcad,
+  author	= {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone and
+		  Tonetta, Stefano},
+  title	= {From {PSL} to {NBA}: a Modular Symbolic Encoding},
+  booktitle	= {Proceedings of the 6th conference on Formal Methods in Computer
+		  Aided Design (FMCAD'06)},
+  pages	= {125--133},
+  year		= {2006},
+  publisher	= {IEEE Computer Society},
+  doi		= {10.1109/FMCAD.2006.19}
+}
+
 @Article{	  cimatti.08.tcad,
   author	= {Alessandro Cimatti and Marco Roveri and Stefano Tonetta},
   journal	= {IEEE Transactions on Computer Aided Design of Integrated

flake.lock

@@ -0,0 +1,43 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1642700792,
+        "narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "846b2ae0fc4cc943637d3d1def4454213e203cba",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1643503720,
+        "narHash": "sha256-tJic20ufuRnG8V+fTCd3YU6xl1ImxNspoEkXHct0AG4=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "0f316e4d72daed659233817ffe52bf08e081b5de",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-21.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,209 @@
+{
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.11";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+  outputs = { self, nixpkgs, flake-utils, ... }:
+    flake-utils.lib.eachSystem
+      [
+        "x86_64-linux"
+      ]
+
+      (system:
+        let
+          pkgs = import nixpkgs { inherit system; };
+          lib = pkgs.lib;
+
+          mkSpotApps = appNames:
+            pkgs.lib.genAttrs appNames
+              (name: flake-utils.lib.mkApp {
+                drv = self.packages.${system}.spot;
+                name = name;
+              });
+
+          spotPackage =
+            let
+              inherit (builtins)
+                filter
+                head
+                isString
+                match
+                readFile
+                split
+              ;
+
+              # NOTE: Maintaining the version separately would be a pain, and we
+              # can't have a flake.nix.in with a @VERSION@ because it would make
+              # the flake unusable without running autoconf first, defeating some
+              # of its purpose.
+              #
+              # So let's get it the hard way instead :)
+              extractVersionRegex = ''^AC_INIT\(\[spot], \[([^]]+)], \[spot@lrde\.epita\.fr]\)$'';
+              getLines = (fileContent:
+                filter isString (split "\n" fileContent)
+              );
+              findVersionLine = (lines:
+                lib.lists.findFirst
+                  (l: lib.strings.hasPrefix "AC_INIT(" l)
+                  null
+                  lines
+              );
+              getVersion = (file:
+                let
+                  lines = getLines (readFile file);
+                  versionLine = findVersionLine lines;
+                  version = head (match extractVersionRegex versionLine);
+                in
+                  version
+              );
+            in
+              {
+                lib,
+                pkgs,
+                stdenv,
+                # FIXME: do we want this flag?
+                buildOrgDoc ? false,
+                # Whether to enable Spot's Python 3 bindings
+                enablePython ? false
+              }:
+              stdenv.mkDerivation {
+                pname = "spot";
+                version = getVersion ./configure.ac;
+
+                src = self;
+
+                enableParallelBuilding = true;
+
+                # NOTE: Nix enables a lot of hardening flags by default, some of
+                # these probably harm performance so I've disabled everything
+                # (haven't benchmarked with vs without these, though).
+                hardeningDisable = [ "all" ];
+
+                # NOTE: mktexpk fails without a HOME set
+                preBuild = ''
+                  export HOME=$TMPDIR
+                  patchShebangs tools
+                '' + (if buildOrgDoc then ''
+                ln -s ${pkgs.plantuml}/lib/plantuml.jar doc/org/plantuml.jar
+              '' else ''
+                  touch doc/org-stamp
+                '');
+
+                configureFlags = [
+                  "--disable-devel"
+                  "--enable-optimizations"
+                ] ++ lib.optional (!enablePython) [
+                  "--disable-python"
+                ];
+
+                nativeBuildInputs = with pkgs; [
+                  autoreconfHook
+
+                  autoconf
+                  automake
+                  bison
+                  flex
+                  libtool
+                  perl
+                ] ++ lib.optional buildOrgDoc [
+                  graphviz
+                  groff
+                  plantuml
+                  pdf2svg
+                  R
+                ] ++ lib.optional enablePython [
+                  python3
+                  swig4
+                ];
+
+                buildInputs = with pkgs; [
+                  # should provide the minimum amount of packages necessary for
+                  # building tl.pdf
+                  (texlive.combine {
+                    inherit (texlive)
+                      scheme-basic
+                      latexmk
+
+                      booktabs
+                      doi
+                      doublestroke
+                      koma-script
+                      mathabx
+                      mathpazo
+                      metafont
+                      microtype
+                      nag
+                      pgf
+                      standalone
+                      stmaryrd
+                      tabulary
+                      todonotes
+                      wasy
+                      wasysym
+                    ;
+                  })
+                ];
+              };
+        in
+          {
+            defaultPackage = self.packages.${system}.spot;
+
+            packages = {
+              # binaries + library only
+              spot = pkgs.callPackage spotPackage {};
+
+              # NOTE: clang build is broken on Nix when linking to stdlib++, using
+              #       libcxx instead. See:
+              #       https://github.com/NixOS/nixpkgs/issues/91285
+              spotClang = pkgs.callPackage spotPackage {
+                stdenv = pkgs.llvmPackages.libcxxStdenv;
+              };
+
+              spotWithOrgDoc = pkgs.callPackage spotPackage {
+                buildOrgDoc = true;
+              };
+
+              spotWithPython = pkgs.python3Packages.toPythonModule (
+                pkgs.callPackage spotPackage {
+                  enablePython = true;
+                }
+              );
+
+              spotFull = pkgs.python3Packages.toPythonModule (
+                pkgs.callPackage spotPackage {
+                  buildOrgDoc = true; enablePython = true;
+                }
+              );
+            };
+
+            apps = mkSpotApps [
+              "autcross"
+              "autfilt"
+              "dstar2tgba"
+              "genaut"
+              "genltl"
+              "ltl2tgba"
+              "ltl2tgta"
+              "ltlcross"
+              "ltldo"
+              "ltlfilt"
+              "ltlgrind"
+              "ltlsynt"
+              "randaut"
+              "randltl"
+            ];
+
+            devShell = pkgs.mkShell {
+              name = "spot-dev";
+              inputsFrom = [ self.packages.${system}.spotFull ];
+              buildInputs = [
+                pkgs.gdb
+
+                (pkgs.python3.withPackages (p: [
+                  p.jupyter
+                  p.ipython # otherwise ipython module isn't found when running ipynb tests
+                ]))
+              ];
+            };
+          });
+}

python/spot/impl.i

@@ -94,6 +94,7 @@
 #include <spot/tl/nenoform.hh>
 #include <spot/tl/print.hh>
 #include <spot/tl/simplify.hh>
+#include <spot/tl/sonf.hh>
 #include <spot/tl/unabbrev.hh>
 #include <spot/tl/randomltl.hh>
 #include <spot/tl/length.hh>
@@ -517,6 +518,7 @@ namespace std {
   %template(vectorbdd) vector<bdd>;
   %template(aliasvector) vector<pair<string, bdd>>;
   %template(vectorstring) vector<string>;
+  %template(pair_formula_vectorstring) pair<spot::formula, vector<string>>;
   %template(atomic_prop_set) set<spot::formula>;
   %template(relabeling_map) map<spot::formula, spot::formula>;
 }
@@ -531,6 +533,8 @@ namespace std {
 %include <spot/twa/bdddict.hh>
 %include <spot/twa/bddprint.hh>
 %include <spot/twa/formula2bdd.hh>
+%template(formula_to_bdd) spot::formula_to_bdd<spot::twa_graph>;
+
 %include <spot/twa/fwd.hh>
  /* These operators may raise exceptions, and we do not
     want Swig4 to convert those exceptions to NotImplemented. */
@@ -577,6 +581,7 @@ namespace std {
 %include <spot/tl/contain.hh>
 %include <spot/tl/dot.hh>
 %include <spot/tl/nenoform.hh>
+%include <spot/tl/sonf.hh>
 %include <spot/tl/print.hh>
 %include <spot/tl/simplify.hh>
 %include <spot/tl/unabbrev.hh>

spot/tl/Makefile.am

@@ -44,6 +44,7 @@ tl_HEADERS =					\
   remove_x.hh					\
   simplify.hh					\
   snf.hh					\
+  sonf.hh					\
   unabbrev.hh
 
 noinst_LTLIBRARIES = libtl.la
@@ -68,4 +69,5 @@ libtl_la_SOURCES =				\
   remove_x.cc					\
   simplify.cc					\
   snf.cc					\
+  sonf.cc					\
   unabbrev.cc

spot/tl/sonf.cc

@@ -0,0 +1,185 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
+//
+// 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 "config.h"
+#include <spot/tl/nenoform.hh>
+#include <spot/tl/sonf.hh>
+
+#include <string>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+namespace spot
+{
+  namespace
+  {
+    /// Uses `extractor` to extract some parts of the formula and replace them
+    /// with atomic propositions.
+    ///
+    /// Returns (f & g1 & g2 & .. & gn) with g1..gn the extracted subformulas.
+    ///
+    /// `extractor` should be a lambda taking the following parameters as input:
+    ///
+    /// - `formula` the formula to process
+    /// - `std::vector<formula>&` the vector that stores extracted subformulas
+    /// - `auto&&` itself, in case it needs to call itself recursively
+    ///   (formula::map for example)
+    /// - `bool` a boolean indicating whether the lambda is currently being
+    ///   called at the formula's "root"
+    /// - `bool` a boolean indicating whether the lambda is currently being
+    ///   called inside a toplevel `and` construct.
+    ///
+    /// Note that the last 2 boolean arguments can be used as you see fit in
+    /// your recursive calls, the first one being set to true in the original
+    /// call, and the second one to false.
+    ///
+    /// `extractor` should return the new rewritten formula.
+    ///
+    /// auto sample_extractor = [](formula f,
+    ///                            std::vector<formula>& extracted,
+    ///                            auto&& extractor,
+    ///                            bool top_level,
+    ///                            bool in_top_level_and) -> formula
+    template<typename Ext>
+    static formula
+    extract(formula f, Ext extractor)
+    {
+      std::vector<formula> extracted;
+      formula new_f = extractor(f, extracted, extractor, true, false);
+      extracted.push_back(new_f);
+      return formula::And(extracted);
+    }
+  }
+
+  std::pair<formula, std::vector<std::string>>
+  suffix_operator_normal_form(formula f, const std::string prefix)
+  {
+    // SONF can only be applied to formulas in negative normal form
+    f = negative_normal_form(f);
+
+    std::unordered_set<std::string> used_aps;
+    std::vector<std::string> added_aps;
+    size_t count = 0;
+
+    // identify all used ap names to avoid them when generating new ones
+    auto ap_indexer = [&used_aps](formula f) noexcept {
+      if (f.is(op::ap))
+        {
+          used_aps.insert(f.ap_name());
+          return true;
+        }
+
+      return false;
+    };
+
+    f.traverse(ap_indexer);
+
+    auto new_ap_name =
+      [&used_aps, &added_aps, &prefix, &count]() noexcept -> std::string
+    {
+      std::string new_name = prefix + std::to_string(count++);
+      while (used_aps.find(new_name) != used_aps.end())
+        new_name = prefix + std::to_string(count++);
+      used_aps.insert(new_name);
+      added_aps.push_back(new_name);
+      return new_name;
+    };
+
+    // extracts the SERE part and replaces it with an atomic proposition,
+    // storing the extracted formula in `extracted` and returning the rewritten
+    // original formula
+    auto sonf_extract = [&](formula f,
+                            std::vector<formula>& extracted,
+                            auto&& extractor,
+                            bool top_level,
+                            bool in_top_level_and) noexcept -> formula
+    {
+      const auto kind = f.kind();
+
+      switch (kind)
+        {
+        case op::G:
+          {
+            // skip if shape is G(!ap | (regex []-> formula)) and at top level
+            if ((top_level || in_top_level_and)
+                && f[0].is(op::Or)     // G(_ | _)
+                && f[0][0].is(op::Not)       // G(!_ | _)
+                && f[0][0][0].is(op::ap)       // G(!ap | _)
+                && f[0][1].is(op::EConcat, op::UConcat)) // G(!ap | (_ []-> _))
+                return f;
+            else
+              return f.map(extractor, extracted, extractor, false, false);
+          }
+        case op::EConcat:
+        case op::UConcat:
+          {
+            // recurse into rhs first (_ []-> rhs)
+            formula rhs =
+              f[1].map(extractor, extracted, extractor, false, false);
+            f = formula::binop(kind, f[0], rhs);
+
+            formula ap = formula::ap(new_ap_name());
+            extracted.push_back(formula::G(formula::Or({formula::Not(ap), f})));
+            return ap;
+          }
+        default:
+          // tracking if we're in a op::And at the formula root
+          in_top_level_and = top_level && f.is(op::And);
+          return f.map(extractor, extracted, extractor,
+                       false, in_top_level_and);
+        }
+    };
+
+    f = extract(f, sonf_extract);
+
+    auto ltl_extract = [&](formula f,
+                           std::vector<formula>& extracted,
+                           auto&& extractor,
+                           [[maybe_unused]]
+                           bool top_level,
+                           [[maybe_unused]]
+                           bool in_top_level_and) noexcept -> formula
+    {
+      switch (f.kind())
+        {
+        case op::EConcat:
+        case op::UConcat:
+          {
+            formula rhs = f[1];
+
+            if (rhs.is(op::ap))
+              return f;
+
+            formula ap = formula::ap(new_ap_name());
+            extracted.push_back(
+              formula::G(formula::Or({formula::Not(ap), rhs})));
+
+            return formula::binop(f.kind(), f[0], ap);
+          }
+        default:
+          return f.map(extractor, extracted, extractor, false, false);
+        }
+    };
+
+    f = extract(f, ltl_extract);
+
+    return {f, added_aps};
+  }
+}

spot/tl/sonf.hh

@@ -0,0 +1,44 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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/>.
+
+#pragma once
+
+#include <string>
+#include <utility>
+#include <vector>
+
+#include <spot/tl/formula.hh>
+
+namespace spot
+{
+  /// \ingroup tl_rewriting
+  /// \brief Helper to rewrite a PSL formula in Suffix Operator Normal Form.
+  ///
+  /// SONF is described in section 4 of \cite cimatti.06.fmcad
+  ///
+  /// The formula output by this function is guaranteed to be in Negative Normal
+  /// Form.
+  ///
+  /// \param f the PSL formula to rewrite
+  /// \param prefix the prefix to use to name newly introduced aps
+  /// \return a pair with the rewritten formula, and a vector containing the
+  ///         names of newly introduced aps
+  SPOT_API std::pair<formula, std::vector<std::string>>
+  suffix_operator_normal_form(formula f, const std::string prefix);
+}

spot/twa/twa.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2013-2021 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011, 2013-2022 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -761,7 +761,7 @@ namespace spot
     void register_aps_from_dict()
     {
       if (!aps_.empty())
-        throw std::runtime_error("register_ap_from_dict() may not be"
+        throw std::runtime_error("register_aps_from_dict() may not be"
                                  " called on an automaton that has already"
                                  " registered some AP");
       auto& m = get_dict()->bdd_map;

tests/Makefile.am

@@ -198,7 +198,8 @@ TESTS_tl = \
   core/stutter-ltl.test \
   core/hierarchy.test \
   core/mempool.test \
-  core/format.test
+  core/format.test \
+  core/sonf.test
 
 TESTS_graph = \
   core/graph.test \
@@ -445,6 +446,7 @@ TESTS_python = \
   python/setxor.py \
   python/simplacc.py \
   python/simstate.py \
+  python/sonf.py \
   python/split.py \
   python/streett_totgba.py \
   python/streett_totgba2.py \

tests/core/bricks.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -21,12 +21,13 @@
 . ./defs
 set -e
 
-seq 0 1999 > expected
+# The seq command is not always available, but we assume awk is.
+$AWK 'BEGIN{for(x=0;x<2000;++x) print x;}' >expected
 
 ../bricks > stdout
 
-cat stdout | head -n 2000 | awk '{print $2}' | sed 's/{//g' | \
-    awk -F',' '{print $1}' | sort -n > map
+cat stdout | head -n 2000 | $AWK '{print $2}' | sed 's/{//g' | \
+    $AWK -F',' '{print $1}' | sort -n > map
 
 diff expected map
 

tests/core/defs.in

@@ -1,5 +1,5 @@
 # -*- mode: shell-script; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2013, 2015 Laboratoire de Recherche
+# Copyright (C) 2009, 2010, 2012, 2013, 2015, 2022 Laboratoire de Recherche
 # et Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -57,6 +57,7 @@ case $srcdir in
   *) srcdir=../$srcdir
 esac
 
+AWK='@AWK@'
 DOT='@DOT@'
 LBTT="@LBTT@"
 LBTT_TRANSLATE="@LBTT_TRANSLATE@"

tests/core/prodchain.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,7 +23,8 @@ set -e
 
 set x
 shift
-for i in `seq 1 42`; do
+for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \
+         22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do
   ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa
 done
 for i in *.hoa; do

tests/core/sonf.test

@@ -0,0 +1,85 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2021 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# 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/>.
+
+. ./defs
+set -e
+
+cat >input <<EOF
+G(c -> Fa) & G(b -> ({x[*]}[]-> c))
+{x[*]}[]-> F({y[*]}<>-> GFz)
+<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17)))
+{{true} || {[*0]}}[]-> (false)
+{{p14} & {{p0}[*]}}[]-> (p11)
+{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18)))))
+X({{true} || {[*0]}}[]-> ((p17) U ((p8) && (p17))))
+({{{p4} || {p5} || {{p16} <-> {{p15} -> {p11}}}}[*]}[]-> (false)) -> (p8)
+{[*1..6]}[]-> ((p9) V ((p9) || (!((p4) && (p19)))))
+X({{{[*0]} || {{{p10};{p14}}[:*2..3]}}[:*]}<>-> (p8))
+{{true} && {{p8}[*]}}<>-> (!(p10))
+<>(!(({{p7}[*1..2]}<>-> (p11)) V ((!(p9)) && ([]((p11) || (X(p10)))))))
+<>({{!{{p5} || {{!{p2}} <-> {p7}}}} & {[*]}}<>-> (p17))
+{{p0} || {{{[*0..2]}[:*2]}[*]}}<>-> ((p1) && (p6))
+EOF
+
+cat >expected <<EOF
+G(!c|Fa)&G(!b|({x[*]}[]-> c))
+s1&G(!s2|GFz)&G(!s0|({y[*]}<>-> s2))&G(!s3|Fs0)&G(!s1|({x[*]}[]-> s3))
+F(s0 R (1 U p17))&G(p9|!p17|!s1)&G(!s0|({p12[*0..3]}[]-> s1))
+s0&G!s1&G(!s0|({1|[*0]}[]-> s1))
+s0&G(!s0|({p14&p0[*]}[]-> p11))
+s0&G(!s1|(p3 R (p3|(X(0)&(p2 R p18)))))&G(!s0|({{!p3|p6}[*]}[]-> s1))
+Xs0&G(!s1|(p17 U (p8&p17)))&G(!s0|({1|[*0]}[]-> s1))
+(p8|s0)&G(!s0|({{p4|p5|{p16 && {p11|!p15}}|{!p11 && p15 && !p16}}[*]}<>-> s1))
+s0&G(!s1|(p9 R (!p4|p9|!p19)))&G(!s0|({[*1..6]}[]-> s1))
+G(!s0|({{[*0]|{p10;p14}[:*2..3]}[:*]}<>-> p8))&Xs0
+s0&G(!p10|!s1)&G(!s0|({1 && p8[*]}<>-> s1))
+F(s0 U (p9|F(!p11&X!p10)))&G(!p11|!s1)&G(!s0|({p7[*1..2]}[]-> s1))
+G(!s0|({{!p5 && {{!p2 && !p7}|{p2 && p7}}}&[*]}<>-> p17))&Fs0
+s0&G(!s1|(p1&p6))&G(!s0|({p0|[*0..2][:*2][*]}<>-> s1))
+EOF
+
+cat >expected-aps <<EOF
+
+s0 s1 s2 s3
+s0 s1
+s0 s1
+s0
+s0 s1
+s0 s1
+s0 s1
+s0 s1
+s0
+s0 s1
+s0 s1
+s0
+s0 s1
+EOF
+
+ltlfilt -F input --sonf=s --sonf-aps=stdout-aps \
+    | sed 's/ \([|&]\) /\1/g' > stdout
+diff expected stdout
+diff expected-aps stdout-aps
+
+# check idempotence
+ltlfilt -F expected --sonf=s --sonf-aps=stdout-aps \
+    | sed 's/ \([|&]\) /\1/g' > stdout
+diff expected stdout
+# should be 14 empty lines, no new aps introduced this time
+test "$(wc -l -m stdout-aps | awk '{print $1 " " $2}')" = "14 14"

tests/python/298.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -20,21 +20,23 @@
 # Test for parts of Issue #298.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a1 = spot.automaton("""genltl --dac=51 | ltl2tgba --med |""")
 a1 = spot.degeneralize_tba(a1)
 r1 = spot.tgba_determinize(a1, True, False, False)
-assert r1.num_sets() == 3
-assert a1.prop_complete().is_false();
+tc.assertEqual(r1.num_sets(), 3)
+tc.assertTrue(a1.prop_complete().is_false())
 # This used to fail in 2.9.5 and earlier.
-assert r1.prop_complete().is_maybe();
-assert spot.is_complete(r1)
+tc.assertTrue(r1.prop_complete().is_maybe())
+tc.assertTrue(spot.is_complete(r1))
 
 a2 = spot.automaton("""genltl --dac=51 | ltl2tgba --high |""")
 a2 = spot.degeneralize_tba(a2)
 r2 = spot.tgba_determinize(a2, True, False, False)
 # This used to fail in 2.9.5 and earlier.
-assert r2.num_sets() == 3
-assert a2.prop_complete().is_false();
-assert r2.prop_complete().is_maybe();
-assert spot.is_complete(r2)
+tc.assertEqual(r2.num_sets(), 3)
+tc.assertTrue(a2.prop_complete().is_false())
+tc.assertTrue(r2.prop_complete().is_maybe())
+tc.assertTrue(spot.is_complete(r2))

tests/python/341.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,7 +19,8 @@
 
 import spot
 from subprocess import _active
-
+from unittest import TestCase
+tc = TestCase()
 
 def two_intersecting_automata():
     """return two random automata with a non-empty intersection"""
@@ -34,4 +35,4 @@ for i in range(5):
 
 n = len(_active)
 print(n, "active processes")
-assert(n == 0)
+tc.assertEqual(n, 0)

tests/python/471.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de l'Epita
 # (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -20,9 +20,12 @@
 # Test for Issue #471.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
+
 a = spot.translate('Fa')
 a = spot.to_generalized_rabin(a, False)
 r1 = a.intersecting_run(a)
 r2 = a.accepting_run()
-assert str(r1) == str(r2)
-assert a.prop_weak().is_true()
+tc.assertEqual(str(r1), str(r2))
+tc.assertTrue(a.prop_weak().is_true())

tests/python/accparse2.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2018  Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2017-2018, 2022  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,99 +18,101 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.acc_cond(5)
 a.set_acceptance(spot.acc_code('parity min odd 5'))
-assert(a.is_parity() == [True, False, True])
+tc.assertEqual(a.is_parity(), [True, False, True])
 a.set_acceptance('parity max even 5')
-assert(a.is_parity() == [True, True, False])
+tc.assertEqual(a.is_parity(), [True, True, False])
 a.set_acceptance('generalized-Buchi 5')
-assert(a.is_parity()[0] == False)
-assert(a.is_parity(True)[0] == False)
+tc.assertEqual(a.is_parity()[0], False)
+tc.assertEqual(a.is_parity(True)[0], False)
 a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')
-assert(a.is_parity()[0] == False)
-assert(a.is_parity(True) == [True, True, False])
+tc.assertEqual(a.is_parity()[0], False)
+tc.assertEqual(a.is_parity(True), [True, True, False])
 
-assert a.maybe_accepting([1, 2, 3], [0, 4]).is_true()
-assert a.maybe_accepting([0], []).is_true()
-assert a.maybe_accepting([0], [3]).is_false()
-assert a.maybe_accepting([0, 3], []).is_maybe()
-assert a.maybe_accepting([2, 3], [3]).is_false()
-assert a.maybe_accepting([2, 3], []).is_maybe()
-assert a.maybe_accepting([2], []).is_true()
-assert a.maybe_accepting([0, 1], []).is_maybe()
-assert a.maybe_accepting([0, 1], [1]).is_false()
+tc.assertTrue(a.maybe_accepting([1, 2, 3], [0, 4]).is_true())
+tc.assertTrue(a.maybe_accepting([0], []).is_true())
+tc.assertTrue(a.maybe_accepting([0], [3]).is_false())
+tc.assertTrue(a.maybe_accepting([0, 3], []).is_maybe())
+tc.assertTrue(a.maybe_accepting([2, 3], [3]).is_false())
+tc.assertTrue(a.maybe_accepting([2, 3], []).is_maybe())
+tc.assertTrue(a.maybe_accepting([2], []).is_true())
+tc.assertTrue(a.maybe_accepting([0, 1], []).is_maybe())
+tc.assertTrue(a.maybe_accepting([0, 1], [1]).is_false())
 
 a.set_acceptance('Fin(0)|Fin(1)')
-assert a.maybe_accepting([0, 1], [1]).is_maybe()
-assert a.maybe_accepting([0, 1], [0, 1]).is_false()
-assert a.maybe_accepting([0], []).is_true()
-assert a.maybe_accepting([], [0]).is_true()
+tc.assertTrue(a.maybe_accepting([0, 1], [1]).is_maybe())
+tc.assertTrue(a.maybe_accepting([0, 1], [0, 1]).is_false())
+tc.assertTrue(a.maybe_accepting([0], []).is_true())
+tc.assertTrue(a.maybe_accepting([], [0]).is_true())
 
 a = spot.acc_cond(0)
 a.set_acceptance('all')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 0)
-assert(a.is_parity() == [True, True, True])
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 0)
+tc.assertEqual(a.is_parity(), [True, True, True])
 a.set_acceptance('none')
-assert(a.is_rabin() == 0)
-assert(a.is_streett() == -1)
-assert(a.is_parity() == [True, True, False])
+tc.assertEqual(a.is_rabin(), 0)
+tc.assertEqual(a.is_streett(), -1)
+tc.assertEqual(a.is_parity(), [True, True, False])
 
 a = spot.acc_cond('(Fin(0)&Inf(1))')
-assert(a.is_rabin() == 1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance('Inf(1)&Fin(0)')
-assert(a.is_rabin() == 1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance('(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 1)
 a.set_acceptance('Inf(1)|Fin(0)')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 1)
 
 a = spot.acc_cond('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))')
-assert(a.is_rabin() == 2)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 2)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))'))
-assert(a.is_rabin() == 2)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 2)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance(spot.acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))'))
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))'))
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance(spot.acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))'))
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))')
-assert(a.is_rabin() == 2)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), 2)
+tc.assertEqual(a.is_streett(), -1)
 
 a.set_acceptance('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 2)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 2)
 a.set_acceptance('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 2)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 2)
 a.set_acceptance('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == -1)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), -1)
 a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))')
-assert(a.is_rabin() == -1)
-assert(a.is_streett() == 2)
+tc.assertEqual(a.is_rabin(), -1)
+tc.assertEqual(a.is_streett(), 2)
 
 a = spot.acc_code('Inf(0)&Inf(1)&Inf(3) | Fin(0)&(Fin(1)|Fin(3))')
 u = a.symmetries()
-assert u[0] == 0
-assert u[1] == 1
-assert u[2] == 2
-assert u[3] == 1
+tc.assertEqual(u[0], 0)
+tc.assertEqual(u[1], 1)
+tc.assertEqual(u[2], 2)
+tc.assertEqual(u[3], 1)

tests/python/aiger.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et
 # Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot, buddy
+from unittest import TestCase
+tc = TestCase()
 
 strats = (("""HOA: v1
 States: 4
@@ -3346,7 +3348,7 @@ for strat_string, (ins_str, outs_str) in strats:
                         print(f"Mode is {m+ss+ddx+uud}")
                         print(f"""Strat is \n{strat_s.to_str("hoa")}""")
                         print(f"""Aig as aut is \n{strat2_s.to_str("hoa")}""")
-                        assert 0
+                        raise AssertionError("not a specialization")
 
 
 # Check stepwise simulation
@@ -3386,7 +3388,7 @@ for (i, e_latch) in zip(ins, exp_latches):
 
 # Variable names
 
-assert(spot.aiger_circuit("""aag 2 2 0 2 0
+tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0
 2
 4
 2
@@ -3394,9 +3396,9 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0
 i0 a
 i1 b c
 c
-""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1')
+""").to_str(), 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1')
 
-assert(spot.aiger_circuit("""aag 2 2 0 2 0
+tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0
 2
 4
 2
@@ -3404,7 +3406,7 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0
 o0 x
 o1 y
 c
-""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y')
+""").to_str(), 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y')
 
 
 def report_missing_exception():
@@ -3415,7 +3417,7 @@ try:
 0
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:1: invalid header line"
+    tc.assertEqual(str(e), "\n<string>:1: invalid header line")
 else:
     report_missing_exception()
 
@@ -3423,14 +3425,15 @@ try:
     spot.aiger_circuit("""aag 2 2 3 2 0
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:1: more variables than indicated by max var"
+    tc.assertEqual(str(e),
+                   "\n<string>:1: more variables than indicated by max var")
 else:
     report_missing_exception()
 
 try:
     spot.aiger_circuit("""aag 2 2 0 2 0\n""")
 except SyntaxError as e:
-    assert str(e) == "\n<string>:2: expecting input number 2"
+    tc.assertEqual(str(e), "\n<string>:2: expecting input number 2")
 else:
     report_missing_exception()
 
@@ -3439,7 +3442,7 @@ try:
 3
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:2: expecting input number 2"
+    tc.assertEqual(str(e), "\n<string>:2: expecting input number 2")
 else:
     report_missing_exception()
 
@@ -3448,7 +3451,7 @@ try:
 3 4 5
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:2: invalid format for an input"
+    tc.assertEqual(str(e), "\n<string>:2: invalid format for an input")
 else:
     report_missing_exception()
 
@@ -3457,7 +3460,7 @@ try:
 2
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:3: expecting input number 4"
+    tc.assertEqual(str(e), "\n<string>:3: expecting input number 4")
 else:
     report_missing_exception()
 
@@ -3468,7 +3471,7 @@ try:
 1
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:4: invalid format for a latch"
+    tc.assertEqual(str(e), "\n<string>:4: invalid format for a latch")
 else:
     report_missing_exception()
 
@@ -3479,7 +3482,7 @@ try:
 1 1
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:4: expecting latch number 6"
+    tc.assertEqual(str(e), "\n<string>:4: expecting latch number 6")
 else:
     report_missing_exception()
 
@@ -3490,7 +3493,7 @@ try:
 6 1
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:5: expecting latch number 8"
+    tc.assertEqual(str(e), "\n<string>:5: expecting latch number 8")
 else:
     report_missing_exception()
 
@@ -3502,7 +3505,7 @@ try:
 8 7
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:6: expecting an output"
+    tc.assertEqual(str(e), "\n<string>:6: expecting an output")
 else:
     report_missing_exception()
 
@@ -3515,7 +3518,7 @@ try:
 9 9 9
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:6: invalid format for an output"
+    tc.assertEqual(str(e), "\n<string>:6: invalid format for an output")
 else:
     report_missing_exception()
 
@@ -3528,7 +3531,7 @@ try:
 9 9 9
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:6: invalid format for an output"
+    tc.assertEqual(str(e), "\n<string>:6: invalid format for an output")
 else:
     report_missing_exception()
 
@@ -3541,7 +3544,7 @@ try:
 9
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:7: expecting AND gate number 10"
+    tc.assertEqual(str(e), "\n<string>:7: expecting AND gate number 10")
 else:
     report_missing_exception()
 
@@ -3555,7 +3558,7 @@ try:
 10 3 8 9
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:7: invalid format for an AND gate"
+    tc.assertEqual(str(e), "\n<string>:7: invalid format for an AND gate")
 else:
     report_missing_exception()
 
@@ -3569,7 +3572,7 @@ try:
 10 3
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:7: invalid format for an AND gate"
+    tc.assertEqual(str(e), "\n<string>:7: invalid format for an AND gate")
 else:
     report_missing_exception()
 
@@ -3583,7 +3586,7 @@ try:
 10 3 8
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:8: expecting AND gate number 12"
+    tc.assertEqual(str(e), "\n<string>:8: expecting AND gate number 12")
 else:
     report_missing_exception()
 
@@ -3599,7 +3602,7 @@ try:
 i0
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:9: could not parse as input name"
+    tc.assertEqual(str(e), "\n<string>:9: could not parse as input name")
 else:
     report_missing_exception()
 
@@ -3616,7 +3619,7 @@ i0 foo
 i3 bar
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:10: value 3 exceeds input count"
+    tc.assertEqual(str(e), "\n<string>:10: value 3 exceeds input count")
 else:
     report_missing_exception()
 
@@ -3633,7 +3636,7 @@ i1 bar
 i0 foo
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:9: expecting name for input 0"
+    tc.assertEqual(str(e), "\n<string>:9: expecting name for input 0")
 else:
     report_missing_exception()
 
@@ -3650,8 +3653,8 @@ i0 name with spaces
 i1 name with spaces
 """)
 except SyntaxError as e:
-    assert str(e) == \
-        "\n<string>:10: name 'name with spaces' already used"
+    tc.assertEqual(str(e), \
+        "\n<string>:10: name 'name with spaces' already used")
 else:
     report_missing_exception()
 
@@ -3669,7 +3672,7 @@ i1 bar
 o0
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:11: could not parse as output name"
+    tc.assertEqual(str(e), "\n<string>:11: could not parse as output name")
 else:
     report_missing_exception()
 
@@ -3689,7 +3692,7 @@ o1 hmm
 o0 foo bar baz
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:12: expecting name for output 0"
+    tc.assertEqual(str(e), "\n<string>:12: expecting name for output 0")
 else:
     report_missing_exception()
 
@@ -3709,7 +3712,7 @@ o0 hmm
 o2 foo bar baz
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:13: value 2 exceeds output count"
+    tc.assertEqual(str(e), "\n<string>:13: value 2 exceeds output count")
 else:
     report_missing_exception()
 
@@ -3729,7 +3732,7 @@ o0 foo
 o1 foo
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:13: name 'foo' already used"
+    tc.assertEqual(str(e), "\n<string>:13: name 'foo' already used")
 else:
     report_missing_exception()
 
@@ -3749,7 +3752,7 @@ o0 foo
 o1 bar
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:13: name 'bar' already used"
+    tc.assertEqual(str(e), "\n<string>:13: name 'bar' already used")
 else:
     report_missing_exception()
 
@@ -3770,7 +3773,7 @@ o1 baz
 this is a bug
 """)
 except SyntaxError as e:
-    assert str(e) == "\n<string>:14: unsupported line type"
+    tc.assertEqual(str(e), "\n<string>:14: unsupported line type")
 else:
     report_missing_exception()
 
@@ -3791,8 +3794,8 @@ c
 this is not a bug
 """)
 except SyntaxError as e:
-    assert str(e) == \
-        "\n<string>:10: either all or none of the inputs should be named"
+    tc.assertEqual(str(e), \
+        "\n<string>:10: either all or none of the inputs should be named")
 else:
     report_missing_exception()
 
@@ -3815,8 +3818,8 @@ c
 this is not a bug
 """)
 except SyntaxError as e:
-    assert str(e) == \
-        "\n<string>:11-12: either all or none of the inputs should be named"
+    tc.assertEqual(str(e), \
+        "\n<string>:11-12: either all or none of the inputs should be named")
 else:
     report_missing_exception()
 
@@ -3841,8 +3844,8 @@ c
 this is not a bug
 """)
 except SyntaxError as e:
-    assert str(e) == \
-        "\n<string>:14-16: either all or none of the outputs should be named"
+    tc.assertEqual(str(e), \
+        "\n<string>:14-16: either all or none of the outputs should be named")
 else:
     report_missing_exception()
 
@@ -3866,4 +3869,4 @@ o2 bar
 c
 this is not a bug
 """).to_str()
-assert x == spot.aiger_circuit(x).to_str()
+tc.assertEqual(x, spot.aiger_circuit(x).to_str())

tests/python/aliases.py

@@ -20,6 +20,8 @@
 # Test for parts of Issue #497.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.automaton("""
 HOA: v1
@@ -63,11 +65,11 @@ State: 0
 --END--""")
 s = aut.to_str('hoa')
 aut2 = spot.automaton(s)
-assert aut.equivalent_to(aut2)
+tc.assertTrue(aut.equivalent_to(aut2))
 s2 = aut.to_str('hoa')
-assert s == s2
+tc.assertEqual(s, s2)
 
-assert s == """HOA: v1
+tc.assertEqual(s, """HOA: v1
 States: 1
 Start: 0
 AP: 3 "x" "y" "z"
@@ -105,7 +107,7 @@ State: 0
 [@a&2 | @p1&@p0&2] 0
 [@a&2] 0
 [@p0&2 | @p1&2] 0
---END--"""
+--END--""")
 
 # Check what happens to aliases when an AP has been removed, but
 # the aliases have been preserved...
@@ -115,7 +117,7 @@ aut3 = rem.strip(aut)
 spot.set_aliases(aut3, spot.get_aliases(aut))
 s2 = aut3.to_str('hoa')
 # Aliases based on "x" should have disappeared.
-assert(s2 == """HOA: v1
+tc.assertEqual(s2, """HOA: v1
 States: 1
 Start: 0
 AP: 2 "y" "z"

tests/python/alternating.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2017, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2016-2017, 2021-2022 Laboratoire de Recherche
+# et Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -20,6 +20,8 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.make_twa_graph(spot._bdd_dict)
 
@@ -38,9 +40,8 @@ aut.new_edge(2, 2, p1 | p2)
 
 tr = [(s, [[x for x in aut.univ_dests(i)] for i in aut.out(s)])
       for s in range(3)]
-print(tr)
-assert [(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])] == tr
-assert not aut.is_existential()
+tc.assertEqual([(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])], tr)
+tc.assertFalse(aut.is_existential())
 
 received = False
 try:
@@ -49,11 +50,10 @@ try:
             pass
 except RuntimeError:
     received = True
-assert received
+tc.assertTrue(received)
 
 h = aut.to_str('hoa')
-print(h)
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "p1" "p2"
@@ -68,22 +68,20 @@ State: 1
 [0&1] 0&2&1
 State: 2
 [0 | 1] 2
---END--"""
+--END--""")
 
 aut2 = spot.automaton(h)
 h2 = aut2.to_str('hoa')
-print(h2)
-assert h != h2
+tc.assertNotEqual(h, h2)
 
 # This will sort destination groups
 aut.merge_univ_dests()
 h = aut.to_str('hoa')
-assert h == h2
+tc.assertEqual(h, h2)
 
 aut2.set_univ_init_state([0, 1])
 h3 = aut2.to_str('hoa')
-print(h3)
-assert h3 == """HOA: v1
+tc.assertEqual(h3, """HOA: v1
 States: 3
 Start: 0&1
 AP: 2 "p1" "p2"
@@ -98,23 +96,22 @@ State: 1
 [0&1] 0&1&2
 State: 2
 [0 | 1] 2
---END--"""
+--END--""")
 
 st = spot.states_and(aut, [0, 2])
 st2 = spot.states_and(aut, [1, st])
 st3 = spot.states_and(aut, [0, 1, 2])
-assert (st, st2, st3) == (3, 4, 5)
+tc.assertEqual((st, st2, st3), (3, 4, 5))
 
 received = False
 try:
     st4 = spot.states_and(aut, [])
 except RuntimeError:
     received = True
-assert received
+tc.assertTrue(received)
 
 h = aut.to_str('hoa')
-print(h)
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 6
 Start: 0
 AP: 2 "p1" "p2"
@@ -136,11 +133,10 @@ State: 4
 [0&1] 0&1&2
 State: 5
 [0&1] 0&1&2
---END--"""
+--END--""")
 
 h = spot.split_edges(aut).to_str('hoa')
-print(h)
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 6
 Start: 0
 AP: 2 "p1" "p2"
@@ -168,7 +164,7 @@ State: 4
 [0&1] 0&1&2
 State: 5
 [0&1] 0&1&2
---END--"""
+--END--""")
 
 
 # remove_univ_otf
@@ -206,11 +202,11 @@ State: 2
 --END--"""
 
 desalt = spot.remove_univ_otf(aut)
-assert(desalt.to_str('hoa') == out)
+tc.assertEqual(desalt.to_str('hoa'), out)
 
-assert aut.num_states() == 3
-assert aut.num_edges() == 3
+tc.assertEqual(aut.num_states(), 3)
+tc.assertEqual(aut.num_edges(), 3)
 aut.edge_storage(3).cond = buddy.bddfalse
 aut.purge_dead_states()
-assert aut.num_states() == 1
-assert aut.num_edges() == 0
+tc.assertEqual(aut.num_states(), 1)
+tc.assertEqual(aut.num_edges(), 0)

tests/python/bdddict.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019, 2021 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2019, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -17,8 +17,8 @@
 # You should have received a copy of the GNU General Public License
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-# Make sure we can leep track of BDD association in Python using bdd_dict, as
-# discussed in issue #372.
+# Make sure we can keep track of BDD association in Python using bdd_dict, as
+# discussed in (deleted???) issue #372.
 
 # CPython use reference counting, so that automata are destructed
 # when we expect them to be.   However other implementations like
@@ -33,6 +33,8 @@ else:
         gc.collect()
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 
 class bdd_holder:
@@ -64,7 +66,7 @@ class bdd_holder3:
 
 
 def check_ok():
-    assert type(bdict.varnum(spot.formula.ap("a"))) is int
+    tc.assertIs(type(bdict.varnum(spot.formula.ap("a"))), int)
 
 
 def check_nok():
@@ -123,7 +125,7 @@ debug("h2")
 h3 = bdd_holder3(h2)
 var = bdict.register_anonymous_variables(1, h3)
 debug("h3")
-assert var == 2
+tc.assertEqual(var, 2)
 del h2
 gcollect()
 debug("-h2")

tests/python/bdditer.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -24,11 +24,13 @@
 import spot
 import buddy
 import sys
+from unittest import TestCase
+tc = TestCase()
 
 run = spot.translate('a & !b').accepting_run()
 b = run.prefix[0].label
 c = buddy.bdd_satone(b)
-assert c != buddy.bddfalse
+tc.assertNotEqual(c, buddy.bddfalse)
 res = []
 while c != buddy.bddtrue:
     var = buddy.bdd_var(c)
@@ -40,23 +42,23 @@ while c != buddy.bddtrue:
         res.append(var)
         c = h
 
-assert res == [0, -1]
+tc.assertEqual(res, [0, -1])
 
 res2 = []
 for i in run.aut.ap():
     res2.append((str(i), run.aut.register_ap(i)))
-assert str(res2) == "[('a', 0), ('b', 1)]"
+tc.assertEqual(str(res2), "[('a', 0), ('b', 1)]")
 
 
 f = spot.bdd_to_formula(b)
-assert f._is(spot.op_And)
-assert f[0]._is(spot.op_ap)
-assert f[1]._is(spot.op_Not)
-assert f[1][0]._is(spot.op_ap)
-assert str(f) == 'a & !b'
+tc.assertTrue(f._is(spot.op_And))
+tc.assertTrue(f[0]._is(spot.op_ap))
+tc.assertTrue(f[1]._is(spot.op_Not))
+tc.assertTrue(f[1][0]._is(spot.op_ap))
+tc.assertEqual(str(f), 'a & !b')
 
 try:
     f = spot.bdd_to_formula(b, spot.make_bdd_dict())
     sys.exit(2)
 except RuntimeError as e:
-    assert "not in the dictionary" in str(e)
+    tc.assertIn("not in the dictionary", str(e))

tests/python/bugdet.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement
+# de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,6 +22,8 @@
 # sent to the Spot mailing list on 2016-10-31.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.automaton("""
 HOA: v1
@@ -80,12 +82,12 @@ State: 7 {0}
 # was fine.
 print("use_simulation=True")
 b1 = spot.tgba_determinize(b, False, True, True, True)
-assert b1.num_states() == 5
+tc.assertEqual(b1.num_states(), 5)
 b1 = spot.remove_fin(spot.dualize(b1))
-assert not a.intersects(b1)
+tc.assertFalse(a.intersects(b1))
 
 print("\nuse_simulation=False")
 b2 = spot.tgba_determinize(b, False, True, False, True)
-assert b2.num_states() == 5
+tc.assertEqual(b2.num_states(), 5)
 b2 = spot.remove_fin(spot.dualize(b2))
-assert not a.intersects(b2)
+tc.assertFalse(a.intersects(b2))

tests/python/complement_semidet.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
 
 
 def complement(aut):
@@ -35,4 +37,4 @@ for aut in spot.automata(
 
     comp = complement(aut)
     semidet_comp = spot.complement_semidet(aut, True)
-    assert(comp.equivalent_to(semidet_comp))
+    tc.assertTrue(comp.equivalent_to(semidet_comp))

tests/python/declenv.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -21,6 +21,8 @@
 # This file tests various error conditions on the twa API
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 env = spot.declarative_environment()
 env.declare("a")
@@ -28,26 +30,27 @@ env.declare("b")
 
 f1a = spot.parse_infix_psl("a U b")
 f1b = spot.parse_infix_psl("a U b", env)
-assert not f1a.errors
-assert not f1b.errors
+tc.assertFalse(f1a.errors)
+tc.assertFalse(f1b.errors)
+
 # In the past, atomic propositions requires via different environments were
 # never equal, but this feature was never used and we changed that in Spot 2.0
 # for the sake of simplicity.
-assert f1a.f == f1b.f
+tc.assertEqual(f1a.f, f1b.f)
 
 f2 = spot.parse_infix_psl("(a U b) U c", env)
-assert f2.errors
+tc.assertTrue(f2.errors)
 ostr = spot.ostringstream()
 f2.format_errors(ostr)
 err = ostr.str()
-assert "unknown atomic proposition `c'" in err
+tc.assertIn("unknown atomic proposition `c'", err)
 
 f3 = spot.parse_prefix_ltl("R a d", env)
-assert f3.errors
+tc.assertTrue(f3.errors)
 ostr = spot.ostringstream()
 f3.format_errors(ostr)
 err = ostr.str()
-assert "unknown atomic proposition `d'" in err
+tc.assertIn("unknown atomic proposition `d'", err)
 
 f4 = spot.parse_prefix_ltl("R a b", env)
-assert not f4.errors
+tc.assertFalse(f4.errors)

tests/python/decompose_scc.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et
 # Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.translate('(Ga -> Gb) W c')
 si = spot.scc_info(aut)
@@ -26,10 +28,10 @@ si = spot.scc_info(aut)
 # if the generation of the automaton changes, so just scan
 # for it.
 rej = [j for j in range(si.scc_count()) if si.is_rejecting_scc(j)]
-assert len(rej) == 1
+tc.assertEqual(len(rej), 1)
 s = spot.decompose_scc(si, rej[0]).to_str('hoa', '1.1')
 
-assert (s == """HOA: v1.1
+tc.assertEqual(s, """HOA: v1.1
 States: 3
 Start: 0
 AP: 3 "b" "a" "c"
@@ -56,7 +58,8 @@ except RuntimeError:
 else:
     raise AssertionError
 
-assert (spot.decompose_scc(si, 0, True).to_str('hoa', '1.1') == """HOA: v1.1
+tc.assertEqual(spot.decompose_scc(si, 0, True).to_str('hoa', '1.1'),
+"""HOA: v1.1
 States: 4
 Start: 0
 AP: 3 "b" "a" "c"
@@ -81,7 +84,8 @@ State: 3
 [1] 3
 --END--""")
 
-assert (spot.decompose_scc(si, 2, True).to_str('hoa', '1.1') == """HOA: v1.1
+tc.assertEqual(spot.decompose_scc(si, 2, True).to_str('hoa', '1.1'),
+"""HOA: v1.1
 States: 2
 Start: 0
 AP: 3 "b" "a" "c"
@@ -103,4 +107,4 @@ try:
 except RuntimeError:
     pass
 else:
-    raise AssertionError
+    raise AssertionError("missing exception")

tests/python/det.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.translate('FGa | FGb')
 
@@ -26,10 +28,10 @@ a = spot.translate('FGa | FGb')
 d = spot.tgba_determinize(a, False, True, True, True,
                           None, -1, True)
 cld = list(d.get_original_classes())
-assert [0, 1, 2, 3, 3] == cld
+tc.assertEqual([0, 1, 2, 3, 3], cld)
 
 e = spot.sbacc(d)
-assert e.get_original_states() is None
+tc.assertIsNone(e.get_original_states())
 cle = list(e.get_original_classes())
-assert len(cle) == e.num_states()
-assert set(cle) == set(cld)
+tc.assertEqual(len(cle), e.num_states())
+tc.assertEqual(set(cle), set(cld))

tests/python/dualize.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -20,6 +20,8 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
 
 match_strings = [('is_buchi', 'is_co_buchi'),
                  ('is_generalized_buchi', 'is_generalized_co_buchi'),
@@ -79,19 +81,19 @@ def test_aut(aut, d=None):
 
 
 def test_complement(aut):
-    assert aut.is_deterministic()
+    tc.assertTrue(aut.is_deterministic())
     d = spot.dualize(aut)
     s = spot.product_or(aut, d)
-    assert spot.dualize(s).is_empty()
+    tc.assertTrue(spot.dualize(s).is_empty())
 
 
 def test_assert(a, d=None):
     t = test_aut(a, d)
     if not t[0]:
-        print (t[1])
-        print (a.to_str('hoa'))
-        print (spot.dualize(a).to_str('hoa'))
-        assert False
+        print(t[1])
+        print(a.to_str('hoa'))
+        print(spot.dualize(a).to_str('hoa'))
+    tc.assertTrue(t[0])
 
 
 aut = spot.translate('a')
@@ -101,7 +103,7 @@ test_assert(aut)
 dual = spot.dualize(aut)
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 3
 Start: 1
 AP: 1 "a"
@@ -117,7 +119,7 @@ State: 1
 [!0] 2
 State: 2
 [t] 2
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -141,7 +143,7 @@ test_assert(aut)
 dual = spot.dualize(aut)
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 4
 Start: 0
 AP: 2 "a" "b"
@@ -161,7 +163,7 @@ State: 2 {0}
 [!1] 3
 State: 3
 [t] 3
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -186,7 +188,7 @@ test_assert(aut)
 dual = spot.dualize(aut)
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 2
 Start: 1
 AP: 2 "a" "b"
@@ -198,7 +200,7 @@ State: 0
 [t] 0
 State: 1
 [!0 | !1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -219,10 +221,10 @@ State: 3 {1}
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 2
 Start: 1
 AP: 2 "a" "b"
@@ -234,7 +236,7 @@ State: 0
 [t] 0
 State: 1
 [!0 | !1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -255,10 +257,10 @@ State: 3 {0}
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 5
 Start: 0
 AP: 2 "a" "b"
@@ -280,7 +282,7 @@ State: 3 {0}
 [t] 3
 State: 4
 [t] 4
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -302,10 +304,10 @@ State: 2
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 4
 Start: 0
 AP: 2 "a" "b"
@@ -327,7 +329,7 @@ State: 2
 [!0&!1] 0&2
 State: 3
 [t] 3
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -348,10 +350,10 @@ State: 2
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
@@ -362,7 +364,7 @@ properties: deterministic terminal
 --BODY--
 State: 0
 [t] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -382,10 +384,10 @@ State: 2
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
@@ -396,7 +398,7 @@ properties: deterministic terminal
 --BODY--
 State: 0
 [t] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -419,7 +421,7 @@ State: 2
 dual = spot.dualize(aut)
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -435,7 +437,7 @@ State: 1 {0}
 [t] 1
 State: 2
 [t] 2
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -456,10 +458,10 @@ State: 2
 
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 2
 Start: 0
 AP: 1 "a"
@@ -471,7 +473,7 @@ State: 0
 [!0] 1
 State: 1 {0}
 [t] 1
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -495,10 +497,10 @@ State: 3 {0}
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 3
 Start: 0
 AP: 1 "a"
@@ -515,7 +517,7 @@ State: 1
 [0] 2
 State: 2 {0}
 [t] 2
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -536,10 +538,10 @@ State: 2
 --END--""")
 
 dual = spot.dualize(aut)
-assert dualtype(aut, dual)
+tc.assertTrue(dualtype(aut, dual))
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 3
 Start: 0
 AP: 1 "a"
@@ -555,14 +557,14 @@ State: 1 {0}
 [t] 0
 State: 2 {1}
 [t] 0
---END--"""
+--END--""")
 
 aut = spot.translate('G!a R XFb')
 test_assert(aut)
 dual = spot.dualize(aut)
 h = dual.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 5
 Start: 0
 AP: 2 "a" "b"
@@ -589,7 +591,7 @@ State: 3 {0}
 [0] 4
 State: 4
 [t] 4
---END--"""
+--END--""")
 
 opts = spot.option_map()
 opts.set('output', spot.randltlgenerator.LTL)

tests/python/ecfalse.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 
 import spot
 from buddy import bddfalse, bddtrue
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.automaton("""
 HOA: v1
@@ -43,8 +45,8 @@ for e in a.out(1):
     if e.dst == 0:
         e.cond = bddfalse
 
-assert a.accepting_run() is None
-assert a.is_empty()
+tc.assertIsNone(a.accepting_run())
+tc.assertTrue(a.is_empty())
 
 for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']:
     print(name)
@@ -52,13 +54,13 @@ for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']:
     res = ec.check()
     if res is not None:
         print(res.accepting_run())
-    assert res is None
+    tc.assertIsNone(res)
 
 si = spot.scc_info(a)
-assert si.scc_count() == 1 # only one accessible SCC
+tc.assertEqual(si.scc_count(), 1) # only one accessible SCC
 a.set_init_state(0)
 si = spot.scc_info(a)
-assert si.scc_count() == 2
+tc.assertEqual(si.scc_count(), 2)
 
 a = spot.automaton("""HOA: v1 States: 11 Start: 0 AP: 2 "a" "b" Acceptance: 8
 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & ((Fin(4) & Inf(5)) | (Fin(6) & Inf(7)))
@@ -71,16 +73,16 @@ State: 5 State: 6 State: 7 [!0&!1] 1 {4 6 7} [!0&!1] 2 {5 6} State: 8 [!0&!1] 2
 {4} State: 9 [!0&!1] 2 {0 4} [!0&!1] 4 {3 4} State: 10 --END-- """)
 
 r = a.accepting_run()
-assert r is not None
-assert r.replay(spot.get_cout())
+tc.assertIsNotNone(r)
+tc.assertTrue(r.replay(spot.get_cout()))
 for e in a.out(7):
     if e.dst == 2:
         e.cond = bddfalse
 s = a.accepting_run()
-assert s is not None
-assert s.replay(spot.get_cout())
+tc.assertIsNotNone(s)
+tc.assertTrue(s.replay(spot.get_cout()))
 for e in a.out(2):
     if e.dst == 1:
         e.cond = bddfalse
 s = a.accepting_run()
-assert s is None
+tc.assertIsNone(s)

tests/python/except.py

@@ -24,6 +24,8 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
 
 
 def report_missing_exception():
@@ -35,7 +37,7 @@ aut.set_acceptance(spot.acc_cond("parity min even 4"))
 try:
     spot.iar(aut)
 except RuntimeError as e:
-    assert 'iar() expects Rabin-like or Streett-like input' in str(e)
+    tc.assertIn('iar() expects Rabin-like or Streett-like input', str(e))
 else:
     report_missing_exception()
 
@@ -43,7 +45,7 @@ alt = spot.dualize(spot.translate('FGa | FGb'))
 try:
     spot.tgba_determinize(alt)
 except RuntimeError as e:
-    assert 'tgba_determinize() does not support alternation' in str(e)
+    tc.assertIn('tgba_determinize() does not support alternation', str(e))
 else:
     report_missing_exception()
 
@@ -52,18 +54,18 @@ aps = aut.ap()
 rem = spot.remove_ap()
 rem.add_ap('"a"=0,b')
 aut = rem.strip(aut)
-assert aut.ap() == aps[2:]
+tc.assertEqual(aut.ap(), aps[2:])
 try:
     rem.add_ap('"a=0,b')
 except ValueError as e:
-    assert """missing closing '"'""" in str(e)
+    tc.assertIn("""missing closing '"'""", str(e))
 else:
     report_missing_exception()
 
 try:
     rem.add_ap('a=0=b')
 except ValueError as e:
-    assert """unexpected '=' at position 3""" in str(e)
+    tc.assertIn("""unexpected '=' at position 3""", str(e))
 else:
     report_missing_exception()
 
@@ -73,7 +75,7 @@ for meth in ('scc_has_rejecting_cycle', 'is_inherently_weak_scc',
     try:
         getattr(spot, meth)(si, 20)
     except ValueError as e:
-        assert "invalid SCC number" in str(e)
+        tc.assertIn("invalid SCC number", str(e))
     else:
         report_missing_exception()
 
@@ -89,14 +91,15 @@ si = spot.scc_info(alt)
 try:
     si.determine_unknown_acceptance()
 except RuntimeError as e:
-    assert "scc_info::determine_unknown_acceptance() does not supp" in str(e)
+    tc.assertIn("scc_info::determine_unknown_acceptance() does not supp",
+                str(e))
 else:
     report_missing_exception()
 
 try:
     alt.set_init_state(999)
 except ValueError as e:
-    assert "set_init_state()" in str(e)
+    tc.assertIn("set_init_state()", str(e))
 else:
     report_missing_exception()
 
@@ -107,7 +110,7 @@ alt.set_init_state(u)
 try:
     alt.set_init_state(u - 1)
 except ValueError as e:
-    assert "set_init_state()" in str(e)
+    tc.assertIn("set_init_state()", str(e))
 else:
     report_missing_exception()
 
@@ -116,21 +119,21 @@ r = spot.twa_run(aut)
 try:
     a = r.as_twa()
 except RuntimeError as e:
-    assert "empty cycle" in str(e)
+    tc.assertIn("empty cycle", str(e))
 else:
     report_missing_exception()
 
 try:
     a = r.replay(spot.get_cout())
 except RuntimeError as e:
-    assert "empty cycle" in str(e)
+    tc.assertIn("empty cycle", str(e))
 else:
     report_missing_exception()
 
 try:
     a = r.reduce()
 except RuntimeError as e:
-    assert "empty cycle" in str(e)
+    tc.assertIn("empty cycle", str(e))
 else:
     report_missing_exception()
 
@@ -138,12 +141,12 @@ a = spot.translate('Fa')
 a = spot.to_generalized_rabin(a, False)
 r = a.accepting_run()
 r = r.reduce()
-assert r.cycle[0].acc == spot.mark_t([1])
+tc.assertEqual(r.cycle[0].acc, spot.mark_t([1]))
 r.cycle[0].acc = spot.mark_t([0])
 try:
     r.reduce();
 except RuntimeError as e:
-    assert "expects an accepting cycle" in str(e)
+    tc.assertIn("expects an accepting cycle", str(e))
 else:
     report_missing_exception()
 
@@ -151,7 +154,7 @@ f = spot.formula('GF(a | Gb)')
 try:
     spot.gf_guarantee_to_ba(f, spot._bdd_dict)
 except RuntimeError as e:
-    assert "guarantee" in str(e)
+    tc.assertIn("guarantee", str(e))
 else:
     report_missing_exception()
 
@@ -159,7 +162,7 @@ f = spot.formula('FG(a | Fb)')
 try:
     spot.fg_safety_to_dca(f, spot._bdd_dict)
 except RuntimeError as e:
-    assert "safety" in str(e)
+    tc.assertIn("safety", str(e))
 else:
     report_missing_exception()
 
@@ -168,28 +171,28 @@ m = spot.mark_t([n - 1])
 try:
     m = spot.mark_t([0]) << n
 except RuntimeError as e:
-    assert "Too many acceptance sets" in str(e)
+    tc.assertIn("Too many acceptance sets", str(e))
 else:
     report_missing_exception()
 
 try:
     m.set(n)
 except RuntimeError as e:
-    assert "bit index is out of bounds" in str(e)
+    tc.assertIn("bit index is out of bounds", str(e))
 else:
     report_missing_exception()
 
 try:
     m = spot.mark_t([0, n, 1])
 except RuntimeError as e:
-    assert "Too many acceptance sets used.  The limit is" in str(e)
+    tc.assertIn("Too many acceptance sets used.  The limit is", str(e))
 else:
     report_missing_exception()
 
 try:
     spot.complement_semidet(spot.translate('Gb R a', 'ba'))
 except RuntimeError as e:
-    assert "requires a semi-deterministic input" in str(e)
+    tc.assertIn("requires a semi-deterministic input", str(e))
 else:
     report_missing_exception()
 
@@ -197,52 +200,55 @@ try:
     spot.translate('F(G(a | !a) & ((b <-> c) W d))', 'det', 'any')
 except ValueError as e:
     s = str(e)
-    assert 'det' in s
-    assert 'any' in s
+    tc.assertIn('det', s)
+    tc.assertIn('any', s)
 else:
     report_missing_exception()
 
 a1 = spot.translate('FGa')
 a2 = spot.translate('Gb')
-assert not spot.is_deterministic(a1)
-assert spot.is_deterministic(a2)
+tc.assertFalse(spot.is_deterministic(a1))
+tc.assertTrue(spot.is_deterministic(a2))
 try:
     spot.product_xor(a1, a2)
 except RuntimeError as e:
-    assert "product_xor() only works with deterministic automata" in str(e)
+    tc.assertIn("product_xor() only works with deterministic automata", str(e))
 else:
     report_missing_exception()
 try:
     spot.product_xor(a2, a1)
 except RuntimeError as e:
-    assert "product_xor() only works with deterministic automata" in str(e)
+    tc.assertIn("product_xor() only works with deterministic automata", str(e))
 else:
     report_missing_exception()
 try:
     spot.product_xnor(a1, a2)
 except RuntimeError as e:
-    assert "product_xnor() only works with deterministic automata" in str(e)
+    tc.assertIn("product_xnor() only works with deterministic automata", str(e))
 else:
     report_missing_exception()
 try:
     spot.product_xnor(a2, a1)
 except RuntimeError as e:
-    assert "product_xnor() only works with deterministic automata" in str(e)
+    tc.assertIn("product_xnor() only works with deterministic automata", str(e))
 else:
     report_missing_exception()
 
 try:
     spot.solve_safety_game(a1)
 except RuntimeError as e:
-    assert "solve_safety_game(): arena should have true acceptance" in str(e)
+    tc.assertIn(
+        "solve_safety_game(): arena should have true acceptance",
+        str(e))
 else:
     report_missing_exception()
 
 try:
     spot.solve_parity_game(a1)
 except RuntimeError as e:
-    assert "solve_parity_game(): arena must have max-odd acceptance condition" \
-        in str(e)
+    tc.assertIn(
+        "solve_parity_game(): arena must have max-odd acceptance condition",
+        str(e))
 else:
     report_missing_exception()
 
@@ -250,16 +256,16 @@ else:
 try:
     spot.formula_Star(spot.formula("a"), 10, 333)
 except OverflowError as e:
-    assert "333" in str(e)
-    assert "254" in str(e)
+    tc.assertIn("333", str(e))
+    tc.assertIn("254", str(e))
 else:
     report_missing_exception()
 
 try:
     spot.formula_FStar(spot.formula("a"), 333, 400)
 except OverflowError as e:
-    assert "333" in str(e)
-    assert "254" in str(e)
+    tc.assertIn("333", str(e))
+    tc.assertIn("254", str(e))
 else:
     report_missing_exception()
 
@@ -267,15 +273,15 @@ try:
     spot.formula_nested_unop_range(spot.op_F, spot.op_Or, 333, 400,
                                    spot.formula("a"))
 except OverflowError as e:
-    assert "333" in str(e)
-    assert "254" in str(e)
+    tc.assertIn("333", str(e))
+    tc.assertIn("254", str(e))
 else:
     report_missing_exception()
 
 try:
     spot.formula_FStar(spot.formula("a"), 50, 40)
 except OverflowError as e:
-    assert "reversed" in str(e)
+    tc.assertIn("reversed", str(e))
 else:
     report_missing_exception()
 
@@ -287,5 +293,41 @@ try:
     a.to_str()
 except RuntimeError as e:
     se = str(e)
-    assert "synthesis-outputs" in se
-    assert "unregistered proposition" in se
+    tc.assertIn("synthesis-outputs", se)
+    tc.assertIn("unregistered proposition", se)
+else:
+    report_missing_exception()
+
+
+a = spot.make_twa_graph()
+s = a.new_state()
+b = spot.formula_to_bdd("a & b", a.get_dict(), a)
+a.new_edge(s, s, b, [])
+try:
+    print(a.to_str('hoa'))
+except RuntimeError as e:
+    tc.assertIn("unregistered atomic propositions", str(e))
+else:
+    report_missing_exception()
+
+a.register_aps_from_dict()
+tc.assertEqual(a.to_str('hoa'), """HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0&1] 0
+--END--""")
+
+try:
+    a.register_aps_from_dict()
+except RuntimeError as e:
+    se = str(e)
+    tc.assertIn("register_aps_from_dict", se)
+    tc.assertIn("already registered", se)
+else:
+    report_missing_exception()

tests/python/formulas.ipynb

@@ -976,6 +976,62 @@
     "print(ap)        # print as a string\n",
     "display(ap)      # LaTeX-style, for notebooks"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Converting to Suffix Operator Normal Form:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/latex": [
+       "$\\mathsf{G} (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{F} a)$"
+      ],
+      "text/plain": [
+       "spot.formula(\"G({x[*]}[]-> Fa)\")"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/latex": [
+       "$\\mathsf{G} \\mathit{sonf\\_}_{0} \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathit{sonf\\_}_{1}))$"
+      ],
+      "text/plain": [
+       "spot.formula(\"Gsonf_0 & G(!sonf_1 | Fa) & G(!sonf_0 | ({x[*]}[]-> sonf_1))\")"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "('sonf_0', 'sonf_1')"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "f = spot.formula('G({x*} []-> Fa)')\n",
+    "display(f)\n",
+    "\n",
+    "# In addition to the formula, returns a list of newly introduced APs\n",
+    "f, aps = spot.suffix_operator_normal_form(f, 'sonf_')\n",
+    "display(f)\n",
+    "display(aps)"
+   ]
   }
  ],
  "metadata": {

tests/python/game.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 g = spot.automaton("""HOA: v1 States: 9 Start: 0 AP: 2 "a" "b"
 acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) properties:
@@ -27,10 +29,10 @@ trans-labels explicit-labels state-acc spot-state-player: 0 1 0 1 0 1
 {1} [0] 8 State: 3 {1} [1] 4 State: 4 {1} [0] 5 State: 5 {1} [0] 6
 State: 6 {1} [1] 7 State: 7 State: 8 {1} [0] 2 --END--""")
 
-assert spot.solve_parity_game(g) == False
+tc.assertFalse(spot.solve_parity_game(g))
 
 s = spot.highlight_strategy(g).to_str("HOA", "1.1")
-assert s == """HOA: v1.1
+tc.assertEqual(s, """HOA: v1.1
 States: 9
 Start: 0
 AP: 2 "a" "b"
@@ -60,4 +62,4 @@ State: 6 {1}
 State: 7
 State: 8 {1}
 [0] 2
---END--"""
+--END--""")

tests/python/gen.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,63 +23,66 @@
 
 import spot.gen as gen
 from sys import exit
+from unittest import TestCase
+tc = TestCase()
 
 k2 = gen.aut_pattern(gen.AUT_KS_NCA, 2)
-assert k2.prop_state_acc()
-assert k2.num_states() == 5
-assert k2.prop_universal().is_false()
-assert k2.prop_inherently_weak().is_false()
-assert k2.prop_stutter_invariant().is_false()
-assert k2.prop_semi_deterministic().is_false()
-assert k2.prop_deterministic().is_false()
-assert k2.prop_terminal().is_false()
+tc.assertTrue(k2.prop_state_acc())
+tc.assertEqual(k2.num_states(), 5)
+tc.assertTrue(k2.prop_universal().is_false())
+tc.assertTrue(k2.prop_inherently_weak().is_false())
+tc.assertTrue(k2.prop_stutter_invariant().is_false())
+tc.assertTrue(k2.prop_semi_deterministic().is_false())
+tc.assertTrue(k2.prop_deterministic().is_false())
+tc.assertTrue(k2.prop_terminal().is_false())
 
 # to_str is defined in the spot package, so this makes sure
 # the type returned by spot.gen.ks_nca() is the correct one.
-assert 'to_str' in dir(k2)
+tc.assertIn('to_str', dir(k2))
 
 k3 = gen.aut_pattern(gen.AUT_L_NBA, 3)
-assert k3.num_states() == 10
-assert k3.prop_state_acc()
-assert k3.prop_universal().is_false()
-assert k3.prop_inherently_weak().is_false()
-assert k3.prop_stutter_invariant().is_false()
-assert k3.prop_semi_deterministic().is_false()
-assert k3.prop_deterministic().is_false()
-assert k3.prop_terminal().is_false()
+tc.assertEqual(k3.num_states(), 10)
+tc.assertTrue(k3.prop_state_acc())
+tc.assertTrue(k3.prop_universal().is_false())
+tc.assertTrue(k3.prop_inherently_weak().is_false())
+tc.assertTrue(k3.prop_stutter_invariant().is_false())
+tc.assertTrue(k3.prop_semi_deterministic().is_false())
+tc.assertTrue(k3.prop_deterministic().is_false())
+tc.assertTrue(k3.prop_terminal().is_false())
 
-assert k2.get_dict() == k3.get_dict()
+tc.assertEqual(k2.get_dict(), k3.get_dict())
 
 try:
     gen.aut_pattern(gen.AUT_KS_NCA, 0)
 except RuntimeError as e:
-    assert 'positive argument' in str(e)
+    tc.assertIn('positive argument', str(e))
 else:
     exit(2)
 
 f = gen.ltl_pattern(gen.LTL_AND_F, 3)
-assert f.size() == 3
-assert gen.ltl_pattern_name(gen.LTL_AND_F) == "and-f"
+tc.assertEqual(f.size(), 3)
+tc.assertEqual(gen.ltl_pattern_name(gen.LTL_AND_F), "and-f")
 
 try:
     gen.ltl_pattern(1000, 3)
 except RuntimeError as e:
-    assert 'unsupported pattern' in str(e)
+    tc.assertIn('unsupported pattern', str(e))
 else:
     exit(2)
 
 try:
     gen.ltl_pattern(gen.LTL_OR_G, -10)
 except RuntimeError as e:
-    assert 'or-g' in str(e)
-    assert 'positive' in str(e)
+    tc.assertIn('or-g', str(e))
+    tc.assertIn('positive', str(e))
 else:
     exit(2)
 
-assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5),
-                                                    (gen.LTL_GH_Q, 3),
-                                                    gen.LTL_EH_PATTERNS))
+tc.assertEqual(40, sum(p.size()
+                       for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5),
+                                                 (gen.LTL_GH_Q, 3),
+                                                 gen.LTL_EH_PATTERNS)))
 
-assert 32 == sum(p.num_states()
-                 for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3),
-                                           (gen.AUT_KS_NCA, 5)))
+tc.assertEqual(32, sum(p.num_states()
+                       for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3),
+                                                 (gen.AUT_KS_NCA, 5))))

tests/python/genem.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,6 +22,8 @@
 # are usable with methods from the spot package.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a1 = spot.automaton('''
 HOA: v1  name: "aut"  States: 4  Start: 0  AP: 0
@@ -179,7 +181,7 @@ def generic_emptiness2_rec(aut):
                 # Find some Fin set, we necessarily have one, otherwise the SCC
                 # would have been found to be either rejecting or accepting.
                 fo = acc.fin_one()
-                assert fo >= 0, acc
+                tc.assertTrue(fo >= 0, acc)
                 for part in si.split_on_sets(scc, [fo]):
                     if not generic_emptiness2(part):
                         return False
@@ -309,10 +311,10 @@ def run_bench(automata):
                + str(res3b)[0] + str(res3c)[0] + str(res3d)[0]
                + str(res4)[0] + str(res5)[0])
         print(res)
-        assert res in ('TTTTTTTT', 'FFFFFFFF')
+        tc.assertIn(res, ('TTTTTTTT', 'FFFFFFFF'))
         if res == 'FFFFFFFF':
             run3 = spot.generic_accepting_run(aut)
-            assert run3.replay(spot.get_cout()) is True
+            tc.assertTrue(run3.replay(spot.get_cout()))
 
 
 run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360, act])

tests/python/implies.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2022 Laboratoire de Recherche et Développement
 # de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
 
 import sys
 from buddy import *
+from unittest import TestCase
+tc = TestCase()
 
 bdd_init(10000, 10000)
 bdd_setvarnum(5)
@@ -33,26 +35,26 @@ e = V[1] & V[2] & -V[3] & V[4]
 f = V[0] & -V[3] & V[4]
 g = -V[0] | V[1]
 
-assert(bdd_implies(b, a))
-assert(not bdd_implies(a, b))
-assert(not bdd_implies(c, a))
-assert(bdd_implies(a, d))
-assert(bdd_implies(b, d))
-assert(bdd_implies(c, d))
-assert(bdd_implies(d, d))
-assert(not bdd_implies(e, d))
-assert(not bdd_implies(d, e))
-assert(not bdd_implies(f, e))
-assert(not bdd_implies(e, f))
-assert(bdd_implies(bddfalse, f))
-assert(not bdd_implies(bddtrue, f))
-assert(bdd_implies(f, bddtrue))
-assert(not bdd_implies(f, bddfalse))
-assert(bdd_implies(a, g))
+tc.assertTrue(bdd_implies(b, a))
+tc.assertFalse(bdd_implies(a, b))
+tc.assertFalse(bdd_implies(c, a))
+tc.assertTrue(bdd_implies(a, d))
+tc.assertTrue(bdd_implies(b, d))
+tc.assertTrue(bdd_implies(c, d))
+tc.assertTrue(bdd_implies(d, d))
+tc.assertFalse(bdd_implies(e, d))
+tc.assertFalse(bdd_implies(d, e))
+tc.assertFalse(bdd_implies(f, e))
+tc.assertFalse(bdd_implies(e, f))
+tc.assertTrue(bdd_implies(bddfalse, f))
+tc.assertFalse(bdd_implies(bddtrue, f))
+tc.assertTrue(bdd_implies(f, bddtrue))
+tc.assertFalse(bdd_implies(f, bddfalse))
+tc.assertTrue(bdd_implies(a, g))
 
 a = (-V[2] & (-V[1] | V[0])) | (-V[0] & V[1] & V[2])
 b = V[1] | -V[2]
-assert(bdd_implies(a, b))
+tc.assertTrue(bdd_implies(a, b))
 
 # Cleanup all BDD variables before calling bdd_done(), otherwise
 # bdd_delref will be called after bdd_done() and this is unsafe in

tests/python/intrun.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 # This issue was reported by Florian Renkin.  The reduce() call used in
 # intersecting_run() was bogus, and could incorrectly reduce a word
@@ -34,5 +36,5 @@ trans-labels explicit-labels trans-acc complete properties: deterministic
 State: 3 [t] 1 {1 2} State: 4 [!0&1] 4 {2} [!0&!1] 3 {2} [0] 2 {0 2} --END--""")
 r = b.intersecting_run(spot.complement(a));
 c = spot.twa_word(r).as_automaton()
-assert c.intersects(b)
-assert not c.intersects(a)
+tc.assertTrue(c.intersects(b))
+tc.assertFalse(c.intersects(a))

tests/python/kripke.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,9 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
+
 bdict = spot.make_bdd_dict()
 k = spot.make_kripke_graph(bdict)
 p1 = buddy.bdd_ithvar(k.register_ap("p1"))
@@ -51,25 +54,25 @@ State: [0&1] 1 "0"
 State: [!0&!1] 2 "2"
 2 1
 --END--"""
-assert hoa == k.to_str('HOA')
-assert k.num_states() == 3
-assert k.num_edges() == 5
+tc.assertEqual(hoa, k.to_str('HOA'))
+tc.assertEqual(k.num_states(), 3)
+tc.assertEqual(k.num_edges(), 5)
 
 res = []
 for e in k.out(s1):
     res.append((e.src, e.dst))
-assert res == [(1, 0), (1, 2)]
+tc.assertEqual(res, [(1, 0), (1, 2)])
 
 res = []
 for e in k.edges():
     res.append((e.src, e.dst))
-assert res == [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)]
+tc.assertEqual(res, [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)])
 
 res = []
 for s in k.states():
     res.append(s.cond())
-assert res == [cond1, cond2, cond3]
+tc.assertEqual(res, [cond1, cond2, cond3])
 
-assert k.states()[0].cond() == cond1
-assert k.states()[1].cond() == cond2
-assert k.states()[2].cond() == cond3
+tc.assertEqual(k.states()[0].cond(), cond1)
+tc.assertEqual(k.states()[1].cond(), cond2)
+tc.assertEqual(k.states()[2].cond(), cond3)

tests/python/langmap.py

@@ -1,6 +1,6 @@
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016, 2017, 2020 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE)
+# Copyright (C) 2016, 2017, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE)
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 
 import spot
 import sys
+from unittest import TestCase
+tc = TestCase()
 
 
 def hstates(txt):
@@ -31,13 +33,10 @@ def hstates(txt):
 def test(f, opt, expected):
     aut = spot.translate(f, *opt, 'deterministic')
     v = spot.language_map(aut)
-    assert len(v) == aut.num_states()
+    tc.assertEqual(len(v), aut.num_states())
     spot.highlight_languages(aut)
     l = hstates(aut.to_str('hoa', '1.1'))
-    if l != expected:
-        print('for {}\nexpected: {}\n but got: {}'.format(f, expected, l),
-              file=sys.stderr)
-        exit(1)
+    tc.assertEqual(l, expected)
 
 
 test('GF(a) & GFb & c', ['Buchi', 'SBAcc'], '1 0 2 0 3 0')
@@ -50,6 +49,6 @@ test('Xa', ['Buchi', 'SBAcc'], '')
 try:
     test('FGa', ['Buchi'], '')
 except RuntimeError as e:
-    assert 'language_map only works with deterministic automata'in str(e)
+    tc.assertIn('language_map only works with deterministic automata', str(e))
 else:
     exit(1)

tests/python/ltl2tgba.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021 Laboratoire de Recherche
-# et Développement de l'Epita (LRDE).
+# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021-2022 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.
@@ -98,7 +98,7 @@ if f:
     elif taa_opt:
         a = concrete = spot.ltl_to_taa(f, dict)
     else:
-        assert "unspecified translator"
+        raise RuntimeError("unspecified translator")
 
     if wdba:
         a = spot.ensure_digraph(a)
@@ -117,7 +117,7 @@ if f:
     elif output == 6:
         spot.print_lbtt(cout, a)
     else:
-        assert "unknown output option"
+        raise RuntimeError("unknown output option")
 
     if degeneralize_opt:
         del degeneralized
@@ -137,4 +137,6 @@ del dict
 # not necessary in other implementations.
 from platform import python_implementation
 if python_implementation() == 'CPython':
-    assert spot.fnode_instances_check()
+    from unittest import TestCase
+    tc = TestCase()
+    tc.assertTrue(spot.fnode_instances_check())

tests/python/ltlf.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de
 # l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 lcc = spot.language_containment_checker()
 
@@ -43,5 +45,5 @@ for f in formulas:
     f4 = spot.formula_And([spot.from_ltlf(f2), cst])
     print("{}\t=>\t{}".format(f1, f3))
     print("{}\t=>\t{}".format(f2, f4))
-    assert lcc.equal(f3, f4)
+    tc.assertTrue(lcc.equal(f3, f4))
     print()

tests/python/ltlparse.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009-2012, 2014-2017, 2019, 2021 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2009-2012, 2014-2017, 2019, 2021-2022 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.
@@ -22,6 +22,8 @@
 
 import sys
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 e = spot.default_environment.instance()
 
@@ -41,11 +43,11 @@ for str1, isl in l:
     pf = spot.parse_infix_psl(str2, e)
     if pf.format_errors(spot.get_cout()):
         sys.exit(1)
-    assert isl == pf.f.is_leaf()
+    tc.assertEqual(isl, pf.f.is_leaf())
     del pf
 
-assert spot.formula('a').is_leaf()
-assert spot.formula('0').is_leaf()
+tc.assertTrue(spot.formula('a').is_leaf())
+tc.assertTrue(spot.formula('0').is_leaf())
 
 for str1 in ['a * b', 'a xor b', 'a <-> b']:
     pf = spot.parse_infix_boolean(str1, e, False)
@@ -66,21 +68,21 @@ for (x, op) in [('a* <-> b*', "`<->'"),
                 ('a*[=2]', "[=...]"),
                 ('a*[->2]', "[->...]")]:
     f5 = spot.parse_infix_sere(x)
-    assert f5.errors
+    tc.assertTrue(f5.errors)
     ostr = spot.ostringstream()
     f5.format_errors(ostr)
     err = ostr.str()
-    assert "not a Boolean expression" in err
-    assert op in err
-    assert "SERE" in err
+    tc.assertIn("not a Boolean expression", err)
+    tc.assertIn(op, err)
+    tc.assertIn("SERE", err)
     del f5
 
 f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]')
-assert not f6.errors
+tc.assertFalse(f6.errors)
 del f6
 
 f6 = spot.parse_infix_sere('-')
-assert f6.errors
+tc.assertTrue(f6.errors)
 del f6
 
 for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"),
@@ -150,12 +152,12 @@ for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"),
                  ('{"X}', "missing closing brace"),
                  ]:
     f7 = spot.parse_infix_psl(x)
-    assert f7.errors
+    tc.assertTrue(f7.errors)
     ostr = spot.ostringstream()
     f7.format_errors(ostr)
     err = ostr.str()
     print(err)
-    assert msg in err
+    tc.assertIn(msg, err)
     del f7
 
 for (x, msg) in [('a&', "missing right operand for \"and operator\""),
@@ -174,12 +176,12 @@ for (x, msg) in [('a&', "missing right operand for \"and operator\""),
                  ('!', "missing right operand for \"not operator\""),
                  ]:
     f8 = spot.parse_infix_boolean(x)
-    assert f8.errors
+    tc.assertTrue(f8.errors)
     ostr = spot.ostringstream()
     f8.format_errors(ostr)
     err = ostr.str()
     print(err)
-    assert msg in err
+    tc.assertIn(msg, err)
     del f8
 
 for (x, msg) in [('a->', "missing right operand for \"implication operator\""),
@@ -191,12 +193,12 @@ for (x, msg) in [('a->', "missing right operand for \"implication operator\""),
                  ]:
     f9 = spot.parse_infix_psl(x, spot.default_environment.instance(),
                               False, True)
-    assert f9.errors
+    tc.assertTrue(f9.errors)
     ostr = spot.ostringstream()
     f9.format_errors(ostr)
     err = ostr.str()
     print(err)
-    assert msg in err
+    tc.assertIn(msg, err)
     del f9
 
 # force GC before fnode_instances_check(), unless it's CPython
@@ -205,15 +207,15 @@ if python_implementation() != 'CPython':
     import gc
     gc.collect()
 
-assert spot.fnode_instances_check()
+tc.assertTrue(spot.fnode_instances_check())
 
 f = spot.formula_F(2, 4, spot.formula_ap("a"))
-assert f == spot.formula("XX(a | X(a | X(a)))")
+tc.assertEqual(f, spot.formula("XX(a | X(a | X(a)))"))
 f = spot.formula_G(2, 4, spot.formula_ap("a"))
-assert f == spot.formula("XX(a & X(a & X(a)))")
+tc.assertEqual(f, spot.formula("XX(a & X(a & X(a)))"))
 f = spot.formula_X(2, spot.formula_ap("a"))
-assert f == spot.formula("XX(a)")
+tc.assertEqual(f, spot.formula("XX(a)"))
 f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a"))
-assert f == spot.formula("XXG(a)")
+tc.assertEqual(f, spot.formula("XXG(a)"))
 f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a"))
-assert f == spot.formula("XXF(a)")
+tc.assertEqual(f, spot.formula("XXF(a)"))

tests/python/ltlsimple.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021 Laboratoire de
+# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021-2022 Laboratoire de
 # Recherche et Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systemes Répartis Coopératifs (SRC), Université Pierre
@@ -22,6 +22,8 @@
 
 import spot
 import sys
+from unittest import TestCase
+tc = TestCase()
 
 # Some of the tests here assume timely destructor calls, as they occur
 # in the the reference-counted CPython implementation.  Other
@@ -35,13 +37,13 @@ b = spot.formula.ap('b')
 c = spot.formula.ap('c')
 c2 = spot.formula.ap('c')
 
-assert c == c2
+tc.assertEqual(c, c2)
 
 op = spot.formula.And([a, b])
 op2 = spot.formula.And([op, c])
 op3 = spot.formula.And([a, c, b])
 
-assert op2 == op3
+tc.assertEqual(op2, op3)
 
 # The symbol for a subformula which hasn't been cloned is better
 # suppressed, so we don't attempt to reuse it elsewhere.
@@ -52,12 +54,12 @@ sys.stdout.write('op2 = %s\n' % str(op2))
 del a, b, c2
 
 sys.stdout.write('op3 = %s\n' % str(op3))
-assert op2 == op3
+tc.assertEqual(op2, op3)
 
 op4 = spot.formula.Or([op2, op3])
 
 sys.stdout.write('op4 = %s\n' % str(op4))
-assert op4 == op2
+tc.assertEqual(op4, op2)
 
 del op2, op3, op4
 
@@ -78,10 +80,11 @@ f5 = spot.formula.Xor(F, c)
 del a, b, c, T, F, f1, f2, f4, f5
 
 if is_cpython:
-    assert spot.fnode_instances_check()
+    tc.assertTrue(spot.fnode_instances_check())
 
 # ----------------------------------------------------------------------
-assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']"
+tc.assertEqual(str([str(x) for x in spot.formula('a &b & c')]),
+               "['a', 'b', 'c']")
 
 
 def switch_g_f(x):
@@ -93,7 +96,7 @@ def switch_g_f(x):
 
 
 f = spot.formula('GFa & XFGb & Fc & G(a | b | Fd)')
-assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)'
+tc.assertEqual(str(switch_g_f(f)), 'FGa & XGFb & Gc & F(a | b | Gd)')
 
 x = 0
 
@@ -105,7 +108,7 @@ def count_g(f):
 
 
 f.traverse(count_g)
-assert x == 3
+tc.assertEqual(x, 3)
 
 # ----------------------------------------------------------------------
 
@@ -121,14 +124,14 @@ LBT for shell:     echo {f:lq} | ...
 Default for CSV:   ...,{f:c},...
 Wring, centered:   {f:w:~^50}""".format(f=formula)
 
-assert res == """\
+tc.assertEqual(res, """\
 Default output:    a U (b U "$strange[0]=name")
 Spin syntax:       a U (b U ($strange[0]=name))
 (Spin syntax):     (a) U ((b) U ($strange[0]=name))
 Default for shell: echo 'a U (b U "$strange[0]=name")' | ...
 LBT for shell:     echo 'U "a" U "b" "$strange[0]=name"' | ...
 Default for CSV:   ...,"a U (b U ""$strange[0]=name"")",...
-Wring, centered:   ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~"""
+Wring, centered:   ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~""")
 
 
 opt = spot.tl_simplifier_options(False, True, True,
@@ -144,9 +147,8 @@ for (input, output) in [('(a&b)<->b', 'b->(a&b)'),
                         ('b xor (!(a&b))', 'b->(a&b)'),
                         ('!b xor (a&b)', 'b->(a&b)')]:
     f = spot.tl_simplifier(opt).simplify(input)
-    print(input, f, output)
-    assert(f == output)
-    assert(spot.are_equivalent(input, output))
+    tc.assertEqual(f, output)
+    tc.assertTrue(spot.are_equivalent(input, output))
 
 
 def myparse(input):
@@ -157,7 +159,7 @@ def myparse(input):
 
 # This used to fail, because myparse would return a pointer
 # to pf.f inside the destroyed pf.
-assert myparse('a U b') == spot.formula('a U b')
+tc.assertEqual(myparse('a U b'), spot.formula('a U b'))
 
-assert spot.is_liveness('a <-> GFb')
-assert not spot.is_liveness('a & GFb')
+tc.assertTrue(spot.is_liveness('a <-> GFb'))
+tc.assertFalse(spot.is_liveness('a & GFb'))

tests/python/mealy.py

@@ -19,6 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot, buddy
+from unittest import TestCase
+tc = TestCase()
 
 # Testing Sat-based approach
 
@@ -42,8 +44,8 @@ spot.set_state_players(a, [False,True,False,True,False,True])
 spot.set_synthesis_outputs(a, o1&o2)
 
 b = spot.minimize_mealy(a)
-assert(list(spot.get_state_players(b)).count(False) == 2)
-assert(spot.is_split_mealy_specialization(a, b))
+tc.assertEqual(list(spot.get_state_players(b)).count(False), 2)
+tc.assertTrue(spot.is_split_mealy_specialization(a, b))
 
 test_auts = [
 ("""HOA: v1
@@ -371,21 +373,21 @@ for (mealy_str, nenv_min) in test_auts:
         elif aap.ap_name().startswith("i"):
             ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name()))
         else:
-            assert("""Aps must start with either "i" or "o".""")
+            raise AssertionError("""Aps must start with either "i" or "o".""")
 
     spot.set_synthesis_outputs(mealy, outs)
 
     mealy_min_ks = spot.minimize_mealy(mealy, -1)
 
     n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)])
-    assert(n_e == nenv_min)
-    assert(spot.is_split_mealy_specialization(mealy, mealy_min_ks))
+    tc.assertEqual(n_e, nenv_min)
+    tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_ks))
 
     # Test un- and resplit
     tmp = spot.unsplit_2step(mealy_min_ks)
     mealy_min_rs = spot.split_2step(tmp, spot.get_synthesis_outputs(tmp), False)
-    assert(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True))
-    assert(spot.are_equivalent(mealy_min_ks, mealy_min_rs))
+    tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True))
+    tc.assertTrue(spot.are_equivalent(mealy_min_ks, mealy_min_rs))
 
 
 # Testing bisimulation (with output assignment)
@@ -515,15 +517,15 @@ spot.set_synthesis_outputs(aut,
   & buddy.bdd_ithvar(
    aut.register_ap("u02alarm29control0f1d2alarm29turn2off1b")))
 min_equiv = spot.reduce_mealy(aut, False)
-assert min_equiv.num_states() == 6
-assert spot.are_equivalent(min_equiv, aut)
+tc.assertEqual(min_equiv.num_states(), 6)
+tc.assertTrue(spot.are_equivalent(min_equiv, aut))
 
 # Build an automaton that recognizes a subset of the language of the original
 # automaton
 min_sub = spot.reduce_mealy(aut, True)
-assert min_sub.num_states() == 5
+tc.assertEqual(min_sub.num_states(), 5)
 prod = spot.product(spot.complement(aut), min_sub)
-assert spot.generic_emptiness_check(prod)
+tc.assertTrue(spot.generic_emptiness_check(prod))
 
 aut = spot.automaton("""
 HOA: v1
@@ -564,7 +566,7 @@ State: 0
 
 # An example that shows that we should not build a tree when we use inclusion.
 res = spot.reduce_mealy(aut, True)
-assert res.to_str() == exp
+tc.assertEqual(res.to_str(), exp)
 
 aut = spot.automaton("""
 HOA: v1
@@ -608,4 +610,4 @@ State: 1
 --END--"""
 
 res = spot.reduce_mealy(aut, True)
-assert res.to_str() == exp
+tc.assertEqual(res.to_str(), exp)

tests/python/merge.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.automaton("""
 HOA: v1
@@ -39,7 +41,7 @@ State: 2
 out = spot.simplify_acceptance(aut)
 hoa = out.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -54,8 +56,8 @@ State: 1
 [1] 2 {0}
 State: 2
 [1] 0
---END--"""
-assert spot.are_equivalent(out, aut)
+--END--""")
+tc.assertTrue(spot.are_equivalent(out, aut))
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -75,7 +77,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -90,7 +92,7 @@ State: 1
 [1] 2 {0}
 State: 2
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -111,7 +113,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -126,7 +128,7 @@ State: 1
 [1] 2
 State: 2
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -146,7 +148,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -161,7 +163,7 @@ State: 1
 [1] 2 {1}
 State: 2
 [1] 0 {0}
---END--"""
+--END--""")
 
 aut = spot.automaton("""
 HOA: v1
@@ -182,7 +184,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -197,7 +199,7 @@ State: 1
 [1] 2
 State: 2
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -217,7 +219,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -232,7 +234,7 @@ State: 1 {0}
 [1] 2
 State: 2 {0}
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -252,7 +254,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -267,7 +269,7 @@ State: 1 {0}
 [1] 2
 State: 2 {0}
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -287,7 +289,7 @@ State: 2
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -301,7 +303,7 @@ State: 1 {1}
 [1] 2
 State: 2
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 4
@@ -335,7 +337,7 @@ State: 3 {1 3}
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 4
 Start: 0
 AP: 2 "a" "b"
@@ -364,7 +366,7 @@ State: 3 {1}
 [0&!1] 0
 [!0&1] 3
 [0&1] 2
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -388,7 +390,7 @@ State: 2
 out = spot.simplify_acceptance(aut)
 hoa = out.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "p0" "p1"
@@ -406,8 +408,8 @@ State: 1
 State: 2
 [0] 2 {0}
 [!0] 1 {0}
---END--"""
-assert spot.are_equivalent(out, aut)
+--END--""")
+tc.assertTrue(spot.are_equivalent(out, aut))
 
 aut = spot.automaton("""HOA: v1
 States: 4
@@ -435,7 +437,7 @@ State: 3
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 4
 Start: 0
 AP: 2 "p0" "p1"
@@ -457,7 +459,7 @@ State: 3
 [0&1] 0 {1}
 [0&!1] 3 {1 2}
 [!0] 1 {3}
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 1
@@ -475,7 +477,7 @@ State: 0 {1 2}
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 1
 Start: 0
 AP: 2 "p0" "p1"
@@ -486,7 +488,7 @@ properties: deterministic
 --BODY--
 State: 0
 [t] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 2
@@ -506,7 +508,7 @@ State: 1
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 2
 Start: 0
 AP: 2 "p0" "p1"
@@ -519,7 +521,7 @@ State: 0
 [!0] 1 {2}
 State: 1
 [t] 1 {1 2}
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 1
@@ -536,7 +538,7 @@ State: 0 {0 1 3}
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 1
 Start: 0
 AP: 2 "p0" "p1"
@@ -547,7 +549,7 @@ properties: deterministic
 --BODY--
 State: 0
 [t] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 2
@@ -568,7 +570,7 @@ State: 1
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 2
 Start: 0
 AP: 2 "p0" "p1"
@@ -583,7 +585,7 @@ State: 0
 State: 1
 [0] 1
 [!0] 0 {1}
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 2
@@ -602,7 +604,7 @@ State: 1 {1}
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 2
 Start: 0
 AP: 2 "p0" "p1"
@@ -615,7 +617,7 @@ State: 0
 [t] 1
 State: 1
 [t] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -636,7 +638,7 @@ State: 2 {2}
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "p0" "p1"
@@ -650,7 +652,7 @@ State: 1 {0}
 [t] 1
 State: 2 {2}
 [t] 1
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -672,7 +674,7 @@ State: 2 {1 2 3}
 out = spot.simplify_acceptance(aut)
 hoa = out.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "p0" "p1"
@@ -687,8 +689,8 @@ State: 1 {1}
 [t] 2
 State: 2 {0 1}
 [t] 1
---END--"""
-assert spot.are_equivalent(out, aut)
+--END--""")
+tc.assertTrue(spot.are_equivalent(out, aut))
 
 aut = spot.automaton("""HOA: v1
 States: 2
@@ -708,7 +710,7 @@ State: 1
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
 
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 2
 Start: 0
 AP: 2 "p0" "p1"
@@ -722,7 +724,7 @@ State: 0
 State: 1
 [0] 1
 [!0] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -740,7 +742,7 @@ State: 2
 --END--""")
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -755,7 +757,7 @@ State: 1
 [1] 2
 State: 2
 [1] 0
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -773,7 +775,7 @@ State: 2
 --END--""")
 spot.simplify_acceptance_here(aut)
 hoa = aut.to_str('hoa')
-assert hoa == """HOA: v1
+tc.assertEqual(hoa, """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -788,4 +790,4 @@ State: 1
 [1] 2
 State: 2
 [1] 0
---END--"""
+--END--""")

tests/python/mergedge.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020, 2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2020-2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -20,12 +20,14 @@
 
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a"
 Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""")
-assert aut.num_edges() == 2
+tc.assertEqual(aut.num_edges(), 2)
 aut.merge_edges()
-assert aut.num_edges() == 1
+tc.assertEqual(aut.num_edges(), 1)
 
 aut = spot.automaton("""
 HOA: v1
@@ -44,15 +46,15 @@ State: 1
 [0 | 1] 1
 [0&!1] 1 {0}
 --END--""")
-assert aut.num_edges() == 5
+tc.assertEqual(aut.num_edges(), 5)
 aut.merge_edges()
-assert aut.num_edges() == 5
-assert not spot.is_deterministic(aut)
+tc.assertEqual(aut.num_edges(), 5)
+tc.assertFalse(spot.is_deterministic(aut))
 aut = spot.split_edges(aut)
-assert aut.num_edges() == 9
+tc.assertEqual(aut.num_edges(), 9)
 aut.merge_edges()
-assert aut.num_edges() == 5
-assert spot.is_deterministic(aut)
+tc.assertEqual(aut.num_edges(), 5)
+tc.assertTrue(spot.is_deterministic(aut))
 
 aut = spot.automaton("""
 HOA: v1
@@ -74,15 +76,15 @@ State: 2
 [0] 1
 --END--""")
 aut.merge_states()
-assert aut.num_edges() == 4
-assert aut.num_states() == 2
-assert spot.is_deterministic(aut)
-assert aut.prop_complete()
+tc.assertEqual(aut.num_edges(), 4)
+tc.assertEqual(aut.num_states(), 2)
+tc.assertTrue(spot.is_deterministic(aut))
+tc.assertTrue(aut.prop_complete())
 aut.merge_states()
-assert aut.num_edges() == 4
-assert aut.num_states() == 2
-assert spot.is_deterministic(aut)
-assert aut.prop_complete()
+tc.assertEqual(aut.num_edges(), 4)
+tc.assertEqual(aut.num_states(), 2)
+tc.assertTrue(spot.is_deterministic(aut))
+tc.assertTrue(aut.prop_complete())
 
 
 aa = spot.automaton("""

tests/python/misc-ec.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,9 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
+
 aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'Buchi', 'SBAcc')
 ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut)
 n = 0
@@ -27,7 +30,7 @@ while True:
         break
     print(res.accepting_run())
     n += 1
-assert n == 2
+tc.assertEqual(n, 2)
 
 for name in ['SE05', 'CVWY90', 'GV04']:
     aut = spot.translate("GFa && GFb")
@@ -35,13 +38,13 @@ for name in ['SE05', 'CVWY90', 'GV04']:
         ec = spot.make_emptiness_check_instantiator(name)[0].instantiate(aut)
         print(ec.check().accepting_run())
     except RuntimeError as e:
-        assert "Büchi or weak" in str(e)
+        tc.assertIn("Büchi or weak", str(e))
 
 aut = spot.translate("a", 'monitor')
 try:
     ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut)
 except RuntimeError as e:
-    assert "at least one" in str(e)
+    tc.assertIn("at least one", str(e))
 
 aut = spot.translate("a", 'ba')
 ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut)

tests/python/optionmap.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2010, 2012, 2018 Laboratoire de Recherche et Développement
-# de l'EPITA.
+# Copyright (C) 2010, 2012, 2018, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 # Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -21,65 +21,67 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 o = spot.option_map()
 res = o.parse_options("optA, opta=2M, optb =4 ; optB =       7\
                        ,   optC=  10")
-assert not res
+tc.assertFalse(res)
 
-assert o.get('optA') == 1
-assert o.get('opta') == 2*1024*1024
-assert o.get('optb') == 4
-assert o.get('optB') == 7
-assert o.get('optC') == 10
-assert o.get('none') == 0
-assert o.get('none', 16) == 16
+tc.assertEqual(o.get('optA'), 1)
+tc.assertEqual(o.get('opta'), 2*1024*1024)
+tc.assertEqual(o.get('optb'), 4)
+tc.assertEqual(o.get('optB'), 7)
+tc.assertEqual(o.get('optC'), 10)
+tc.assertEqual(o.get('none'), 0)
+tc.assertEqual(o.get('none', 16), 16)
 
 o.set('optb', 40)
-assert o.get('optb') == 40
+tc.assertEqual(o.get('optb'), 40)
 
 res = o.parse_options("!optA !optb optC, !optB")
-assert not res
-assert o.get('optA') == 0
-assert o.get('opta') == 2*1024*1024
-assert o.get('optb') == 0
-assert o.get('optB') == 0
-assert o.get('optC') == 1
+tc.assertFalse(res)
+tc.assertEqual(o.get('optA'), 0)
+tc.assertEqual(o.get('opta'), 2*1024*1024)
+tc.assertEqual(o.get('optb'), 0)
+tc.assertEqual(o.get('optB'), 0)
+tc.assertEqual(o.get('optC'), 1)
 
 res = o.parse_options("!")
-assert res == "!"
+tc.assertEqual(res, "!")
 
 res = o.parse_options("foo, !opt = 1")
-assert res == "!opt = 1"
+tc.assertEqual(res, "!opt = 1")
 
 res = o.parse_options("foo=3, opt == 1")
-assert res == "opt == 1"
+tc.assertEqual(res, "opt == 1")
 
 res = o.parse_options("foo=3opt == 1")
-assert res == "3opt == 1"
+tc.assertEqual(res, "3opt == 1")
 
 aut1 = spot.translate('GF(a <-> XXa)', 'det')
-assert aut1.num_states() == 4
+tc.assertEqual(aut1.num_states(), 4)
 aut2 = spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0')
-assert aut2.num_states() == 9
+tc.assertEqual(aut2.num_states(), 9)
 
 try:
     spot.translate('GF(a <-> XXa)', 'det', xargs='foobar=1')
 except RuntimeError as e:
-    assert "option 'foobar' was not used" in str(e)
+    tc.assertIn("option 'foobar' was not used", str(e))
 else:
     raise RuntimeError("missing exception")
 
 try:
     spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=0')
 except RuntimeError as e:
-    assert "option 'gf-guarantee' was not used" in str(e)
+    tc.assertIn("option 'gf-guarantee' was not used", str(e))
 else:
     raise RuntimeError("missing exception")
 
 try:
     spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=x')
 except RuntimeError as e:
-    assert "failed to parse option at: 'gf-guarantee=x'" in str(e)
+    tc.assertIn("failed to parse option at: 'gf-guarantee=x'", str(e))
 else:
     raise RuntimeError("missing exception")

tests/python/origstate.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017  Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2015, 2017, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 
 import spot
 from sys import exit
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.automaton("""
 HOA: v1
@@ -38,7 +40,7 @@ State: 1
 """)
 
 aut2 = spot.degeneralize(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -56,10 +58,10 @@ State: 1
 [1] 2
 State: 2 {0}
 [1] 2
---END--"""
+--END--""")
 
 aut2.copy_state_names_from(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -77,7 +79,7 @@ State: 1 "0#0"
 [1] 2
 State: 2 "1#1" {0}
 [1] 2
---END--"""
+--END--""")
 
 aut2.set_init_state(2)
 aut2.purge_unreachable_states()
@@ -93,16 +95,16 @@ properties: deterministic
 State: 0 "1#1" {0}
 [1] 0
 --END--"""
-assert aut2.to_str() == ref
+tc.assertEqual(aut2.to_str(), ref)
 # This makes sure that the original-states vector has also been renamed.
 aut2.copy_state_names_from(aut)
-assert aut2.to_str() == ref
+tc.assertEqual(aut2.to_str(), ref)
 
 aut2 = spot.degeneralize(aut)
 aut2.release_named_properties()
 try:
     aut2.copy_state_names_from(aut)
 except RuntimeError as e:
-    assert "state does not exist in source automaton" in str(e)
+    tc.assertIn("state does not exist in source automaton", str(e))
 else:
     exit(1)

tests/python/otfcrash.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2018  Laboratoire de Recherche et Développement
+# Copyright (C) 2016, 2018, 2022  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -23,6 +23,8 @@ import spot.aux
 import tempfile
 import shutil
 import sys
+from unittest import TestCase
+tc = TestCase()
 
 spot.ltsmin.require('divine')
 
@@ -51,4 +53,4 @@ system async;
         p = spot.otf_product(k, a)
         return p.is_empty()
 
-    assert(modelcheck('X "R.found"', m) == True)
+    tc.assertTrue(modelcheck('X "R.found"', m))

tests/python/parity.py

@@ -19,36 +19,38 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 max_even_5 = spot.acc_code.parity(True, False, 5)
-assert max_even_5 == spot.acc_code.parity_max_even(5)
-assert max_even_5 == spot.acc_code.parity_max(False, 5)
+tc.assertEqual(max_even_5, spot.acc_code.parity_max_even(5))
+tc.assertEqual(max_even_5, spot.acc_code.parity_max(False, 5))
 min_even_5 = spot.acc_code.parity(False, False, 5)
-assert min_even_5 == spot.acc_code.parity_min_even(5)
-assert min_even_5 == spot.acc_code.parity_min(False, 5)
+tc.assertEqual(min_even_5, spot.acc_code.parity_min_even(5))
+tc.assertEqual(min_even_5, spot.acc_code.parity_min(False, 5))
 
 max_odd_5 = spot.acc_code.parity(True, True, 5)
-assert max_odd_5 == spot.acc_code.parity_max_odd(5)
-assert max_odd_5 == spot.acc_code.parity_max(True, 5)
+tc.assertEqual(max_odd_5, spot.acc_code.parity_max_odd(5))
+tc.assertEqual(max_odd_5, spot.acc_code.parity_max(True, 5))
 min_odd_5 = spot.acc_code.parity(False, True, 5)
-assert min_odd_5 == spot.acc_code.parity_min_odd(5)
-assert min_odd_5 == spot.acc_code.parity_min(True, 5)
+tc.assertEqual(min_odd_5, spot.acc_code.parity_min_odd(5))
+tc.assertEqual(min_odd_5, spot.acc_code.parity_min(True, 5))
 
 
 for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'):
     a1 = spot.translate(f, 'parity')
-    assert a1.acc().is_parity()
+    tc.assertTrue(a1.acc().is_parity())
     a2 = spot.translate(f).postprocess('parity')
-    assert a2.acc().is_parity()
+    tc.assertTrue(a2.acc().is_parity())
     a3 = spot.translate(f, 'det').postprocess('parity', 'colored')
-    assert a3.acc().is_parity()
-    assert spot.is_colored(a3)
+    tc.assertTrue(a3.acc().is_parity())
+    tc.assertTrue(spot.is_colored(a3))
 
 a = spot.translate('GFa & GFb')
 try:
     spot.change_parity_here(a, spot.parity_kind_same, spot.parity_style_even)
 except RuntimeError as e:
-    assert 'input should have parity acceptance' in str(e)
+    tc.assertIn('input should have parity acceptance', str(e))
 else:
     exit(2)
 
@@ -64,7 +66,7 @@ State: 0
 --END--
 """)
 spot.cleanup_parity_here(a)
-assert a.to_str() == """HOA: v1
+tc.assertEqual(a.to_str(), """HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
@@ -75,7 +77,7 @@ properties: deterministic
 --BODY--
 State: 0
 [t] 0
---END--"""
+--END--""")
 
 a = spot.automaton("""
 HOA: v1
@@ -89,7 +91,7 @@ State: 0
 --END--
 """)
 spot.cleanup_parity_here(a)
-assert a.to_str() == """HOA: v1
+tc.assertEqual(a.to_str(), """HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
@@ -100,7 +102,7 @@ properties: deterministic
 --BODY--
 State: 0
 [t] 0
---END--"""
+--END--""")
 
 a = spot.automaton("""HOA: v1
 States: 3
@@ -120,39 +122,39 @@ State: 2
 try:
 	spot.get_state_players(a)
 except RuntimeError as e:
-  assert "not a game" in str(e)
+  tc.assertIn("not a game", str(e))
 else:
   report_missing_exception()
 
 try:
     spot.set_state_player(a, 1, True)
 except RuntimeError as e:
-    assert "Can only" in str(e)
+    tc.assertIn("Can only", str(e))
 else:
     report_missing__exception()
 spot.set_state_players(a, (False, True, False))
-assert spot.get_state_player(a, 0) == False
-assert spot.get_state_player(a, 1) == True
-assert spot.get_state_player(a, 2) == False
+tc.assertEqual(spot.get_state_player(a, 0), False)
+tc.assertEqual(spot.get_state_player(a, 1), True)
+tc.assertEqual(spot.get_state_player(a, 2), False)
 
 try:
 	spot.set_state_players(a, [True, False, False, False])
 except RuntimeError as e:
-  assert "many owners as states" in str(e)
+  tc.assertIn("many owners as states", str(e))
 else:
   report_missing_exception()
 
 try:
 	spot.get_state_player(a, 4)
 except RuntimeError as e:
-  assert "invalid state number" in str(e)
+  tc.assertIn("invalid state number", str(e))
 else:
   report_missing_exception()
 
 try:
 	spot.set_state_player(a, 4, True)
 except RuntimeError as e:
-  assert "invalid state number" in str(e)
+  tc.assertIn("invalid state number", str(e))
 else:
   report_missing_exception()
 
@@ -168,4 +170,4 @@ oi.erase()
 # postprocess used to call reduce_parity that did not
 # work correctly on automata with deleted edges.
 sm = a.postprocess("gen", "small")
-assert sm.num_states() == 3
+tc.assertEqual(sm.num_states(), 3)

tests/python/parsetgba.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2012, 2014, 2015, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 
 import os
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 contents = '''
 HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi
@@ -34,7 +36,7 @@ out.close()
 
 a = spot.parse_aut(filename, spot.make_bdd_dict())
 
-assert not a.errors
+tc.assertFalse(a.errors)
 
 spot.print_dot(spot.get_cout(), a.aut)
 

tests/python/pdegen.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019, 2020, 2021 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2019, 2020, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -23,6 +23,8 @@
 
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a, b, d, f = spot.automata("""
 HOA: v1
@@ -73,19 +75,19 @@ State: 1
 --END--
 """)
 
-assert spot.is_partially_degeneralizable(a) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(a), [0, 1])
 da = spot.partial_degeneralize(a, [0, 1])
-assert da.equivalent_to(a)
-assert da.num_states() == 2
+tc.assertTrue(da.equivalent_to(a))
+tc.assertEqual(da.num_states(), 2)
 
-assert spot.is_partially_degeneralizable(b) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(b), [0, 1])
 db = spot.partial_degeneralize(b, [0, 1])
-assert db.equivalent_to(b)
-assert db.num_states() == 3
+tc.assertTrue(db.equivalent_to(b))
+tc.assertEqual(db.num_states(), 3)
 
 db.copy_state_names_from(b)
 dbhoa = db.to_str('hoa')
-assert dbhoa == """HOA: v1
+tc.assertEqual(dbhoa, """HOA: v1
 States: 3
 Start: 0
 AP: 1 "p0"
@@ -99,28 +101,28 @@ State: 1 "0#0" {0 1}
 [0] 2
 State: 2 "1#0" {1}
 [0] 1
---END--"""
+--END--""")
 
 c = spot.automaton("randaut -A'(Fin(0)&Inf(1)&Inf(2))|Fin(2)' 1 |")
-assert spot.is_partially_degeneralizable(c) == [1, 2]
+tc.assertEqual(spot.is_partially_degeneralizable(c), [1, 2])
 dc = spot.partial_degeneralize(c, [1, 2])
-assert dc.equivalent_to(c)
-assert str(dc.get_acceptance()) == '(Fin(0) & Inf(2)) | Fin(1)'
+tc.assertTrue(dc.equivalent_to(c))
+tc.assertEqual(str(dc.get_acceptance()), '(Fin(0) & Inf(2)) | Fin(1)')
 
-assert spot.is_partially_degeneralizable(d) == []
+tc.assertEqual(spot.is_partially_degeneralizable(d), [])
 dd = spot.partial_degeneralize(d, [])
-assert dd.equivalent_to(d)
-assert dd.num_states() == 1
-assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)'
+tc.assertTrue(dd.equivalent_to(d))
+tc.assertEqual(dd.num_states(), 1)
+tc.assertEqual(str(dd.get_acceptance()), 'Inf(1) & Fin(0)')
 
 e = spot.dualize(b)
 de = spot.partial_degeneralize(e, [0, 1])
-assert de.equivalent_to(e)
-assert de.num_states() == 4
+tc.assertTrue(de.equivalent_to(e))
+tc.assertEqual(de.num_states(), 4)
 
 de.copy_state_names_from(e)
 dehoa = de.to_str('hoa')
-assert dehoa == """HOA: v1
+tc.assertEqual(dehoa, """HOA: v1
 States: 4
 Start: 0
 AP: 1 "p0"
@@ -140,18 +142,18 @@ State: 2 "3#0"
 State: 3 "2#0"
 [0] 1 {0}
 [!0] 2
---END--"""
+--END--""")
 
-assert spot.is_partially_degeneralizable(de) == []
+tc.assertEqual(spot.is_partially_degeneralizable(de), [])
 
 df = spot.partial_degeneralize(f, [0, 1])
 df.equivalent_to(f)
-assert str(df.acc()) == '(1, Fin(0))'
+tc.assertEqual(str(df.acc()), '(1, Fin(0))')
 
 try:
     df = spot.partial_degeneralize(f, [0, 1, 2])
 except RuntimeError as e:
-    assert 'partial_degeneralize(): {0,1,2} does not' in str(e)
+    tc.assertIn('partial_degeneralize(): {0,1,2} does not', str(e))
 else:
     raise RuntimeError("missing exception")
 
@@ -165,13 +167,13 @@ State: 2 [0&!1&2] 3 {1 4 9} State: 3 [0&!1&2] 4 {0 1 5 9} State: 4 [!0&!1&2] 1
 State: 7 [0&!1&!2] 0 {4 7} --END--""")
 
 daut5 = spot.degeneralize_tba(aut5)
-assert daut5.equivalent_to(aut5)
+tc.assertTrue(daut5.equivalent_to(aut5))
 sets = list(range(aut5.num_sets()))
-assert spot.is_partially_degeneralizable(aut5) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut5), sets)
 pdaut5 = spot.partial_degeneralize(aut5, sets)
-assert pdaut5.equivalent_to(aut5)
-assert daut5.num_states() == 9
-assert pdaut5.num_states() == 8
+tc.assertTrue(pdaut5.equivalent_to(aut5))
+tc.assertEqual(daut5.num_states(), 9)
+tc.assertEqual(pdaut5.num_states(), 8)
 
 aut6 = spot.automaton("""HOA: v1 States: 6 Start: 0 AP: 3 "p0" "p1" "p2"
 acc-name: generalized-Buchi 3 Acceptance: 3 Inf(0)&Inf(1)&Inf(2) properties:
@@ -180,13 +182,13 @@ trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0
 [0&1&!2] 5 {1} State: 4 [!0&1&!2] 0 {1 2} [0&!1&!2] 3 {0} State: 5 [!0&1&2] 1
 --END-- """)
 daut6 = spot.degeneralize_tba(aut6)
-assert daut6.equivalent_to(aut6)
+tc.assertTrue(daut6.equivalent_to(aut6))
 sets = list(range(aut6.num_sets()))
-assert spot.is_partially_degeneralizable(aut6) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut6), sets)
 pdaut6 = spot.partial_degeneralize(aut6, sets)
-assert pdaut6.equivalent_to(aut6)
-assert daut6.num_states() == 8
-assert pdaut6.num_states() == 8
+tc.assertTrue(pdaut6.equivalent_to(aut6))
+tc.assertEqual(daut6.num_states(), 8)
+tc.assertEqual(pdaut6.num_states(), 8)
 
 
 aut7 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
@@ -197,13 +199,13 @@ State: 0 [0&!1&2] 1 {2 3} State: 1 [0&!1&2] 0 {0 2} [0&!1&!2] 6 State: 2
 [!0&!1&!2] 3 State: 5 [0&1&!2] 0 [!0&1&2] 7 State: 6 [0&1&2] 2 {1} State: 7
 [!0&!1&2] 0 {0} [!0&1&!2] 4 --END--""")
 daut7 = spot.degeneralize_tba(aut7)
-assert daut7.equivalent_to(aut7)
+tc.assertTrue(daut7.equivalent_to(aut7))
 sets = list(range(aut7.num_sets()))
-assert spot.is_partially_degeneralizable(aut7) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut7), sets)
 pdaut7 = spot.partial_degeneralize(aut7, sets)
-assert pdaut7.equivalent_to(aut7)
-assert daut7.num_states() == 10
-assert pdaut7.num_states() == 10
+tc.assertTrue(pdaut7.equivalent_to(aut7))
+tc.assertEqual(daut7.num_states(), 10)
+tc.assertEqual(pdaut7.num_states(), 10)
 
 aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2"
 acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)
@@ -213,19 +215,19 @@ State: 0 [!0&1&!2] 7 {0} State: 1 [!0&1&2] 1 {4} [0&!1&2] 6 {1 2} State: 2
 5 [!0&1&!2] 0 {1 3} State: 6 [0&1&2] 4 [0&1&!2] 6 State: 7 [!0&!1&!2] 1
 --END--""")
 daut8 = spot.degeneralize_tba(aut8)
-assert daut8.equivalent_to(aut8)
+tc.assertTrue(daut8.equivalent_to(aut8))
 sets = list(range(aut8.num_sets()))
-assert spot.is_partially_degeneralizable(aut8) == sets
+tc.assertEqual(spot.is_partially_degeneralizable(aut8), sets)
 pdaut8 = spot.partial_degeneralize(aut8, sets)
-assert pdaut8.equivalent_to(aut8)
-assert daut8.num_states() == 22
-assert pdaut8.num_states() == 9
+tc.assertTrue(pdaut8.equivalent_to(aut8))
+tc.assertEqual(daut8.num_states(), 22)
+tc.assertEqual(pdaut8.num_states(), 9)
 
 aut9 = spot.dualize(aut8)
 pdaut9 = spot.partial_degeneralize(aut9, sets)
-assert pdaut9.equivalent_to(aut9)
+tc.assertTrue(pdaut9.equivalent_to(aut9))
 # one more state than aut9, because dualize completed the automaton.
-assert pdaut9.num_states() == 10
+tc.assertEqual(pdaut9.num_states(), 10)
 
 aut10 = spot.automaton("""HOA: v1
 States: 3
@@ -242,10 +244,10 @@ State: 2
 [0] 0 {1}
 [!0] 1
 --END--""")
-assert spot.is_partially_degeneralizable(aut10) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(aut10), [0, 1])
 pdaut10 = spot.partial_degeneralize(aut10, [0, 1])
-assert pdaut10.equivalent_to(aut10)
-assert pdaut10.to_str() ==  """HOA: v1
+tc.assertTrue(pdaut10.equivalent_to(aut10))
+tc.assertEqual(pdaut10.to_str(),  """HOA: v1
 States: 3
 Start: 0
 AP: 1 "p0"
@@ -260,7 +262,7 @@ State: 1
 State: 2
 [0] 0 {1}
 [!0] 1
---END--"""
+--END--""")
 
 aut11 = spot.automaton("""HOA: v1
 States: 3
@@ -277,10 +279,10 @@ State: 2
 [0] 0 {1}
 [!0] 1
 --END--""")
-assert spot.is_partially_degeneralizable(aut11) == [0, 1]
+tc.assertEqual(spot.is_partially_degeneralizable(aut11), [0, 1])
 pdaut11 = spot.partial_degeneralize(aut11, [0, 1])
-assert pdaut11.equivalent_to(aut11)
-assert pdaut11.to_str() ==  """HOA: v1
+tc.assertTrue(pdaut11.equivalent_to(aut11))
+tc.assertEqual(pdaut11.to_str(),  """HOA: v1
 States: 3
 Start: 0
 AP: 1 "p0"
@@ -295,7 +297,7 @@ State: 1
 State: 2
 [0] 0 {2}
 [!0] 1
---END--"""
+--END--""")
 
 aut12 = spot.automaton("""HOA: v1
 States: 3
@@ -313,24 +315,24 @@ State: 2
 [0] 0
 [!0] 1 {3}
 --END--""")
-assert spot.is_partially_degeneralizable(aut12) == [0,1]
+tc.assertEqual(spot.is_partially_degeneralizable(aut12), [0,1])
 aut12b = spot.partial_degeneralize(aut12, [0,1])
 aut12c = spot.partial_degeneralize(aut12b, [1,2])
-assert aut12c.equivalent_to(aut12)
-assert aut12c.num_states() == 9
+tc.assertTrue(aut12c.equivalent_to(aut12))
+tc.assertEqual(aut12c.num_states(), 9)
 
 aut12d = spot.partial_degeneralize(aut12, [0,1,3])
 aut12e = spot.partial_degeneralize(aut12d, [0,1])
-assert aut12e.equivalent_to(aut12)
-assert aut12e.num_states() == 9
+tc.assertTrue(aut12e.equivalent_to(aut12))
+tc.assertEqual(aut12e.num_states(), 9)
 
 aut12f = spot.partial_degeneralize(aut12)
-assert aut12f.equivalent_to(aut12)
-assert aut12f.num_states() == 9
+tc.assertTrue(aut12f.equivalent_to(aut12))
+tc.assertEqual(aut12f.num_states(), 9)
 
 # Check handling of original-states
 dot = aut12f.to_str('dot', 'd')
-assert dot == """digraph "" {
+tc.assertEqual(dot, """digraph "" {
   rankdir=LR
   label="Inf(2) | (Inf(1) & Fin(0))\\n[Rabin-like 2]"
   labelloc="t"
@@ -367,10 +369,10 @@ assert dot == """digraph "" {
   8 -> 4 [label="p0\\n{1,2}"]
   8 -> 7 [label="p0"]
 }
-"""
+""")
 
 aut12g = spot.partial_degeneralize(aut12f)
-assert aut12f == aut12g
+tc.assertEqual(aut12f, aut12g)
 
 aut13 = spot.automaton("""HOA: v1
 States: 2
@@ -390,8 +392,8 @@ State: 1
 [!0&!1&2&3] 1 {0 2}
 --END--""")
 aut13g = spot.partial_degeneralize(aut13)
-assert aut13g.equivalent_to(aut13)
-assert aut13g.num_states() == 3
+tc.assertTrue(aut13g.equivalent_to(aut13))
+tc.assertEqual(aut13g.num_states(), 3)
 
 
 aut14 = spot.automaton("""HOA: v1
@@ -412,8 +414,8 @@ State: 1
 --END--
 """)
 aut14g = spot.partial_degeneralize(aut14)
-assert aut14g.equivalent_to(aut14)
-assert aut14g.num_states() == 3
+tc.assertTrue(aut14g.equivalent_to(aut14))
+tc.assertEqual(aut14g.num_states(), 3)
 
 # Extracting an SCC from this large automaton will produce an automaton A in
 # which original-states refers to states larger than those in A.  Some version
@@ -439,4 +441,4 @@ State: 10 [!0&1] 4 [0&1] 8 [!0&!1] 10 {0 1 2 3 5} [0&!1] 13 {1 2 3} State: 11
 si = spot.scc_info(aut15)
 aut15b = si.split_on_sets(2, [])[0]; d
 aut15c = spot.partial_degeneralize(aut15b)
-assert aut15c.equivalent_to(aut15b)
+tc.assertTrue(aut15c.equivalent_to(aut15b))

tests/python/prodexpt.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016-2017, 2019-2020 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2016-2017, 2019-2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 # make sure that we are not allowed to build the product of two automata with
 # different dictionaries.
@@ -94,14 +96,14 @@ State: 60 40 38 60 68 State: 61 40 41 57 61 State: 62 40 59 44 62 State:
 State: 70 40 59 57 70 State: 71 40 63 57 71 State: 72 40 69 57 72 --END--
 ''')
 res = spot.product(left, right)
-assert res.num_states() == 977
-assert res.num_edges() == 8554
+tc.assertEqual(res.num_states(), 977)
+tc.assertEqual(res.num_edges(), 8554)
 res = spot.product(left, right, spot.output_aborter(1000, 6000))
-assert res is None
+tc.assertIsNone(res)
 res = spot.product(left, right, spot.output_aborter(900, 9000))
-assert res is None
+tc.assertIsNone(res)
 res = spot.product(left, right, spot.output_aborter(1000, 9000))
-assert res is not None
+tc.assertIsNotNone(res)
 
 a, b = spot.automata("""HOA: v1 States: 1 Start: 0 AP: 0 acc-name: all
 Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete
@@ -110,7 +112,7 @@ properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0
 properties: trans-labels explicit-labels state-acc complete properties:
 deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 --END--""")
 out = spot.product(a, b).to_str()
-assert out == """HOA: v1
+tc.assertEqual(out, """HOA: v1
 States: 1
 Start: 0
 AP: 0
@@ -120,9 +122,9 @@ properties: trans-labels explicit-labels state-acc deterministic
 properties: stutter-invariant terminal
 --BODY--
 State: 0
---END--"""
+--END--""")
 out = spot.product_susp(a, b).to_str()
-assert out == """HOA: v1
+tc.assertEqual(out, """HOA: v1
 States: 1
 Start: 0
 AP: 0
@@ -132,4 +134,4 @@ properties: trans-labels explicit-labels state-acc deterministic
 properties: stutter-invariant terminal
 --BODY--
 State: 0
---END--"""
+--END--""")

tests/python/randgen.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2015, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,9 +18,11 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 o = spot.option_map()
 g = spot.randltlgenerator(0, o)
-assert str(g.next()) == '1'
-assert str(g.next()) == '0'
-assert str(g.next()) == 'None'
+tc.assertEqual(str(g.next()), '1')
+tc.assertEqual(str(g.next()), '0')
+tc.assertEqual(str(g.next()), 'None')

tests/python/relabel.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2019  Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2015, 2017-2019, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 f = spot.formula('GF(a & b) -> (FG(a & b) & Gc)')
 m = spot.relabeling_map()
@@ -26,19 +28,18 @@ res = ""
 for old, new in m.items():
     res += "#define {} {}\n".format(old, new)
 res += str(g)
-print(res)
-assert(res == """#define p0 a & b
+tc.assertEqual(res, """#define p0 a & b
 #define p1 c
 GFp0 -> (FGp0 & Gp1)""")
 
 h = spot.relabel_apply(g, m)
-assert h == f
+tc.assertEqual(h, f)
 
 autg = g.translate()
 spot.relabel_here(autg, m)
-assert str(autg.ap()) == \
-    '(spot.formula("a"), spot.formula("b"), spot.formula("c"))'
-assert spot.isomorphism_checker.are_isomorphic(autg, f.translate())
+tc.assertEqual(str(autg.ap()), \
+    '(spot.formula("a"), spot.formula("b"), spot.formula("c"))')
+tc.assertTrue(spot.isomorphism_checker.are_isomorphic(autg, f.translate()))
 
 a = spot.formula('a')
 u = spot.formula('a U b')
@@ -46,11 +47,11 @@ m[a] = u
 try:
     spot.relabel_here(autg, m)
 except RuntimeError as e:
-    assert "new labels" in str(e)
+    tc.assertIn("new labels", str(e))
 
 m = spot.relabeling_map()
 m[u] = a
 try:
     spot.relabel_here(autg, m)
 except RuntimeError as e:
-    assert "old labels" in str(e)
+    tc.assertIn("old labels", str(e))

tests/python/remfin.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et Développement de
-# l'Epita
+# Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 # This test used to trigger an assertion (or a segfault)
 # in scc_filter_states().
@@ -41,7 +43,7 @@ State: 2
 aut.prop_inherently_weak(True)
 aut = spot.dualize(aut)
 aut1 = spot.scc_filter_states(aut)
-assert(aut1.to_str('hoa') == """HOA: v1
+tc.assertEqual(aut1.to_str('hoa'), """HOA: v1
 States: 2
 Start: 0
 AP: 1 "a"
@@ -56,17 +58,17 @@ State: 1
 [t] 1
 --END--""")
 
-assert(aut.scc_filter_states().to_str() == aut1.to_str())
-assert(aut1.get_name() == None)
+tc.assertEqual(aut.scc_filter_states().to_str(), aut1.to_str())
+tc.assertIsNone(aut1.get_name())
 aut1.set_name("test me")
-assert(aut1.get_name() == "test me")
+tc.assertEqual(aut1.get_name(), "test me")
 # The method is the same as the function
 
 a = spot.translate('true', 'low', 'any')
-assert(a.prop_universal().is_maybe())
-assert(a.prop_unambiguous().is_maybe())
-assert(a.is_deterministic() == True)
-assert(a.is_unambiguous() == True)
+tc.assertTrue(a.prop_universal().is_maybe())
+tc.assertTrue(a.prop_unambiguous().is_maybe())
+tc.assertTrue(a.is_deterministic())
+tc.assertTrue(a.is_unambiguous())
 
 a = spot.automaton("""
 HOA: v1
@@ -92,4 +94,4 @@ State: 2
 """)
 b = spot.remove_fin(a)
 size = (b.num_states(), b.num_edges())
-assert size == (5, 13);
+tc.assertEqual(size, (5, 13))

tests/python/removeap.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019  Laboratoire de Recherche et Développement
+# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,16 +18,18 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 
 aut = spot.translate('a U (c & Gb)')
-assert not spot.is_terminal_automaton(aut)
-assert aut.prop_terminal().is_false()
+tc.assertFalse(spot.is_terminal_automaton(aut))
+tc.assertTrue(aut.prop_terminal().is_false())
 rem = spot.remove_ap()
 rem.add_ap("b")
 aut = rem.strip(aut)
-assert not aut.prop_terminal().is_false()
-assert spot.is_terminal_automaton(aut)
-assert aut.prop_terminal().is_true()
+tc.assertFalse(aut.prop_terminal().is_false())
+tc.assertTrue(spot.is_terminal_automaton(aut))
+tc.assertTrue(aut.prop_terminal().is_true())
 aut = rem.strip(aut)
-assert aut.prop_terminal().is_true()
+tc.assertTrue(aut.prop_terminal().is_true())

tests/python/rs_like.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.vector_rs_pair()
 
@@ -30,12 +32,13 @@ mall = spot.mark_t()
 
 def test_rs(acc, rs, expected_res, expected_pairs):
     res, p = getattr(acc, 'is_' + rs + '_like')()
-    assert res == expected_res
+    tc.assertEqual(res, expected_res)
     if expected_res:
         expected_pairs.sort()
         p = sorted(p)
         for a, b in zip(p, expected_pairs):
-            assert a.fin == b.fin and a.inf == b.inf
+            tc.assertEqual(a.fin, b.fin)
+            tc.assertEqual(a.inf, b.inf)
 
 
 def switch_pairs(pairs):

tests/python/satmin.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2020, 2021  Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2015, 2020, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,232 +18,234 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 
 aut = spot.translate('GFa & GFb', 'Buchi', 'SBAcc')
-assert aut.num_sets() == 1
-assert aut.num_states() == 3
-assert aut.is_deterministic()
+tc.assertEqual(aut.num_sets(), 1)
+tc.assertEqual(aut.num_states(), 3)
+tc.assertTrue(aut.is_deterministic())
 
 
 min1 = spot.sat_minimize(aut, acc='Rabin 1')
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_langmap=True)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=0)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=2)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=50)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=-1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=0)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=1)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=2)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=50)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_naive=True)
-assert min1.num_sets() == 2
-assert min1.num_states() == 2
+tc.assertEqual(min1.num_sets(), 2)
+tc.assertEqual(min1.num_states(), 2)
 
 
 min2 = spot.sat_minimize(aut, acc='Streett 2')
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_langmap=True)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=0)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=2)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=50)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=-1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=0)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=1)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=2)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=50)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_naive=True)
-assert min2.num_sets() == 4
-assert min2.num_states() == 1
+tc.assertEqual(min2.num_sets(), 4)
+tc.assertEqual(min2.num_states(), 1)
 
 
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_langmap=True)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=1,
                          sat_incr_steps=0)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=1,
                          sat_incr_steps=1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=1,
                          sat_incr_steps=2)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=1,
                          sat_incr_steps=50)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=2)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=2,
                          sat_incr_steps=-1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=2,
                          sat_incr_steps=0)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=2,
                          sat_incr_steps=1)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=2,
                          sat_incr_steps=2)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_incr=2,
                          sat_incr_steps=50)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 min3 = spot.sat_minimize(aut, acc='Rabin 2',
                          state_based=True, max_states=5, sat_naive=True)
-assert min3.num_sets() == 4
-assert min3.num_states() == 3
+tc.assertEqual(min3.num_sets(), 4)
+tc.assertEqual(min3.num_states(), 3)
 
 
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_langmap=True)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=1, sat_incr_steps=0)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=1, sat_incr_steps=1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=1, sat_incr_steps=2)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=1, sat_incr_steps=50)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=2)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=2, sat_incr_steps=-1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=2, sat_incr_steps=0)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=2, sat_incr_steps=1)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=2, sat_incr_steps=2)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_incr=2, sat_incr_steps=50)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 min4 = spot.sat_minimize(aut, acc='parity max odd 3',
                          colored=True, sat_naive=True)
-assert min4.num_sets() == 3
-assert min4.num_states() == 2
+tc.assertEqual(min4.num_sets(), 3)
+tc.assertEqual(min4.num_states(), 2)
 
 
 aut = spot.translate('GFa')
-assert aut.num_sets() == 1
-assert aut.num_states() == 1
-assert aut.is_deterministic()
+tc.assertEqual(aut.num_sets(), 1)
+tc.assertEqual(aut.num_states(), 1)
+tc.assertTrue(aut.is_deterministic())
 out = spot.sat_minimize(aut, state_based=True)
-assert out.num_states() == 2
+tc.assertEqual(out.num_states(), 2)
 out = spot.sat_minimize(aut, state_based=True, max_states=1)
-assert out is None
+tc.assertTrue(out is None)

tests/python/sbacc.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017-2018, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017-2018, 2021, 2022 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -18,13 +18,15 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
-aut = spot.translate('GFa')
-assert aut.num_states() == 1
-assert not aut.prop_state_acc().is_true()
-aut = spot.sbacc(aut)
-assert aut.num_states() == 2
-assert aut.prop_state_acc().is_true()
+from unittest import TestCase
+tc = TestCase()
 
+aut = spot.translate('GFa')
+tc.assertEqual(aut.num_states(), 1)
+tc.assertFalse(aut.prop_state_acc().is_true())
+aut = spot.sbacc(aut)
+tc.assertEqual(aut.num_states(), 2)
+tc.assertTrue(aut.prop_state_acc().is_true())
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -48,7 +50,7 @@ s = spot.sbacc(aut)
 s.copy_state_names_from(aut)
 h = s.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 2
 Start: 0
 AP: 2 "a" "b"
@@ -59,7 +61,7 @@ State: 0 "0"
 [0] 1
 State: 1 "2" {1}
 [t] 1
---END--"""
+--END--""")
 
 aut = spot.automaton("""HOA: v1
 States: 3
@@ -83,7 +85,7 @@ d = spot.degeneralize(aut)
 d.copy_state_names_from(aut)
 h = d.to_str('hoa')
 
-assert h == """HOA: v1
+tc.assertEqual(h, """HOA: v1
 States: 2
 Start: 0
 AP: 2 "a" "b"
@@ -95,4 +97,4 @@ State: 0 "0#0"
 [0] 1
 State: 1 "2#0" {0}
 [t] 1
---END--"""
+--END--""")

tests/python/sccfilter.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -22,6 +22,8 @@
 # Major)
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.automaton("""
 HOA: v1.1
@@ -43,7 +45,7 @@ State: 1 "bar"
 --END--
 """)
 
-assert (spot.scc_filter(a, True).to_str('hoa', '1.1') == """HOA: v1.1
+tc.assertEqual(spot.scc_filter(a, True).to_str('hoa', '1.1'), """HOA: v1.1
 States: 2
 Start: 0
 AP: 1 "a"

tests/python/sccinfo.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.translate('(Ga -> Gb) W c')
 
@@ -26,11 +28,11 @@ try:
     si = spot.scc_info(a, 10)
     exit(2)
 except RuntimeError as e:
-    assert "initial state does not exist" in str(e)
+    tc.assertIn("initial state does not exist", str(e))
 
 si = spot.scc_info(a)
 n = si.scc_count()
-assert n == 4
+tc.assertEqual(n, 4)
 
 acc = 0
 rej = 0
@@ -39,24 +41,24 @@ for i in range(n):
     acc += si.is_accepting_scc(i)
     rej += si.is_rejecting_scc(i)
     triv += si.is_trivial(i)
-assert acc == 3
-assert rej == 1
-assert triv == 0
+tc.assertEqual(acc, 3)
+tc.assertEqual(rej, 1)
+tc.assertEqual(triv, 0)
 
 for scc in si:
     acc -= scc.is_accepting()
     rej -= scc.is_rejecting()
     triv -= scc.is_trivial()
-assert acc == 0
-assert rej == 0
-assert triv == 0
+tc.assertEqual(acc, 0)
+tc.assertEqual(rej, 0)
+tc.assertEqual(triv, 0)
 
 l0 = si.states_of(0)
 l1 = si.states_of(1)
 l2 = si.states_of(2)
 l3 = si.states_of(3)
 l = sorted(list(l0) + list(l1) + list(l2) + list(l3))
-assert l == [0, 1, 2, 3, 4]
+tc.assertEqual(l, [0, 1, 2, 3, 4])
 
 i = si.initial()
 todo = [i]
@@ -73,14 +75,14 @@ while todo:
         if s not in seen:
             seen.add(s)
             todo.append(s)
-assert seen == {0, 1, 2, 3}
-assert trans == [(0, 0), (0, 1), (0, 2), (0, 3),
-                 (2, 0), (2, 1), (2, 2), (2, 4),
-                 (3, 3), (4, 1), (4, 4), (1, 1)]
-assert transi == [(0, 0, 1), (0, 2, 3), (2, 0, 6),
-                  (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)]
+tc.assertEqual(seen, {0, 1, 2, 3})
+tc.assertEqual(trans, [(0, 0), (0, 1), (0, 2), (0, 3),
+                       (2, 0), (2, 1), (2, 2), (2, 4),
+                       (3, 3), (4, 1), (4, 4), (1, 1)])
+tc.assertEqual(transi, [(0, 0, 1), (0, 2, 3), (2, 0, 6),
+                        (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)])
 
-assert not spot.is_weak_automaton(a, si)
+tc.assertFalse(spot.is_weak_automaton(a, si))
 
 
 a = spot.automaton("""
@@ -107,8 +109,8 @@ State: 3
 """)
 si = spot.scc_info(a)
 si.determine_unknown_acceptance()
-assert si.scc_count() == 2
-assert si.is_accepting_scc(0)
-assert not si.is_rejecting_scc(0)
-assert si.is_rejecting_scc(1)
-assert not si.is_accepting_scc(1)
+tc.assertEqual(si.scc_count(), 2)
+tc.assertTrue(si.is_accepting_scc(0))
+tc.assertFalse(si.is_rejecting_scc(0))
+tc.assertTrue(si.is_rejecting_scc(1))
+tc.assertFalse(si.is_accepting_scc(1))

tests/python/sccsplit.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
+# de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,9 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
+
 
 aut = spot.translate('GF(a <-> Xa) & GF(b <-> XXb)')
 si = spot.scc_info(aut)
@@ -27,4 +30,4 @@ for aut2 in si.split_on_sets(0, [0]):
     # This call to to_str() used to fail because split_on_sets had not
     # registered the atomic propositions of aut
     s += aut2.to_str()
-assert spot.automaton(s).num_states() == 8
+tc.assertEqual(spot.automaton(s).num_states(), 8)

tests/python/semidet.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 formulas = [('(Gp0 | Fp1) M 1', False, True),
             ('(!p1 U p1) U X(!p0 -> Fp1)', False, True),
@@ -31,9 +33,9 @@ for f, isd, issd in formulas:
     aut = spot.translate(f)
     # The formula with isd=True, issd=True is the only one
     # for which both properties are already set.
-    assert (aut.prop_deterministic().is_maybe() or
-            aut.prop_semi_deterministic().is_maybe() or
-            isd == issd)
+    tc.assertTrue(aut.prop_deterministic().is_maybe() or
+                  aut.prop_semi_deterministic().is_maybe() or
+                  isd == issd)
     spot.check_determinism(aut)
-    assert aut.prop_deterministic() == isd
-    assert aut.prop_semi_deterministic() == issd
+    tc.assertEqual(aut.prop_deterministic(), isd)
+    tc.assertEqual(aut.prop_semi_deterministic(), issd)

tests/python/setacc.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2018, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2016, 2018, 2021, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,54 +19,56 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 
 # Test case reduced from a report from Juraj Major <major@fi.muni.cz>.
 a = spot.make_twa_graph(spot._bdd_dict)
 a.set_acceptance(0, spot.acc_code("t"))
-assert(a.prop_state_acc() == True)
+tc.assertTrue(a.prop_state_acc())
 a.set_acceptance(1, spot.acc_code("Fin(0)"))
-assert(a.prop_state_acc() == spot.trival.maybe())
+tc.assertEqual(a.prop_state_acc(), spot.trival.maybe())
 
 
 # Some tests for used_inf_fin_sets(), which return a pair of mark_t.
 (inf, fin) = a.get_acceptance().used_inf_fin_sets()
-assert inf == []
-assert fin == [0]
+tc.assertEqual(inf, [])
+tc.assertEqual(fin, [0])
 (inf, fin) = spot.acc_code("(Fin(0)|Inf(1))&Fin(2)&Inf(0)").used_inf_fin_sets()
-assert inf == [0, 1]
-assert fin == [0, 2]
+tc.assertEqual(inf, [0, 1])
+tc.assertEqual(fin, [0, 2])
 
 # is_rabin_like() returns (bool, [(inf, fin), ...])
 (b, v) = spot.acc_cond("(Fin(0)&Inf(1))|(Fin(2)&Inf(0))").is_rabin_like()
-assert b == True
-assert len(v) == 2
-assert v[0].fin == [0]
-assert v[0].inf == [1]
-assert v[1].fin == [2]
-assert v[1].inf == [0]
+tc.assertTrue(b)
+tc.assertEqual(len(v), 2)
+tc.assertEqual(v[0].fin, [0])
+tc.assertEqual(v[0].inf, [1])
+tc.assertEqual(v[1].fin, [2])
+tc.assertEqual(v[1].inf, [0])
 (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_rabin_like()
-assert b == False
-assert len(v) == 0
+tc.assertFalse(b)
+tc.assertEqual(len(v), 0)
 (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_streett_like()
-assert b == True
-assert repr(v) == \
-    '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))'
+tc.assertTrue(b)
+tc.assertEqual(repr(v), \
+    '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))')
 v2 = (spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))
-assert v == v2
+tc.assertEqual(v, v2)
 
 acc = spot.acc_cond("generalized-Rabin 1 2")
 (b, v) = acc.is_generalized_rabin()
-assert b == True
-assert v == (2,)
+tc.assertTrue(b)
+tc.assertEqual(v, (2,))
 (b, v) = acc.is_generalized_streett()
-assert b == False
-assert v == ()
+tc.assertFalse(b)
+tc.assertEqual(v, ())
 (b, v) = acc.is_streett_like()
-assert b == True
+tc.assertTrue(b)
 ve = (spot.rs_pair([0], []), spot.rs_pair([], [1]), spot.rs_pair([], [2]))
-assert v == ve
-assert acc.name() == "generalized-Rabin 1 2"
+tc.assertEqual(v, ve)
+tc.assertEqual(acc.name(), "generalized-Rabin 1 2")
 
 # At the time of writting, acc_cond does not yet recognize
 # "generalized-Streett", as there is no definition for that in the HOA format,
@@ -74,23 +76,23 @@ assert acc.name() == "generalized-Rabin 1 2"
 # being a generalized-Streett.  See issue #249.
 acc = spot.acc_cond("Inf(0)|Fin(1)|Fin(2)")
 (b, v) = acc.is_generalized_streett()
-assert b == True
-assert v == (2,)
+tc.assertTrue(b)
+tc.assertEqual(v, (2,))
 (b, v) = acc.is_generalized_rabin()
-assert b == False
-assert v == ()
+tc.assertFalse(b)
+tc.assertEqual(v, ())
 # FIXME: We should have a way to disable the following output, as it is not
 # part of HOA v1.
-assert acc.name() == "generalized-Streett 1 2"
+tc.assertEqual(acc.name(), "generalized-Streett 1 2")
 
 
 # issue #469.  This test is meaningful only if Spot is compiled with
 # --enable-max-accsets=64 or more.
 try:
     m = spot.mark_t([33])
-    assert m.lowest() == m
+    tc.assertEqual(m.lowest(), m)
     n = spot.mark_t([33,34])
-    assert n.lowest() == m
+    tc.assertEqual(n.lowest(), m)
 except RuntimeError as e:
     if "Too many acceptance sets used." in str(e):
         pass
@@ -102,24 +104,24 @@ except RuntimeError as e:
 from gc import collect
 acc = spot.translate('a').acc()
 collect()
-assert acc == spot.acc_cond('Inf(0)')
+tc.assertEqual(acc, spot.acc_cond('Inf(0)'))
 acc = spot.translate('b').get_acceptance()
 collect()
-assert acc == spot.acc_code('Inf(0)')
+tc.assertEqual(acc, spot.acc_code('Inf(0)'))
 
 
 c = spot.acc_cond('Fin(0)&Fin(1)&(Inf(2)|Fin(3))')
 m1 = c.fin_unit()
 m2 = c.inf_unit()
-assert m1 == [0,1]
-assert m2 == []
+tc.assertEqual(m1, [0,1])
+tc.assertEqual(m2, [])
 c = spot.acc_cond('Inf(0)&Inf(1)&(Inf(2)|Fin(3))')
 m1 = c.fin_unit()
 m2 = c.inf_unit()
-assert m1 == []
-assert m2 == [0,1]
+tc.assertEqual(m1, [])
+tc.assertEqual(m2, [0,1])
 c = spot.acc_cond('Inf(0)&Inf(1)|(Inf(2)|Fin(3))')
 m1 = c.fin_unit()
 m2 = c.inf_unit()
-assert m1 == []
-assert m2 == []
+tc.assertEqual(m1, [])
+tc.assertEqual(m2, [])

tests/python/setxor.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement
-# de l'EPITA.
+# Copyright (C) 2010, 2011, 2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 
 import sys
 from buddy import *
+from unittest import TestCase
+tc = TestCase()
 
 bdd_init(10000, 10000)
 bdd_setvarnum(5)
@@ -29,18 +31,18 @@ a = V[0] & -V[1] & V[2] & -V[3]
 b = V[0] & V[1] & V[2] & -V[3]
 c = -V[0] & V[1] & -V[2] & -V[3]
 
-assert(c == bdd_setxor(a, b))
-assert(c == bdd_setxor(b, a))
-assert(a == bdd_setxor(b, c))
-assert(a == bdd_setxor(c, b))
-assert(b == bdd_setxor(a, c))
-assert(b == bdd_setxor(c, a))
+tc.assertEqual(c, bdd_setxor(a, b))
+tc.assertEqual(c, bdd_setxor(b, a))
+tc.assertEqual(a, bdd_setxor(b, c))
+tc.assertEqual(a, bdd_setxor(c, b))
+tc.assertEqual(b, bdd_setxor(a, c))
+tc.assertEqual(b, bdd_setxor(c, a))
 
 d = V[1] & V[2] & -V[3] & V[4]
 e = V[0] & V[1] & -V[2] & -V[3] & V[4]
 
-assert(e == bdd_setxor(a, d))
-assert(e == bdd_setxor(d, a))
+tc.assertEqual(e, bdd_setxor(a, d))
+tc.assertEqual(e, bdd_setxor(d, a))
 
 # Cleanup all BDD variables before calling bdd_done(), otherwise
 # bdd_delref will be called after bdd_done() and this is unsafe in

tests/python/simplacc.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita
 # (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 
 auts = list(spot.automata("""
@@ -70,19 +72,19 @@ explicit-labels trans-acc deterministic --BODY-- State: 0 [0&!1] 0 {2 3}
 res = []
 for a in auts:
     b = spot.simplify_acceptance(a)
-    assert b.equivalent_to(a)
+    tc.assertTrue(b.equivalent_to(a))
     res.append(str(b.get_acceptance()))
     c = spot.simplify_acceptance(b)
-    assert b.get_acceptance() == c.get_acceptance()
+    tc.assertEqual(b.get_acceptance(), c.get_acceptance())
 
     a.set_acceptance(a.num_sets(), a.get_acceptance().complement())
     b = spot.simplify_acceptance(a)
-    assert b.equivalent_to(a)
+    tc.assertTrue(b.equivalent_to(a))
     res.append(str(b.get_acceptance()))
     c = spot.simplify_acceptance(b)
-    assert b.get_acceptance() == c.get_acceptance()
+    tc.assertEqual(b.get_acceptance(), c.get_acceptance())
 
-assert res == [
+tc.assertEqual(res, [
     'Inf(0)',
     'Fin(0)',
     'Inf(1) & Fin(0)',
@@ -101,4 +103,4 @@ assert res == [
     '(Inf(0) | Fin(2)) & Inf(1)',
     '(Fin(2) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2))',
     '(Inf(2) | (Fin(1) & Inf(0))) & (Fin(0)|Fin(2))',
-    ]
+    ])

tests/python/simstate.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2015, 2017-2018, 2020-2021  Laboratoire de Recherche
+# Copyright (C) 2015, 2017-2018, 2020-2022  Laboratoire de Recherche
 # et Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
 
 import spot
 from sys import exit
+from unittest import TestCase
+tc = TestCase()
 
 # CPython use reference counting, so that automata are destructed
 # when we expect them to be.   However other implementations like
@@ -48,7 +50,7 @@ State: 1
 """)
 
 aut2 = spot.simulation(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
@@ -59,10 +61,10 @@ properties: deterministic
 --BODY--
 State: 0 {0}
 [t] 0
---END--"""
+--END--""")
 
 aut2.copy_state_names_from(aut)
-assert aut2.to_str() == """HOA: v1
+tc.assertEqual(aut2.to_str(), """HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
@@ -73,7 +75,7 @@ properties: deterministic
 --BODY--
 State: 0 "[0,1]" {0}
 [t] 0
---END--"""
+--END--""")
 
 del aut
 del aut2
@@ -82,7 +84,7 @@ gcollect()
 aut = spot.translate('GF((p0 -> Gp0) R p1)')
 
 daut = spot.tgba_determinize(aut, True)
-assert daut.to_str() == """HOA: v1
+tc.assertEqual(daut.to_str(), """HOA: v1
 States: 3
 Start: 0
 AP: 2 "p1" "p0"
@@ -106,7 +108,7 @@ State: 2 "{₀[0]₀}{₁[1]₁}"
 [!0&1] 2
 [0&!1] 0 {0}
 [0&1] 1 {2}
---END--"""
+--END--""")
 
 del aut
 del daut
@@ -129,7 +131,7 @@ State: 1
 """)
 
 daut = spot.tgba_determinize(aut, True)
-assert daut.to_str() == """HOA: v1
+tc.assertEqual(daut.to_str(), """HOA: v1
 States: 12
 Start: 0
 AP: 2 "a" "b"
@@ -185,18 +187,18 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}"
 [!0&1] 2 {0}
 [0&!1] 6 {0}
 [0&1] 9 {0}
---END--"""
+--END--""")
 
 a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)')
 a = spot.degeneralize_tba(a)
-assert a.num_states() == 8
+tc.assertEqual(a.num_states(), 8)
 b = spot.simulation(a)
-assert b.num_states() == 3
+tc.assertEqual(b.num_states(), 3)
 b.set_init_state(1)
 b.purge_unreachable_states()
 b.copy_state_names_from(a)
 
-assert b.to_str() == """HOA: v1
+tc.assertEqual(b.to_str(), """HOA: v1
 States: 1
 Start: 0
 AP: 2 "p0" "p1"
@@ -208,7 +210,7 @@ properties: deterministic stutter-invariant
 State: 0 "[1,7]"
 [1] 0
 [!1] 0 {0}
---END--"""
+--END--""")
 
 aut = spot.automaton('''HOA: v1
 States: 12
@@ -267,7 +269,7 @@ State: 11
 [0&!1] 6 {0}
 [0&1] 9 {0}
 --END--''')
-assert spot.reduce_iterated(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1
 States: 9
 Start: 0
 AP: 2 "a" "b"
@@ -308,7 +310,7 @@ State: 8
 [0&!1] 4 {0}
 [!0&1] 6
 [0&1] 7
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 States: 6
@@ -332,7 +334,7 @@ State: 4
 State: 5
 [0] 5
 --END--''')
-assert spot.reduce_iterated(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -347,7 +349,7 @@ State: 1
 [0] 2
 State: 2
 [1] 2
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 States: 5
@@ -374,7 +376,7 @@ State: 4
 [0&1&!2&3] 4 {0}
 --END--''')
 
-assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1
 States: 5
 Start: 0
 AP: 4 "p0" "p2" "p3" "p1"
@@ -395,7 +397,7 @@ State: 3
 [0&!1&2&3] 3 {1}
 State: 4
 [0&!1&2&3] 4 {0}
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 States: 2
@@ -410,7 +412,7 @@ State: 0
 State: 1
 [0] 0
 --END--''')
-assert spot.reduce_direct_sim(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_sim(aut).to_str(), '''HOA: v1
 States: 1
 Start: 0
 AP: 2 "a" "b"
@@ -418,7 +420,7 @@ Acceptance: 2 Fin(0) & Fin(1)
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 name: "(p1 U p2) U p3"
@@ -445,7 +447,7 @@ State: 3
 [1] 1
 [0&!1] 3
 --END--''')
-assert spot.reduce_direct_cosim_sba(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_cosim_sba(aut).to_str(), '''HOA: v1
 States: 4
 Start: 0
 AP: 3 "p2" "p3" "p1"
@@ -468,7 +470,7 @@ State: 2
 State: 3
 [0] 1
 [!0&2] 3
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 States: 4
@@ -488,7 +490,7 @@ State: 2
 State: 3 {0}
 [1] 3
 --END--''')
-assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1
 States: 3
 Start: 0
 AP: 2 "a" "b"
@@ -502,9 +504,9 @@ State: 1
 [1] 2
 State: 2 {0}
 [1] 2
---END--'''
+--END--''')
 
-assert spot.reduce_direct_sim_sba(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_direct_sim_sba(aut).to_str(), '''HOA: v1
 States: 2
 Start: 0
 AP: 2 "a" "b"
@@ -516,7 +518,7 @@ State: 0
 [0] 1
 State: 1 {0}
 [1] 1
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 States: 3
@@ -532,7 +534,7 @@ State: 1
 State: 2 {0}
 [0] 2
 --END--''')
-assert spot.reduce_iterated_sba(aut).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated_sba(aut).to_str(), '''HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
@@ -542,7 +544,7 @@ properties: deterministic
 --BODY--
 State: 0 {0}
 [0] 0
---END--'''
+--END--''')
 
 aut = spot.automaton('''HOA: v1
 States: 30
@@ -630,7 +632,7 @@ State: 28
 State: 29
 [0&!1&!2&!3] 29
 --END--''')
-assert spot.reduce_iterated(a).to_str() == '''HOA: v1
+tc.assertEqual(spot.reduce_iterated(a).to_str(), '''HOA: v1
 States: 8
 Start: 0
 AP: 2 "p0" "p1"
@@ -669,7 +671,7 @@ State: 7
 [!1] 1 {0}
 [0&1] 5
 [1] 7
---END--'''
+--END--''')
 
 
 # issue #452
@@ -707,4 +709,4 @@ State: 8
 [@p] 3 {0 1}
 --END--""")
 aut = spot.simulation(aut)
-assert aut.num_states() == 1
+tc.assertEqual(aut.num_states(), 1)

tests/python/sonf.py

@@ -0,0 +1,43 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita
+# (LRDE).
+#
+# 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/>.
+
+import spot
+from unittest import TestCase
+tc = TestCase()
+
+formulas = """\
+{x[*]}[]-> F({y[*]}<>-> GFz)
+<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17)))
+{{true} || {[*0]}}[]-> (false)
+{{p14} & {{p0}[*]}}[]-> (p11)
+{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18)))))
+"""
+
+for f1 in formulas.splitlines():
+    f1 = spot.formula(f1)
+    a1 = spot.translate(f1)
+
+    f2, aps = spot.suffix_operator_normal_form(f1, 'sonf_')
+    a2 = spot.translate(f2)
+    rm = spot.remove_ap()
+    for ap in aps:
+        rm.add_ap(ap)
+    a2 = rm.strip(a2)
+
+    tc.assertTrue(spot.are_equivalent(a1, a2))

tests/python/split.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2021 Laboratoire de Recherche et
+# Copyright (C) 2018-2022 Laboratoire de Recherche et
 # Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -19,6 +19,8 @@
 
 import spot
 import buddy
+from unittest import TestCase
+tc = TestCase()
 
 # CPython use reference counting, so that automata are destructed
 # when we expect them to be.   However other implementations like
@@ -51,16 +53,17 @@ def do_split(f, out_list):
     return aut, s
 
 aut, s = do_split('(FG !a) <-> (GF b)', ['b'])
-assert equiv(aut, spot.unsplit_2step(s))
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
 
 del aut
 del s
 gcollect()
 
 aut, s = do_split('GFa && GFb', ['b'])
-assert equiv(aut, spot.unsplit_2step(s))
-# FIXME see below
-# assert str_diff("""HOA: v1
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
+# FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable
+#       we should investigate this.  See Issue #502.
+# tc.assertEqual("""HOA: v1
 # States: 3
 # Start: 0
 # AP: 2 "a" "b"
@@ -86,10 +89,11 @@ del s
 gcollect()
 
 aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['ack'])
-assert equiv(aut, spot.unsplit_2step(s))
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))
+
 # FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable
-#       we should investigate this
-# assert s.to_str() == """HOA: v1
+#       we should investigate this.  See Issue #502.
+# tc.assertEqual(s.to_str(), """HOA: v1
 # States: 9
 # Start: 0
 # AP: 4 "ack" "req" "go" "grant"
@@ -122,7 +126,7 @@ assert equiv(aut, spot.unsplit_2step(s))
 # [!0] 1
 # State: 8 {0}
 # [!3] 2
-# --END--"""
+# --END--""")
 
 del aut
 del s
@@ -131,4 +135,4 @@ gcollect()
 aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \
     && g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))',
                   ['g_0', 'g_1'])
-assert equiv(aut, spot.unsplit_2step(s))
+tc.assertTrue(equiv(aut, spot.unsplit_2step(s)))

tests/python/streett_totgba.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2017-2018, 2021-2022 Laboratoire de Recherche et
+# Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,7 +22,8 @@ import spot
 import os
 import shutil
 import sys
-
+from unittest import TestCase
+tc = TestCase()
 
 def tgba(a):
     if not a.is_existential():
@@ -33,11 +34,11 @@ def tgba(a):
 
 def test_aut(aut):
     stgba = tgba(aut)
-    assert stgba.equivalent_to(aut)
+    tc.assertTrue(stgba.equivalent_to(aut))
     os.environ["SPOT_STREETT_CONV_MIN"] = '1'
     sftgba = tgba(aut)
     del os.environ["SPOT_STREETT_CONV_MIN"]
-    assert stgba.equivalent_to(sftgba)
+    tc.assertTrue(stgba.equivalent_to(sftgba))
 
     slike = spot.simplify_acceptance(aut)
 
@@ -45,8 +46,7 @@ def test_aut(aut):
     os.environ["SPOT_STREETT_CONV_MIN"] = "1"
     slftgba = tgba(slike)
     del os.environ["SPOT_STREETT_CONV_MIN"]
-    assert sltgba.equivalent_to(slftgba)
-
+    tc.assertTrue(sltgba.equivalent_to(slftgba))
 
 if shutil.which('ltl2dstar') is None:
     sys.exit(77)

tests/python/streett_totgba2.py

@@ -1,7 +1,7 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
-# l'EPITA.
+# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
+# de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
 #
@@ -19,6 +19,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 # Issue 316
 a = spot.automaton("""
@@ -60,11 +62,11 @@ State: 7 {1 3 4}
 """)
 
 tgba = spot.streett_to_generalized_buchi(a)
-assert tgba.acc().is_generalized_buchi()
+tc.assertTrue(tgba.acc().is_generalized_buchi())
 ba = spot.simplify_acceptance(a)
-assert ba.acc().is_buchi()
+tc.assertTrue(ba.acc().is_buchi())
 
 nba = spot.dualize(ba.postprocess('generic', 'deterministic'))
 ntgba = spot.dualize(tgba.postprocess('generic', 'deterministic'))
-assert not ba.intersects(ntgba)
-assert not tgba.intersects(nba)
+tc.assertFalse(ba.intersects(ntgba))
+tc.assertFalse(tgba.intersects(nba))

tests/python/stutter.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2019-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2019-2022 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,6 +23,8 @@
 
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 
 def explain_stut(f):
@@ -45,20 +47,20 @@ def explain_stut(f):
 
 # Test from issue #388
 w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc')
-assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}'
-assert str(w2) == 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}'
+tc.assertEqual(str(w1), 'a & !b & !c; cycle{!a & b & !c}')
+tc.assertEqual(str(w2), 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}')
 
 # Test from issue #401
 w1, w2 = explain_stut('G({x} |-> ({x[+]} <>-> ({Y1[+]} <>=> Y2)))')
-assert str(w1) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}'
-assert str(w2) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}'
+tc.assertEqual(str(w1), 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}')
+tc.assertEqual(str(w2), 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}')
 
 # Related to issue #401 as well.  sl() and sl2() should upgrade
 # the t acceptance condition into inf(0).
 pos = spot.translate('Xa & XXb')
 w = pos.accepting_word().as_automaton()
-assert w.acc().is_t()
+tc.assertTrue(w.acc().is_t())
 a = spot.sl2(w)
-assert a.acc().is_buchi()
+tc.assertTrue(a.acc().is_buchi())
 a = spot.sl(w)
-assert a.acc().is_buchi()
+tc.assertTrue(a.acc().is_buchi())

tests/python/sum.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -20,6 +20,8 @@
 import spot
 import sys
 import itertools
+from unittest import TestCase
+tc = TestCase()
 
 # make sure that we are not allowed to build the sum of two automata with
 # different dictionaries.
@@ -65,8 +67,8 @@ for p in zip(phi1, phi2):
 
     p0orp1 = spot.formula.Or(p)
     a1ora2 = spot.remove_alternation(spot.sum(a1, a2), True)
-    assert p0orp1.equivalent_to(a1ora2)
+    tc.assertTrue(p0orp1.equivalent_to(a1ora2))
 
     p0andp1 = spot.formula.And(p)
     a1anda2 = spot.remove_alternation(spot.sum_and(a1, a2), True)
-    assert p0andp1.equivalent_to(a1anda2)
+    tc.assertTrue(p0andp1.equivalent_to(a1anda2))

tests/python/synthesis.py

@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 # A shared variable caused the 2nd call to ltl_to_game to give an incorrect
 # result.
@@ -25,11 +27,11 @@ for i in range(0, 2):
     gi = spot.synthesis_info()
     gi.s = spot.synthesis_info.algo_LAR
     game = spot.ltl_to_game("(Ga) <-> (Fb)", ["b"], gi)
-    assert not spot.solve_game(game)
+    tc.assertFalse(spot.solve_game(game))
 
 # A game can have only inputs
 game = spot.ltl_to_game("GFa", [])
-assert(game.to_str() == """HOA: v1
+tc.assertEqual(game.to_str(), """HOA: v1
 States: 3
 Start: 0
 AP: 1 "a"

tests/python/toparity.py

@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de
 # l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -21,6 +21,8 @@
 import spot
 from itertools import zip_longest
 from buddy import bddfalse
+from unittest import TestCase
+tc = TestCase()
 
 # Tests for the new version of to_parity
 
@@ -114,17 +116,16 @@ def test(aut, expected_num_states=[], full=True):
         if opt is not None and opt.parity_prefix is False:
             # Reduce the number of colors to help are_equivalent
             spot.reduce_parity_here(p1)
-        assert spot.are_equivalent(aut, p1)
+        tc.assertTrue(spot.are_equivalent(aut, p1))
         if expected_num is not None:
-            # print(p1.num_states(), expected_num)
-            assert p1.num_states() == expected_num
+            tc.assertEqual(p1.num_states(), expected_num)
         if full and opt is not None:
             # Make sure passing opt is the same as setting
             # each argument individually
             p2 = spot.to_parity(aut, opt)
-            assert p2.num_states() == p1st
-            assert p2.num_edges() == p1ed
-            assert p2.num_sets() == p1se
+            tc.assertEqual(p2.num_states(), p1st)
+            tc.assertEqual(p2.num_edges(), p1ed)
+            tc.assertEqual(p2.num_sets(), p1se)
 
 test(spot.automaton("""HOA: v1
 name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) &
@@ -351,7 +352,7 @@ State: 0
 [!0&!1] 0
 --END--""")
 p = spot.to_parity_old(a, True)
-assert spot.are_equivalent(a, p)
+tc.assertTrue(spot.are_equivalent(a, p))
 test(a)
 
 a = spot.automaton("""
@@ -363,8 +364,8 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4}
 4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END--
 """)
 p = spot.to_parity_old(a, True)
-assert p.num_states() == 22
-assert spot.are_equivalent(a, p)
+tc.assertEqual(p.num_states(), 22)
+tc.assertTrue(spot.are_equivalent(a, p))
 test(a, [8, 6, 6, 6, 6, 6, 6, 6])
 
 # Force a few edges to false, to make sure to_parity() is OK with that.
@@ -377,22 +378,22 @@ for e in a.out(3):
         e.cond = bddfalse
         break
 p = spot.to_parity_old(a, True)
-assert p.num_states() == 22
-assert spot.are_equivalent(a, p)
+tc.assertEqual(p.num_states(), 22)
+tc.assertTrue(spot.are_equivalent(a, p))
 test(a, [7, 6, 6, 6, 6, 6, 6, 6])
 
 for f in spot.randltl(4, 400):
     d = spot.translate(f, "det", "G")
     p = spot.to_parity_old(d, True)
-    assert spot.are_equivalent(p, d)
+    tc.assertTrue(spot.are_equivalent(p, d))
 
 for f in spot.randltl(5, 2000):
     n = spot.translate(f)
     p = spot.to_parity_old(n, True)
-    assert spot.are_equivalent(n, p)
+    tc.assertTrue(spot.are_equivalent(n, p))
 
 # Issue #390.
 a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det')
 b = spot.to_parity_old(a, True)
-assert a.equivalent_to(b)
+tc.assertTrue(a.equivalent_to(b))
 test(a, [7, 7, 3, 7, 7, 7, 3, 3])

tests/python/toweak.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2020  Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 phi1 = """GFb
 X(!b | GF!a)
@@ -33,7 +35,7 @@ b | (a & XF(b R a)) | (!a & XG(!b U !a))"""
 def test_phi(phi):
     a = spot.translate(phi, 'GeneralizedBuchi', 'SBAcc')
     res = spot.to_weak_alternating(spot.dualize(a))
-    assert res.equivalent_to(spot.formula.Not(spot.formula(phi)))
+    tc.assertTrue(res.equivalent_to(spot.formula.Not(spot.formula(phi))))
 
 
 for p in phi1.split('\n'):
@@ -83,4 +85,4 @@ State: 6
 --END--
 """)
 a2 = spot.to_weak_alternating(a2)
-assert a2.equivalent_to(phi2)
+tc.assertTrue(a2.equivalent_to(phi2))

tests/python/tra2tba.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016-2018, 2020-2021  Laboratoire de Recherche
+# Copyright (C) 2016-2018, 2020-2022  Laboratoire de Recherche
 # et Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 # CPython use reference counting, so that automata are destructed
 # when we expect them to be.   However other implementations like
@@ -57,7 +59,7 @@ State: 1
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 2.
 aut = spot.automaton("""
@@ -97,7 +99,7 @@ State: 2
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 3.
 aut = spot.automaton("""
@@ -128,7 +130,7 @@ State: 0
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 4.
 aut = spot.automaton("""
@@ -168,7 +170,7 @@ State: 2 {0}
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 5.
 aut = spot.automaton("""
@@ -214,7 +216,7 @@ State: 3 {0}
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 6.
 aut = spot.automaton("""
@@ -257,7 +259,7 @@ State: 2 {0}
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 7.
 aut = spot.automaton("""
@@ -292,7 +294,7 @@ State: 1 {0}
 --END--"""
 
 res = spot.remove_fin(aut)
-assert(res.to_str('hoa') == exp)
+tc.assertEqual(res.to_str('hoa'), exp)
 
 # Test 8.
 aut = spot.automaton("""
@@ -372,9 +374,9 @@ State: 7
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
 
 # Test 9.
 aut = spot.automaton("""
@@ -411,9 +413,9 @@ State: 1
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
 
 # Test 10.
 aut = spot.automaton("""
@@ -453,9 +455,9 @@ State: 2 {0}
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
 
 # Test 11.
 aut = spot.automaton("""
@@ -493,9 +495,9 @@ State: 1
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
 
 # Different order for rabin_to_buchi_if_realizable() due to merge_edges() not
 # being called.  This is on purpose: the edge order should match exactly the
@@ -518,9 +520,9 @@ State: 1
 --END--"""
 res = spot.rabin_to_buchi_if_realizable(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp2)
+    tc.assertEqual(res.to_str('hoa'), exp2)
 else:
-    assert(res.equivalent_to(spot.automaton(exp2)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp2)))
 
 # Test 12.
 aut = spot.automaton("""
@@ -565,9 +567,9 @@ State: 3 {0}
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
 
 # Test 13.
 aut = spot.automaton("""
@@ -615,9 +617,9 @@ State: 1
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
 
 # rabin_to_buchi_if_realizable() does not call merge_edges() on purpose: the
 # edge order should match exactly the original automaton.
@@ -644,9 +646,9 @@ State: 1
 
 res = spot.rabin_to_buchi_if_realizable(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp2)
+    tc.assertEqual(res.to_str('hoa'), exp2)
 else:
-    assert(res.equivalent_to(spot.automaton(exp2)))
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp2)))
 
 # Test 14.
 aut = spot.automaton("""
@@ -681,7 +683,7 @@ State: 1
 
 res = spot.remove_fin(aut)
 if is_cpython:
-    assert(res.to_str('hoa') == exp)
+    tc.assertEqual(res.to_str('hoa'), exp)
 else:
-    assert(res.equivalent_to(spot.automaton(exp)))
-assert spot.rabin_to_buchi_if_realizable(aut) is None
+    tc.assertTrue(res.equivalent_to(spot.automaton(exp)))
+tc.assertIsNone(spot.rabin_to_buchi_if_realizable(aut))

tests/python/trival.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2016, 2018  Laboratoire de Recherche et Développement
+# Copyright (C) 2016, 2018, 2022  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -18,30 +18,32 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 v1 = spot.trival()
 v2 = spot.trival(False)
 v3 = spot.trival(True)
 v4 = spot.trival_maybe()
-assert v1 != v2
-assert v1 != v3
-assert v2 != v3
-assert v2 == spot.trival(spot.trival.no_value)
-assert v2 != spot.trival(spot.trival.yes_value)
-assert v4 != v2
-assert v4 != v3
-assert v2 == False
-assert True == v3
-assert v2 != True
-assert False != v3
-assert v4 == spot.trival_maybe()
-assert v4 == spot.trival(spot.trival.maybe_value)
-assert v3
-assert -v2
-assert not -v1
-assert not v1
-assert not -v3
+tc.assertNotEqual(v1, v2)
+tc.assertNotEqual(v1, v3)
+tc.assertNotEqual(v2, v3)
+tc.assertEqual(v2, spot.trival(spot.trival.no_value))
+tc.assertNotEqual(v2, spot.trival(spot.trival.yes_value))
+tc.assertNotEqual(v4, v2)
+tc.assertNotEqual(v4, v3)
+tc.assertEqual(v2, False)
+tc.assertEqual(True, v3)
+tc.assertNotEqual(v2, True)
+tc.assertNotEqual(False, v3)
+tc.assertEqual(v4, spot.trival_maybe())
+tc.assertEqual(v4, spot.trival(spot.trival.maybe_value))
+tc.assertTrue(v3)
+tc.assertTrue(-v2)
+tc.assertFalse(-v1)
+tc.assertFalse(v1)
+tc.assertFalse(-v3)
 
 for u in (v1, v2, v3):
     for v in (v1, v2, v3):
-        assert (u & v) == -(-u | -v)
+        tc.assertEqual((u & v), -(-u | -v))

tests/python/twagraph.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2017, 2021-2022 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,6 +22,8 @@
 
 import spot
 from buddy import bddtrue, bddfalse
+from unittest import TestCase
+tc = TestCase()
 
 aut = spot.make_twa_graph(spot.make_bdd_dict())
 
@@ -29,98 +31,98 @@ try:
     print(aut.to_str())
     exit(2)
 except RuntimeError as e:
-    assert "no state" in str(e)
+    tc.assertIn("no state", str(e))
 
 try:
     aut.set_init_state(2)
 except ValueError as e:
-    assert "nonexisting" in str(e)
+    tc.assertIn("nonexisting", str(e))
 
 try:
     aut.set_univ_init_state([2, 1])
 except ValueError as e:
-    assert "nonexisting" in str(e)
+    tc.assertIn("nonexisting", str(e))
 
 aut.new_states(3)
 aut.set_init_state(2)
-assert aut.get_init_state_number() == 2
+tc.assertEqual(aut.get_init_state_number(), 2)
 aut.set_univ_init_state([2, 1])
-assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number()))
+tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number())))
 
 try:
     aut.get_init_state()
 except RuntimeError as e:
     s = str(e)
-    assert "abstract interface" in s and "alternating automata" in s
+    tc.assertIn("abstract interface" in s and "alternating automata", s)
 
 cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all())
-assert aut.to_str() == cpy.to_str()
+tc.assertEqual(aut.to_str(), cpy.to_str())
 all = aut.set_buchi()
-assert aut.to_str() != cpy.to_str()
+tc.assertNotEqual(aut.to_str(), cpy.to_str())
 cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all())
 aut.new_acc_edge(0, 1, bddtrue, True)
-assert aut.num_edges() == 1 + cpy.num_edges()
+tc.assertEqual(aut.num_edges(), 1 + cpy.num_edges())
 
 aut.prop_universal(True)
 aut.set_name("some name")
 cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False,
                                                  False, False, False))
-assert cpy.prop_universal() != aut.prop_universal()
-assert cpy.prop_universal() == spot.trival.maybe()
-assert cpy.get_name() == None
+tc.assertNotEqual(cpy.prop_universal(), aut.prop_universal())
+tc.assertEqual(cpy.prop_universal(), spot.trival.maybe())
+tc.assertEqual(cpy.get_name(), None)
 cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False,
                                                  False, False, False), True)
-assert cpy.get_name() == "some name"
+tc.assertEqual(cpy.get_name(), "some name")
 
 from copy import copy
 cpy = copy(aut)
-assert aut.to_str() == cpy.to_str()
+tc.assertEqual(aut.to_str(), cpy.to_str())
 cpy.set_init_state(1)
-assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number()))
-assert cpy.get_init_state_number() == 1
-assert cpy.get_name() == "some name"
+tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number())))
+tc.assertEqual(cpy.get_init_state_number(), 1)
+tc.assertEqual(cpy.get_name(), "some name")
 
 try:
     s = aut.state_acc_sets(0)
 except RuntimeError as e:
-    assert "state-based acceptance" in str(e)
+    tc.assertIn("state-based acceptance", str(e))
 
 try:
     s = aut.state_is_accepting(0)
 except RuntimeError as e:
-    assert "state-based acceptance" in str(e)
+    tc.assertIn("state-based acceptance", str(e))
 
 aut.prop_state_acc(True)
 
-assert aut.state_acc_sets(0) == all
-assert aut.state_is_accepting(0) == True
+tc.assertEqual(aut.state_acc_sets(0), all)
+tc.assertEqual(aut.state_is_accepting(0), True)
 
 aut.set_init_state(0)
 aut.purge_unreachable_states()
 i = aut.get_init_state()
-assert aut.state_is_accepting(i) == True
+tc.assertEqual(aut.state_is_accepting(i), True)
 
 it = aut.succ_iter(i)
 it.first()
-assert aut.edge_number(it) == 1
-assert aut.state_number(it.dst()) == 1
-assert aut.edge_storage(it).src == 0
-assert aut.edge_storage(1).src == 0
-assert aut.edge_data(it).cond == bddtrue
-assert aut.edge_data(1).cond == bddtrue
+tc.assertEqual(aut.edge_number(it), 1)
+tc.assertEqual(aut.state_number(it.dst()), 1)
+tc.assertEqual(aut.edge_storage(it).src, 0)
+tc.assertEqual(aut.edge_storage(1).src, 0)
+tc.assertEqual(aut.edge_data(it).cond, bddtrue)
+tc.assertEqual(aut.edge_data(1).cond, bddtrue)
 aut.release_iter(it)
 
 aut.purge_dead_states()
 i = aut.get_init_state()
-assert aut.state_is_accepting(i) == False
+tc.assertEqual(aut.state_is_accepting(i), False)
 
 aut = spot.translate('FGa')
 # Kill the edge between state 0 and 1
-assert aut.edge_storage(2).src == 0
-assert aut.edge_storage(2).dst == 1
+tc.assertEqual(aut.edge_storage(2).src, 0)
+tc.assertEqual(aut.edge_storage(2).dst, 1)
 aut.edge_data(2).cond = bddfalse
-assert aut.num_edges() == 3
-assert aut.num_states() == 2
+tc.assertEqual(aut.num_edges(), 3)
+tc.assertEqual(aut.num_states(), 2)
 aut.purge_dead_states()
-assert aut.num_edges() == 1
-assert aut.num_states() == 1
+tc.assertEqual(aut.num_edges(), 1)
+tc.assertEqual(aut.num_states(), 1)

tests/python/zlktree.py

@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita
-# (LRDE).
+# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -18,6 +18,8 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 import spot
+from unittest import TestCase
+tc = TestCase()
 
 a = spot.automaton("""HOA: v1 States: 5 Start: 0 AP: 2 "p0" "p1"
 Acceptance: 4 Inf(3) | Fin(3) properties: trans-labels explicit-labels
@@ -25,8 +27,8 @@ trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3}
 [0&!1] 0 {2} [!0&1] 1 {2} State: 2 [!0&1] 0 {0 2} [!0&!1] 1 State: 3
 [!0&1] 2 State: 4 [0&!1] 3 --END--""")
 b = spot.zielonka_tree_transform(a)
-assert spot.are_equivalent(a, b)
-assert b.acc().is_buchi()
+tc.assertTrue(spot.are_equivalent(a, b))
+tc.assertTrue(b.acc().is_buchi())
 
 def report_missing_exception():
     raise RuntimeError("missing exception")
@@ -45,95 +47,96 @@ State: 2 [0&1] 8 {3} [0&1] 2 {1} [!0&1] 4 {3 4} [!0&!1] 3 {2 5} State:
 [!0&!1] 2 {5} [!0&!1] 0 {3} [!0&!1] 5 --END--""")
 aa = spot.acd(a)
 try:
-    assert aa.has_rabin_shape()
+    tc.assertTrue(aa.has_rabin_shape())
 except RuntimeError as e:
-    assert 'CHECK_RABIN' in str(e)
+    tc.assertIn('CHECK_RABIN', str(e))
 else:
     report_missing_exception()
 
 try:
-    assert not aa.has_streett_shape()
+    tc.assertFalse(aa.has_streett_shape())
 except RuntimeError as e:
-    assert 'CHECK_STREETT' in str(e)
+    tc.assertIn('CHECK_STREETT', str(e))
 else:
     report_missing_exception()
 
 try:
-    assert not aa.has_parity_shape()
+    tc.assertFalse(aa.has_parity_shape())
 except RuntimeError as e:
-    assert 'CHECK_PARITY' in str(e)
+    tc.assertIn('CHECK_PARITY', str(e))
 else:
     report_missing_exception()
 
 
 aa = spot.acd(a, spot.acd_options_CHECK_RABIN)
-assert aa.has_rabin_shape()
-assert aa.node_count() == 13
+tc.assertTrue(aa.has_rabin_shape())
+tc.assertEqual(aa.node_count(), 13)
 
 try:
-    assert not aa.has_streett_shape()
+    tc.assertFalse(aa.has_streett_shape())
 except RuntimeError as e:
-    assert 'CHECK_STREETT' in str(e)
+    tc.assertIn('CHECK_STREETT', str(e))
 else:
     report_missing_exception()
 
 try:
-    assert aa.has_parity_shape()
+    tc.assertTrue(aa.has_parity_shape())
 except RuntimeError as e:
-    assert 'CHECK_PARITY' in str(e)
+    tc.assertIn('CHECK_PARITY', str(e))
 else:
     report_missing_exception()
 
 aa = spot.acd(a, (spot.acd_options_CHECK_PARITY |
                   spot.acd_options_ABORT_WRONG_SHAPE))
-assert aa.has_rabin_shape()
-assert not aa.has_streett_shape()
-assert not aa.has_parity_shape()
-assert aa.node_count() == 0
+tc.assertTrue(aa.has_rabin_shape())
+tc.assertFalse(aa.has_streett_shape())
+tc.assertFalse(aa.has_parity_shape())
+tc.assertEqual(aa.node_count(), 0)
+
 try:
     aa.first_branch(0)
 except RuntimeError as e:
-    assert 'ABORT_WRONG_SHAPE' in str(e)
+    tc.assertIn('ABORT_WRONG_SHAPE', str(e))
 else:
     report_missing_exception()
 
 try:
     aa.step(0, 0)
 except RuntimeError as e:
-    assert 'incorrect branch number' in str(e)
+    tc.assertIn('incorrect branch number', str(e))
 else:
     report_missing_exception()
 
 try:
     aa.node_acceptance(0)
 except RuntimeError as e:
-    assert 'unknown node' in str(e)
+    tc.assertIn('unknown node', str(e))
 else:
     report_missing_exception()
 
 try:
     aa.edges_of_node(0)
 except RuntimeError as e:
-    assert 'unknown node' in str(e)
+    tc.assertIn('unknown node', str(e))
 else:
     report_missing_exception()
 
 try:
     aa.node_level(0)
 except RuntimeError as e:
-    assert 'unknown node' in str(e)
+    tc.assertIn('unknown node', str(e))
 else:
     report_missing_exception()
 
 a = spot.translate('true')
 a.set_acceptance(spot.acc_cond('f'))
 b = spot.acd_transform(a)
-assert a.equivalent_to(b)
+tc.assertTrue(a.equivalent_to(b))
 
 a = spot.translate('true')
 a.set_acceptance(spot.acc_cond('f'))
 b = spot.zielonka_tree_transform(a)
-assert a.equivalent_to(b)
+tc.assertTrue(a.equivalent_to(b))
 
 a = spot.automaton("""HOA: v1 name: "^ G F p0 G F p1" States: 5 Start:
 2 AP: 2 "a" "b" acc-name: Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) |
@@ -144,8 +147,8 @@ complete properties: deterministic --BODY-- State: 0 {0} [!0&!1] 0
 2} [!0&!1] 1 [0&!1] 4 [!0&1] 3 [0&1] 2 State: 4 {0 3} [!0&!1] 0 [0&!1]
 4 [!0&1] 3 [0&1] 2 --END--""")
 b = spot.acd_transform_sbacc(a, True)
-assert str(b.acc()) == '(3, Fin(0) & (Inf(1) | Fin(2)))'
-assert a.equivalent_to(b)
+tc.assertEqual(str(b.acc()), '(3, Fin(0) & (Inf(1) | Fin(2)))')
+tc.assertTrue(a.equivalent_to(b))
 b = spot.acd_transform_sbacc(a, False)
-assert str(b.acc()) == '(2, Fin(0) & Inf(1))'
-assert a.equivalent_to(b)
+tc.assertEqual(str(b.acc()), '(2, Fin(0) & Inf(1))')
+tc.assertTrue(a.equivalent_to(b))

tests/run.in

@@ -104,18 +104,21 @@ export srcdir
 
 case $1 in
   *.ipynb)
-    PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
+    PYTHONPATH=$pypath:$PYTHONPATH \
+    DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
     PYTHONIOENCODING=utf-8:surrogateescape \
     exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";;
   *.py)
-    PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
+    PYTHONPATH=$pypath:$PYTHONPATH \
+    DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
     exec $PREFIXCMD @PYTHON@ "$@";;
   *.test)
     exec sh -x "$@";;
   *.pl)
     exec $PERL "$@";;
   *python*|*jupyter*|*pypy*)
-    PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
+    PYTHONPATH=$pypath:$PYTHONPATH \
+    DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \
     exec $PREFIXCMD "$@";;
   *)
     echo "Unknown extension" >&2

tests/sanity/style.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009-2022 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 # Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -392,6 +392,27 @@ for dir in "${INCDIR-..}" "${INCDIR-..}/../bin" "${INCDIR-..}/../tests"; do
   done || : # Make sure sh does not abort when read exits with false.
 done
 
+# Rules for Python tests
+for dir in "${INCDIR-..}/../tests"; do
+
+  find "$dir" -name "*.py" -a -type f -a -print |
+  while read file; do
+    fail=false
+
+    # Strip comments.
+    sed 's,[	 ]*#.*,,' < $file > $tmp
+
+    $GREP '[	 ]$' $tmp &&
+      diag 'Trailing whitespace.'
+
+    $GREP -E '([	 ]|^)assert[ (]' $tmp &&
+	diag "replace assert keywords by unittest assertion tests"
+
+    $fail && echo "$file" >>failures.style
+  done || : # Make sure sh does not abort when read exits with false.
+done
+
+
 if test -f failures.style; then
    echo "The following files contain style errors:"
    cat failures.style