diff --git a/.gitignore b/.gitignore index 117213ced..7392a79db 100644 --- a/.gitignore +++ b/.gitignore @@ -81,4 +81,3 @@ GTAGS *.dsc *.gcov spot.spec -default.nix diff --git a/HACKING b/HACKING index c6e127a70..8841b033c 100644 --- a/HACKING +++ b/HACKING @@ -290,8 +290,8 @@ would understand with: make check LOG_DRIVER=$PWD/tools/test-driver-teamcity -C++ Coding conventions -====================== +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,43 +682,3 @@ 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. diff --git a/Makefile.am b/Makefile.am index 668996fc0..a0dc9a316 100644 --- a/Makefile.am +++ b/Makefile.am @@ -68,8 +68,7 @@ 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 \ - default.nix default.nix.in + spot.spec spot.spec.in dist-hook: gen-ChangeLog @@ -115,6 +114,3 @@ 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 $@ diff --git a/NEWS b/NEWS index 345ec7fdd..5e7816b7b 100644 --- a/NEWS +++ b/NEWS @@ -74,12 +74,6 @@ 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: diff --git a/default.nix.in b/default.nix.in deleted file mode 100644 index 8101e4f74..000000000 --- a/default.nix.in +++ /dev/null @@ -1,35 +0,0 @@ -# -*- 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 . - -{ pkgs ? import {} }: -let - version = "@VERSION@"; -in -pkgs.stdenv.mkDerivation { - inherit version; - pname = "spot"; - - buildInputs = [ - pkgs.python3 - ]; - - src = ./.; - - enableParallelBuilding = true; -} diff --git a/flake.lock b/flake.lock deleted file mode 100644 index 6907c7263..000000000 --- a/flake.lock +++ /dev/null @@ -1,43 +0,0 @@ -{ - "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 -} diff --git a/flake.nix b/flake.nix deleted file mode 100644 index 10062e7a5..000000000 --- a/flake.nix +++ /dev/null @@ -1,209 +0,0 @@ -{ - 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 - ])) - ]; - }; - }); -} diff --git a/python/spot/impl.i b/python/spot/impl.i index b5293634f..7132a5cc6 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -90,7 +90,6 @@ #include #include -#include #include #include #include @@ -534,8 +533,6 @@ namespace std { %include %include %include -%template(formula_to_bdd) spot::formula_to_bdd; - %include /* These operators may raise exceptions, and we do not want Swig4 to convert those exceptions to NotImplemented. */ @@ -580,7 +577,6 @@ namespace std { %include %include -%include %include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index 7440cbae3..cdedddffd 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -28,7 +28,6 @@ tl_HEADERS = \ contain.hh \ declenv.hh \ defaultenv.hh \ - derive.hh \ dot.hh \ environment.hh \ exclusive.hh \ @@ -54,7 +53,6 @@ libtl_la_SOURCES = \ contain.cc \ declenv.cc \ defaultenv.cc \ - derive.cc \ dot.cc \ exclusive.cc \ formula.cc \ diff --git a/spot/tl/derive.cc b/spot/tl/derive.cc deleted file mode 100644 index 2b1873ed2..000000000 --- a/spot/tl/derive.cc +++ /dev/null @@ -1,558 +0,0 @@ -// -*- 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 . - -#include "config.h" -#include -#include -#include -#include -#include - -namespace spot -{ - namespace - { - static std::pair - first(formula f, const bdd_dict_ptr& d, void* owner) - { - if (f.is_boolean()) - { - bdd res = formula_to_bdd(f, d, owner); - return { res, bdd_support(res) }; - } - - switch (f.kind()) - { - // handled by is_boolean above - case op::ff: - case op::tt: - case op::ap: - case op::And: - case op::Or: - SPOT_UNREACHABLE(); - - case op::eword: - return { bddfalse, bddtrue }; - - case op::OrRat: - { - bdd res = bddfalse; - bdd support = bddtrue; - for (auto subformula : f) - { - auto [r, sup] = first(subformula, d, owner); - res |= r; - support &= sup; - } - return { res, support }; - } - - case op::AndRat: - { - bdd res = bddtrue; - bdd support = bddtrue; - for (auto subformula : f) - { - auto [r, sup] = first(subformula, d, owner); - res &= r; - support &= sup; - } - return { res, support }; - } - - case op::AndNLM: - return first(rewrite_and_nlm(f), d, owner); - - case op::Concat: - { - auto [res, support] = first(f[0], d, owner); - - if (f[0].accepts_eword()) - { - auto [r, sup] = first(f.all_but(0), d, owner); - res |= r; - support &= sup; - } - - return { res, support }; - } - - case op::Fusion: - { - auto [res, support] = first(f[0], d, owner); - - // this should be computed only if f[0] recognizes words of size 1 - // or accepts eword ? - auto p = first(f.all_but(0), d, owner); - - return { res, support & p.second }; - } - - case op::Star: - case op::first_match: - return first(f[0], d, owner); - - case op::FStar: - { - auto [res, support] = first(f[0], d, owner); - - if (f.min() == 0) - res = bddtrue; - - return { res, support }; - } - - default: - std::cerr << "unimplemented kind " - << static_cast(f.kind()) - << std::endl; - SPOT_UNIMPLEMENTED(); - } - - return { bddfalse, bddtrue }; - } - - static std::vector - formula_aps(formula f) - { - auto res = std::unordered_set(); - - f.traverse([&res](formula f) - { - if (f.is(op::ap)) - { - res.insert(f.ap_name()); - return true; - } - - return false; - }); - - return std::vector(res.begin(), res.end()); - } - } - - formula - rewrite_and_nlm(formula f) - { - unsigned s = f.size(); - std::vector final; - std::vector non_final; - - for (auto g: f) - if (g.accepts_eword()) - final.emplace_back(g); - else - non_final.emplace_back(g); - - if (non_final.empty()) - // (a* & b*);c = (a*|b*);c - return formula::OrRat(std::move(final)); - if (!final.empty()) - { - // let F_i be final formulae - // N_i be non final formula - // (F_1 & ... & F_n & N_1 & ... & N_m) - // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) - // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] - formula f = formula::OrRat(std::move(final)); - formula n = formula::AndNLM(std::move(non_final)); - formula t = formula::one_star(); - formula ft = formula::Concat({f, t}); - formula nt = formula::Concat({n, t}); - formula ftn = formula::AndRat({ft, n}); - formula fnt = formula::AndRat({f, nt}); - return formula::OrRat({ftn, fnt}); - } - // No final formula. - // Translate N_1 & N_2 & ... & N_n into - // N_1 && (N_2;[*]) && ... && (N_n;[*]) - // | (N_1;[*]) && N_2 && ... && (N_n;[*]) - // | (N_1;[*]) && (N_2;[*]) && ... && N_n - formula star = formula::one_star(); - std::vector disj; - for (unsigned n = 0; n < s; ++n) - { - std::vector conj; - for (unsigned m = 0; m < s; ++m) - { - formula g = f[m]; - if (n != m) - g = formula::Concat({g, star}); - conj.emplace_back(g); - } - disj.emplace_back(formula::AndRat(std::move(conj))); - } - return formula::OrRat(std::move(disj)); - } - - twa_graph_ptr - derive_finite_automaton_with_first(formula f, bool deterministic) - { - auto bdd_dict = make_bdd_dict(); - auto aut = make_twa_graph(bdd_dict); - - aut->prop_state_acc(true); - const auto acc_mark = aut->set_buchi(); - - auto formula2state = robin_hood::unordered_map(); - - unsigned init_state = aut->new_state(); - aut->set_init_state(init_state); - - formula2state.insert({ f, init_state }); - - auto f_aps = formula_aps(f); - for (auto& ap : f_aps) - aut->register_ap(ap); - - auto todo = std::vector>(); - todo.push_back({f, init_state}); - - auto state_names = new std::vector(); - std::ostringstream ss; - ss << f; - state_names->push_back(ss.str()); - - auto find_dst = [&](formula derivative) -> unsigned - { - unsigned dst; - auto it = formula2state.find(derivative); - if (it != formula2state.end()) - { - dst = it->second; - } - else - { - dst = aut->new_state(); - todo.push_back({derivative, dst}); - formula2state.insert({derivative, dst}); - std::ostringstream ss; - ss << derivative; - state_names->push_back(ss.str()); - } - - return dst; - }; - - while (!todo.empty()) - { - auto [curr_f, curr_state] = todo[todo.size() - 1]; - todo.pop_back(); - - auto curr_acc_mark = curr_f.accepts_eword() - ? acc_mark - : acc_cond::mark_t(); - - auto [firsts, firsts_support] = first(curr_f, bdd_dict, aut.get()); - for (const bdd one : minterms_of(firsts, firsts_support)) - { - formula derivative = - partial_derivation(curr_f, one, bdd_dict, aut.get()); - - // no transition possible from this letter - if (derivative.is(op::ff)) - continue; - - // either the formula isn't an OrRat, or if it is we consider it as - // as a whole to get a deterministic automaton - if (deterministic || !derivative.is(op::OrRat)) - { - auto dst = find_dst(derivative); - aut->new_edge(curr_state, dst, one, curr_acc_mark); - continue; - } - - // formula is an OrRat and we want a non deterministic automaton, - // so consider each child as a destination - for (const auto& subformula : derivative) - { - auto dst = find_dst(subformula); - aut->new_edge(curr_state, dst, one, curr_acc_mark); - } - } - - // if state has no transitions and should be accepting, create - // artificial transition - if (aut->get_graph().state_storage(curr_state).succ == 0 - && curr_f.accepts_eword()) - aut->new_edge(curr_state, curr_state, bddfalse, acc_mark); - } - - aut->set_named_prop("state-names", state_names); - - aut->merge_edges(); - - return aut; - } - - twa_graph_ptr - derive_finite_automaton(formula f, bool deterministic) - { - auto bdd_dict = make_bdd_dict(); - auto aut = make_twa_graph(bdd_dict); - - aut->prop_state_acc(true); - const auto acc_mark = aut->set_buchi(); - - auto formula2state = robin_hood::unordered_map(); - - unsigned init_state = aut->new_state(); - aut->set_init_state(init_state); - - formula2state.insert({ f, init_state }); - - auto f_aps = formula_aps(f); - for (auto& ap : f_aps) - aut->register_ap(ap); - bdd all_aps = aut->ap_vars(); - - auto todo = std::vector>(); - todo.push_back({f, init_state}); - - auto state_names = new std::vector(); - std::ostringstream ss; - ss << f; - state_names->push_back(ss.str()); - - auto find_dst = [&](formula derivative) -> unsigned - { - unsigned dst; - auto it = formula2state.find(derivative); - if (it != formula2state.end()) - { - dst = it->second; - } - else - { - dst = aut->new_state(); - todo.push_back({derivative, dst}); - formula2state.insert({derivative, dst}); - std::ostringstream ss; - ss << derivative; - state_names->push_back(ss.str()); - } - - return dst; - }; - - while (!todo.empty()) - { - auto [curr_f, curr_state] = todo[todo.size() - 1]; - todo.pop_back(); - - auto curr_acc_mark = curr_f.accepts_eword() - ? acc_mark - : acc_cond::mark_t(); - - for (const bdd one : minterms_of(bddtrue, all_aps)) - { - formula derivative = - partial_derivation(curr_f, one, bdd_dict, aut.get()); - - // no transition possible from this letter - if (derivative.is(op::ff)) - continue; - - // either the formula isn't an OrRat, or if it is we consider it as - // as a whole to get a deterministic automaton - if (deterministic || !derivative.is(op::OrRat)) - { - auto dst = find_dst(derivative); - aut->new_edge(curr_state, dst, one, curr_acc_mark); - continue; - } - - // formula is an OrRat and we want a non deterministic automaton, - // so consider each child as a destination - for (const auto& subformula : derivative) - { - auto dst = find_dst(subformula); - aut->new_edge(curr_state, dst, one, curr_acc_mark); - } - } - - // if state has no transitions and should be accepting, create - // artificial transition - if (aut->get_graph().state_storage(curr_state).succ == 0 - && curr_f.accepts_eword()) - aut->new_edge(curr_state, curr_state, bddfalse, acc_mark); - } - - aut->set_named_prop("state-names", state_names); - - aut->merge_edges(); - - return aut; - } - - twa_graph_ptr - derive_automaton_with_first(formula f, bool deterministic) - { - auto finite = derive_finite_automaton_with_first(f, deterministic); - - return from_finite(finite); - } - - twa_graph_ptr - derive_automaton(formula f, bool deterministic) - { - auto finite = derive_finite_automaton(f, deterministic); - - return from_finite(finite); - } - - formula - partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d, - void* owner) - { - if (f.is_boolean()) - { - auto f_bdd = formula_to_bdd(f, d, owner); - - if (bdd_implies(var, f_bdd)) - return formula::eword(); - - return formula::ff(); - } - - switch (f.kind()) - { - // handled by is_boolean above - case op::ff: - case op::tt: - case op::ap: - SPOT_UNREACHABLE(); - - case op::eword: - return formula::ff(); - - // d(E.F) = { d(E).F } U { c(E).d(F) } - case op::Concat: - { - formula E = f[0]; - formula F = f.all_but(0); - - auto res = - formula::Concat({ partial_derivation(E, var, d, owner), F }); - - if (E.accepts_eword()) - res = formula::OrRat( - { res, partial_derivation(F, var, d, owner) }); - - return res; - } - - // d(E*) = d(E).E* - // d(E[*i..j]) = d(E).E[*(i-1)..(j-1)] - case op::Star: - { - auto min = f.min() == 0 ? 0 : (f.min() - 1); - auto max = f.max() == formula::unbounded() - ? formula::unbounded() - : (f.max() - 1); - - formula d_E = partial_derivation(f[0], var, d, owner); - - return formula::Concat({ d_E, formula::Star(f[0], min, max) }); - } - - // d(E[:*i..j]) = E:E[:*(i-1)..(j-1)] + (eword if i == 0 or c(d(E))) - case op::FStar: - { - formula E = f[0]; - - if (f.min() == 0 && f.max() == 0) - return formula::tt(); - - auto d_E = partial_derivation(E, var, d, owner); - - auto min = f.min() == 0 ? 0 : (f.min() - 1); - auto max = f.max() == formula::unbounded() - ? formula::unbounded() - : (f.max() - 1); - - auto results = std::vector(); - - auto E_i_j_minus = formula::FStar(E, min, max); - results.push_back(formula::Fusion({ d_E, E_i_j_minus })); - - if (d_E.accepts_eword()) - results.push_back(d_E); - - if (f.min() == 0) - results.push_back(formula::eword()); - - return formula::OrRat(std::move(results)); - } - - // d(E && F) = d(E) && d(F) - // d(E + F) = {d(E)} U {d(F)} - case op::AndRat: - case op::OrRat: - { - std::vector subderivations; - for (auto subformula : f) - { - auto subderivation = - partial_derivation(subformula, var, d, owner); - subderivations.push_back(subderivation); - } - return formula::multop(f.kind(), std::move(subderivations)); - } - - case op::AndNLM: - { - formula rewrite = rewrite_and_nlm(f); - return partial_derivation(rewrite, var, d, owner); - } - - // d(E:F) = {d(E):F} U {c(d(E)).d(F)} - case op::Fusion: - { - formula E = f[0]; - formula F = f.all_but(0); - - auto d_E = partial_derivation(E, var, d, owner); - auto res = formula::Fusion({ d_E, F }); - - if (d_E.accepts_eword()) - res = - formula::OrRat({ res, partial_derivation(F, var, d, owner) }); - - return res; - } - - case op::first_match: - { - formula E = f[0]; - auto d_E = partial_derivation(E, var, d, owner); - // if d_E.accepts_eword(), first_match(d_E) will return eword - return formula::first_match(d_E); - } - - default: - std::cerr << "unimplemented kind " - << static_cast(f.kind()) - << std::endl; - SPOT_UNIMPLEMENTED(); - } - return formula::ff(); - } -} diff --git a/spot/tl/derive.hh b/spot/tl/derive.hh deleted file mode 100644 index 1947951ed..000000000 --- a/spot/tl/derive.hh +++ /dev/null @@ -1,52 +0,0 @@ -// -*- 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 . - -#pragma once - -#include - -#include - -#include -#include -#include - -namespace spot -{ - /// \ingroup tl_misc - /// \brief Produce a SERE formula's partial derivative - SPOT_API formula - partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d, - void* owner); - - SPOT_API twa_graph_ptr - derive_automaton(formula f, bool deterministic = true); - - SPOT_API twa_graph_ptr - derive_automaton_with_first(formula f, bool deterministic = true); - - SPOT_API twa_graph_ptr - derive_finite_automaton(formula f, bool deterministic = true); - - SPOT_API twa_graph_ptr - derive_finite_automaton_with_first(formula f, bool deterministic = true); - - SPOT_API formula - rewrite_and_nlm(formula f); -} diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 819a90962..cb1e208ec 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013-2022 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2013-2021 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_aps_from_dict() may not be" + throw std::runtime_error("register_ap_from_dict() may not be" " called on an automaton that has already" " registered some AP"); auto& m = get_dict()->bdd_map; diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 8da719776..051514550 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -164,15 +164,11 @@ namespace spot // them. }); - bool is_state_acc = this->prop_state_acc().is_true(); - unsigned out = 0; unsigned in = 1; // Skip any leading false edge. - while (in < tend - && trans[in].cond == bddfalse - && (!is_state_acc || trans[in].src != trans[in].dst)) + while (in < tend && trans[in].cond == bddfalse) ++in; if (in < tend) { @@ -181,9 +177,7 @@ namespace spot trans[out] = trans[in]; for (++in; in < tend; ++in) { - if (trans[in].cond == bddfalse - && (!is_state_acc - || trans[in].src != trans[in].dst)) // Unusable edge + if (trans[in].cond == bddfalse) // Unusable edge continue; // Merge edges with the same source, destination, and // colors. (We test the source last, because this is the diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 783a35285..3566abc97 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -24,7 +24,6 @@ #include #include #include -#include #include #include #include @@ -754,7 +753,55 @@ namespace spot SPOT_UNREACHABLE(); case op::AndNLM: { - return recurse_and_concat(rewrite_and_nlm(f)); + unsigned s = f.size(); + vec final; + vec non_final; + + for (auto g: f) + if (g.accepts_eword()) + final.emplace_back(g); + else + non_final.emplace_back(g); + + if (non_final.empty()) + // (a* & b*);c = (a*|b*);c + return recurse_and_concat(formula::OrRat(std::move(final))); + if (!final.empty()) + { + // let F_i be final formulae + // N_i be non final formula + // (F_1 & ... & F_n & N_1 & ... & N_m) + // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) + // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] + formula f = formula::OrRat(std::move(final)); + formula n = formula::AndNLM(std::move(non_final)); + formula t = formula::one_star(); + formula ft = formula::Concat({f, t}); + formula nt = formula::Concat({n, t}); + formula ftn = formula::AndRat({ft, n}); + formula fnt = formula::AndRat({f, nt}); + return recurse_and_concat(formula::OrRat({ftn, fnt})); + } + // No final formula. + // Translate N_1 & N_2 & ... & N_n into + // N_1 && (N_2;[*]) && ... && (N_n;[*]) + // | (N_1;[*]) && N_2 && ... && (N_n;[*]) + // | (N_1;[*]) && (N_2;[*]) && ... && N_n + formula star = formula::one_star(); + vec disj; + for (unsigned n = 0; n < s; ++n) + { + vec conj; + for (unsigned m = 0; m < s; ++m) + { + formula g = f[m]; + if (n != m) + g = formula::Concat({g, star}); + conj.emplace_back(g); + } + disj.emplace_back(formula::AndRat(std::move(conj))); + } + return recurse_and_concat(formula::OrRat(std::move(disj))); } case op::AndRat: { @@ -2224,59 +2271,4 @@ namespace spot return a; } - twa_graph_ptr - sere_to_tgba(formula f, const bdd_dict_ptr& dict) - { - f = negative_normal_form(f); - - tl_simplifier* s = new tl_simplifier(dict); - twa_graph_ptr a = make_twa_graph(dict); - - translate_dict d(a, s, false, false, false); - ratexp_to_dfa sere2dfa(d); - - auto [dfa, namer, state] = sere2dfa.succ(f); - - // language was empty, build an automaton with one non accepting state - if (dfa == nullptr) - { - auto res = make_twa_graph(dict); - res->set_init_state(res->new_state()); - res->prop_universal(true); - res->prop_complete(false); - res->prop_stutter_invariant(true); - res->prop_terminal(true); - res->prop_state_acc(true); - return res; - } - - auto res = make_twa_graph(dfa, {false, false, true, false, false, false}); - - // HACK: translate_dict registers the atomic propositions in the "final" - // automaton that would be produced by a full translation, not in the - // intermediate automaton we're interested in. We can copy them from the - // resulting automaton. - res->copy_ap_of(a); - - res->prop_state_acc(true); - const auto acc_mark = res->set_buchi(); - - size_t sn = namer->state_to_name.size(); - for (size_t i = 0; i < sn; ++i) - { - formula g = namer->state_to_name[i]; - if (g.accepts_eword()) - { - if (res->get_graph().state_storage(i).succ == 0) - res->new_edge(i, i, bddfalse, acc_mark); - else - { - for (auto& e : res->out(i)) - e.acc = acc_mark; - } - } - } - - return res; - } } diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index aa9bc1d1d..8c1827490 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -88,7 +88,4 @@ namespace spot tl_simplifier* simplifier = nullptr, bool unambiguous = false, const output_aborter* aborter = nullptr); - - SPOT_API twa_graph_ptr - sere_to_tgba(formula f, const bdd_dict_ptr& dict); } diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index b693015fd..942a1b4b5 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -244,51 +244,4 @@ namespace spot } - twa_graph_ptr from_finite(const_twa_graph_ptr aut, const char* alive) - { - twa_graph_ptr res = - make_twa_graph(aut, - { true, false, true, false, false, false }); - - if (aut->get_named_prop>("state-names")) - res->copy_state_names_from(aut); - auto* names = res->get_named_prop>("state-names"); - - unsigned alive_sink = res->new_state(); - if (names != nullptr) - names->push_back("sink"); - auto acc = res->acc().all_sets(); - auto alive_bdd = bdd_ithvar(res->register_ap(alive)); - res->new_edge(alive_sink, alive_sink, !alive_bdd, acc); - - unsigned ns = res->num_states(); - for (unsigned s = 0; s < ns; ++s) - { - if (s == alive_sink) - continue; - - bool was_acc = res->state_is_accepting(s); - - // erase accepting marks, require alive on non-accepting transition, - // and remove self-loop edges used to mark acceptance - auto i = res->out_iteraser(s); - while (i) - { - if (i->src == i->dst && i->cond == bddfalse) - { - i.erase(); - continue; - } - - i->cond &= alive_bdd; - i->acc = {}; - ++i; - } - - if (was_acc) - res->new_edge(s, alive_sink, !alive_bdd); - } - - return res; - } } diff --git a/spot/twaalgos/remprop.hh b/spot/twaalgos/remprop.hh index 4b496e65a..09d75ffac 100644 --- a/spot/twaalgos/remprop.hh +++ b/spot/twaalgos/remprop.hh @@ -54,8 +54,5 @@ namespace spot SPOT_API twa_graph_ptr to_finite(const_twa_graph_ptr aut, const char* alive = "alive"); - /// \brief The opposite of the to_finite operation - SPOT_API twa_graph_ptr - from_finite(const_twa_graph_ptr aut, const char* alive = "alive"); } diff --git a/tests/core/bricks.test b/tests/core/bricks.test index 37ff57cb0..b98c7e856 100644 --- a/tests/core/bricks.test +++ b/tests/core/bricks.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2020 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -21,13 +21,12 @@ . ./defs set -e -# The seq command is not always available, but we assume awk is. -$AWK 'BEGIN{for(x=0;x<2000;++x) print x;}' >expected +seq 0 1999 > 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 diff --git a/tests/core/defs.in b/tests/core/defs.in index d06a3b67d..7df6fdf77 100644 --- a/tests/core/defs.in +++ b/tests/core/defs.in @@ -1,5 +1,5 @@ # -*- mode: shell-script; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2013, 2015, 2022 Laboratoire de Recherche +# Copyright (C) 2009, 2010, 2012, 2013, 2015 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,7 +57,6 @@ case $srcdir in *) srcdir=../$srcdir esac -AWK='@AWK@' DOT='@DOT@' LBTT="@LBTT@" LBTT_TRANSLATE="@LBTT_TRANSLATE@" diff --git a/tests/core/prodchain.test b/tests/core/prodchain.test index 0a7f1a1d9..b5037782f 100755 --- a/tests/core/prodchain.test +++ b/tests/core/prodchain.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,8 +23,7 @@ set -e set x shift -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 +for i in `seq 1 42`; do ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa done for i in *.hoa; do diff --git a/tests/python/298.py b/tests/python/298.py index 89ddbdb0c..d4865c440 100644 --- a/tests/python/298.py +++ b/tests/python/298.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -20,23 +20,21 @@ # 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) -tc.assertEqual(r1.num_sets(), 3) -tc.assertTrue(a1.prop_complete().is_false()) +assert r1.num_sets() == 3 +assert a1.prop_complete().is_false(); # This used to fail in 2.9.5 and earlier. -tc.assertTrue(r1.prop_complete().is_maybe()) -tc.assertTrue(spot.is_complete(r1)) +assert r1.prop_complete().is_maybe(); +assert 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. -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)) +assert r2.num_sets() == 3 +assert a2.prop_complete().is_false(); +assert r2.prop_complete().is_maybe(); +assert spot.is_complete(r2) diff --git a/tests/python/341.py b/tests/python/341.py index e828ab07c..4c5937149 100644 --- a/tests/python/341.py +++ b/tests/python/341.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,8 +19,7 @@ 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""" @@ -35,4 +34,4 @@ for i in range(5): n = len(_active) print(n, "active processes") -tc.assertEqual(n, 0) +assert(n == 0) diff --git a/tests/python/471.py b/tests/python/471.py index 0fe180554..6fee3a2d3 100644 --- a/tests/python/471.py +++ b/tests/python/471.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -20,12 +20,9 @@ # 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() -tc.assertEqual(str(r1), str(r2)) -tc.assertTrue(a.prop_weak().is_true()) +assert str(r1) == str(r2) +assert a.prop_weak().is_true() diff --git a/tests/python/accparse2.py b/tests/python/accparse2.py index d9c7274a0..4e6eb1cb3 100644 --- a/tests/python/accparse2.py +++ b/tests/python/accparse2.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,101 +18,99 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() a = spot.acc_cond(5) a.set_acceptance(spot.acc_code('parity min odd 5')) -tc.assertEqual(a.is_parity(), [True, False, True]) +assert(a.is_parity() == [True, False, True]) a.set_acceptance('parity max even 5') -tc.assertEqual(a.is_parity(), [True, True, False]) +assert(a.is_parity() == [True, True, False]) a.set_acceptance('generalized-Buchi 5') -tc.assertEqual(a.is_parity()[0], False) -tc.assertEqual(a.is_parity(True)[0], False) +assert(a.is_parity()[0] == False) +assert(a.is_parity(True)[0] == False) a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))') -tc.assertEqual(a.is_parity()[0], False) -tc.assertEqual(a.is_parity(True), [True, True, False]) +assert(a.is_parity()[0] == False) +assert(a.is_parity(True) == [True, True, 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()) +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() a.set_acceptance('Fin(0)|Fin(1)') -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()) +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() a = spot.acc_cond(0) a.set_acceptance('all') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), 0) -tc.assertEqual(a.is_parity(), [True, True, True]) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 0) +assert(a.is_parity() == [True, True, True]) a.set_acceptance('none') -tc.assertEqual(a.is_rabin(), 0) -tc.assertEqual(a.is_streett(), -1) -tc.assertEqual(a.is_parity(), [True, True, False]) +assert(a.is_rabin() == 0) +assert(a.is_streett() == -1) +assert(a.is_parity() == [True, True, False]) a = spot.acc_cond('(Fin(0)&Inf(1))') -tc.assertEqual(a.is_rabin(), 1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == 1) +assert(a.is_streett() == -1) a.set_acceptance('Inf(1)&Fin(0)') -tc.assertEqual(a.is_rabin(), 1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == 1) +assert(a.is_streett() == -1) a.set_acceptance('(Fin(0)|Inf(1))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), 1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 1) a.set_acceptance('Inf(1)|Fin(0)') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), 1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 1) a = spot.acc_cond('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))') -tc.assertEqual(a.is_rabin(), 2) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == 2) +assert(a.is_streett() == -1) a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))')) -tc.assertEqual(a.is_rabin(), 2) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == 2) +assert(a.is_streett() == -1) a.set_acceptance(spot.acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))')) -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))')) -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) a.set_acceptance(spot.acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))')) -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) a.set_acceptance('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))') -tc.assertEqual(a.is_rabin(), 2) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == 2) +assert(a.is_streett() == -1) a.set_acceptance('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), 2) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 2) a.set_acceptance('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), 2) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 2) a.set_acceptance('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) a.set_acceptance('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) a.set_acceptance('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), -1) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))') -tc.assertEqual(a.is_rabin(), -1) -tc.assertEqual(a.is_streett(), 2) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 2) a = spot.acc_code('Inf(0)&Inf(1)&Inf(3) | Fin(0)&(Fin(1)|Fin(3))') u = a.symmetries() -tc.assertEqual(u[0], 0) -tc.assertEqual(u[1], 1) -tc.assertEqual(u[2], 2) -tc.assertEqual(u[3], 1) +assert u[0] == 0 +assert u[1] == 1 +assert u[2] == 2 +assert u[3] == 1 diff --git a/tests/python/aiger.py b/tests/python/aiger.py index f490465b0..5148fef5f 100644 --- a/tests/python/aiger.py +++ b/tests/python/aiger.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021, 2022 Laboratoire de Recherche et +# Copyright (C) 2021 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot, buddy -from unittest import TestCase -tc = TestCase() strats = (("""HOA: v1 States: 4 @@ -3348,7 +3346,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")}""") - raise AssertionError("not a specialization") + assert 0 # Check stepwise simulation @@ -3388,7 +3386,7 @@ for (i, e_latch) in zip(ins, exp_latches): # Variable names -tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0 +assert(spot.aiger_circuit("""aag 2 2 0 2 0 2 4 2 @@ -3396,9 +3394,9 @@ tc.assertEqual(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') -tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0 +assert(spot.aiger_circuit("""aag 2 2 0 2 0 2 4 2 @@ -3406,7 +3404,7 @@ tc.assertEqual(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(): @@ -3417,7 +3415,7 @@ try: 0 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:1: invalid header line") + assert str(e) == "\n:1: invalid header line" else: report_missing_exception() @@ -3425,15 +3423,14 @@ try: spot.aiger_circuit("""aag 2 2 3 2 0 """) except SyntaxError as e: - tc.assertEqual(str(e), - "\n:1: more variables than indicated by max var") + assert str(e) == "\n: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: - tc.assertEqual(str(e), "\n:2: expecting input number 2") + assert str(e) == "\n:2: expecting input number 2" else: report_missing_exception() @@ -3442,7 +3439,7 @@ try: 3 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:2: expecting input number 2") + assert str(e) == "\n:2: expecting input number 2" else: report_missing_exception() @@ -3451,7 +3448,7 @@ try: 3 4 5 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:2: invalid format for an input") + assert str(e) == "\n:2: invalid format for an input" else: report_missing_exception() @@ -3460,7 +3457,7 @@ try: 2 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:3: expecting input number 4") + assert str(e) == "\n:3: expecting input number 4" else: report_missing_exception() @@ -3471,7 +3468,7 @@ try: 1 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:4: invalid format for a latch") + assert str(e) == "\n:4: invalid format for a latch" else: report_missing_exception() @@ -3482,7 +3479,7 @@ try: 1 1 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:4: expecting latch number 6") + assert str(e) == "\n:4: expecting latch number 6" else: report_missing_exception() @@ -3493,7 +3490,7 @@ try: 6 1 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:5: expecting latch number 8") + assert str(e) == "\n:5: expecting latch number 8" else: report_missing_exception() @@ -3505,7 +3502,7 @@ try: 8 7 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:6: expecting an output") + assert str(e) == "\n:6: expecting an output" else: report_missing_exception() @@ -3518,7 +3515,7 @@ try: 9 9 9 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:6: invalid format for an output") + assert str(e) == "\n:6: invalid format for an output" else: report_missing_exception() @@ -3531,7 +3528,7 @@ try: 9 9 9 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:6: invalid format for an output") + assert str(e) == "\n:6: invalid format for an output" else: report_missing_exception() @@ -3544,7 +3541,7 @@ try: 9 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:7: expecting AND gate number 10") + assert str(e) == "\n:7: expecting AND gate number 10" else: report_missing_exception() @@ -3558,7 +3555,7 @@ try: 10 3 8 9 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:7: invalid format for an AND gate") + assert str(e) == "\n:7: invalid format for an AND gate" else: report_missing_exception() @@ -3572,7 +3569,7 @@ try: 10 3 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:7: invalid format for an AND gate") + assert str(e) == "\n:7: invalid format for an AND gate" else: report_missing_exception() @@ -3586,7 +3583,7 @@ try: 10 3 8 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:8: expecting AND gate number 12") + assert str(e) == "\n:8: expecting AND gate number 12" else: report_missing_exception() @@ -3602,7 +3599,7 @@ try: i0 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:9: could not parse as input name") + assert str(e) == "\n:9: could not parse as input name" else: report_missing_exception() @@ -3619,7 +3616,7 @@ i0 foo i3 bar """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:10: value 3 exceeds input count") + assert str(e) == "\n:10: value 3 exceeds input count" else: report_missing_exception() @@ -3636,7 +3633,7 @@ i1 bar i0 foo """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:9: expecting name for input 0") + assert str(e) == "\n:9: expecting name for input 0" else: report_missing_exception() @@ -3653,8 +3650,8 @@ i0 name with spaces i1 name with spaces """) except SyntaxError as e: - tc.assertEqual(str(e), \ - "\n:10: name 'name with spaces' already used") + assert str(e) == \ + "\n:10: name 'name with spaces' already used" else: report_missing_exception() @@ -3672,7 +3669,7 @@ i1 bar o0 """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:11: could not parse as output name") + assert str(e) == "\n:11: could not parse as output name" else: report_missing_exception() @@ -3692,7 +3689,7 @@ o1 hmm o0 foo bar baz """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:12: expecting name for output 0") + assert str(e) == "\n:12: expecting name for output 0" else: report_missing_exception() @@ -3712,7 +3709,7 @@ o0 hmm o2 foo bar baz """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:13: value 2 exceeds output count") + assert str(e) == "\n:13: value 2 exceeds output count" else: report_missing_exception() @@ -3732,7 +3729,7 @@ o0 foo o1 foo """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:13: name 'foo' already used") + assert str(e) == "\n:13: name 'foo' already used" else: report_missing_exception() @@ -3752,7 +3749,7 @@ o0 foo o1 bar """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:13: name 'bar' already used") + assert str(e) == "\n:13: name 'bar' already used" else: report_missing_exception() @@ -3773,7 +3770,7 @@ o1 baz this is a bug """) except SyntaxError as e: - tc.assertEqual(str(e), "\n:14: unsupported line type") + assert str(e) == "\n:14: unsupported line type" else: report_missing_exception() @@ -3794,8 +3791,8 @@ c this is not a bug """) except SyntaxError as e: - tc.assertEqual(str(e), \ - "\n:10: either all or none of the inputs should be named") + assert str(e) == \ + "\n:10: either all or none of the inputs should be named" else: report_missing_exception() @@ -3818,8 +3815,8 @@ c this is not a bug """) except SyntaxError as e: - tc.assertEqual(str(e), \ - "\n:11-12: either all or none of the inputs should be named") + assert str(e) == \ + "\n:11-12: either all or none of the inputs should be named" else: report_missing_exception() @@ -3844,8 +3841,8 @@ c this is not a bug """) except SyntaxError as e: - tc.assertEqual(str(e), \ - "\n:14-16: either all or none of the outputs should be named") + assert str(e) == \ + "\n:14-16: either all or none of the outputs should be named" else: report_missing_exception() @@ -3869,4 +3866,4 @@ o2 bar c this is not a bug """).to_str() -tc.assertEqual(x, spot.aiger_circuit(x).to_str()) +assert x == spot.aiger_circuit(x).to_str() diff --git a/tests/python/aliases.py b/tests/python/aliases.py index 40dd4d0ec..6f861a880 100644 --- a/tests/python/aliases.py +++ b/tests/python/aliases.py @@ -20,8 +20,6 @@ # Test for parts of Issue #497. import spot -from unittest import TestCase -tc = TestCase() aut = spot.automaton(""" HOA: v1 @@ -65,11 +63,11 @@ State: 0 --END--""") s = aut.to_str('hoa') aut2 = spot.automaton(s) -tc.assertTrue(aut.equivalent_to(aut2)) +assert aut.equivalent_to(aut2) s2 = aut.to_str('hoa') -tc.assertEqual(s, s2) +assert s == s2 -tc.assertEqual(s, """HOA: v1 +assert s == """HOA: v1 States: 1 Start: 0 AP: 3 "x" "y" "z" @@ -107,7 +105,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... @@ -117,7 +115,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. -tc.assertEqual(s2, """HOA: v1 +assert(s2 == """HOA: v1 States: 1 Start: 0 AP: 2 "y" "z" diff --git a/tests/python/alternating.py b/tests/python/alternating.py index 5b38ca378..7b3a5d713 100755 --- a/tests/python/alternating.py +++ b/tests/python/alternating.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016-2017, 2021-2022 Laboratoire de Recherche -# et Développement de l'EPITA. +# Copyright (C) 2016, 2017, 2021 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -20,8 +20,6 @@ import spot import buddy -from unittest import TestCase -tc = TestCase() aut = spot.make_twa_graph(spot._bdd_dict) @@ -40,8 +38,9 @@ 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)] -tc.assertEqual([(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])], tr) -tc.assertFalse(aut.is_existential()) +print(tr) +assert [(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])] == tr +assert not aut.is_existential() received = False try: @@ -50,10 +49,11 @@ try: pass except RuntimeError: received = True -tc.assertTrue(received) +assert received h = aut.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +print(h) +assert h == """HOA: v1 States: 3 Start: 0 AP: 2 "p1" "p2" @@ -68,20 +68,22 @@ State: 1 [0&1] 0&2&1 State: 2 [0 | 1] 2 ---END--""") +--END--""" aut2 = spot.automaton(h) h2 = aut2.to_str('hoa') -tc.assertNotEqual(h, h2) +print(h2) +assert h != h2 # This will sort destination groups aut.merge_univ_dests() h = aut.to_str('hoa') -tc.assertEqual(h, h2) +assert h == h2 aut2.set_univ_init_state([0, 1]) h3 = aut2.to_str('hoa') -tc.assertEqual(h3, """HOA: v1 +print(h3) +assert h3 == """HOA: v1 States: 3 Start: 0&1 AP: 2 "p1" "p2" @@ -96,22 +98,23 @@ 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]) -tc.assertEqual((st, st2, st3), (3, 4, 5)) +assert (st, st2, st3) == (3, 4, 5) received = False try: st4 = spot.states_and(aut, []) except RuntimeError: received = True -tc.assertTrue(received) +assert received h = aut.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +print(h) +assert h == """HOA: v1 States: 6 Start: 0 AP: 2 "p1" "p2" @@ -133,10 +136,11 @@ State: 4 [0&1] 0&1&2 State: 5 [0&1] 0&1&2 ---END--""") +--END--""" h = spot.split_edges(aut).to_str('hoa') -tc.assertEqual(h, """HOA: v1 +print(h) +assert h == """HOA: v1 States: 6 Start: 0 AP: 2 "p1" "p2" @@ -164,7 +168,7 @@ State: 4 [0&1] 0&1&2 State: 5 [0&1] 0&1&2 ---END--""") +--END--""" # remove_univ_otf @@ -202,11 +206,11 @@ State: 2 --END--""" desalt = spot.remove_univ_otf(aut) -tc.assertEqual(desalt.to_str('hoa'), out) +assert(desalt.to_str('hoa') == out) -tc.assertEqual(aut.num_states(), 3) -tc.assertEqual(aut.num_edges(), 3) +assert aut.num_states() == 3 +assert aut.num_edges() == 3 aut.edge_storage(3).cond = buddy.bddfalse aut.purge_dead_states() -tc.assertEqual(aut.num_states(), 1) -tc.assertEqual(aut.num_edges(), 0) +assert aut.num_states() == 1 +assert aut.num_edges() == 0 diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py index b7b442b1f..d6222b58f 100644 --- a/tests/python/bdddict.py +++ b/tests/python/bdddict.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019, 2021, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2019, 2021 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 . -# Make sure we can keep track of BDD association in Python using bdd_dict, as -# discussed in (deleted???) issue #372. +# Make sure we can leep track of BDD association in Python using bdd_dict, as +# discussed in issue #372. # CPython use reference counting, so that automata are destructed # when we expect them to be. However other implementations like @@ -33,8 +33,6 @@ else: gc.collect() import spot -from unittest import TestCase -tc = TestCase() class bdd_holder: @@ -66,7 +64,7 @@ class bdd_holder3: def check_ok(): - tc.assertIs(type(bdict.varnum(spot.formula.ap("a"))), int) + assert type(bdict.varnum(spot.formula.ap("a"))) is int def check_nok(): @@ -125,7 +123,7 @@ debug("h2") h3 = bdd_holder3(h2) var = bdict.register_anonymous_variables(1, h3) debug("h3") -tc.assertEqual(var, 2) +assert var == 2 del h2 gcollect() debug("-h2") diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py index 95cc441b3..3d3bb7894 100644 --- a/tests/python/bdditer.py +++ b/tests/python/bdditer.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et +# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,13 +24,11 @@ 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) -tc.assertNotEqual(c, buddy.bddfalse) +assert c != buddy.bddfalse res = [] while c != buddy.bddtrue: var = buddy.bdd_var(c) @@ -42,23 +40,23 @@ while c != buddy.bddtrue: res.append(var) c = h -tc.assertEqual(res, [0, -1]) +assert res == [0, -1] res2 = [] for i in run.aut.ap(): res2.append((str(i), run.aut.register_ap(i))) -tc.assertEqual(str(res2), "[('a', 0), ('b', 1)]") +assert str(res2) == "[('a', 0), ('b', 1)]" f = spot.bdd_to_formula(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') +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' try: f = spot.bdd_to_formula(b, spot.make_bdd_dict()) sys.exit(2) except RuntimeError as e: - tc.assertIn("not in the dictionary", str(e)) + assert "not in the dictionary" in str(e) diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py index 19434c967..9e06e0db3 100644 --- a/tests/python/bugdet.py +++ b/tests/python/bugdet.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement -# de l'EPITA. +# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -22,8 +22,6 @@ # sent to the Spot mailing list on 2016-10-31. import spot -from unittest import TestCase -tc = TestCase() a = spot.automaton(""" HOA: v1 @@ -82,12 +80,12 @@ State: 7 {0} # was fine. print("use_simulation=True") b1 = spot.tgba_determinize(b, False, True, True, True) -tc.assertEqual(b1.num_states(), 5) +assert b1.num_states() == 5 b1 = spot.remove_fin(spot.dualize(b1)) -tc.assertFalse(a.intersects(b1)) +assert not a.intersects(b1) print("\nuse_simulation=False") b2 = spot.tgba_determinize(b, False, True, False, True) -tc.assertEqual(b2.num_states(), 5) +assert b2.num_states() == 5 b2 = spot.remove_fin(spot.dualize(b2)) -tc.assertFalse(a.intersects(b2)) +assert not a.intersects(b2) diff --git a/tests/python/complement_semidet.py b/tests/python/complement_semidet.py index da06749a3..5ab4557bc 100644 --- a/tests/python/complement_semidet.py +++ b/tests/python/complement_semidet.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -19,8 +19,6 @@ import spot import buddy -from unittest import TestCase -tc = TestCase() def complement(aut): @@ -37,4 +35,4 @@ for aut in spot.automata( comp = complement(aut) semidet_comp = spot.complement_semidet(aut, True) - tc.assertTrue(comp.equivalent_to(semidet_comp)) + assert(comp.equivalent_to(semidet_comp)) diff --git a/tests/python/declenv.py b/tests/python/declenv.py index 3ab47736b..868f6ca1d 100644 --- a/tests/python/declenv.py +++ b/tests/python/declenv.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -21,8 +21,6 @@ # 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") @@ -30,27 +28,26 @@ env.declare("b") f1a = spot.parse_infix_psl("a U b") f1b = spot.parse_infix_psl("a U b", env) -tc.assertFalse(f1a.errors) -tc.assertFalse(f1b.errors) - +assert not f1a.errors +assert not 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. -tc.assertEqual(f1a.f, f1b.f) +assert f1a.f == f1b.f f2 = spot.parse_infix_psl("(a U b) U c", env) -tc.assertTrue(f2.errors) +assert f2.errors ostr = spot.ostringstream() f2.format_errors(ostr) err = ostr.str() -tc.assertIn("unknown atomic proposition `c'", err) +assert "unknown atomic proposition `c'" in err f3 = spot.parse_prefix_ltl("R a d", env) -tc.assertTrue(f3.errors) +assert f3.errors ostr = spot.ostringstream() f3.format_errors(ostr) err = ostr.str() -tc.assertIn("unknown atomic proposition `d'", err) +assert "unknown atomic proposition `d'" in err f4 = spot.parse_prefix_ltl("R a b", env) -tc.assertFalse(f4.errors) +assert not f4.errors diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py index 47741fb72..5f6ad46cb 100644 --- a/tests/python/decompose_scc.py +++ b/tests/python/decompose_scc.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et +# Copyright (C) 2017, 2021 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() aut = spot.translate('(Ga -> Gb) W c') si = spot.scc_info(aut) @@ -28,10 +26,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)] -tc.assertEqual(len(rej), 1) +assert len(rej) == 1 s = spot.decompose_scc(si, rej[0]).to_str('hoa', '1.1') -tc.assertEqual(s, """HOA: v1.1 +assert (s == """HOA: v1.1 States: 3 Start: 0 AP: 3 "b" "a" "c" @@ -58,8 +56,7 @@ except RuntimeError: else: raise AssertionError -tc.assertEqual(spot.decompose_scc(si, 0, True).to_str('hoa', '1.1'), -"""HOA: v1.1 +assert (spot.decompose_scc(si, 0, True).to_str('hoa', '1.1') == """HOA: v1.1 States: 4 Start: 0 AP: 3 "b" "a" "c" @@ -84,8 +81,7 @@ State: 3 [1] 3 --END--""") -tc.assertEqual(spot.decompose_scc(si, 2, True).to_str('hoa', '1.1'), -"""HOA: v1.1 +assert (spot.decompose_scc(si, 2, True).to_str('hoa', '1.1') == """HOA: v1.1 States: 2 Start: 0 AP: 3 "b" "a" "c" @@ -107,4 +103,4 @@ try: except RuntimeError: pass else: - raise AssertionError("missing exception") + raise AssertionError diff --git a/tests/python/det.py b/tests/python/det.py index 36fa31ff3..03f07c096 100644 --- a/tests/python/det.py +++ b/tests/python/det.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -19,8 +19,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() a = spot.translate('FGa | FGb') @@ -28,10 +26,10 @@ a = spot.translate('FGa | FGb') d = spot.tgba_determinize(a, False, True, True, True, None, -1, True) cld = list(d.get_original_classes()) -tc.assertEqual([0, 1, 2, 3, 3], cld) +assert [0, 1, 2, 3, 3] == cld e = spot.sbacc(d) -tc.assertIsNone(e.get_original_states()) +assert e.get_original_states() is None cle = list(e.get_original_classes()) -tc.assertEqual(len(cle), e.num_states()) -tc.assertEqual(set(cle), set(cld)) +assert len(cle) == e.num_states() +assert set(cle) == set(cld) diff --git a/tests/python/dualize.py b/tests/python/dualize.py index b870e1e5e..81d2a2b23 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -20,8 +20,6 @@ import spot import buddy -from unittest import TestCase -tc = TestCase() match_strings = [('is_buchi', 'is_co_buchi'), ('is_generalized_buchi', 'is_generalized_co_buchi'), @@ -81,19 +79,19 @@ def test_aut(aut, d=None): def test_complement(aut): - tc.assertTrue(aut.is_deterministic()) + assert aut.is_deterministic() d = spot.dualize(aut) s = spot.product_or(aut, d) - tc.assertTrue(spot.dualize(s).is_empty()) + assert 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')) - tc.assertTrue(t[0]) + print (t[1]) + print (a.to_str('hoa')) + print (spot.dualize(a).to_str('hoa')) + assert False aut = spot.translate('a') @@ -103,7 +101,7 @@ test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 3 Start: 1 AP: 1 "a" @@ -119,7 +117,7 @@ State: 1 [!0] 2 State: 2 [t] 2 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -143,7 +141,7 @@ test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" @@ -163,7 +161,7 @@ State: 2 {0} [!1] 3 State: 3 [t] 3 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -188,7 +186,7 @@ test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 2 Start: 1 AP: 2 "a" "b" @@ -200,7 +198,7 @@ State: 0 [t] 0 State: 1 [!0 | !1] 0 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -221,10 +219,10 @@ State: 3 {1} --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 2 Start: 1 AP: 2 "a" "b" @@ -236,7 +234,7 @@ State: 0 [t] 0 State: 1 [!0 | !1] 0 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -257,10 +255,10 @@ State: 3 {0} --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 5 Start: 0 AP: 2 "a" "b" @@ -282,7 +280,7 @@ State: 3 {0} [t] 3 State: 4 [t] 4 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -304,10 +302,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" @@ -329,7 +327,7 @@ State: 2 [!0&!1] 0&2 State: 3 [t] 3 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -350,10 +348,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -364,7 +362,7 @@ properties: deterministic terminal --BODY-- State: 0 [t] 0 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -384,10 +382,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -398,7 +396,7 @@ properties: deterministic terminal --BODY-- State: 0 [t] 0 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -421,7 +419,7 @@ State: 2 dual = spot.dualize(aut) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -437,7 +435,7 @@ State: 1 {0} [t] 1 State: 2 [t] 2 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -458,10 +456,10 @@ State: 2 dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 2 Start: 0 AP: 1 "a" @@ -473,7 +471,7 @@ State: 0 [!0] 1 State: 1 {0} [t] 1 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -497,10 +495,10 @@ State: 3 {0} --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 3 Start: 0 AP: 1 "a" @@ -517,7 +515,7 @@ State: 1 [0] 2 State: 2 {0} [t] 2 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -538,10 +536,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -tc.assertTrue(dualtype(aut, dual)) +assert dualtype(aut, dual) h = dual.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 3 Start: 0 AP: 1 "a" @@ -557,14 +555,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') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 5 Start: 0 AP: 2 "a" "b" @@ -591,7 +589,7 @@ State: 3 {0} [0] 4 State: 4 [t] 4 ---END--""") +--END--""" opts = spot.option_map() opts.set('output', spot.randltlgenerator.LTL) diff --git a/tests/python/ecfalse.py b/tests/python/ecfalse.py index ccbaa2693..36301914b 100644 --- a/tests/python/ecfalse.py +++ b/tests/python/ecfalse.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ import spot from buddy import bddfalse, bddtrue -from unittest import TestCase -tc = TestCase() a = spot.automaton(""" HOA: v1 @@ -45,8 +43,8 @@ for e in a.out(1): if e.dst == 0: e.cond = bddfalse -tc.assertIsNone(a.accepting_run()) -tc.assertTrue(a.is_empty()) +assert a.accepting_run() is None +assert a.is_empty() for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']: print(name) @@ -54,13 +52,13 @@ for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']: res = ec.check() if res is not None: print(res.accepting_run()) - tc.assertIsNone(res) + assert res is None si = spot.scc_info(a) -tc.assertEqual(si.scc_count(), 1) # only one accessible SCC +assert si.scc_count() == 1 # only one accessible SCC a.set_init_state(0) si = spot.scc_info(a) -tc.assertEqual(si.scc_count(), 2) +assert 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))) @@ -73,16 +71,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() -tc.assertIsNotNone(r) -tc.assertTrue(r.replay(spot.get_cout())) +assert r is not None +assert r.replay(spot.get_cout()) for e in a.out(7): if e.dst == 2: e.cond = bddfalse s = a.accepting_run() -tc.assertIsNotNone(s) -tc.assertTrue(s.replay(spot.get_cout())) +assert s is not None +assert s.replay(spot.get_cout()) for e in a.out(2): if e.dst == 1: e.cond = bddfalse s = a.accepting_run() -tc.assertIsNone(s) +assert s is None diff --git a/tests/python/except.py b/tests/python/except.py index 8674721c9..178e419b4 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -24,8 +24,6 @@ import spot import buddy -from unittest import TestCase -tc = TestCase() def report_missing_exception(): @@ -37,7 +35,7 @@ aut.set_acceptance(spot.acc_cond("parity min even 4")) try: spot.iar(aut) except RuntimeError as e: - tc.assertIn('iar() expects Rabin-like or Streett-like input', str(e)) + assert 'iar() expects Rabin-like or Streett-like input' in str(e) else: report_missing_exception() @@ -45,7 +43,7 @@ alt = spot.dualize(spot.translate('FGa | FGb')) try: spot.tgba_determinize(alt) except RuntimeError as e: - tc.assertIn('tgba_determinize() does not support alternation', str(e)) + assert 'tgba_determinize() does not support alternation' in str(e) else: report_missing_exception() @@ -54,18 +52,18 @@ aps = aut.ap() rem = spot.remove_ap() rem.add_ap('"a"=0,b') aut = rem.strip(aut) -tc.assertEqual(aut.ap(), aps[2:]) +assert aut.ap() == aps[2:] try: rem.add_ap('"a=0,b') except ValueError as e: - tc.assertIn("""missing closing '"'""", str(e)) + assert """missing closing '"'""" in str(e) else: report_missing_exception() try: rem.add_ap('a=0=b') except ValueError as e: - tc.assertIn("""unexpected '=' at position 3""", str(e)) + assert """unexpected '=' at position 3""" in str(e) else: report_missing_exception() @@ -75,7 +73,7 @@ for meth in ('scc_has_rejecting_cycle', 'is_inherently_weak_scc', try: getattr(spot, meth)(si, 20) except ValueError as e: - tc.assertIn("invalid SCC number", str(e)) + assert "invalid SCC number" in str(e) else: report_missing_exception() @@ -91,15 +89,14 @@ si = spot.scc_info(alt) try: si.determine_unknown_acceptance() except RuntimeError as e: - tc.assertIn("scc_info::determine_unknown_acceptance() does not supp", - str(e)) + assert "scc_info::determine_unknown_acceptance() does not supp" in str(e) else: report_missing_exception() try: alt.set_init_state(999) except ValueError as e: - tc.assertIn("set_init_state()", str(e)) + assert "set_init_state()" in str(e) else: report_missing_exception() @@ -110,7 +107,7 @@ alt.set_init_state(u) try: alt.set_init_state(u - 1) except ValueError as e: - tc.assertIn("set_init_state()", str(e)) + assert "set_init_state()" in str(e) else: report_missing_exception() @@ -119,21 +116,21 @@ r = spot.twa_run(aut) try: a = r.as_twa() except RuntimeError as e: - tc.assertIn("empty cycle", str(e)) + assert "empty cycle" in str(e) else: report_missing_exception() try: a = r.replay(spot.get_cout()) except RuntimeError as e: - tc.assertIn("empty cycle", str(e)) + assert "empty cycle" in str(e) else: report_missing_exception() try: a = r.reduce() except RuntimeError as e: - tc.assertIn("empty cycle", str(e)) + assert "empty cycle" in str(e) else: report_missing_exception() @@ -141,12 +138,12 @@ a = spot.translate('Fa') a = spot.to_generalized_rabin(a, False) r = a.accepting_run() r = r.reduce() -tc.assertEqual(r.cycle[0].acc, spot.mark_t([1])) +assert r.cycle[0].acc == spot.mark_t([1]) r.cycle[0].acc = spot.mark_t([0]) try: r.reduce(); except RuntimeError as e: - tc.assertIn("expects an accepting cycle", str(e)) + assert "expects an accepting cycle" in str(e) else: report_missing_exception() @@ -154,7 +151,7 @@ f = spot.formula('GF(a | Gb)') try: spot.gf_guarantee_to_ba(f, spot._bdd_dict) except RuntimeError as e: - tc.assertIn("guarantee", str(e)) + assert "guarantee" in str(e) else: report_missing_exception() @@ -162,7 +159,7 @@ f = spot.formula('FG(a | Fb)') try: spot.fg_safety_to_dca(f, spot._bdd_dict) except RuntimeError as e: - tc.assertIn("safety", str(e)) + assert "safety" in str(e) else: report_missing_exception() @@ -171,28 +168,28 @@ m = spot.mark_t([n - 1]) try: m = spot.mark_t([0]) << n except RuntimeError as e: - tc.assertIn("Too many acceptance sets", str(e)) + assert "Too many acceptance sets" in str(e) else: report_missing_exception() try: m.set(n) except RuntimeError as e: - tc.assertIn("bit index is out of bounds", str(e)) + assert "bit index is out of bounds" in str(e) else: report_missing_exception() try: m = spot.mark_t([0, n, 1]) except RuntimeError as e: - tc.assertIn("Too many acceptance sets used. The limit is", str(e)) + assert "Too many acceptance sets used. The limit is" in str(e) else: report_missing_exception() try: spot.complement_semidet(spot.translate('Gb R a', 'ba')) except RuntimeError as e: - tc.assertIn("requires a semi-deterministic input", str(e)) + assert "requires a semi-deterministic input" in str(e) else: report_missing_exception() @@ -200,55 +197,52 @@ try: spot.translate('F(G(a | !a) & ((b <-> c) W d))', 'det', 'any') except ValueError as e: s = str(e) - tc.assertIn('det', s) - tc.assertIn('any', s) + assert 'det' in s + assert 'any' in s else: report_missing_exception() a1 = spot.translate('FGa') a2 = spot.translate('Gb') -tc.assertFalse(spot.is_deterministic(a1)) -tc.assertTrue(spot.is_deterministic(a2)) +assert not spot.is_deterministic(a1) +assert spot.is_deterministic(a2) try: spot.product_xor(a1, a2) except RuntimeError as e: - tc.assertIn("product_xor() only works with deterministic automata", str(e)) + assert "product_xor() only works with deterministic automata" in str(e) else: report_missing_exception() try: spot.product_xor(a2, a1) except RuntimeError as e: - tc.assertIn("product_xor() only works with deterministic automata", str(e)) + assert "product_xor() only works with deterministic automata" in str(e) else: report_missing_exception() try: spot.product_xnor(a1, a2) except RuntimeError as e: - tc.assertIn("product_xnor() only works with deterministic automata", str(e)) + assert "product_xnor() only works with deterministic automata" in str(e) else: report_missing_exception() try: spot.product_xnor(a2, a1) except RuntimeError as e: - tc.assertIn("product_xnor() only works with deterministic automata", str(e)) + assert "product_xnor() only works with deterministic automata" in str(e) else: report_missing_exception() try: spot.solve_safety_game(a1) except RuntimeError as e: - tc.assertIn( - "solve_safety_game(): arena should have true acceptance", - str(e)) + assert "solve_safety_game(): arena should have true acceptance" in str(e) else: report_missing_exception() try: spot.solve_parity_game(a1) except RuntimeError as e: - tc.assertIn( - "solve_parity_game(): arena must have max-odd acceptance condition", - str(e)) + assert "solve_parity_game(): arena must have max-odd acceptance condition" \ + in str(e) else: report_missing_exception() @@ -256,16 +250,16 @@ else: try: spot.formula_Star(spot.formula("a"), 10, 333) except OverflowError as e: - tc.assertIn("333", str(e)) - tc.assertIn("254", str(e)) + assert "333" in str(e) + assert "254" in str(e) else: report_missing_exception() try: spot.formula_FStar(spot.formula("a"), 333, 400) except OverflowError as e: - tc.assertIn("333", str(e)) - tc.assertIn("254", str(e)) + assert "333" in str(e) + assert "254" in str(e) else: report_missing_exception() @@ -273,15 +267,15 @@ try: spot.formula_nested_unop_range(spot.op_F, spot.op_Or, 333, 400, spot.formula("a")) except OverflowError as e: - tc.assertIn("333", str(e)) - tc.assertIn("254", str(e)) + assert "333" in str(e) + assert "254" in str(e) else: report_missing_exception() try: spot.formula_FStar(spot.formula("a"), 50, 40) except OverflowError as e: - tc.assertIn("reversed", str(e)) + assert "reversed" in str(e) else: report_missing_exception() @@ -293,41 +287,5 @@ try: a.to_str() except RuntimeError as e: se = str(e) - 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() + assert "synthesis-outputs" in se + assert "unregistered proposition" in se diff --git a/tests/python/game.py b/tests/python/game.py index d7aec2f38..9d77c153d 100644 --- a/tests/python/game.py +++ b/tests/python/game.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2020 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -19,8 +19,6 @@ # along with this program. If not, see . 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: @@ -29,10 +27,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--""") -tc.assertFalse(spot.solve_parity_game(g)) +assert spot.solve_parity_game(g) == False s = spot.highlight_strategy(g).to_str("HOA", "1.1") -tc.assertEqual(s, """HOA: v1.1 +assert s == """HOA: v1.1 States: 9 Start: 0 AP: 2 "a" "b" @@ -62,4 +60,4 @@ State: 6 {1} State: 7 State: 8 {1} [0] 2 ---END--""") +--END--""" diff --git a/tests/python/gen.py b/tests/python/gen.py index a9fed6890..dd844741c 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2017 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,66 +23,63 @@ import spot.gen as gen from sys import exit -from unittest import TestCase -tc = TestCase() k2 = gen.aut_pattern(gen.AUT_KS_NCA, 2) -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()) +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() # to_str is defined in the spot package, so this makes sure # the type returned by spot.gen.ks_nca() is the correct one. -tc.assertIn('to_str', dir(k2)) +assert 'to_str' in dir(k2) k3 = gen.aut_pattern(gen.AUT_L_NBA, 3) -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 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(k2.get_dict(), k3.get_dict()) +assert k2.get_dict() == k3.get_dict() try: gen.aut_pattern(gen.AUT_KS_NCA, 0) except RuntimeError as e: - tc.assertIn('positive argument', str(e)) + assert 'positive argument' in str(e) else: exit(2) f = gen.ltl_pattern(gen.LTL_AND_F, 3) -tc.assertEqual(f.size(), 3) -tc.assertEqual(gen.ltl_pattern_name(gen.LTL_AND_F), "and-f") +assert f.size() == 3 +assert gen.ltl_pattern_name(gen.LTL_AND_F) == "and-f" try: gen.ltl_pattern(1000, 3) except RuntimeError as e: - tc.assertIn('unsupported pattern', str(e)) + assert 'unsupported pattern' in str(e) else: exit(2) try: gen.ltl_pattern(gen.LTL_OR_G, -10) except RuntimeError as e: - tc.assertIn('or-g', str(e)) - tc.assertIn('positive', str(e)) + assert 'or-g' in str(e) + assert 'positive' in str(e) else: exit(2) -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 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(32, sum(p.num_states() - for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), - (gen.AUT_KS_NCA, 5)))) +assert 32 == sum(p.num_states() + for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), + (gen.AUT_KS_NCA, 5))) diff --git a/tests/python/genem.py b/tests/python/genem.py index 0c9d0809a..5da9ce85c 100644 --- a/tests/python/genem.py +++ b/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,8 +22,6 @@ # 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 @@ -181,7 +179,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() - tc.assertTrue(fo >= 0, acc) + assert fo >= 0, acc for part in si.split_on_sets(scc, [fo]): if not generic_emptiness2(part): return False @@ -311,10 +309,10 @@ def run_bench(automata): + str(res3b)[0] + str(res3c)[0] + str(res3d)[0] + str(res4)[0] + str(res5)[0]) print(res) - tc.assertIn(res, ('TTTTTTTT', 'FFFFFFFF')) + assert res in ('TTTTTTTT', 'FFFFFFFF') if res == 'FFFFFFFF': run3 = spot.generic_accepting_run(aut) - tc.assertTrue(run3.replay(spot.get_cout())) + assert run3.replay(spot.get_cout()) is True run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360, act]) diff --git a/tests/python/implies.py b/tests/python/implies.py index 24d74b720..2e4e64ddd 100755 --- a/tests/python/implies.py +++ b/tests/python/implies.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2012, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2012 Laboratoire de Recherche et Développement # de l'EPITA. # # This file is part of Spot, a model checking library. @@ -19,8 +19,6 @@ import sys from buddy import * -from unittest import TestCase -tc = TestCase() bdd_init(10000, 10000) bdd_setvarnum(5) @@ -35,26 +33,26 @@ e = V[1] & V[2] & -V[3] & V[4] f = V[0] & -V[3] & V[4] g = -V[0] | V[1] -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)) +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)) a = (-V[2] & (-V[1] | V[0])) | (-V[0] & V[1] & V[2]) b = V[1] | -V[2] -tc.assertTrue(bdd_implies(a, b)) +assert(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 diff --git a/tests/python/intrun.py b/tests/python/intrun.py index e3b708a95..c86c6d643 100644 --- a/tests/python/intrun.py +++ b/tests/python/intrun.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,8 +18,6 @@ # along with this program. If not, see . 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 @@ -36,5 +34,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() -tc.assertTrue(c.intersects(b)) -tc.assertFalse(c.intersects(a)) +assert c.intersects(b) +assert not c.intersects(a) diff --git a/tests/python/kripke.py b/tests/python/kripke.py index fa92b3fa9..f3ce218b2 100644 --- a/tests/python/kripke.py +++ b/tests/python/kripke.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,9 +19,6 @@ 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")) @@ -54,25 +51,25 @@ State: [0&1] 1 "0" State: [!0&!1] 2 "2" 2 1 --END--""" -tc.assertEqual(hoa, k.to_str('HOA')) -tc.assertEqual(k.num_states(), 3) -tc.assertEqual(k.num_edges(), 5) +assert hoa == k.to_str('HOA') +assert k.num_states() == 3 +assert k.num_edges() == 5 res = [] for e in k.out(s1): res.append((e.src, e.dst)) -tc.assertEqual(res, [(1, 0), (1, 2)]) +assert res == [(1, 0), (1, 2)] res = [] for e in k.edges(): res.append((e.src, e.dst)) -tc.assertEqual(res, [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)]) +assert res == [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)] res = [] for s in k.states(): res.append(s.cond()) -tc.assertEqual(res, [cond1, cond2, cond3]) +assert res == [cond1, cond2, cond3] -tc.assertEqual(k.states()[0].cond(), cond1) -tc.assertEqual(k.states()[1].cond(), cond2) -tc.assertEqual(k.states()[2].cond(), cond3) +assert k.states()[0].cond() == cond1 +assert k.states()[1].cond() == cond2 +assert k.states()[2].cond() == cond3 diff --git a/tests/python/langmap.py b/tests/python/langmap.py index 723a5c0d5..6fd860986 100644 --- a/tests/python/langmap.py +++ b/tests/python/langmap.py @@ -1,6 +1,6 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017, 2020, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE) +# Copyright (C) 2016, 2017, 2020 Laboratoire de Recherche et Développement +# de l'Epita (LRDE) # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ import spot import sys -from unittest import TestCase -tc = TestCase() def hstates(txt): @@ -33,10 +31,13 @@ def hstates(txt): def test(f, opt, expected): aut = spot.translate(f, *opt, 'deterministic') v = spot.language_map(aut) - tc.assertEqual(len(v), aut.num_states()) + assert len(v) == aut.num_states() spot.highlight_languages(aut) l = hstates(aut.to_str('hoa', '1.1')) - tc.assertEqual(l, expected) + if l != expected: + print('for {}\nexpected: {}\n but got: {}'.format(f, expected, l), + file=sys.stderr) + exit(1) test('GF(a) & GFb & c', ['Buchi', 'SBAcc'], '1 0 2 0 3 0') @@ -49,6 +50,6 @@ test('Xa', ['Buchi', 'SBAcc'], '') try: test('FGa', ['Buchi'], '') except RuntimeError as e: - tc.assertIn('language_map only works with deterministic automata', str(e)) + assert 'language_map only works with deterministic automata'in str(e) else: exit(1) diff --git a/tests/python/ltl2tgba.py b/tests/python/ltl2tgba.py index 913c557be..25fff4566 100755 --- a/tests/python/ltl2tgba.py +++ b/tests/python/ltl2tgba.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021-2022 Laboratoire de -# Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021 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: - raise RuntimeError("unspecified translator") + assert "unspecified translator" if wdba: a = spot.ensure_digraph(a) @@ -117,7 +117,7 @@ if f: elif output == 6: spot.print_lbtt(cout, a) else: - raise RuntimeError("unknown output option") + assert "unknown output option" if degeneralize_opt: del degeneralized @@ -137,6 +137,4 @@ del dict # not necessary in other implementations. from platform import python_implementation if python_implementation() == 'CPython': - from unittest import TestCase - tc = TestCase() - tc.assertTrue(spot.fnode_instances_check()) + assert spot.fnode_instances_check() diff --git a/tests/python/ltlf.py b/tests/python/ltlf.py index b13432d3e..5676a2a1b 100644 --- a/tests/python/ltlf.py +++ b/tests/python/ltlf.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2016 Laboratoire de Recherche et Développement de # l'Epita # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() lcc = spot.language_containment_checker() @@ -45,5 +43,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)) - tc.assertTrue(lcc.equal(f3, f4)) + assert lcc.equal(f3, f4) print() diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index 208e0c321..98562743c 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009-2012, 2014-2017, 2019, 2021-2022 Laboratoire de -# Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2009-2012, 2014-2017, 2019, 2021 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,8 +22,6 @@ import sys import spot -from unittest import TestCase -tc = TestCase() e = spot.default_environment.instance() @@ -43,11 +41,11 @@ for str1, isl in l: pf = spot.parse_infix_psl(str2, e) if pf.format_errors(spot.get_cout()): sys.exit(1) - tc.assertEqual(isl, pf.f.is_leaf()) + assert isl == pf.f.is_leaf() del pf -tc.assertTrue(spot.formula('a').is_leaf()) -tc.assertTrue(spot.formula('0').is_leaf()) +assert spot.formula('a').is_leaf() +assert spot.formula('0').is_leaf() for str1 in ['a * b', 'a xor b', 'a <-> b']: pf = spot.parse_infix_boolean(str1, e, False) @@ -68,21 +66,21 @@ for (x, op) in [('a* <-> b*', "`<->'"), ('a*[=2]', "[=...]"), ('a*[->2]', "[->...]")]: f5 = spot.parse_infix_sere(x) - tc.assertTrue(f5.errors) + assert f5.errors ostr = spot.ostringstream() f5.format_errors(ostr) err = ostr.str() - tc.assertIn("not a Boolean expression", err) - tc.assertIn(op, err) - tc.assertIn("SERE", err) + assert "not a Boolean expression" in err + assert op in err + assert "SERE" in err del f5 f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]') -tc.assertFalse(f6.errors) +assert not f6.errors del f6 f6 = spot.parse_infix_sere('-') -tc.assertTrue(f6.errors) +assert f6.errors del f6 for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), @@ -152,12 +150,12 @@ for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), ('{"X}', "missing closing brace"), ]: f7 = spot.parse_infix_psl(x) - tc.assertTrue(f7.errors) + assert f7.errors ostr = spot.ostringstream() f7.format_errors(ostr) err = ostr.str() print(err) - tc.assertIn(msg, err) + assert msg in err del f7 for (x, msg) in [('a&', "missing right operand for \"and operator\""), @@ -176,12 +174,12 @@ for (x, msg) in [('a&', "missing right operand for \"and operator\""), ('!', "missing right operand for \"not operator\""), ]: f8 = spot.parse_infix_boolean(x) - tc.assertTrue(f8.errors) + assert f8.errors ostr = spot.ostringstream() f8.format_errors(ostr) err = ostr.str() print(err) - tc.assertIn(msg, err) + assert msg in err del f8 for (x, msg) in [('a->', "missing right operand for \"implication operator\""), @@ -193,12 +191,12 @@ for (x, msg) in [('a->', "missing right operand for \"implication operator\""), ]: f9 = spot.parse_infix_psl(x, spot.default_environment.instance(), False, True) - tc.assertTrue(f9.errors) + assert f9.errors ostr = spot.ostringstream() f9.format_errors(ostr) err = ostr.str() print(err) - tc.assertIn(msg, err) + assert msg in err del f9 # force GC before fnode_instances_check(), unless it's CPython @@ -207,15 +205,15 @@ if python_implementation() != 'CPython': import gc gc.collect() -tc.assertTrue(spot.fnode_instances_check()) +assert spot.fnode_instances_check() f = spot.formula_F(2, 4, spot.formula_ap("a")) -tc.assertEqual(f, spot.formula("XX(a | X(a | X(a)))")) +assert f == spot.formula("XX(a | X(a | X(a)))") f = spot.formula_G(2, 4, spot.formula_ap("a")) -tc.assertEqual(f, spot.formula("XX(a & X(a & X(a)))")) +assert f == spot.formula("XX(a & X(a & X(a)))") f = spot.formula_X(2, spot.formula_ap("a")) -tc.assertEqual(f, spot.formula("XX(a)")) +assert f == spot.formula("XX(a)") f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a")) -tc.assertEqual(f, spot.formula("XXG(a)")) +assert f == spot.formula("XXG(a)") f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a")) -tc.assertEqual(f, spot.formula("XXF(a)")) +assert f == spot.formula("XXF(a)") diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index c21c3b7f1..7b88f07dc 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021-2022 Laboratoire de +# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021 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,8 +22,6 @@ 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 @@ -37,13 +35,13 @@ b = spot.formula.ap('b') c = spot.formula.ap('c') c2 = spot.formula.ap('c') -tc.assertEqual(c, c2) +assert c == c2 op = spot.formula.And([a, b]) op2 = spot.formula.And([op, c]) op3 = spot.formula.And([a, c, b]) -tc.assertEqual(op2, op3) +assert op2 == op3 # The symbol for a subformula which hasn't been cloned is better # suppressed, so we don't attempt to reuse it elsewhere. @@ -54,12 +52,12 @@ sys.stdout.write('op2 = %s\n' % str(op2)) del a, b, c2 sys.stdout.write('op3 = %s\n' % str(op3)) -tc.assertEqual(op2, op3) +assert op2 == op3 op4 = spot.formula.Or([op2, op3]) sys.stdout.write('op4 = %s\n' % str(op4)) -tc.assertEqual(op4, op2) +assert op4 == op2 del op2, op3, op4 @@ -80,11 +78,10 @@ f5 = spot.formula.Xor(F, c) del a, b, c, T, F, f1, f2, f4, f5 if is_cpython: - tc.assertTrue(spot.fnode_instances_check()) + assert spot.fnode_instances_check() # ---------------------------------------------------------------------- -tc.assertEqual(str([str(x) for x in spot.formula('a &b & c')]), - "['a', 'b', 'c']") +assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']" def switch_g_f(x): @@ -96,7 +93,7 @@ def switch_g_f(x): f = spot.formula('GFa & XFGb & Fc & G(a | b | Fd)') -tc.assertEqual(str(switch_g_f(f)), 'FGa & XGFb & Gc & F(a | b | Gd)') +assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)' x = 0 @@ -108,7 +105,7 @@ def count_g(f): f.traverse(count_g) -tc.assertEqual(x, 3) +assert x == 3 # ---------------------------------------------------------------------- @@ -124,14 +121,14 @@ LBT for shell: echo {f:lq} | ... Default for CSV: ...,{f:c},... Wring, centered: {f:w:~^50}""".format(f=formula) -tc.assertEqual(res, """\ +assert 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, @@ -147,8 +144,9 @@ 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) - tc.assertEqual(f, output) - tc.assertTrue(spot.are_equivalent(input, output)) + print(input, f, output) + assert(f == output) + assert(spot.are_equivalent(input, output)) def myparse(input): @@ -159,7 +157,7 @@ def myparse(input): # This used to fail, because myparse would return a pointer # to pf.f inside the destroyed pf. -tc.assertEqual(myparse('a U b'), spot.formula('a U b')) +assert myparse('a U b') == spot.formula('a U b') -tc.assertTrue(spot.is_liveness('a <-> GFb')) -tc.assertFalse(spot.is_liveness('a & GFb')) +assert spot.is_liveness('a <-> GFb') +assert not spot.is_liveness('a & GFb') diff --git a/tests/python/mealy.py b/tests/python/mealy.py index 71c7739f9..da71d1bfb 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -19,8 +19,6 @@ # along with this program. If not, see . import spot, buddy -from unittest import TestCase -tc = TestCase() # Testing Sat-based approach @@ -44,8 +42,8 @@ spot.set_state_players(a, [False,True,False,True,False,True]) spot.set_synthesis_outputs(a, o1&o2) b = spot.minimize_mealy(a) -tc.assertEqual(list(spot.get_state_players(b)).count(False), 2) -tc.assertTrue(spot.is_split_mealy_specialization(a, b)) +assert(list(spot.get_state_players(b)).count(False) == 2) +assert(spot.is_split_mealy_specialization(a, b)) test_auts = [ ("""HOA: v1 @@ -373,21 +371,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: - raise AssertionError("""Aps must start with either "i" or "o".""") + assert("""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)]) - tc.assertEqual(n_e, nenv_min) - tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_ks)) + assert(n_e == nenv_min) + assert(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) - tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True)) - tc.assertTrue(spot.are_equivalent(mealy_min_ks, mealy_min_rs)) + assert(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True)) + assert(spot.are_equivalent(mealy_min_ks, mealy_min_rs)) # Testing bisimulation (with output assignment) @@ -517,15 +515,15 @@ spot.set_synthesis_outputs(aut, & buddy.bdd_ithvar( aut.register_ap("u02alarm29control0f1d2alarm29turn2off1b"))) min_equiv = spot.reduce_mealy(aut, False) -tc.assertEqual(min_equiv.num_states(), 6) -tc.assertTrue(spot.are_equivalent(min_equiv, aut)) +assert min_equiv.num_states() == 6 +assert 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) -tc.assertEqual(min_sub.num_states(), 5) +assert min_sub.num_states() == 5 prod = spot.product(spot.complement(aut), min_sub) -tc.assertTrue(spot.generic_emptiness_check(prod)) +assert spot.generic_emptiness_check(prod) aut = spot.automaton(""" HOA: v1 @@ -566,7 +564,7 @@ State: 0 # An example that shows that we should not build a tree when we use inclusion. res = spot.reduce_mealy(aut, True) -tc.assertEqual(res.to_str(), exp) +assert res.to_str() == exp aut = spot.automaton(""" HOA: v1 @@ -610,4 +608,4 @@ State: 1 --END--""" res = spot.reduce_mealy(aut, True) -tc.assertEqual(res.to_str(), exp) +assert res.to_str() == exp diff --git a/tests/python/merge.py b/tests/python/merge.py index 893916953..c56d8f309 100644 --- a/tests/python/merge.py +++ b/tests/python/merge.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() aut = spot.automaton(""" HOA: v1 @@ -41,7 +39,7 @@ State: 2 out = spot.simplify_acceptance(aut) hoa = out.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -56,8 +54,8 @@ State: 1 [1] 2 {0} State: 2 [1] 0 ---END--""") -tc.assertTrue(spot.are_equivalent(out, aut)) +--END--""" +assert spot.are_equivalent(out, aut) aut = spot.automaton("""HOA: v1 States: 3 @@ -77,7 +75,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -92,7 +90,7 @@ State: 1 [1] 2 {0} State: 2 [1] 0 ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -113,7 +111,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -128,7 +126,7 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -148,7 +146,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -163,7 +161,7 @@ State: 1 [1] 2 {1} State: 2 [1] 0 {0} ---END--""") +--END--""" aut = spot.automaton(""" HOA: v1 @@ -184,7 +182,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -199,7 +197,7 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -219,7 +217,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -234,7 +232,7 @@ State: 1 {0} [1] 2 State: 2 {0} [1] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -254,7 +252,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -269,7 +267,7 @@ State: 1 {0} [1] 2 State: 2 {0} [1] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -289,7 +287,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -303,7 +301,7 @@ State: 1 {1} [1] 2 State: 2 [1] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 4 @@ -337,7 +335,7 @@ State: 3 {1 3} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" @@ -366,7 +364,7 @@ State: 3 {1} [0&!1] 0 [!0&1] 3 [0&1] 2 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -390,7 +388,7 @@ State: 2 out = spot.simplify_acceptance(aut) hoa = out.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" @@ -408,8 +406,8 @@ State: 1 State: 2 [0] 2 {0} [!0] 1 {0} ---END--""") -tc.assertTrue(spot.are_equivalent(out, aut)) +--END--""" +assert spot.are_equivalent(out, aut) aut = spot.automaton("""HOA: v1 States: 4 @@ -437,7 +435,7 @@ State: 3 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 4 Start: 0 AP: 2 "p0" "p1" @@ -459,7 +457,7 @@ State: 3 [0&1] 0 {1} [0&!1] 3 {1 2} [!0] 1 {3} ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 1 @@ -477,7 +475,7 @@ State: 0 {1 2} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 1 Start: 0 AP: 2 "p0" "p1" @@ -488,7 +486,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 2 @@ -508,7 +506,7 @@ State: 1 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -521,7 +519,7 @@ State: 0 [!0] 1 {2} State: 1 [t] 1 {1 2} ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 1 @@ -538,7 +536,7 @@ State: 0 {0 1 3} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 1 Start: 0 AP: 2 "p0" "p1" @@ -549,7 +547,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 2 @@ -570,7 +568,7 @@ State: 1 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -585,7 +583,7 @@ State: 0 State: 1 [0] 1 [!0] 0 {1} ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 2 @@ -604,7 +602,7 @@ State: 1 {1} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -617,7 +615,7 @@ State: 0 [t] 1 State: 1 [t] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -638,7 +636,7 @@ State: 2 {2} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" @@ -652,7 +650,7 @@ State: 1 {0} [t] 1 State: 2 {2} [t] 1 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -674,7 +672,7 @@ State: 2 {1 2 3} out = spot.simplify_acceptance(aut) hoa = out.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" @@ -689,8 +687,8 @@ State: 1 {1} [t] 2 State: 2 {0 1} [t] 1 ---END--""") -tc.assertTrue(spot.are_equivalent(out, aut)) +--END--""" +assert spot.are_equivalent(out, aut) aut = spot.automaton("""HOA: v1 States: 2 @@ -710,7 +708,7 @@ State: 1 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -724,7 +722,7 @@ State: 0 State: 1 [0] 1 [!0] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -742,7 +740,7 @@ State: 2 --END--""") spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -757,7 +755,7 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -775,7 +773,7 @@ State: 2 --END--""") spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -tc.assertEqual(hoa, """HOA: v1 +assert hoa == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -790,4 +788,4 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""") +--END--""" diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py index 4e97abe23..e55bdabf2 100644 --- a/tests/python/mergedge.py +++ b/tests/python/mergedge.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020-2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2020, 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -20,14 +20,12 @@ 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--""") -tc.assertEqual(aut.num_edges(), 2) +assert aut.num_edges() == 2 aut.merge_edges() -tc.assertEqual(aut.num_edges(), 1) +assert aut.num_edges() == 1 aut = spot.automaton(""" HOA: v1 @@ -46,15 +44,15 @@ State: 1 [0 | 1] 1 [0&!1] 1 {0} --END--""") -tc.assertEqual(aut.num_edges(), 5) +assert aut.num_edges() == 5 aut.merge_edges() -tc.assertEqual(aut.num_edges(), 5) -tc.assertFalse(spot.is_deterministic(aut)) +assert aut.num_edges() == 5 +assert not spot.is_deterministic(aut) aut = spot.split_edges(aut) -tc.assertEqual(aut.num_edges(), 9) +assert aut.num_edges() == 9 aut.merge_edges() -tc.assertEqual(aut.num_edges(), 5) -tc.assertTrue(spot.is_deterministic(aut)) +assert aut.num_edges() == 5 +assert spot.is_deterministic(aut) aut = spot.automaton(""" HOA: v1 @@ -76,15 +74,15 @@ State: 2 [0] 1 --END--""") aut.merge_states() -tc.assertEqual(aut.num_edges(), 4) -tc.assertEqual(aut.num_states(), 2) -tc.assertTrue(spot.is_deterministic(aut)) -tc.assertTrue(aut.prop_complete()) +assert aut.num_edges() == 4 +assert aut.num_states() == 2 +assert spot.is_deterministic(aut) +assert aut.prop_complete() aut.merge_states() -tc.assertEqual(aut.num_edges(), 4) -tc.assertEqual(aut.num_states(), 2) -tc.assertTrue(spot.is_deterministic(aut)) -tc.assertTrue(aut.prop_complete()) +assert aut.num_edges() == 4 +assert aut.num_states() == 2 +assert spot.is_deterministic(aut) +assert aut.prop_complete() aa = spot.automaton(""" diff --git a/tests/python/misc-ec.py b/tests/python/misc-ec.py index 85d4aaa47..d1234bd69 100644 --- a/tests/python/misc-ec.py +++ b/tests/python/misc-ec.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2017, 2020 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,9 +18,6 @@ # along with this program. If not, see . 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 @@ -30,7 +27,7 @@ while True: break print(res.accepting_run()) n += 1 -tc.assertEqual(n, 2) +assert n == 2 for name in ['SE05', 'CVWY90', 'GV04']: aut = spot.translate("GFa && GFb") @@ -38,13 +35,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: - tc.assertIn("Büchi or weak", str(e)) + assert "Büchi or weak" in str(e) aut = spot.translate("a", 'monitor') try: ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) except RuntimeError as e: - tc.assertIn("at least one", str(e)) + assert "at least one" in str(e) aut = spot.translate("a", 'ba') ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) diff --git a/tests/python/optionmap.py b/tests/python/optionmap.py index ad526f510..667ef0b19 100755 --- a/tests/python/optionmap.py +++ b/tests/python/optionmap.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2012, 2018, 2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2010, 2012, 2018 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,67 +21,65 @@ # along with this program. If not, see . 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") -tc.assertFalse(res) +assert not res -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) +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 o.set('optb', 40) -tc.assertEqual(o.get('optb'), 40) +assert o.get('optb') == 40 res = o.parse_options("!optA !optb optC, !optB") -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) +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 res = o.parse_options("!") -tc.assertEqual(res, "!") +assert res == "!" res = o.parse_options("foo, !opt = 1") -tc.assertEqual(res, "!opt = 1") +assert res == "!opt = 1" res = o.parse_options("foo=3, opt == 1") -tc.assertEqual(res, "opt == 1") +assert res == "opt == 1" res = o.parse_options("foo=3opt == 1") -tc.assertEqual(res, "3opt == 1") +assert res == "3opt == 1" aut1 = spot.translate('GF(a <-> XXa)', 'det') -tc.assertEqual(aut1.num_states(), 4) +assert aut1.num_states() == 4 aut2 = spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') -tc.assertEqual(aut2.num_states(), 9) +assert aut2.num_states() == 9 try: spot.translate('GF(a <-> XXa)', 'det', xargs='foobar=1') except RuntimeError as e: - tc.assertIn("option 'foobar' was not used", str(e)) + assert "option 'foobar' was not used" in str(e) else: raise RuntimeError("missing exception") try: spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=0') except RuntimeError as e: - tc.assertIn("option 'gf-guarantee' was not used", str(e)) + assert "option 'gf-guarantee' was not used" in str(e) else: raise RuntimeError("missing exception") try: spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=x') except RuntimeError as e: - tc.assertIn("failed to parse option at: 'gf-guarantee=x'", str(e)) + assert "failed to parse option at: 'gf-guarantee=x'" in str(e) else: raise RuntimeError("missing exception") diff --git a/tests/python/origstate.py b/tests/python/origstate.py index 15a7ab0ad..0ca013889 100644 --- a/tests/python/origstate.py +++ b/tests/python/origstate.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017, 2022 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ import spot from sys import exit -from unittest import TestCase -tc = TestCase() aut = spot.automaton(""" HOA: v1 @@ -40,7 +38,7 @@ State: 1 """) aut2 = spot.degeneralize(aut) -tc.assertEqual(aut2.to_str(), """HOA: v1 +assert aut2.to_str() == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -58,10 +56,10 @@ State: 1 [1] 2 State: 2 {0} [1] 2 ---END--""") +--END--""" aut2.copy_state_names_from(aut) -tc.assertEqual(aut2.to_str(), """HOA: v1 +assert aut2.to_str() == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -79,7 +77,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() @@ -95,16 +93,16 @@ properties: deterministic State: 0 "1#1" {0} [1] 0 --END--""" -tc.assertEqual(aut2.to_str(), ref) +assert aut2.to_str() == ref # This makes sure that the original-states vector has also been renamed. aut2.copy_state_names_from(aut) -tc.assertEqual(aut2.to_str(), ref) +assert aut2.to_str() == ref aut2 = spot.degeneralize(aut) aut2.release_named_properties() try: aut2.copy_state_names_from(aut) except RuntimeError as e: - tc.assertIn("state does not exist in source automaton", str(e)) + assert "state does not exist in source automaton" in str(e) else: exit(1) diff --git a/tests/python/otfcrash.py b/tests/python/otfcrash.py index 8e30cb501..69acbcb1a 100644 --- a/tests/python/otfcrash.py +++ b/tests/python/otfcrash.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -23,8 +23,6 @@ import spot.aux import tempfile import shutil import sys -from unittest import TestCase -tc = TestCase() spot.ltsmin.require('divine') @@ -53,4 +51,4 @@ system async; p = spot.otf_product(k, a) return p.is_empty() - tc.assertTrue(modelcheck('X "R.found"', m)) + assert(modelcheck('X "R.found"', m) == True) diff --git a/tests/python/parity.py b/tests/python/parity.py index 6ced51c40..b0389c40e 100644 --- a/tests/python/parity.py +++ b/tests/python/parity.py @@ -19,38 +19,36 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() max_even_5 = spot.acc_code.parity(True, 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)) +assert max_even_5 == spot.acc_code.parity_max_even(5) +assert max_even_5 == spot.acc_code.parity_max(False, 5) min_even_5 = spot.acc_code.parity(False, 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)) +assert min_even_5 == spot.acc_code.parity_min_even(5) +assert min_even_5 == spot.acc_code.parity_min(False, 5) max_odd_5 = spot.acc_code.parity(True, 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)) +assert max_odd_5 == spot.acc_code.parity_max_odd(5) +assert max_odd_5 == spot.acc_code.parity_max(True, 5) min_odd_5 = spot.acc_code.parity(False, 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)) +assert min_odd_5 == spot.acc_code.parity_min_odd(5) +assert 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') - tc.assertTrue(a1.acc().is_parity()) + assert a1.acc().is_parity() a2 = spot.translate(f).postprocess('parity') - tc.assertTrue(a2.acc().is_parity()) + assert a2.acc().is_parity() a3 = spot.translate(f, 'det').postprocess('parity', 'colored') - tc.assertTrue(a3.acc().is_parity()) - tc.assertTrue(spot.is_colored(a3)) + assert a3.acc().is_parity() + assert 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: - tc.assertIn('input should have parity acceptance', str(e)) + assert 'input should have parity acceptance' in str(e) else: exit(2) @@ -66,7 +64,7 @@ State: 0 --END-- """) spot.cleanup_parity_here(a) -tc.assertEqual(a.to_str(), """HOA: v1 +assert a.to_str() == """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -77,7 +75,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""") +--END--""" a = spot.automaton(""" HOA: v1 @@ -91,7 +89,7 @@ State: 0 --END-- """) spot.cleanup_parity_here(a) -tc.assertEqual(a.to_str(), """HOA: v1 +assert a.to_str() == """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -102,7 +100,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""") +--END--""" a = spot.automaton("""HOA: v1 States: 3 @@ -122,39 +120,39 @@ State: 2 try: spot.get_state_players(a) except RuntimeError as e: - tc.assertIn("not a game", str(e)) + assert "not a game" in str(e) else: report_missing_exception() try: spot.set_state_player(a, 1, True) except RuntimeError as e: - tc.assertIn("Can only", str(e)) + assert "Can only" in str(e) else: report_missing__exception() spot.set_state_players(a, (False, True, 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) +assert spot.get_state_player(a, 0) == False +assert spot.get_state_player(a, 1) == True +assert spot.get_state_player(a, 2) == False try: spot.set_state_players(a, [True, False, False, False]) except RuntimeError as e: - tc.assertIn("many owners as states", str(e)) + assert "many owners as states" in str(e) else: report_missing_exception() try: spot.get_state_player(a, 4) except RuntimeError as e: - tc.assertIn("invalid state number", str(e)) + assert "invalid state number" in str(e) else: report_missing_exception() try: spot.set_state_player(a, 4, True) except RuntimeError as e: - tc.assertIn("invalid state number", str(e)) + assert "invalid state number" in str(e) else: report_missing_exception() @@ -170,4 +168,4 @@ oi.erase() # postprocess used to call reduce_parity that did not # work correctly on automata with deleted edges. sm = a.postprocess("gen", "small") -tc.assertEqual(sm.num_states(), 3) +assert sm.num_states() == 3 diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py index 038b33a19..cbcacb183 100755 --- a/tests/python/parsetgba.py +++ b/tests/python/parsetgba.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2012, 2014, 2015, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ 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 @@ -36,7 +34,7 @@ out.close() a = spot.parse_aut(filename, spot.make_bdd_dict()) -tc.assertFalse(a.errors) +assert not a.errors spot.print_dot(spot.get_cout(), a.aut) diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 12bc9e39a..02150d375 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019, 2020, 2021, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2019, 2020, 2021 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -23,8 +23,6 @@ import spot -from unittest import TestCase -tc = TestCase() a, b, d, f = spot.automata(""" HOA: v1 @@ -75,19 +73,19 @@ State: 1 --END-- """) -tc.assertEqual(spot.is_partially_degeneralizable(a), [0, 1]) +assert spot.is_partially_degeneralizable(a) == [0, 1] da = spot.partial_degeneralize(a, [0, 1]) -tc.assertTrue(da.equivalent_to(a)) -tc.assertEqual(da.num_states(), 2) +assert da.equivalent_to(a) +assert da.num_states() == 2 -tc.assertEqual(spot.is_partially_degeneralizable(b), [0, 1]) +assert spot.is_partially_degeneralizable(b) == [0, 1] db = spot.partial_degeneralize(b, [0, 1]) -tc.assertTrue(db.equivalent_to(b)) -tc.assertEqual(db.num_states(), 3) +assert db.equivalent_to(b) +assert db.num_states() == 3 db.copy_state_names_from(b) dbhoa = db.to_str('hoa') -tc.assertEqual(dbhoa, """HOA: v1 +assert dbhoa == """HOA: v1 States: 3 Start: 0 AP: 1 "p0" @@ -101,28 +99,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 |") -tc.assertEqual(spot.is_partially_degeneralizable(c), [1, 2]) +assert spot.is_partially_degeneralizable(c) == [1, 2] dc = spot.partial_degeneralize(c, [1, 2]) -tc.assertTrue(dc.equivalent_to(c)) -tc.assertEqual(str(dc.get_acceptance()), '(Fin(0) & Inf(2)) | Fin(1)') +assert dc.equivalent_to(c) +assert str(dc.get_acceptance()) == '(Fin(0) & Inf(2)) | Fin(1)' -tc.assertEqual(spot.is_partially_degeneralizable(d), []) +assert spot.is_partially_degeneralizable(d) == [] dd = spot.partial_degeneralize(d, []) -tc.assertTrue(dd.equivalent_to(d)) -tc.assertEqual(dd.num_states(), 1) -tc.assertEqual(str(dd.get_acceptance()), 'Inf(1) & Fin(0)') +assert dd.equivalent_to(d) +assert dd.num_states() == 1 +assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)' e = spot.dualize(b) de = spot.partial_degeneralize(e, [0, 1]) -tc.assertTrue(de.equivalent_to(e)) -tc.assertEqual(de.num_states(), 4) +assert de.equivalent_to(e) +assert de.num_states() == 4 de.copy_state_names_from(e) dehoa = de.to_str('hoa') -tc.assertEqual(dehoa, """HOA: v1 +assert dehoa == """HOA: v1 States: 4 Start: 0 AP: 1 "p0" @@ -142,18 +140,18 @@ State: 2 "3#0" State: 3 "2#0" [0] 1 {0} [!0] 2 ---END--""") +--END--""" -tc.assertEqual(spot.is_partially_degeneralizable(de), []) +assert spot.is_partially_degeneralizable(de) == [] df = spot.partial_degeneralize(f, [0, 1]) df.equivalent_to(f) -tc.assertEqual(str(df.acc()), '(1, Fin(0))') +assert str(df.acc()) == '(1, Fin(0))' try: df = spot.partial_degeneralize(f, [0, 1, 2]) except RuntimeError as e: - tc.assertIn('partial_degeneralize(): {0,1,2} does not', str(e)) + assert 'partial_degeneralize(): {0,1,2} does not' in str(e) else: raise RuntimeError("missing exception") @@ -167,13 +165,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) -tc.assertTrue(daut5.equivalent_to(aut5)) +assert daut5.equivalent_to(aut5) sets = list(range(aut5.num_sets())) -tc.assertEqual(spot.is_partially_degeneralizable(aut5), sets) +assert spot.is_partially_degeneralizable(aut5) == sets pdaut5 = spot.partial_degeneralize(aut5, sets) -tc.assertTrue(pdaut5.equivalent_to(aut5)) -tc.assertEqual(daut5.num_states(), 9) -tc.assertEqual(pdaut5.num_states(), 8) +assert pdaut5.equivalent_to(aut5) +assert daut5.num_states() == 9 +assert 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: @@ -182,13 +180,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) -tc.assertTrue(daut6.equivalent_to(aut6)) +assert daut6.equivalent_to(aut6) sets = list(range(aut6.num_sets())) -tc.assertEqual(spot.is_partially_degeneralizable(aut6), sets) +assert spot.is_partially_degeneralizable(aut6) == sets pdaut6 = spot.partial_degeneralize(aut6, sets) -tc.assertTrue(pdaut6.equivalent_to(aut6)) -tc.assertEqual(daut6.num_states(), 8) -tc.assertEqual(pdaut6.num_states(), 8) +assert pdaut6.equivalent_to(aut6) +assert daut6.num_states() == 8 +assert pdaut6.num_states() == 8 aut7 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" @@ -199,13 +197,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) -tc.assertTrue(daut7.equivalent_to(aut7)) +assert daut7.equivalent_to(aut7) sets = list(range(aut7.num_sets())) -tc.assertEqual(spot.is_partially_degeneralizable(aut7), sets) +assert spot.is_partially_degeneralizable(aut7) == sets pdaut7 = spot.partial_degeneralize(aut7, sets) -tc.assertTrue(pdaut7.equivalent_to(aut7)) -tc.assertEqual(daut7.num_states(), 10) -tc.assertEqual(pdaut7.num_states(), 10) +assert pdaut7.equivalent_to(aut7) +assert daut7.num_states() == 10 +assert 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) @@ -215,19 +213,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) -tc.assertTrue(daut8.equivalent_to(aut8)) +assert daut8.equivalent_to(aut8) sets = list(range(aut8.num_sets())) -tc.assertEqual(spot.is_partially_degeneralizable(aut8), sets) +assert spot.is_partially_degeneralizable(aut8) == sets pdaut8 = spot.partial_degeneralize(aut8, sets) -tc.assertTrue(pdaut8.equivalent_to(aut8)) -tc.assertEqual(daut8.num_states(), 22) -tc.assertEqual(pdaut8.num_states(), 9) +assert pdaut8.equivalent_to(aut8) +assert daut8.num_states() == 22 +assert pdaut8.num_states() == 9 aut9 = spot.dualize(aut8) pdaut9 = spot.partial_degeneralize(aut9, sets) -tc.assertTrue(pdaut9.equivalent_to(aut9)) +assert pdaut9.equivalent_to(aut9) # one more state than aut9, because dualize completed the automaton. -tc.assertEqual(pdaut9.num_states(), 10) +assert pdaut9.num_states() == 10 aut10 = spot.automaton("""HOA: v1 States: 3 @@ -244,10 +242,10 @@ State: 2 [0] 0 {1} [!0] 1 --END--""") -tc.assertEqual(spot.is_partially_degeneralizable(aut10), [0, 1]) +assert spot.is_partially_degeneralizable(aut10) == [0, 1] pdaut10 = spot.partial_degeneralize(aut10, [0, 1]) -tc.assertTrue(pdaut10.equivalent_to(aut10)) -tc.assertEqual(pdaut10.to_str(), """HOA: v1 +assert pdaut10.equivalent_to(aut10) +assert pdaut10.to_str() == """HOA: v1 States: 3 Start: 0 AP: 1 "p0" @@ -262,7 +260,7 @@ State: 1 State: 2 [0] 0 {1} [!0] 1 ---END--""") +--END--""" aut11 = spot.automaton("""HOA: v1 States: 3 @@ -279,10 +277,10 @@ State: 2 [0] 0 {1} [!0] 1 --END--""") -tc.assertEqual(spot.is_partially_degeneralizable(aut11), [0, 1]) +assert spot.is_partially_degeneralizable(aut11) == [0, 1] pdaut11 = spot.partial_degeneralize(aut11, [0, 1]) -tc.assertTrue(pdaut11.equivalent_to(aut11)) -tc.assertEqual(pdaut11.to_str(), """HOA: v1 +assert pdaut11.equivalent_to(aut11) +assert pdaut11.to_str() == """HOA: v1 States: 3 Start: 0 AP: 1 "p0" @@ -297,7 +295,7 @@ State: 1 State: 2 [0] 0 {2} [!0] 1 ---END--""") +--END--""" aut12 = spot.automaton("""HOA: v1 States: 3 @@ -315,24 +313,24 @@ State: 2 [0] 0 [!0] 1 {3} --END--""") -tc.assertEqual(spot.is_partially_degeneralizable(aut12), [0,1]) +assert spot.is_partially_degeneralizable(aut12) == [0,1] aut12b = spot.partial_degeneralize(aut12, [0,1]) aut12c = spot.partial_degeneralize(aut12b, [1,2]) -tc.assertTrue(aut12c.equivalent_to(aut12)) -tc.assertEqual(aut12c.num_states(), 9) +assert aut12c.equivalent_to(aut12) +assert aut12c.num_states() == 9 aut12d = spot.partial_degeneralize(aut12, [0,1,3]) aut12e = spot.partial_degeneralize(aut12d, [0,1]) -tc.assertTrue(aut12e.equivalent_to(aut12)) -tc.assertEqual(aut12e.num_states(), 9) +assert aut12e.equivalent_to(aut12) +assert aut12e.num_states() == 9 aut12f = spot.partial_degeneralize(aut12) -tc.assertTrue(aut12f.equivalent_to(aut12)) -tc.assertEqual(aut12f.num_states(), 9) +assert aut12f.equivalent_to(aut12) +assert aut12f.num_states() == 9 # Check handling of original-states dot = aut12f.to_str('dot', 'd') -tc.assertEqual(dot, """digraph "" { +assert dot == """digraph "" { rankdir=LR label="Inf(2) | (Inf(1) & Fin(0))\\n[Rabin-like 2]" labelloc="t" @@ -369,10 +367,10 @@ tc.assertEqual(dot, """digraph "" { 8 -> 4 [label="p0\\n{1,2}"] 8 -> 7 [label="p0"] } -""") +""" aut12g = spot.partial_degeneralize(aut12f) -tc.assertEqual(aut12f, aut12g) +assert aut12f == aut12g aut13 = spot.automaton("""HOA: v1 States: 2 @@ -392,8 +390,8 @@ State: 1 [!0&!1&2&3] 1 {0 2} --END--""") aut13g = spot.partial_degeneralize(aut13) -tc.assertTrue(aut13g.equivalent_to(aut13)) -tc.assertEqual(aut13g.num_states(), 3) +assert aut13g.equivalent_to(aut13) +assert aut13g.num_states() == 3 aut14 = spot.automaton("""HOA: v1 @@ -414,8 +412,8 @@ State: 1 --END-- """) aut14g = spot.partial_degeneralize(aut14) -tc.assertTrue(aut14g.equivalent_to(aut14)) -tc.assertEqual(aut14g.num_states(), 3) +assert aut14g.equivalent_to(aut14) +assert 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 @@ -441,4 +439,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) -tc.assertTrue(aut15c.equivalent_to(aut15b)) +assert aut15c.equivalent_to(aut15b) diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py index 4d00b4dae..098bafb26 100644 --- a/tests/python/prodexpt.py +++ b/tests/python/prodexpt.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016-2017, 2019-2020, 2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2016-2017, 2019-2020 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,8 +18,6 @@ # along with this program. If not, see . 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. @@ -96,14 +94,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) -tc.assertEqual(res.num_states(), 977) -tc.assertEqual(res.num_edges(), 8554) +assert res.num_states() == 977 +assert res.num_edges() == 8554 res = spot.product(left, right, spot.output_aborter(1000, 6000)) -tc.assertIsNone(res) +assert res is None res = spot.product(left, right, spot.output_aborter(900, 9000)) -tc.assertIsNone(res) +assert res is None res = spot.product(left, right, spot.output_aborter(1000, 9000)) -tc.assertIsNotNone(res) +assert res is not None 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 @@ -112,7 +110,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() -tc.assertEqual(out, """HOA: v1 +assert out == """HOA: v1 States: 1 Start: 0 AP: 0 @@ -122,9 +120,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() -tc.assertEqual(out, """HOA: v1 +assert out == """HOA: v1 States: 1 Start: 0 AP: 0 @@ -134,4 +132,4 @@ properties: trans-labels explicit-labels state-acc deterministic properties: stutter-invariant terminal --BODY-- State: 0 ---END--""") +--END--""" diff --git a/tests/python/randgen.py b/tests/python/randgen.py index 32762d02e..094ddcb3f 100755 --- a/tests/python/randgen.py +++ b/tests/python/randgen.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,11 +18,9 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() o = spot.option_map() g = spot.randltlgenerator(0, o) -tc.assertEqual(str(g.next()), '1') -tc.assertEqual(str(g.next()), '0') -tc.assertEqual(str(g.next()), 'None') +assert str(g.next()) == '1' +assert str(g.next()) == '0' +assert str(g.next()) == 'None' diff --git a/tests/python/relabel.py b/tests/python/relabel.py index 0de668b12..5a4a370eb 100644 --- a/tests/python/relabel.py +++ b/tests/python/relabel.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2019, 2022 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et Développement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() f = spot.formula('GF(a & b) -> (FG(a & b) & Gc)') m = spot.relabeling_map() @@ -28,18 +26,19 @@ res = "" for old, new in m.items(): res += "#define {} {}\n".format(old, new) res += str(g) -tc.assertEqual(res, """#define p0 a & b +print(res) +assert(res == """#define p0 a & b #define p1 c GFp0 -> (FGp0 & Gp1)""") h = spot.relabel_apply(g, m) -tc.assertEqual(h, f) +assert h == f autg = g.translate() spot.relabel_here(autg, m) -tc.assertEqual(str(autg.ap()), \ - '(spot.formula("a"), spot.formula("b"), spot.formula("c"))') -tc.assertTrue(spot.isomorphism_checker.are_isomorphic(autg, f.translate())) +assert str(autg.ap()) == \ + '(spot.formula("a"), spot.formula("b"), spot.formula("c"))' +assert spot.isomorphism_checker.are_isomorphic(autg, f.translate()) a = spot.formula('a') u = spot.formula('a U b') @@ -47,11 +46,11 @@ m[a] = u try: spot.relabel_here(autg, m) except RuntimeError as e: - tc.assertIn("new labels", str(e)) + assert "new labels" in str(e) m = spot.relabeling_map() m[u] = a try: spot.relabel_here(autg, m) except RuntimeError as e: - tc.assertIn("old labels", str(e)) + assert "old labels" in str(e) diff --git a/tests/python/remfin.py b/tests/python/remfin.py index ffff3e22a..20115a14f 100644 --- a/tests/python/remfin.py +++ b/tests/python/remfin.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et Développement de +# l'Epita # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ import spot -from unittest import TestCase -tc = TestCase() # This test used to trigger an assertion (or a segfault) # in scc_filter_states(). @@ -43,7 +41,7 @@ State: 2 aut.prop_inherently_weak(True) aut = spot.dualize(aut) aut1 = spot.scc_filter_states(aut) -tc.assertEqual(aut1.to_str('hoa'), """HOA: v1 +assert(aut1.to_str('hoa') == """HOA: v1 States: 2 Start: 0 AP: 1 "a" @@ -58,17 +56,17 @@ State: 1 [t] 1 --END--""") -tc.assertEqual(aut.scc_filter_states().to_str(), aut1.to_str()) -tc.assertIsNone(aut1.get_name()) +assert(aut.scc_filter_states().to_str() == aut1.to_str()) +assert(aut1.get_name() == None) aut1.set_name("test me") -tc.assertEqual(aut1.get_name(), "test me") +assert(aut1.get_name() == "test me") # The method is the same as the function a = spot.translate('true', 'low', 'any') -tc.assertTrue(a.prop_universal().is_maybe()) -tc.assertTrue(a.prop_unambiguous().is_maybe()) -tc.assertTrue(a.is_deterministic()) -tc.assertTrue(a.is_unambiguous()) +assert(a.prop_universal().is_maybe()) +assert(a.prop_unambiguous().is_maybe()) +assert(a.is_deterministic() == True) +assert(a.is_unambiguous() == True) a = spot.automaton(""" HOA: v1 @@ -94,4 +92,4 @@ State: 2 """) b = spot.remove_fin(a) size = (b.num_states(), b.num_edges()) -tc.assertEqual(size, (5, 13)) +assert size == (5, 13); diff --git a/tests/python/removeap.py b/tests/python/removeap.py index ba656ac89..7a9268c85 100644 --- a/tests/python/removeap.py +++ b/tests/python/removeap.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2019 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,18 +18,16 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() aut = spot.translate('a U (c & Gb)') -tc.assertFalse(spot.is_terminal_automaton(aut)) -tc.assertTrue(aut.prop_terminal().is_false()) +assert not spot.is_terminal_automaton(aut) +assert aut.prop_terminal().is_false() rem = spot.remove_ap() rem.add_ap("b") aut = rem.strip(aut) -tc.assertFalse(aut.prop_terminal().is_false()) -tc.assertTrue(spot.is_terminal_automaton(aut)) -tc.assertTrue(aut.prop_terminal().is_true()) +assert not aut.prop_terminal().is_false() +assert spot.is_terminal_automaton(aut) +assert aut.prop_terminal().is_true() aut = rem.strip(aut) -tc.assertTrue(aut.prop_terminal().is_true()) +assert aut.prop_terminal().is_true() diff --git a/tests/python/rs_like.py b/tests/python/rs_like.py index 669af5885..7b4ee75cf 100644 --- a/tests/python/rs_like.py +++ b/tests/python/rs_like.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2017 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() a = spot.vector_rs_pair() @@ -32,13 +30,12 @@ mall = spot.mark_t() def test_rs(acc, rs, expected_res, expected_pairs): res, p = getattr(acc, 'is_' + rs + '_like')() - tc.assertEqual(res, expected_res) + assert res == expected_res if expected_res: expected_pairs.sort() p = sorted(p) for a, b in zip(p, expected_pairs): - tc.assertEqual(a.fin, b.fin) - tc.assertEqual(a.inf, b.inf) + assert a.fin == b.fin and a.inf == b.inf def switch_pairs(pairs): diff --git a/tests/python/satmin.py b/tests/python/satmin.py index f9fa466f8..2d28dd405 100644 --- a/tests/python/satmin.py +++ b/tests/python/satmin.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2020, 2021, 2022 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2015, 2020, 2021 Laboratoire de Recherche et Développement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -18,234 +18,232 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() aut = spot.translate('GFa & GFb', 'Buchi', 'SBAcc') -tc.assertEqual(aut.num_sets(), 1) -tc.assertEqual(aut.num_states(), 3) -tc.assertTrue(aut.is_deterministic()) +assert aut.num_sets() == 1 +assert aut.num_states() == 3 +assert aut.is_deterministic() min1 = spot.sat_minimize(aut, acc='Rabin 1') -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_langmap=True) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=0) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=1) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=2) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=50) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=-1) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=0) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=1) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=2) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=50) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_naive=True) -tc.assertEqual(min1.num_sets(), 2) -tc.assertEqual(min1.num_states(), 2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 min2 = spot.sat_minimize(aut, acc='Streett 2') -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_langmap=True) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=0) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=1) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=2) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=50) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=-1) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=0) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=1) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=2) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=50) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_naive=True) -tc.assertEqual(min2.num_sets(), 4) -tc.assertEqual(min2.num_states(), 1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_langmap=True) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=1) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert 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) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_naive=True) -tc.assertEqual(min3.num_sets(), 4) -tc.assertEqual(min3.num_states(), 3) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_langmap=True) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=0) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=1) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=2) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=50) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=-1) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=0) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=1) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=2) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=50) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_naive=True) -tc.assertEqual(min4.num_sets(), 3) -tc.assertEqual(min4.num_states(), 2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 aut = spot.translate('GFa') -tc.assertEqual(aut.num_sets(), 1) -tc.assertEqual(aut.num_states(), 1) -tc.assertTrue(aut.is_deterministic()) +assert aut.num_sets() == 1 +assert aut.num_states() == 1 +assert aut.is_deterministic() out = spot.sat_minimize(aut, state_based=True) -tc.assertEqual(out.num_states(), 2) +assert out.num_states() == 2 out = spot.sat_minimize(aut, state_based=True, max_states=1) -tc.assertTrue(out is None) +assert out is None diff --git a/tests/python/sbacc.py b/tests/python/sbacc.py index 22d937014..445845dbc 100644 --- a/tests/python/sbacc.py +++ b/tests/python/sbacc.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017-2018, 2021, 2022 Laboratoire de Recherche et +# Copyright (C) 2017-2018, 2021 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -18,15 +18,13 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() - aut = spot.translate('GFa') -tc.assertEqual(aut.num_states(), 1) -tc.assertFalse(aut.prop_state_acc().is_true()) +assert aut.num_states() == 1 +assert not aut.prop_state_acc().is_true() aut = spot.sbacc(aut) -tc.assertEqual(aut.num_states(), 2) -tc.assertTrue(aut.prop_state_acc().is_true()) +assert aut.num_states() == 2 +assert aut.prop_state_acc().is_true() + aut = spot.automaton("""HOA: v1 States: 3 @@ -50,7 +48,7 @@ s = spot.sbacc(aut) s.copy_state_names_from(aut) h = s.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -61,7 +59,7 @@ State: 0 "0" [0] 1 State: 1 "2" {1} [t] 1 ---END--""") +--END--""" aut = spot.automaton("""HOA: v1 States: 3 @@ -85,7 +83,7 @@ d = spot.degeneralize(aut) d.copy_state_names_from(aut) h = d.to_str('hoa') -tc.assertEqual(h, """HOA: v1 +assert h == """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -97,4 +95,4 @@ State: 0 "0#0" [0] 1 State: 1 "2#0" {0} [t] 1 ---END--""") +--END--""" diff --git a/tests/python/sccfilter.py b/tests/python/sccfilter.py index 7728b70a6..6edd33e9f 100644 --- a/tests/python/sccfilter.py +++ b/tests/python/sccfilter.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2016 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -22,8 +22,6 @@ # Major) import spot -from unittest import TestCase -tc = TestCase() a = spot.automaton(""" HOA: v1.1 @@ -45,7 +43,7 @@ State: 1 "bar" --END-- """) -tc.assertEqual(spot.scc_filter(a, True).to_str('hoa', '1.1'), """HOA: v1.1 +assert (spot.scc_filter(a, True).to_str('hoa', '1.1') == """HOA: v1.1 States: 2 Start: 0 AP: 1 "a" diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index f8ade7e4b..0ac645726 100644 --- a/tests/python/sccinfo.py +++ b/tests/python/sccinfo.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() a = spot.translate('(Ga -> Gb) W c') @@ -28,11 +26,11 @@ try: si = spot.scc_info(a, 10) exit(2) except RuntimeError as e: - tc.assertIn("initial state does not exist", str(e)) + assert "initial state does not exist" in str(e) si = spot.scc_info(a) n = si.scc_count() -tc.assertEqual(n, 4) +assert n == 4 acc = 0 rej = 0 @@ -41,24 +39,24 @@ for i in range(n): acc += si.is_accepting_scc(i) rej += si.is_rejecting_scc(i) triv += si.is_trivial(i) -tc.assertEqual(acc, 3) -tc.assertEqual(rej, 1) -tc.assertEqual(triv, 0) +assert acc == 3 +assert rej == 1 +assert triv == 0 for scc in si: acc -= scc.is_accepting() rej -= scc.is_rejecting() triv -= scc.is_trivial() -tc.assertEqual(acc, 0) -tc.assertEqual(rej, 0) -tc.assertEqual(triv, 0) +assert acc == 0 +assert rej == 0 +assert 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)) -tc.assertEqual(l, [0, 1, 2, 3, 4]) +assert l == [0, 1, 2, 3, 4] i = si.initial() todo = [i] @@ -75,14 +73,14 @@ while todo: if s not in seen: seen.add(s) todo.append(s) -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 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.assertFalse(spot.is_weak_automaton(a, si)) +assert not spot.is_weak_automaton(a, si) a = spot.automaton(""" @@ -109,8 +107,8 @@ State: 3 """) si = spot.scc_info(a) si.determine_unknown_acceptance() -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)) +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) diff --git a/tests/python/sccsplit.py b/tests/python/sccsplit.py index 4a1781475..9095a1a29 100644 --- a/tests/python/sccsplit.py +++ b/tests/python/sccsplit.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement -# de l'EPITA. +# Copyright (C) 2018 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,9 +19,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() - aut = spot.translate('GF(a <-> Xa) & GF(b <-> XXb)') si = spot.scc_info(aut) @@ -30,4 +27,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() -tc.assertEqual(spot.automaton(s).num_states(), 8) +assert spot.automaton(s).num_states() == 8 diff --git a/tests/python/semidet.py b/tests/python/semidet.py index 9072f5917..856b3b7d2 100644 --- a/tests/python/semidet.py +++ b/tests/python/semidet.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() formulas = [('(Gp0 | Fp1) M 1', False, True), ('(!p1 U p1) U X(!p0 -> Fp1)', False, True), @@ -33,9 +31,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. - tc.assertTrue(aut.prop_deterministic().is_maybe() or - aut.prop_semi_deterministic().is_maybe() or - isd == issd) + assert (aut.prop_deterministic().is_maybe() or + aut.prop_semi_deterministic().is_maybe() or + isd == issd) spot.check_determinism(aut) - tc.assertEqual(aut.prop_deterministic(), isd) - tc.assertEqual(aut.prop_semi_deterministic(), issd) + assert aut.prop_deterministic() == isd + assert aut.prop_semi_deterministic() == issd diff --git a/tests/python/setacc.py b/tests/python/setacc.py index 7246bf5cc..8d20b6a49 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018, 2021, 2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2016, 2018, 2021 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,56 +19,54 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() # Test case reduced from a report from Juraj Major . a = spot.make_twa_graph(spot._bdd_dict) a.set_acceptance(0, spot.acc_code("t")) -tc.assertTrue(a.prop_state_acc()) +assert(a.prop_state_acc() == True) a.set_acceptance(1, spot.acc_code("Fin(0)")) -tc.assertEqual(a.prop_state_acc(), spot.trival.maybe()) +assert(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() -tc.assertEqual(inf, []) -tc.assertEqual(fin, [0]) +assert inf == [] +assert fin == [0] (inf, fin) = spot.acc_code("(Fin(0)|Inf(1))&Fin(2)&Inf(0)").used_inf_fin_sets() -tc.assertEqual(inf, [0, 1]) -tc.assertEqual(fin, [0, 2]) +assert inf == [0, 1] +assert 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() -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]) +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] (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_rabin_like() -tc.assertFalse(b) -tc.assertEqual(len(v), 0) +assert b == False +assert len(v) == 0 (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_streett_like() -tc.assertTrue(b) -tc.assertEqual(repr(v), \ - '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))') +assert b == True +assert 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])) -tc.assertEqual(v, v2) +assert v == v2 acc = spot.acc_cond("generalized-Rabin 1 2") (b, v) = acc.is_generalized_rabin() -tc.assertTrue(b) -tc.assertEqual(v, (2,)) +assert b == True +assert v == (2,) (b, v) = acc.is_generalized_streett() -tc.assertFalse(b) -tc.assertEqual(v, ()) +assert b == False +assert v == () (b, v) = acc.is_streett_like() -tc.assertTrue(b) +assert b == True ve = (spot.rs_pair([0], []), spot.rs_pair([], [1]), spot.rs_pair([], [2])) -tc.assertEqual(v, ve) -tc.assertEqual(acc.name(), "generalized-Rabin 1 2") +assert v == ve +assert 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, @@ -76,23 +74,23 @@ tc.assertEqual(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() -tc.assertTrue(b) -tc.assertEqual(v, (2,)) +assert b == True +assert v == (2,) (b, v) = acc.is_generalized_rabin() -tc.assertFalse(b) -tc.assertEqual(v, ()) +assert b == False +assert v == () # FIXME: We should have a way to disable the following output, as it is not # part of HOA v1. -tc.assertEqual(acc.name(), "generalized-Streett 1 2") +assert 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]) - tc.assertEqual(m.lowest(), m) + assert m.lowest() == m n = spot.mark_t([33,34]) - tc.assertEqual(n.lowest(), m) + assert n.lowest() == m except RuntimeError as e: if "Too many acceptance sets used." in str(e): pass @@ -104,24 +102,24 @@ except RuntimeError as e: from gc import collect acc = spot.translate('a').acc() collect() -tc.assertEqual(acc, spot.acc_cond('Inf(0)')) +assert acc == spot.acc_cond('Inf(0)') acc = spot.translate('b').get_acceptance() collect() -tc.assertEqual(acc, spot.acc_code('Inf(0)')) +assert 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() -tc.assertEqual(m1, [0,1]) -tc.assertEqual(m2, []) +assert m1 == [0,1] +assert m2 == [] c = spot.acc_cond('Inf(0)&Inf(1)&(Inf(2)|Fin(3))') m1 = c.fin_unit() m2 = c.inf_unit() -tc.assertEqual(m1, []) -tc.assertEqual(m2, [0,1]) +assert m1 == [] +assert m2 == [0,1] c = spot.acc_cond('Inf(0)&Inf(1)|(Inf(2)|Fin(3))') m1 = c.fin_unit() m2 = c.inf_unit() -tc.assertEqual(m1, []) -tc.assertEqual(m2, []) +assert m1 == [] +assert m2 == [] diff --git a/tests/python/setxor.py b/tests/python/setxor.py index 2fe69cd99..7cd1e5da1 100755 --- a/tests/python/setxor.py +++ b/tests/python/setxor.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement +# de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ import sys from buddy import * -from unittest import TestCase -tc = TestCase() bdd_init(10000, 10000) bdd_setvarnum(5) @@ -31,18 +29,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] -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)) +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)) d = V[1] & V[2] & -V[3] & V[4] e = V[0] & V[1] & -V[2] & -V[3] & V[4] -tc.assertEqual(e, bdd_setxor(a, d)) -tc.assertEqual(e, bdd_setxor(d, a)) +assert(e == bdd_setxor(a, d)) +assert(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 diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index 50dc2d74a..e742d69a4 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() auts = list(spot.automata(""" @@ -72,19 +70,19 @@ explicit-labels trans-acc deterministic --BODY-- State: 0 [0&!1] 0 {2 3} res = [] for a in auts: b = spot.simplify_acceptance(a) - tc.assertTrue(b.equivalent_to(a)) + assert b.equivalent_to(a) res.append(str(b.get_acceptance())) c = spot.simplify_acceptance(b) - tc.assertEqual(b.get_acceptance(), c.get_acceptance()) + assert b.get_acceptance() == c.get_acceptance() a.set_acceptance(a.num_sets(), a.get_acceptance().complement()) b = spot.simplify_acceptance(a) - tc.assertTrue(b.equivalent_to(a)) + assert b.equivalent_to(a) res.append(str(b.get_acceptance())) c = spot.simplify_acceptance(b) - tc.assertEqual(b.get_acceptance(), c.get_acceptance()) + assert b.get_acceptance() == c.get_acceptance() -tc.assertEqual(res, [ +assert res == [ 'Inf(0)', 'Fin(0)', 'Inf(1) & Fin(0)', @@ -103,4 +101,4 @@ tc.assertEqual(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))', - ]) + ] diff --git a/tests/python/simstate.py b/tests/python/simstate.py index b0b62267d..6c2ca8bc3 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018, 2020-2022 Laboratoire de Recherche +# Copyright (C) 2015, 2017-2018, 2020-2021 Laboratoire de Recherche # et Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -19,8 +19,6 @@ 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 @@ -50,7 +48,7 @@ State: 1 """) aut2 = spot.simulation(aut) -tc.assertEqual(aut2.to_str(), """HOA: v1 +assert aut2.to_str() == """HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" @@ -61,10 +59,10 @@ properties: deterministic --BODY-- State: 0 {0} [t] 0 ---END--""") +--END--""" aut2.copy_state_names_from(aut) -tc.assertEqual(aut2.to_str(), """HOA: v1 +assert aut2.to_str() == """HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" @@ -75,7 +73,7 @@ properties: deterministic --BODY-- State: 0 "[0,1]" {0} [t] 0 ---END--""") +--END--""" del aut del aut2 @@ -84,7 +82,7 @@ gcollect() aut = spot.translate('GF((p0 -> Gp0) R p1)') daut = spot.tgba_determinize(aut, True) -tc.assertEqual(daut.to_str(), """HOA: v1 +assert daut.to_str() == """HOA: v1 States: 3 Start: 0 AP: 2 "p1" "p0" @@ -108,7 +106,7 @@ State: 2 "{₀[0]₀}{₁[1]₁}" [!0&1] 2 [0&!1] 0 {0} [0&1] 1 {2} ---END--""") +--END--""" del aut del daut @@ -131,7 +129,7 @@ State: 1 """) daut = spot.tgba_determinize(aut, True) -tc.assertEqual(daut.to_str(), """HOA: v1 +assert daut.to_str() == """HOA: v1 States: 12 Start: 0 AP: 2 "a" "b" @@ -187,18 +185,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) -tc.assertEqual(a.num_states(), 8) +assert a.num_states() == 8 b = spot.simulation(a) -tc.assertEqual(b.num_states(), 3) +assert b.num_states() == 3 b.set_init_state(1) b.purge_unreachable_states() b.copy_state_names_from(a) -tc.assertEqual(b.to_str(), """HOA: v1 +assert b.to_str() == """HOA: v1 States: 1 Start: 0 AP: 2 "p0" "p1" @@ -210,7 +208,7 @@ properties: deterministic stutter-invariant State: 0 "[1,7]" [1] 0 [!1] 0 {0} ---END--""") +--END--""" aut = spot.automaton('''HOA: v1 States: 12 @@ -269,7 +267,7 @@ State: 11 [0&!1] 6 {0} [0&1] 9 {0} --END--''') -tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1 +assert spot.reduce_iterated(aut).to_str() == '''HOA: v1 States: 9 Start: 0 AP: 2 "a" "b" @@ -310,7 +308,7 @@ State: 8 [0&!1] 4 {0} [!0&1] 6 [0&1] 7 ---END--''') +--END--''' aut = spot.automaton('''HOA: v1 States: 6 @@ -334,7 +332,7 @@ State: 4 State: 5 [0] 5 --END--''') -tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1 +assert spot.reduce_iterated(aut).to_str() == '''HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -349,7 +347,7 @@ State: 1 [0] 2 State: 2 [1] 2 ---END--''') +--END--''' aut = spot.automaton('''HOA: v1 States: 5 @@ -376,7 +374,7 @@ State: 4 [0&1&!2&3] 4 {0} --END--''') -tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1 +assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1 States: 5 Start: 0 AP: 4 "p0" "p2" "p3" "p1" @@ -397,7 +395,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 @@ -412,7 +410,7 @@ State: 0 State: 1 [0] 0 --END--''') -tc.assertEqual(spot.reduce_direct_sim(aut).to_str(), '''HOA: v1 +assert spot.reduce_direct_sim(aut).to_str() == '''HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" @@ -420,7 +418,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" @@ -447,7 +445,7 @@ State: 3 [1] 1 [0&!1] 3 --END--''') -tc.assertEqual(spot.reduce_direct_cosim_sba(aut).to_str(), '''HOA: v1 +assert spot.reduce_direct_cosim_sba(aut).to_str() == '''HOA: v1 States: 4 Start: 0 AP: 3 "p2" "p3" "p1" @@ -470,7 +468,7 @@ State: 2 State: 3 [0] 1 [!0&2] 3 ---END--''') +--END--''' aut = spot.automaton('''HOA: v1 States: 4 @@ -490,7 +488,7 @@ State: 2 State: 3 {0} [1] 3 --END--''') -tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1 +assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -504,9 +502,9 @@ State: 1 [1] 2 State: 2 {0} [1] 2 ---END--''') +--END--''' -tc.assertEqual(spot.reduce_direct_sim_sba(aut).to_str(), '''HOA: v1 +assert spot.reduce_direct_sim_sba(aut).to_str() == '''HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -518,7 +516,7 @@ State: 0 [0] 1 State: 1 {0} [1] 1 ---END--''') +--END--''' aut = spot.automaton('''HOA: v1 States: 3 @@ -534,7 +532,7 @@ State: 1 State: 2 {0} [0] 2 --END--''') -tc.assertEqual(spot.reduce_iterated_sba(aut).to_str(), '''HOA: v1 +assert spot.reduce_iterated_sba(aut).to_str() == '''HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -544,7 +542,7 @@ properties: deterministic --BODY-- State: 0 {0} [0] 0 ---END--''') +--END--''' aut = spot.automaton('''HOA: v1 States: 30 @@ -632,7 +630,7 @@ State: 28 State: 29 [0&!1&!2&!3] 29 --END--''') -tc.assertEqual(spot.reduce_iterated(a).to_str(), '''HOA: v1 +assert spot.reduce_iterated(a).to_str() == '''HOA: v1 States: 8 Start: 0 AP: 2 "p0" "p1" @@ -671,7 +669,7 @@ State: 7 [!1] 1 {0} [0&1] 5 [1] 7 ---END--''') +--END--''' # issue #452 @@ -709,4 +707,4 @@ State: 8 [@p] 3 {0 1} --END--""") aut = spot.simulation(aut) -tc.assertEqual(aut.num_states(), 1) +assert aut.num_states() == 1 diff --git a/tests/python/sonf.py b/tests/python/sonf.py index 40af758b0..558f90c63 100644 --- a/tests/python/sonf.py +++ b/tests/python/sonf.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() formulas = """\ {x[*]}[]-> F({y[*]}<>-> GFz) @@ -40,4 +38,4 @@ for f1 in formulas.splitlines(): rm.add_ap(ap) a2 = rm.strip(a2) - tc.assertTrue(spot.are_equivalent(a1, a2)) + assert(spot.are_equivalent(a1, a2)) diff --git a/tests/python/split.py b/tests/python/split.py index b916f494f..adab5a931 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2022 Laboratoire de Recherche et +# Copyright (C) 2018-2021 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -19,8 +19,6 @@ 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 @@ -53,17 +51,16 @@ def do_split(f, out_list): return aut, s aut, s = do_split('(FG !a) <-> (GF b)', ['b']) -tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) +assert equiv(aut, spot.unsplit_2step(s)) del aut del s gcollect() aut, s = do_split('GFa && GFb', ['b']) -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 +assert equiv(aut, spot.unsplit_2step(s)) +# FIXME see below +# assert str_diff("""HOA: v1 # States: 3 # Start: 0 # AP: 2 "a" "b" @@ -89,11 +86,10 @@ del s gcollect() aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['ack']) -tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) - +assert 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(s.to_str(), """HOA: v1 +# we should investigate this +# assert s.to_str() == """HOA: v1 # States: 9 # Start: 0 # AP: 4 "ack" "req" "go" "grant" @@ -126,7 +122,7 @@ tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) # [!0] 1 # State: 8 {0} # [!3] 2 -# --END--""") +# --END--""" del aut del s @@ -135,4 +131,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']) -tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) +assert equiv(aut, spot.unsplit_2step(s)) diff --git a/tests/python/streett_totgba.py b/tests/python/streett_totgba.py index 8a18defbc..1c0bfc13e 100644 --- a/tests/python/streett_totgba.py +++ b/tests/python/streett_totgba.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017-2018, 2021-2022 Laboratoire de Recherche et -# Développement de l'EPITA. +# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -22,8 +22,7 @@ import spot import os import shutil import sys -from unittest import TestCase -tc = TestCase() + def tgba(a): if not a.is_existential(): @@ -34,11 +33,11 @@ def tgba(a): def test_aut(aut): stgba = tgba(aut) - tc.assertTrue(stgba.equivalent_to(aut)) + assert stgba.equivalent_to(aut) os.environ["SPOT_STREETT_CONV_MIN"] = '1' sftgba = tgba(aut) del os.environ["SPOT_STREETT_CONV_MIN"] - tc.assertTrue(stgba.equivalent_to(sftgba)) + assert stgba.equivalent_to(sftgba) slike = spot.simplify_acceptance(aut) @@ -46,7 +45,8 @@ def test_aut(aut): os.environ["SPOT_STREETT_CONV_MIN"] = "1" slftgba = tgba(slike) del os.environ["SPOT_STREETT_CONV_MIN"] - tc.assertTrue(sltgba.equivalent_to(slftgba)) + assert sltgba.equivalent_to(slftgba) + if shutil.which('ltl2dstar') is None: sys.exit(77) diff --git a/tests/python/streett_totgba2.py b/tests/python/streett_totgba2.py index 5ff97a369..852eff0af 100644 --- a/tests/python/streett_totgba2.py +++ b/tests/python/streett_totgba2.py @@ -1,7 +1,7 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement -# de l'EPITA. +# Copyright (C) 2018 Laboratoire de Recherche et Développement de +# l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,8 +19,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() # Issue 316 a = spot.automaton(""" @@ -62,11 +60,11 @@ State: 7 {1 3 4} """) tgba = spot.streett_to_generalized_buchi(a) -tc.assertTrue(tgba.acc().is_generalized_buchi()) +assert tgba.acc().is_generalized_buchi() ba = spot.simplify_acceptance(a) -tc.assertTrue(ba.acc().is_buchi()) +assert ba.acc().is_buchi() nba = spot.dualize(ba.postprocess('generic', 'deterministic')) ntgba = spot.dualize(tgba.postprocess('generic', 'deterministic')) -tc.assertFalse(ba.intersects(ntgba)) -tc.assertFalse(tgba.intersects(nba)) +assert not ba.intersects(ntgba) +assert not tgba.intersects(nba) diff --git a/tests/python/stutter.py b/tests/python/stutter.py index 05c28fda9..dafb03b7e 100644 --- a/tests/python/stutter.py +++ b/tests/python/stutter.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019-2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2019-2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,8 +23,6 @@ import spot -from unittest import TestCase -tc = TestCase() def explain_stut(f): @@ -47,20 +45,20 @@ def explain_stut(f): # Test from issue #388 w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc') -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}') +assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}' +assert 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)))') -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}') +assert str(w1) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}' +assert 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() -tc.assertTrue(w.acc().is_t()) +assert w.acc().is_t() a = spot.sl2(w) -tc.assertTrue(a.acc().is_buchi()) +assert a.acc().is_buchi() a = spot.sl(w) -tc.assertTrue(a.acc().is_buchi()) +assert a.acc().is_buchi() diff --git a/tests/python/sum.py b/tests/python/sum.py index 1f7c6e0a1..7e2e74220 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -20,8 +20,6 @@ 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. @@ -67,8 +65,8 @@ for p in zip(phi1, phi2): p0orp1 = spot.formula.Or(p) a1ora2 = spot.remove_alternation(spot.sum(a1, a2), True) - tc.assertTrue(p0orp1.equivalent_to(a1ora2)) + assert p0orp1.equivalent_to(a1ora2) p0andp1 = spot.formula.And(p) a1anda2 = spot.remove_alternation(spot.sum_and(a1, a2), True) - tc.assertTrue(p0andp1.equivalent_to(a1anda2)) + assert p0andp1.equivalent_to(a1anda2) diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py index e1a88650a..59022624c 100644 --- a/tests/python/synthesis.py +++ b/tests/python/synthesis.py @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() # A shared variable caused the 2nd call to ltl_to_game to give an incorrect # result. @@ -27,11 +25,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) - tc.assertFalse(spot.solve_game(game)) + assert not spot.solve_game(game) # A game can have only inputs game = spot.ltl_to_game("GFa", []) -tc.assertEqual(game.to_str(), """HOA: v1 +assert(game.to_str() == """HOA: v1 States: 3 Start: 0 AP: 1 "a" diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 37e111f9b..df226ebe4 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -21,8 +21,6 @@ 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 @@ -116,16 +114,17 @@ 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) - tc.assertTrue(spot.are_equivalent(aut, p1)) + assert spot.are_equivalent(aut, p1) if expected_num is not None: - tc.assertEqual(p1.num_states(), expected_num) + # print(p1.num_states(), expected_num) + assert 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) - tc.assertEqual(p2.num_states(), p1st) - tc.assertEqual(p2.num_edges(), p1ed) - tc.assertEqual(p2.num_sets(), p1se) + assert p2.num_states() == p1st + assert p2.num_edges() == p1ed + assert p2.num_sets() == p1se test(spot.automaton("""HOA: v1 name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) & @@ -352,7 +351,7 @@ State: 0 [!0&!1] 0 --END--""") p = spot.to_parity_old(a, True) -tc.assertTrue(spot.are_equivalent(a, p)) +assert spot.are_equivalent(a, p) test(a) a = spot.automaton(""" @@ -364,8 +363,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) -tc.assertEqual(p.num_states(), 22) -tc.assertTrue(spot.are_equivalent(a, p)) +assert p.num_states() == 22 +assert 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. @@ -378,22 +377,22 @@ for e in a.out(3): e.cond = bddfalse break p = spot.to_parity_old(a, True) -tc.assertEqual(p.num_states(), 22) -tc.assertTrue(spot.are_equivalent(a, p)) +assert p.num_states() == 22 +assert 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) - tc.assertTrue(spot.are_equivalent(p, d)) + assert spot.are_equivalent(p, d) for f in spot.randltl(5, 2000): n = spot.translate(f) p = spot.to_parity_old(n, True) - tc.assertTrue(spot.are_equivalent(n, p)) + assert spot.are_equivalent(n, p) # Issue #390. a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) -tc.assertTrue(a.equivalent_to(b)) +assert a.equivalent_to(b) test(a, [7, 7, 3, 7, 7, 7, 3, 3]) diff --git a/tests/python/toweak.py b/tests/python/toweak.py index 23dcf66fa..b2d908037 100644 --- a/tests/python/toweak.py +++ b/tests/python/toweak.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -18,8 +18,6 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() phi1 = """GFb X(!b | GF!a) @@ -35,7 +33,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)) - tc.assertTrue(res.equivalent_to(spot.formula.Not(spot.formula(phi)))) + assert res.equivalent_to(spot.formula.Not(spot.formula(phi))) for p in phi1.split('\n'): @@ -85,4 +83,4 @@ State: 6 --END-- """) a2 = spot.to_weak_alternating(a2) -tc.assertTrue(a2.equivalent_to(phi2)) +assert a2.equivalent_to(phi2) diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index 354ced630..b303c010b 100644 --- a/tests/python/tra2tba.py +++ b/tests/python/tra2tba.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016-2018, 2020-2022 Laboratoire de Recherche +# Copyright (C) 2016-2018, 2020-2021 Laboratoire de Recherche # et Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -18,8 +18,6 @@ # along with this program. If not, see . 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 @@ -59,7 +57,7 @@ State: 1 --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 2. aut = spot.automaton(""" @@ -99,7 +97,7 @@ State: 2 --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 3. aut = spot.automaton(""" @@ -130,7 +128,7 @@ State: 0 --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 4. aut = spot.automaton(""" @@ -170,7 +168,7 @@ State: 2 {0} --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 5. aut = spot.automaton(""" @@ -216,7 +214,7 @@ State: 3 {0} --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 6. aut = spot.automaton(""" @@ -259,7 +257,7 @@ State: 2 {0} --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 7. aut = spot.automaton(""" @@ -294,7 +292,7 @@ State: 1 {0} --END--""" res = spot.remove_fin(aut) -tc.assertEqual(res.to_str('hoa'), exp) +assert(res.to_str('hoa') == exp) # Test 8. aut = spot.automaton(""" @@ -374,9 +372,9 @@ State: 7 res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) + assert(res.equivalent_to(spot.automaton(exp))) # Test 9. aut = spot.automaton(""" @@ -413,9 +411,9 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) + assert(res.equivalent_to(spot.automaton(exp))) # Test 10. aut = spot.automaton(""" @@ -455,9 +453,9 @@ State: 2 {0} res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) + assert(res.equivalent_to(spot.automaton(exp))) # Test 11. aut = spot.automaton(""" @@ -495,9 +493,9 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) + assert(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 @@ -520,9 +518,9 @@ State: 1 --END--""" res = spot.rabin_to_buchi_if_realizable(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp2) + assert(res.to_str('hoa') == exp2) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp2))) + assert(res.equivalent_to(spot.automaton(exp2))) # Test 12. aut = spot.automaton(""" @@ -567,9 +565,9 @@ State: 3 {0} res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) + assert(res.equivalent_to(spot.automaton(exp))) # Test 13. aut = spot.automaton(""" @@ -617,9 +615,9 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) + assert(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. @@ -646,9 +644,9 @@ State: 1 res = spot.rabin_to_buchi_if_realizable(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp2) + assert(res.to_str('hoa') == exp2) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp2))) + assert(res.equivalent_to(spot.automaton(exp2))) # Test 14. aut = spot.automaton(""" @@ -683,7 +681,7 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - tc.assertEqual(res.to_str('hoa'), exp) + assert(res.to_str('hoa') == exp) else: - tc.assertTrue(res.equivalent_to(spot.automaton(exp))) -tc.assertIsNone(spot.rabin_to_buchi_if_realizable(aut)) + assert(res.equivalent_to(spot.automaton(exp))) +assert spot.rabin_to_buchi_if_realizable(aut) is None diff --git a/tests/python/trival.py b/tests/python/trival.py index ea844e29c..8fcf6a1fa 100644 --- a/tests/python/trival.py +++ b/tests/python/trival.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018, 2022 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,32 +18,30 @@ # along with this program. If not, see . import spot -from unittest import TestCase -tc = TestCase() v1 = spot.trival() v2 = spot.trival(False) v3 = spot.trival(True) v4 = spot.trival_maybe() -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) +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 for u in (v1, v2, v3): for v in (v1, v2, v3): - tc.assertEqual((u & v), -(-u | -v)) + assert (u & v) == -(-u | -v) diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index 1ebcb8ac5..b8834b211 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2021-2022 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -22,8 +22,6 @@ import spot from buddy import bddtrue, bddfalse -from unittest import TestCase -tc = TestCase() aut = spot.make_twa_graph(spot.make_bdd_dict()) @@ -31,98 +29,98 @@ try: print(aut.to_str()) exit(2) except RuntimeError as e: - tc.assertIn("no state", str(e)) + assert "no state" in str(e) try: aut.set_init_state(2) except ValueError as e: - tc.assertIn("nonexisting", str(e)) + assert "nonexisting" in str(e) try: aut.set_univ_init_state([2, 1]) except ValueError as e: - tc.assertIn("nonexisting", str(e)) + assert "nonexisting" in str(e) aut.new_states(3) aut.set_init_state(2) -tc.assertEqual(aut.get_init_state_number(), 2) +assert aut.get_init_state_number() == 2 aut.set_univ_init_state([2, 1]) -tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number()))) +assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) try: aut.get_init_state() except RuntimeError as e: s = str(e) - tc.assertIn("abstract interface" in s and "alternating automata", s) + assert "abstract interface" in s and "alternating automata" in s cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all()) -tc.assertEqual(aut.to_str(), cpy.to_str()) +assert aut.to_str() == cpy.to_str() all = aut.set_buchi() -tc.assertNotEqual(aut.to_str(), cpy.to_str()) +assert 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) -tc.assertEqual(aut.num_edges(), 1 + cpy.num_edges()) +assert 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)) -tc.assertNotEqual(cpy.prop_universal(), aut.prop_universal()) -tc.assertEqual(cpy.prop_universal(), spot.trival.maybe()) -tc.assertEqual(cpy.get_name(), None) +assert cpy.prop_universal() != aut.prop_universal() +assert cpy.prop_universal() == spot.trival.maybe() +assert cpy.get_name() == None cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False, False, False, False), True) -tc.assertEqual(cpy.get_name(), "some name") +assert cpy.get_name() == "some name" from copy import copy cpy = copy(aut) -tc.assertEqual(aut.to_str(), cpy.to_str()) +assert aut.to_str() == cpy.to_str() cpy.set_init_state(1) -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") +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" try: s = aut.state_acc_sets(0) except RuntimeError as e: - tc.assertIn("state-based acceptance", str(e)) + assert "state-based acceptance" in str(e) try: s = aut.state_is_accepting(0) except RuntimeError as e: - tc.assertIn("state-based acceptance", str(e)) + assert "state-based acceptance" in str(e) aut.prop_state_acc(True) -tc.assertEqual(aut.state_acc_sets(0), all) -tc.assertEqual(aut.state_is_accepting(0), True) +assert aut.state_acc_sets(0) == all +assert aut.state_is_accepting(0) == True aut.set_init_state(0) aut.purge_unreachable_states() i = aut.get_init_state() -tc.assertEqual(aut.state_is_accepting(i), True) +assert aut.state_is_accepting(i) == True it = aut.succ_iter(i) it.first() -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) +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 aut.release_iter(it) aut.purge_dead_states() i = aut.get_init_state() -tc.assertEqual(aut.state_is_accepting(i), False) +assert aut.state_is_accepting(i) == False aut = spot.translate('FGa') # Kill the edge between state 0 and 1 -tc.assertEqual(aut.edge_storage(2).src, 0) -tc.assertEqual(aut.edge_storage(2).dst, 1) +assert aut.edge_storage(2).src == 0 +assert aut.edge_storage(2).dst == 1 aut.edge_data(2).cond = bddfalse -tc.assertEqual(aut.num_edges(), 3) -tc.assertEqual(aut.num_states(), 2) +assert aut.num_edges() == 3 +assert aut.num_states() == 2 aut.purge_dead_states() -tc.assertEqual(aut.num_edges(), 1) -tc.assertEqual(aut.num_states(), 1) +assert aut.num_edges() == 1 +assert aut.num_states() == 1 diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py index e1b0c9e7b..df8fd86f0 100644 --- a/tests/python/zlktree.py +++ b/tests/python/zlktree.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,8 +18,6 @@ # along with this program. If not, see . 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 @@ -27,8 +25,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) -tc.assertTrue(spot.are_equivalent(a, b)) -tc.assertTrue(b.acc().is_buchi()) +assert spot.are_equivalent(a, b) +assert b.acc().is_buchi() def report_missing_exception(): raise RuntimeError("missing exception") @@ -47,96 +45,95 @@ 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: - tc.assertTrue(aa.has_rabin_shape()) + assert aa.has_rabin_shape() except RuntimeError as e: - tc.assertIn('CHECK_RABIN', str(e)) + assert 'CHECK_RABIN' in str(e) else: report_missing_exception() try: - tc.assertFalse(aa.has_streett_shape()) + assert not aa.has_streett_shape() except RuntimeError as e: - tc.assertIn('CHECK_STREETT', str(e)) + assert 'CHECK_STREETT' in str(e) else: report_missing_exception() try: - tc.assertFalse(aa.has_parity_shape()) + assert not aa.has_parity_shape() except RuntimeError as e: - tc.assertIn('CHECK_PARITY', str(e)) + assert 'CHECK_PARITY' in str(e) else: report_missing_exception() aa = spot.acd(a, spot.acd_options_CHECK_RABIN) -tc.assertTrue(aa.has_rabin_shape()) -tc.assertEqual(aa.node_count(), 13) +assert aa.has_rabin_shape() +assert aa.node_count() == 13 try: - tc.assertFalse(aa.has_streett_shape()) + assert not aa.has_streett_shape() except RuntimeError as e: - tc.assertIn('CHECK_STREETT', str(e)) + assert 'CHECK_STREETT' in str(e) else: report_missing_exception() try: - tc.assertTrue(aa.has_parity_shape()) + assert aa.has_parity_shape() except RuntimeError as e: - tc.assertIn('CHECK_PARITY', str(e)) + assert 'CHECK_PARITY' in str(e) else: report_missing_exception() aa = spot.acd(a, (spot.acd_options_CHECK_PARITY | spot.acd_options_ABORT_WRONG_SHAPE)) -tc.assertTrue(aa.has_rabin_shape()) -tc.assertFalse(aa.has_streett_shape()) -tc.assertFalse(aa.has_parity_shape()) -tc.assertEqual(aa.node_count(), 0) - +assert aa.has_rabin_shape() +assert not aa.has_streett_shape() +assert not aa.has_parity_shape() +assert aa.node_count() == 0 try: aa.first_branch(0) except RuntimeError as e: - tc.assertIn('ABORT_WRONG_SHAPE', str(e)) + assert 'ABORT_WRONG_SHAPE' in str(e) else: report_missing_exception() try: aa.step(0, 0) except RuntimeError as e: - tc.assertIn('incorrect branch number', str(e)) + assert 'incorrect branch number' in str(e) else: report_missing_exception() try: aa.node_acceptance(0) except RuntimeError as e: - tc.assertIn('unknown node', str(e)) + assert 'unknown node' in str(e) else: report_missing_exception() try: aa.edges_of_node(0) except RuntimeError as e: - tc.assertIn('unknown node', str(e)) + assert 'unknown node' in str(e) else: report_missing_exception() try: aa.node_level(0) except RuntimeError as e: - tc.assertIn('unknown node', str(e)) + assert 'unknown node' in str(e) else: report_missing_exception() a = spot.translate('true') a.set_acceptance(spot.acc_cond('f')) b = spot.acd_transform(a) -tc.assertTrue(a.equivalent_to(b)) +assert a.equivalent_to(b) a = spot.translate('true') a.set_acceptance(spot.acc_cond('f')) b = spot.zielonka_tree_transform(a) -tc.assertTrue(a.equivalent_to(b)) +assert 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)) | @@ -147,8 +144,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) -tc.assertEqual(str(b.acc()), '(3, Fin(0) & (Inf(1) | Fin(2)))') -tc.assertTrue(a.equivalent_to(b)) +assert str(b.acc()) == '(3, Fin(0) & (Inf(1) | Fin(2)))' +assert a.equivalent_to(b) b = spot.acd_transform_sbacc(a, False) -tc.assertEqual(str(b.acc()), '(2, Fin(0) & Inf(1))') -tc.assertTrue(a.equivalent_to(b)) +assert str(b.acc()) == '(2, Fin(0) & Inf(1))' +assert a.equivalent_to(b) diff --git a/tests/run.in b/tests/run.in index 7eaa7732c..d14bf52a9 100755 --- a/tests/run.in +++ b/tests/run.in @@ -104,21 +104,18 @@ export srcdir case $1 in *.ipynb) - PYTHONPATH=$pypath:$PYTHONPATH \ - DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ PYTHONIOENCODING=utf-8:surrogateescape \ exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";; *.py) - PYTHONPATH=$pypath:$PYTHONPATH \ - DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ exec $PREFIXCMD @PYTHON@ "$@";; *.test) exec sh -x "$@";; *.pl) exec $PERL "$@";; *python*|*jupyter*|*pypy*) - PYTHONPATH=$pypath:$PYTHONPATH \ - DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ exec $PREFIXCMD "$@";; *) echo "Unknown extension" >&2 diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 85ef359b0..8f157014d 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2021 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,27 +392,6 @@ 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