diff --git a/.gitignore b/.gitignore index 7392a79db..117213ced 100644 --- a/.gitignore +++ b/.gitignore @@ -81,3 +81,4 @@ GTAGS *.dsc *.gcov spot.spec +default.nix diff --git a/HACKING b/HACKING index 8841b033c..c6e127a70 100644 --- a/HACKING +++ b/HACKING @@ -290,8 +290,8 @@ would understand with: make check LOG_DRIVER=$PWD/tools/test-driver-teamcity -Coding conventions -================== +C++ Coding conventions +====================== Here some of the conventions we follow in Spot, so that the code looks homogeneous. Please follow these strictly. Since this is free @@ -682,3 +682,43 @@ Other style recommandations * Always code as if the person who ends up maintaining your code is a violent psychopath who knows where you live. + + +Coding conventions for Python Tests +=================================== + +Unless you have some specific reason to write test cases in C++ (for +instance do test some specific C++ constructions, or to use valgrind), +prefer writing test cases in Python. Writing test cases in C++ +requires some compilation, which slows down the test suite. Doing the +same test in Python is therefore faster, and it has the added benefit +of ensuring that the Python bindings works. + +We have two types of Python tests: Python scripts or jupyter +notebooks. Jupyter notebooks are usually used for a sequence of +examples and comments that can also serve as part of the +documentation. Such jupyter notebooks should be added to the list of +code examples in doc/org/tut.org. Testing a notebook is done by the +tests/python/ipnbdoctest.py scripts, which evaluate each cells, and +checks that the obtainted result is equivalent to the result saved in +the notebook. The process is a bit slow, so plain Python scripts +should be prefered for most tests. + +If you do need a notebook to tests Jupyter-specific code but this +notebook should not be shown in the documentation, use a filename +starting with '_'. + +Tests written as Python scripts should follow the same convention as +shell scripts: exit 0 for PASS, exit 77 for SKIP, and any other exit +code for FAIL. + +Do not use assert() in those scripts, as (1) asserts can be disabled, +and (2) they provide poor insights in case of failures. Instead do + + from unittest import TestCase + tc = TestCase() + +and then use tc.assertTrue(...), tc.assertEqual(..., ...), +tc.assertIn(..., ...), etc. In case of failures, those will print +useful messages in the trace of the tests. For instance multiline +strings that should have been equal will be presented with a diff. diff --git a/Makefile.am b/Makefile.am index a0dc9a316..668996fc0 100644 --- a/Makefile.am +++ b/Makefile.am @@ -68,7 +68,8 @@ EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog \ tools/help2man tools/man2html.pl \ tools/test-driver-teamcity $(UTF8) $(DEBIAN) \ m4/gnulib-cache.m4 .dir-locals.el \ - spot.spec spot.spec.in + spot.spec spot.spec.in \ + default.nix default.nix.in dist-hook: gen-ChangeLog @@ -114,3 +115,6 @@ deb: dist spot.spec: configure.ac spot.spec.in sed 's/[@]VERSION[@]/$(VERSION)/;s/[@]GITPATCH[@]/@@@$(GITPATCH)/;s/@@@\.//' spot.spec.in > $@.tmp && mv $@.tmp $@ + +default.nix: configure.ac default.nix.in + sed 's/[@]VERSION[@]/$(VERSION)/' default.nix.in > $@.tmp && mv $@.tmp $@ diff --git a/NEWS b/NEWS index 928a25da2..345ec7fdd 100644 --- a/NEWS +++ b/NEWS @@ -9,8 +9,17 @@ New in spot 2.10.4.dev (net yet released) - autfilt has a new --to-finite option, illustrated on https://spot.lrde.epita.fr/tut12.html + - ltlfilt has a new --sonf option to produce a formula's Suffix + Operator Normal Form, described in [cimatti.06.fmcad]. The + associated option --sonf-aps allows listing the newly introduced + atomic propositions. + Library: + - The new function suffix_operator_normal_form() implements + transformation of formulas to Suffix Operator Normal Form, + described in [cimatti.06.fmcad]. + - "original-classes" is a new named property similar to "original-states". It maps an each state to an unsigned integer such that if two classes are in the same class, they are expected @@ -65,6 +74,12 @@ New in spot 2.10.4.dev (net yet released) - work around a portability issue in Flex 2.6.4 preventing compilation on OpenBSD. + - Do not use the seq command in test cases, it is not available + everywhere. + + - Do not erase the previous contents of the PYTHONPATH environment + variable when running tests, prepend to it instead. + New in spot 2.10.4 (2022-02-01) Bug fixed: diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index cc9e0f02b..af9316192 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -38,6 +38,7 @@ #include #include #include +#include #include #include #include @@ -100,6 +101,8 @@ enum { OPT_SIZE_MAX, OPT_SIZE_MIN, OPT_SKIP_ERRORS, + OPT_SONF, + OPT_SONF_APS, OPT_STUTTER_INSENSITIVE, OPT_SUSPENDABLE, OPT_SYNTACTIC_GUARANTEE, @@ -127,6 +130,11 @@ static const argp_option options[] = { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 0 }, { "nnf", OPT_NNF, nullptr, 0, "rewrite formulas in negative normal form", 0 }, + { "sonf", OPT_SONF, "PREFIX", OPTION_ARG_OPTIONAL, + "rewrite formulas in suffix operator normal form", 0 }, + { "sonf-aps", OPT_SONF_APS, "FILENAME", OPTION_ARG_OPTIONAL, + "when used with --sonf, output the newly introduced atomic " + "propositions", 0 }, { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL, "relabel all atomic propositions, alphabetically unless " \ "specified otherwise", 0 }, @@ -316,6 +324,7 @@ static range opt_nth = { 0, std::numeric_limits::max() }; static int opt_max_count = -1; static long int match_count = 0; static const char* from_ltlf = nullptr; +static const char* sonf = nullptr; // We want all these variables to be destroyed when we exit main, to @@ -327,6 +336,7 @@ static struct opt_t spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::exclusive_ap excl_ap; std::unique_ptr output_define = nullptr; + std::unique_ptr output_sonf = nullptr; spot::formula implied_by = nullptr; spot::formula imply = nullptr; spot::formula equivalent_to = nullptr; @@ -460,6 +470,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_NNF: nnf = true; break; + case OPT_SONF: + sonf = arg ? arg : "sonf_"; + break; + case OPT_SONF_APS: + opt->output_sonf.reset(new output_file(arg ? arg : "-")); + break; case OPT_OBLIGATION: obligation = true; break; @@ -650,6 +666,25 @@ namespace if (nnf) f = simpl.negative_normal_form(f); + if (sonf != nullptr) + { + std::vector new_aps; + std::tie(f, new_aps) = suffix_operator_normal_form(f, sonf); + + if (opt->output_sonf + && output_format != count_output + && output_format != quiet_output) + { + for (size_t i = 0; i < new_aps.size(); ++i) + { + if (i > 0) + opt->output_sonf->ostream() << ' '; + opt->output_sonf->ostream() << new_aps[i]; + } + opt->output_sonf->ostream() << '\n'; + } + } + switch (relabeling) { case ApRelabeling: diff --git a/default.nix.in b/default.nix.in new file mode 100644 index 000000000..8101e4f74 --- /dev/null +++ b/default.nix.in @@ -0,0 +1,35 @@ +# -*- mode: nix; coding: utf-8 -*- +# Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +{ pkgs ? import {} }: +let + version = "@VERSION@"; +in +pkgs.stdenv.mkDerivation { + inherit version; + pname = "spot"; + + buildInputs = [ + pkgs.python3 + ]; + + src = ./.; + + enableParallelBuilding = true; +} diff --git a/doc/spot.bib b/doc/spot.bib index 9f18ad2a9..9d5d6b235 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -214,6 +214,18 @@ doi = {10.1109/DepCoS-RELCOMEX.2009.31} } +@InProceedings{ cimatti.06.fmcad, + author = {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone and + Tonetta, Stefano}, + title = {From {PSL} to {NBA}: a Modular Symbolic Encoding}, + booktitle = {Proceedings of the 6th conference on Formal Methods in Computer + Aided Design (FMCAD'06)}, + pages = {125--133}, + year = {2006}, + publisher = {IEEE Computer Society}, + doi = {10.1109/FMCAD.2006.19} +} + @Article{ cimatti.08.tcad, author = {Alessandro Cimatti and Marco Roveri and Stefano Tonetta}, journal = {IEEE Transactions on Computer Aided Design of Integrated diff --git a/flake.lock b/flake.lock new file mode 100644 index 000000000..6907c7263 --- /dev/null +++ b/flake.lock @@ -0,0 +1,43 @@ +{ + "nodes": { + "flake-utils": { + "locked": { + "lastModified": 1642700792, + "narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "846b2ae0fc4cc943637d3d1def4454213e203cba", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1643503720, + "narHash": "sha256-tJic20ufuRnG8V+fTCd3YU6xl1ImxNspoEkXHct0AG4=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "0f316e4d72daed659233817ffe52bf08e081b5de", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-21.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 000000000..10062e7a5 --- /dev/null +++ b/flake.nix @@ -0,0 +1,209 @@ +{ + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.11"; + flake-utils.url = "github:numtide/flake-utils"; + }; + outputs = { self, nixpkgs, flake-utils, ... }: + flake-utils.lib.eachSystem + [ + "x86_64-linux" + ] + + (system: + let + pkgs = import nixpkgs { inherit system; }; + lib = pkgs.lib; + + mkSpotApps = appNames: + pkgs.lib.genAttrs appNames + (name: flake-utils.lib.mkApp { + drv = self.packages.${system}.spot; + name = name; + }); + + spotPackage = + let + inherit (builtins) + filter + head + isString + match + readFile + split + ; + + # NOTE: Maintaining the version separately would be a pain, and we + # can't have a flake.nix.in with a @VERSION@ because it would make + # the flake unusable without running autoconf first, defeating some + # of its purpose. + # + # So let's get it the hard way instead :) + extractVersionRegex = ''^AC_INIT\(\[spot], \[([^]]+)], \[spot@lrde\.epita\.fr]\)$''; + getLines = (fileContent: + filter isString (split "\n" fileContent) + ); + findVersionLine = (lines: + lib.lists.findFirst + (l: lib.strings.hasPrefix "AC_INIT(" l) + null + lines + ); + getVersion = (file: + let + lines = getLines (readFile file); + versionLine = findVersionLine lines; + version = head (match extractVersionRegex versionLine); + in + version + ); + in + { + lib, + pkgs, + stdenv, + # FIXME: do we want this flag? + buildOrgDoc ? false, + # Whether to enable Spot's Python 3 bindings + enablePython ? false + }: + stdenv.mkDerivation { + pname = "spot"; + version = getVersion ./configure.ac; + + src = self; + + enableParallelBuilding = true; + + # NOTE: Nix enables a lot of hardening flags by default, some of + # these probably harm performance so I've disabled everything + # (haven't benchmarked with vs without these, though). + hardeningDisable = [ "all" ]; + + # NOTE: mktexpk fails without a HOME set + preBuild = '' + export HOME=$TMPDIR + patchShebangs tools + '' + (if buildOrgDoc then '' + ln -s ${pkgs.plantuml}/lib/plantuml.jar doc/org/plantuml.jar + '' else '' + touch doc/org-stamp + ''); + + configureFlags = [ + "--disable-devel" + "--enable-optimizations" + ] ++ lib.optional (!enablePython) [ + "--disable-python" + ]; + + nativeBuildInputs = with pkgs; [ + autoreconfHook + + autoconf + automake + bison + flex + libtool + perl + ] ++ lib.optional buildOrgDoc [ + graphviz + groff + plantuml + pdf2svg + R + ] ++ lib.optional enablePython [ + python3 + swig4 + ]; + + buildInputs = with pkgs; [ + # should provide the minimum amount of packages necessary for + # building tl.pdf + (texlive.combine { + inherit (texlive) + scheme-basic + latexmk + + booktabs + doi + doublestroke + koma-script + mathabx + mathpazo + metafont + microtype + nag + pgf + standalone + stmaryrd + tabulary + todonotes + wasy + wasysym + ; + }) + ]; + }; + in + { + defaultPackage = self.packages.${system}.spot; + + packages = { + # binaries + library only + spot = pkgs.callPackage spotPackage {}; + + # NOTE: clang build is broken on Nix when linking to stdlib++, using + # libcxx instead. See: + # https://github.com/NixOS/nixpkgs/issues/91285 + spotClang = pkgs.callPackage spotPackage { + stdenv = pkgs.llvmPackages.libcxxStdenv; + }; + + spotWithOrgDoc = pkgs.callPackage spotPackage { + buildOrgDoc = true; + }; + + spotWithPython = pkgs.python3Packages.toPythonModule ( + pkgs.callPackage spotPackage { + enablePython = true; + } + ); + + spotFull = pkgs.python3Packages.toPythonModule ( + pkgs.callPackage spotPackage { + buildOrgDoc = true; enablePython = true; + } + ); + }; + + apps = mkSpotApps [ + "autcross" + "autfilt" + "dstar2tgba" + "genaut" + "genltl" + "ltl2tgba" + "ltl2tgta" + "ltlcross" + "ltldo" + "ltlfilt" + "ltlgrind" + "ltlsynt" + "randaut" + "randltl" + ]; + + devShell = pkgs.mkShell { + name = "spot-dev"; + inputsFrom = [ self.packages.${system}.spotFull ]; + buildInputs = [ + pkgs.gdb + + (pkgs.python3.withPackages (p: [ + p.jupyter + p.ipython # otherwise ipython module isn't found when running ipynb tests + ])) + ]; + }; + }); +} diff --git a/python/spot/impl.i b/python/spot/impl.i index 90a38a55a..b5293634f 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -90,10 +90,12 @@ #include #include +#include #include #include #include #include +#include #include #include #include @@ -517,6 +519,7 @@ namespace std { %template(vectorbdd) vector; %template(aliasvector) vector>; %template(vectorstring) vector; + %template(pair_formula_vectorstring) pair>; %template(atomic_prop_set) set; %template(relabeling_map) map; } @@ -531,6 +534,8 @@ 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. */ @@ -575,8 +580,10 @@ namespace std { %include %include +%include %include %include +%include %include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index b7362ae99..7440cbae3 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -28,6 +28,7 @@ tl_HEADERS = \ contain.hh \ declenv.hh \ defaultenv.hh \ + derive.hh \ dot.hh \ environment.hh \ exclusive.hh \ @@ -44,6 +45,7 @@ tl_HEADERS = \ remove_x.hh \ simplify.hh \ snf.hh \ + sonf.hh \ unabbrev.hh noinst_LTLIBRARIES = libtl.la @@ -52,6 +54,7 @@ libtl_la_SOURCES = \ contain.cc \ declenv.cc \ defaultenv.cc \ + derive.cc \ dot.cc \ exclusive.cc \ formula.cc \ @@ -68,4 +71,5 @@ libtl_la_SOURCES = \ remove_x.cc \ simplify.cc \ snf.cc \ + sonf.cc \ unabbrev.cc diff --git a/spot/tl/derive.cc b/spot/tl/derive.cc new file mode 100644 index 000000000..2b1873ed2 --- /dev/null +++ b/spot/tl/derive.cc @@ -0,0 +1,558 @@ +// -*- 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 new file mode 100644 index 000000000..1947951ed --- /dev/null +++ b/spot/tl/derive.hh @@ -0,0 +1,52 @@ +// -*- 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/tl/sonf.cc b/spot/tl/sonf.cc new file mode 100644 index 000000000..29a319039 --- /dev/null +++ b/spot/tl/sonf.cc @@ -0,0 +1,185 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Developpement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "config.h" +#include +#include + +#include +#include +#include +#include + +namespace spot +{ + namespace + { + /// Uses `extractor` to extract some parts of the formula and replace them + /// with atomic propositions. + /// + /// Returns (f & g1 & g2 & .. & gn) with g1..gn the extracted subformulas. + /// + /// `extractor` should be a lambda taking the following parameters as input: + /// + /// - `formula` the formula to process + /// - `std::vector&` the vector that stores extracted subformulas + /// - `auto&&` itself, in case it needs to call itself recursively + /// (formula::map for example) + /// - `bool` a boolean indicating whether the lambda is currently being + /// called at the formula's "root" + /// - `bool` a boolean indicating whether the lambda is currently being + /// called inside a toplevel `and` construct. + /// + /// Note that the last 2 boolean arguments can be used as you see fit in + /// your recursive calls, the first one being set to true in the original + /// call, and the second one to false. + /// + /// `extractor` should return the new rewritten formula. + /// + /// auto sample_extractor = [](formula f, + /// std::vector& extracted, + /// auto&& extractor, + /// bool top_level, + /// bool in_top_level_and) -> formula + template + static formula + extract(formula f, Ext extractor) + { + std::vector extracted; + formula new_f = extractor(f, extracted, extractor, true, false); + extracted.push_back(new_f); + return formula::And(extracted); + } + } + + std::pair> + suffix_operator_normal_form(formula f, const std::string prefix) + { + // SONF can only be applied to formulas in negative normal form + f = negative_normal_form(f); + + std::unordered_set used_aps; + std::vector added_aps; + size_t count = 0; + + // identify all used ap names to avoid them when generating new ones + auto ap_indexer = [&used_aps](formula f) noexcept { + if (f.is(op::ap)) + { + used_aps.insert(f.ap_name()); + return true; + } + + return false; + }; + + f.traverse(ap_indexer); + + auto new_ap_name = + [&used_aps, &added_aps, &prefix, &count]() noexcept -> std::string + { + std::string new_name = prefix + std::to_string(count++); + while (used_aps.find(new_name) != used_aps.end()) + new_name = prefix + std::to_string(count++); + used_aps.insert(new_name); + added_aps.push_back(new_name); + return new_name; + }; + + // extracts the SERE part and replaces it with an atomic proposition, + // storing the extracted formula in `extracted` and returning the rewritten + // original formula + auto sonf_extract = [&](formula f, + std::vector& extracted, + auto&& extractor, + bool top_level, + bool in_top_level_and) noexcept -> formula + { + const auto kind = f.kind(); + + switch (kind) + { + case op::G: + { + // skip if shape is G(!ap | (regex []-> formula)) and at top level + if ((top_level || in_top_level_and) + && f[0].is(op::Or) // G(_ | _) + && f[0][0].is(op::Not) // G(!_ | _) + && f[0][0][0].is(op::ap) // G(!ap | _) + && f[0][1].is(op::EConcat, op::UConcat)) // G(!ap | (_ []-> _)) + return f; + else + return f.map(extractor, extracted, extractor, false, false); + } + case op::EConcat: + case op::UConcat: + { + // recurse into rhs first (_ []-> rhs) + formula rhs = + f[1].map(extractor, extracted, extractor, false, false); + f = formula::binop(kind, f[0], rhs); + + formula ap = formula::ap(new_ap_name()); + extracted.push_back(formula::G(formula::Or({formula::Not(ap), f}))); + return ap; + } + default: + // tracking if we're in a op::And at the formula root + in_top_level_and = top_level && f.is(op::And); + return f.map(extractor, extracted, extractor, + false, in_top_level_and); + } + }; + + f = extract(f, sonf_extract); + + auto ltl_extract = [&](formula f, + std::vector& extracted, + auto&& extractor, + [[maybe_unused]] + bool top_level, + [[maybe_unused]] + bool in_top_level_and) noexcept -> formula + { + switch (f.kind()) + { + case op::EConcat: + case op::UConcat: + { + formula rhs = f[1]; + + if (rhs.is(op::ap)) + return f; + + formula ap = formula::ap(new_ap_name()); + extracted.push_back( + formula::G(formula::Or({formula::Not(ap), rhs}))); + + return formula::binop(f.kind(), f[0], ap); + } + default: + return f.map(extractor, extracted, extractor, false, false); + } + }; + + f = extract(f, ltl_extract); + + return {f, added_aps}; + } +} diff --git a/spot/tl/sonf.hh b/spot/tl/sonf.hh new file mode 100644 index 000000000..37ef5d05d --- /dev/null +++ b/spot/tl/sonf.hh @@ -0,0 +1,44 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include +#include +#include + +#include + +namespace spot +{ + /// \ingroup tl_rewriting + /// \brief Helper to rewrite a PSL formula in Suffix Operator Normal Form. + /// + /// SONF is described in section 4 of \cite cimatti.06.fmcad + /// + /// The formula output by this function is guaranteed to be in Negative Normal + /// Form. + /// + /// \param f the PSL formula to rewrite + /// \param prefix the prefix to use to name newly introduced aps + /// \return a pair with the rewritten formula, and a vector containing the + /// names of newly introduced aps + SPOT_API std::pair> + suffix_operator_normal_form(formula f, const std::string prefix); +} diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index cb1e208ec..819a90962 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013-2021 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2013-2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -761,7 +761,7 @@ namespace spot void register_aps_from_dict() { if (!aps_.empty()) - throw std::runtime_error("register_ap_from_dict() may not be" + throw std::runtime_error("register_aps_from_dict() may not be" " called on an automaton that has already" " registered some AP"); auto& m = get_dict()->bdd_map; diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 051514550..8da719776 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -164,11 +164,15 @@ 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) + while (in < tend + && trans[in].cond == bddfalse + && (!is_state_acc || trans[in].src != trans[in].dst)) ++in; if (in < tend) { @@ -177,7 +181,9 @@ namespace spot trans[out] = trans[in]; for (++in; in < tend; ++in) { - if (trans[in].cond == bddfalse) // Unusable edge + if (trans[in].cond == bddfalse + && (!is_state_acc + || trans[in].src != trans[in].dst)) // 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 3566abc97..783a35285 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -24,6 +24,7 @@ #include #include #include +#include #include #include #include @@ -753,55 +754,7 @@ namespace spot SPOT_UNREACHABLE(); case op::AndNLM: { - 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))); + return recurse_and_concat(rewrite_and_nlm(f)); } case op::AndRat: { @@ -2271,4 +2224,59 @@ 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 8c1827490..aa9bc1d1d 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -88,4 +88,7 @@ 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 942a1b4b5..b693015fd 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -244,4 +244,51 @@ 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 09d75ffac..4b496e65a 100644 --- a/spot/twaalgos/remprop.hh +++ b/spot/twaalgos/remprop.hh @@ -54,5 +54,8 @@ 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/Makefile.am b/tests/Makefile.am index 1b5d63fee..afcd0c8d2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -198,7 +198,8 @@ TESTS_tl = \ core/stutter-ltl.test \ core/hierarchy.test \ core/mempool.test \ - core/format.test + core/format.test \ + core/sonf.test TESTS_graph = \ core/graph.test \ @@ -445,6 +446,7 @@ TESTS_python = \ python/setxor.py \ python/simplacc.py \ python/simstate.py \ + python/sonf.py \ python/split.py \ python/streett_totgba.py \ python/streett_totgba2.py \ diff --git a/tests/core/bricks.test b/tests/core/bricks.test index b98c7e856..37ff57cb0 100644 --- a/tests/core/bricks.test +++ b/tests/core/bricks.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2020 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -21,12 +21,13 @@ . ./defs set -e -seq 0 1999 > expected +# The seq command is not always available, but we assume awk is. +$AWK 'BEGIN{for(x=0;x<2000;++x) print x;}' >expected ../bricks > stdout -cat stdout | head -n 2000 | awk '{print $2}' | sed 's/{//g' | \ - awk -F',' '{print $1}' | sort -n > map +cat stdout | head -n 2000 | $AWK '{print $2}' | sed 's/{//g' | \ + $AWK -F',' '{print $1}' | sort -n > map diff expected map diff --git a/tests/core/defs.in b/tests/core/defs.in index 7df6fdf77..d06a3b67d 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 Laboratoire de Recherche +# Copyright (C) 2009, 2010, 2012, 2013, 2015, 2022 Laboratoire de Recherche # et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -57,6 +57,7 @@ case $srcdir in *) srcdir=../$srcdir esac +AWK='@AWK@' DOT='@DOT@' LBTT="@LBTT@" LBTT_TRANSLATE="@LBTT_TRANSLATE@" diff --git a/tests/core/prodchain.test b/tests/core/prodchain.test index b5037782f..0a7f1a1d9 100755 --- a/tests/core/prodchain.test +++ b/tests/core/prodchain.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,7 +23,8 @@ set -e set x shift -for i in `seq 1 42`; do +for i in 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 \ + 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42; do ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa done for i in *.hoa; do diff --git a/tests/core/sonf.test b/tests/core/sonf.test new file mode 100644 index 000000000..0febfc342 --- /dev/null +++ b/tests/core/sonf.test @@ -0,0 +1,85 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2021 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +cat >input < Fa) & G(b -> ({x[*]}[]-> c)) +{x[*]}[]-> F({y[*]}<>-> GFz) +<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17))) +{{true} || {[*0]}}[]-> (false) +{{p14} & {{p0}[*]}}[]-> (p11) +{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18))))) +X({{true} || {[*0]}}[]-> ((p17) U ((p8) && (p17)))) +({{{p4} || {p5} || {{p16} <-> {{p15} -> {p11}}}}[*]}[]-> (false)) -> (p8) +{[*1..6]}[]-> ((p9) V ((p9) || (!((p4) && (p19))))) +X({{{[*0]} || {{{p10};{p14}}[:*2..3]}}[:*]}<>-> (p8)) +{{true} && {{p8}[*]}}<>-> (!(p10)) +<>(!(({{p7}[*1..2]}<>-> (p11)) V ((!(p9)) && ([]((p11) || (X(p10))))))) +<>({{!{{p5} || {{!{p2}} <-> {p7}}}} & {[*]}}<>-> (p17)) +{{p0} || {{{[*0..2]}[:*2]}[*]}}<>-> ((p1) && (p6)) +EOF + +cat >expected < c)) +s1&G(!s2|GFz)&G(!s0|({y[*]}<>-> s2))&G(!s3|Fs0)&G(!s1|({x[*]}[]-> s3)) +F(s0 R (1 U p17))&G(p9|!p17|!s1)&G(!s0|({p12[*0..3]}[]-> s1)) +s0&G!s1&G(!s0|({1|[*0]}[]-> s1)) +s0&G(!s0|({p14&p0[*]}[]-> p11)) +s0&G(!s1|(p3 R (p3|(X(0)&(p2 R p18)))))&G(!s0|({{!p3|p6}[*]}[]-> s1)) +Xs0&G(!s1|(p17 U (p8&p17)))&G(!s0|({1|[*0]}[]-> s1)) +(p8|s0)&G(!s0|({{p4|p5|{p16 && {p11|!p15}}|{!p11 && p15 && !p16}}[*]}<>-> s1)) +s0&G(!s1|(p9 R (!p4|p9|!p19)))&G(!s0|({[*1..6]}[]-> s1)) +G(!s0|({{[*0]|{p10;p14}[:*2..3]}[:*]}<>-> p8))&Xs0 +s0&G(!p10|!s1)&G(!s0|({1 && p8[*]}<>-> s1)) +F(s0 U (p9|F(!p11&X!p10)))&G(!p11|!s1)&G(!s0|({p7[*1..2]}[]-> s1)) +G(!s0|({{!p5 && {{!p2 && !p7}|{p2 && p7}}}&[*]}<>-> p17))&Fs0 +s0&G(!s1|(p1&p6))&G(!s0|({p0|[*0..2][:*2][*]}<>-> s1)) +EOF + +cat >expected-aps < stdout +diff expected stdout +diff expected-aps stdout-aps + +# check idempotence +ltlfilt -F expected --sonf=s --sonf-aps=stdout-aps \ + | sed 's/ \([|&]\) /\1/g' > stdout +diff expected stdout +# should be 14 empty lines, no new aps introduced this time +test "$(wc -l -m stdout-aps | awk '{print $1 " " $2}')" = "14 14" diff --git a/tests/python/298.py b/tests/python/298.py index d4865c440..89ddbdb0c 100644 --- a/tests/python/298.py +++ b/tests/python/298.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -20,21 +20,23 @@ # Test for parts of Issue #298. import spot +from unittest import TestCase +tc = TestCase() a1 = spot.automaton("""genltl --dac=51 | ltl2tgba --med |""") a1 = spot.degeneralize_tba(a1) r1 = spot.tgba_determinize(a1, True, False, False) -assert r1.num_sets() == 3 -assert a1.prop_complete().is_false(); +tc.assertEqual(r1.num_sets(), 3) +tc.assertTrue(a1.prop_complete().is_false()) # This used to fail in 2.9.5 and earlier. -assert r1.prop_complete().is_maybe(); -assert spot.is_complete(r1) +tc.assertTrue(r1.prop_complete().is_maybe()) +tc.assertTrue(spot.is_complete(r1)) a2 = spot.automaton("""genltl --dac=51 | ltl2tgba --high |""") a2 = spot.degeneralize_tba(a2) r2 = spot.tgba_determinize(a2, True, False, False) # This used to fail in 2.9.5 and earlier. -assert r2.num_sets() == 3 -assert a2.prop_complete().is_false(); -assert r2.prop_complete().is_maybe(); -assert spot.is_complete(r2) +tc.assertEqual(r2.num_sets(), 3) +tc.assertTrue(a2.prop_complete().is_false()) +tc.assertTrue(r2.prop_complete().is_maybe()) +tc.assertTrue(spot.is_complete(r2)) diff --git a/tests/python/341.py b/tests/python/341.py index 4c5937149..e828ab07c 100644 --- a/tests/python/341.py +++ b/tests/python/341.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,7 +19,8 @@ import spot from subprocess import _active - +from unittest import TestCase +tc = TestCase() def two_intersecting_automata(): """return two random automata with a non-empty intersection""" @@ -34,4 +35,4 @@ for i in range(5): n = len(_active) print(n, "active processes") -assert(n == 0) +tc.assertEqual(n, 0) diff --git a/tests/python/471.py b/tests/python/471.py index 6fee3a2d3..0fe180554 100644 --- a/tests/python/471.py +++ b/tests/python/471.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -20,9 +20,12 @@ # Test for Issue #471. import spot +from unittest import TestCase +tc = TestCase() + a = spot.translate('Fa') a = spot.to_generalized_rabin(a, False) r1 = a.intersecting_run(a) r2 = a.accepting_run() -assert str(r1) == str(r2) -assert a.prop_weak().is_true() +tc.assertEqual(str(r1), str(r2)) +tc.assertTrue(a.prop_weak().is_true()) diff --git a/tests/python/accparse2.py b/tests/python/accparse2.py index 4e6eb1cb3..d9c7274a0 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 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2018, 2022 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,99 +18,101 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() a = spot.acc_cond(5) a.set_acceptance(spot.acc_code('parity min odd 5')) -assert(a.is_parity() == [True, False, True]) +tc.assertEqual(a.is_parity(), [True, False, True]) a.set_acceptance('parity max even 5') -assert(a.is_parity() == [True, True, False]) +tc.assertEqual(a.is_parity(), [True, True, False]) a.set_acceptance('generalized-Buchi 5') -assert(a.is_parity()[0] == False) -assert(a.is_parity(True)[0] == False) +tc.assertEqual(a.is_parity()[0], False) +tc.assertEqual(a.is_parity(True)[0], False) a.set_acceptance('Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))') -assert(a.is_parity()[0] == False) -assert(a.is_parity(True) == [True, True, False]) +tc.assertEqual(a.is_parity()[0], False) +tc.assertEqual(a.is_parity(True), [True, True, False]) -assert a.maybe_accepting([1, 2, 3], [0, 4]).is_true() -assert a.maybe_accepting([0], []).is_true() -assert a.maybe_accepting([0], [3]).is_false() -assert a.maybe_accepting([0, 3], []).is_maybe() -assert a.maybe_accepting([2, 3], [3]).is_false() -assert a.maybe_accepting([2, 3], []).is_maybe() -assert a.maybe_accepting([2], []).is_true() -assert a.maybe_accepting([0, 1], []).is_maybe() -assert a.maybe_accepting([0, 1], [1]).is_false() +tc.assertTrue(a.maybe_accepting([1, 2, 3], [0, 4]).is_true()) +tc.assertTrue(a.maybe_accepting([0], []).is_true()) +tc.assertTrue(a.maybe_accepting([0], [3]).is_false()) +tc.assertTrue(a.maybe_accepting([0, 3], []).is_maybe()) +tc.assertTrue(a.maybe_accepting([2, 3], [3]).is_false()) +tc.assertTrue(a.maybe_accepting([2, 3], []).is_maybe()) +tc.assertTrue(a.maybe_accepting([2], []).is_true()) +tc.assertTrue(a.maybe_accepting([0, 1], []).is_maybe()) +tc.assertTrue(a.maybe_accepting([0, 1], [1]).is_false()) a.set_acceptance('Fin(0)|Fin(1)') -assert a.maybe_accepting([0, 1], [1]).is_maybe() -assert a.maybe_accepting([0, 1], [0, 1]).is_false() -assert a.maybe_accepting([0], []).is_true() -assert a.maybe_accepting([], [0]).is_true() +tc.assertTrue(a.maybe_accepting([0, 1], [1]).is_maybe()) +tc.assertTrue(a.maybe_accepting([0, 1], [0, 1]).is_false()) +tc.assertTrue(a.maybe_accepting([0], []).is_true()) +tc.assertTrue(a.maybe_accepting([], [0]).is_true()) a = spot.acc_cond(0) a.set_acceptance('all') -assert(a.is_rabin() == -1) -assert(a.is_streett() == 0) -assert(a.is_parity() == [True, True, True]) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), 0) +tc.assertEqual(a.is_parity(), [True, True, True]) a.set_acceptance('none') -assert(a.is_rabin() == 0) -assert(a.is_streett() == -1) -assert(a.is_parity() == [True, True, False]) +tc.assertEqual(a.is_rabin(), 0) +tc.assertEqual(a.is_streett(), -1) +tc.assertEqual(a.is_parity(), [True, True, False]) a = spot.acc_cond('(Fin(0)&Inf(1))') -assert(a.is_rabin() == 1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), 1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('Inf(1)&Fin(0)') -assert(a.is_rabin() == 1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), 1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('(Fin(0)|Inf(1))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == 1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), 1) a.set_acceptance('Inf(1)|Fin(0)') -assert(a.is_rabin() == -1) -assert(a.is_streett() == 1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), 1) a = spot.acc_cond('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))') -assert(a.is_rabin() == 2) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), 2) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))')) -assert(a.is_rabin() == 2) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), 2) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance(spot.acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))')) -assert(a.is_rabin() == -1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance(spot.acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))')) -assert(a.is_rabin() == -1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance(spot.acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))')) -assert(a.is_rabin() == -1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))') -assert(a.is_rabin() == 2) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), 2) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == 2) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), 2) a.set_acceptance('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == 2) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), 2) a.set_acceptance('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == -1) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), -1) a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))') -assert(a.is_rabin() == -1) -assert(a.is_streett() == 2) +tc.assertEqual(a.is_rabin(), -1) +tc.assertEqual(a.is_streett(), 2) a = spot.acc_code('Inf(0)&Inf(1)&Inf(3) | Fin(0)&(Fin(1)|Fin(3))') u = a.symmetries() -assert u[0] == 0 -assert u[1] == 1 -assert u[2] == 2 -assert u[3] == 1 +tc.assertEqual(u[0], 0) +tc.assertEqual(u[1], 1) +tc.assertEqual(u[2], 2) +tc.assertEqual(u[3], 1) diff --git a/tests/python/aiger.py b/tests/python/aiger.py index 5148fef5f..f490465b0 100644 --- a/tests/python/aiger.py +++ b/tests/python/aiger.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021 Laboratoire de Recherche et +# Copyright (C) 2021, 2022 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot, buddy +from unittest import TestCase +tc = TestCase() strats = (("""HOA: v1 States: 4 @@ -3346,7 +3348,7 @@ for strat_string, (ins_str, outs_str) in strats: print(f"Mode is {m+ss+ddx+uud}") print(f"""Strat is \n{strat_s.to_str("hoa")}""") print(f"""Aig as aut is \n{strat2_s.to_str("hoa")}""") - assert 0 + raise AssertionError("not a specialization") # Check stepwise simulation @@ -3386,7 +3388,7 @@ for (i, e_latch) in zip(ins, exp_latches): # Variable names -assert(spot.aiger_circuit("""aag 2 2 0 2 0 +tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0 2 4 2 @@ -3394,9 +3396,9 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0 i0 a i1 b c c -""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1') +""").to_str(), 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 a\ni1 b c\no0 o0\no1 o1') -assert(spot.aiger_circuit("""aag 2 2 0 2 0 +tc.assertEqual(spot.aiger_circuit("""aag 2 2 0 2 0 2 4 2 @@ -3404,7 +3406,7 @@ assert(spot.aiger_circuit("""aag 2 2 0 2 0 o0 x o1 y c -""").to_str() == 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y') +""").to_str(), 'aag 2 2 0 2 0\n2\n4\n2\n1\ni0 i0\ni1 i1\no0 x\no1 y') def report_missing_exception(): @@ -3415,7 +3417,7 @@ try: 0 """) except SyntaxError as e: - assert str(e) == "\n:1: invalid header line" + tc.assertEqual(str(e), "\n:1: invalid header line") else: report_missing_exception() @@ -3423,14 +3425,15 @@ try: spot.aiger_circuit("""aag 2 2 3 2 0 """) except SyntaxError as e: - assert str(e) == "\n:1: more variables than indicated by max var" + tc.assertEqual(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: - assert str(e) == "\n:2: expecting input number 2" + tc.assertEqual(str(e), "\n:2: expecting input number 2") else: report_missing_exception() @@ -3439,7 +3442,7 @@ try: 3 """) except SyntaxError as e: - assert str(e) == "\n:2: expecting input number 2" + tc.assertEqual(str(e), "\n:2: expecting input number 2") else: report_missing_exception() @@ -3448,7 +3451,7 @@ try: 3 4 5 """) except SyntaxError as e: - assert str(e) == "\n:2: invalid format for an input" + tc.assertEqual(str(e), "\n:2: invalid format for an input") else: report_missing_exception() @@ -3457,7 +3460,7 @@ try: 2 """) except SyntaxError as e: - assert str(e) == "\n:3: expecting input number 4" + tc.assertEqual(str(e), "\n:3: expecting input number 4") else: report_missing_exception() @@ -3468,7 +3471,7 @@ try: 1 """) except SyntaxError as e: - assert str(e) == "\n:4: invalid format for a latch" + tc.assertEqual(str(e), "\n:4: invalid format for a latch") else: report_missing_exception() @@ -3479,7 +3482,7 @@ try: 1 1 """) except SyntaxError as e: - assert str(e) == "\n:4: expecting latch number 6" + tc.assertEqual(str(e), "\n:4: expecting latch number 6") else: report_missing_exception() @@ -3490,7 +3493,7 @@ try: 6 1 """) except SyntaxError as e: - assert str(e) == "\n:5: expecting latch number 8" + tc.assertEqual(str(e), "\n:5: expecting latch number 8") else: report_missing_exception() @@ -3502,7 +3505,7 @@ try: 8 7 """) except SyntaxError as e: - assert str(e) == "\n:6: expecting an output" + tc.assertEqual(str(e), "\n:6: expecting an output") else: report_missing_exception() @@ -3515,7 +3518,7 @@ try: 9 9 9 """) except SyntaxError as e: - assert str(e) == "\n:6: invalid format for an output" + tc.assertEqual(str(e), "\n:6: invalid format for an output") else: report_missing_exception() @@ -3528,7 +3531,7 @@ try: 9 9 9 """) except SyntaxError as e: - assert str(e) == "\n:6: invalid format for an output" + tc.assertEqual(str(e), "\n:6: invalid format for an output") else: report_missing_exception() @@ -3541,7 +3544,7 @@ try: 9 """) except SyntaxError as e: - assert str(e) == "\n:7: expecting AND gate number 10" + tc.assertEqual(str(e), "\n:7: expecting AND gate number 10") else: report_missing_exception() @@ -3555,7 +3558,7 @@ try: 10 3 8 9 """) except SyntaxError as e: - assert str(e) == "\n:7: invalid format for an AND gate" + tc.assertEqual(str(e), "\n:7: invalid format for an AND gate") else: report_missing_exception() @@ -3569,7 +3572,7 @@ try: 10 3 """) except SyntaxError as e: - assert str(e) == "\n:7: invalid format for an AND gate" + tc.assertEqual(str(e), "\n:7: invalid format for an AND gate") else: report_missing_exception() @@ -3583,7 +3586,7 @@ try: 10 3 8 """) except SyntaxError as e: - assert str(e) == "\n:8: expecting AND gate number 12" + tc.assertEqual(str(e), "\n:8: expecting AND gate number 12") else: report_missing_exception() @@ -3599,7 +3602,7 @@ try: i0 """) except SyntaxError as e: - assert str(e) == "\n:9: could not parse as input name" + tc.assertEqual(str(e), "\n:9: could not parse as input name") else: report_missing_exception() @@ -3616,7 +3619,7 @@ i0 foo i3 bar """) except SyntaxError as e: - assert str(e) == "\n:10: value 3 exceeds input count" + tc.assertEqual(str(e), "\n:10: value 3 exceeds input count") else: report_missing_exception() @@ -3633,7 +3636,7 @@ i1 bar i0 foo """) except SyntaxError as e: - assert str(e) == "\n:9: expecting name for input 0" + tc.assertEqual(str(e), "\n:9: expecting name for input 0") else: report_missing_exception() @@ -3650,8 +3653,8 @@ i0 name with spaces i1 name with spaces """) except SyntaxError as e: - assert str(e) == \ - "\n:10: name 'name with spaces' already used" + tc.assertEqual(str(e), \ + "\n:10: name 'name with spaces' already used") else: report_missing_exception() @@ -3669,7 +3672,7 @@ i1 bar o0 """) except SyntaxError as e: - assert str(e) == "\n:11: could not parse as output name" + tc.assertEqual(str(e), "\n:11: could not parse as output name") else: report_missing_exception() @@ -3689,7 +3692,7 @@ o1 hmm o0 foo bar baz """) except SyntaxError as e: - assert str(e) == "\n:12: expecting name for output 0" + tc.assertEqual(str(e), "\n:12: expecting name for output 0") else: report_missing_exception() @@ -3709,7 +3712,7 @@ o0 hmm o2 foo bar baz """) except SyntaxError as e: - assert str(e) == "\n:13: value 2 exceeds output count" + tc.assertEqual(str(e), "\n:13: value 2 exceeds output count") else: report_missing_exception() @@ -3729,7 +3732,7 @@ o0 foo o1 foo """) except SyntaxError as e: - assert str(e) == "\n:13: name 'foo' already used" + tc.assertEqual(str(e), "\n:13: name 'foo' already used") else: report_missing_exception() @@ -3749,7 +3752,7 @@ o0 foo o1 bar """) except SyntaxError as e: - assert str(e) == "\n:13: name 'bar' already used" + tc.assertEqual(str(e), "\n:13: name 'bar' already used") else: report_missing_exception() @@ -3770,7 +3773,7 @@ o1 baz this is a bug """) except SyntaxError as e: - assert str(e) == "\n:14: unsupported line type" + tc.assertEqual(str(e), "\n:14: unsupported line type") else: report_missing_exception() @@ -3791,8 +3794,8 @@ c this is not a bug """) except SyntaxError as e: - assert str(e) == \ - "\n:10: either all or none of the inputs should be named" + tc.assertEqual(str(e), \ + "\n:10: either all or none of the inputs should be named") else: report_missing_exception() @@ -3815,8 +3818,8 @@ c this is not a bug """) except SyntaxError as e: - assert str(e) == \ - "\n:11-12: either all or none of the inputs should be named" + tc.assertEqual(str(e), \ + "\n:11-12: either all or none of the inputs should be named") else: report_missing_exception() @@ -3841,8 +3844,8 @@ c this is not a bug """) except SyntaxError as e: - assert str(e) == \ - "\n:14-16: either all or none of the outputs should be named" + tc.assertEqual(str(e), \ + "\n:14-16: either all or none of the outputs should be named") else: report_missing_exception() @@ -3866,4 +3869,4 @@ o2 bar c this is not a bug """).to_str() -assert x == spot.aiger_circuit(x).to_str() +tc.assertEqual(x, spot.aiger_circuit(x).to_str()) diff --git a/tests/python/aliases.py b/tests/python/aliases.py index 6f861a880..40dd4d0ec 100644 --- a/tests/python/aliases.py +++ b/tests/python/aliases.py @@ -20,6 +20,8 @@ # Test for parts of Issue #497. import spot +from unittest import TestCase +tc = TestCase() aut = spot.automaton(""" HOA: v1 @@ -63,11 +65,11 @@ State: 0 --END--""") s = aut.to_str('hoa') aut2 = spot.automaton(s) -assert aut.equivalent_to(aut2) +tc.assertTrue(aut.equivalent_to(aut2)) s2 = aut.to_str('hoa') -assert s == s2 +tc.assertEqual(s, s2) -assert s == """HOA: v1 +tc.assertEqual(s, """HOA: v1 States: 1 Start: 0 AP: 3 "x" "y" "z" @@ -105,7 +107,7 @@ State: 0 [@a&2 | @p1&@p0&2] 0 [@a&2] 0 [@p0&2 | @p1&2] 0 ---END--""" +--END--""") # Check what happens to aliases when an AP has been removed, but # the aliases have been preserved... @@ -115,7 +117,7 @@ aut3 = rem.strip(aut) spot.set_aliases(aut3, spot.get_aliases(aut)) s2 = aut3.to_str('hoa') # Aliases based on "x" should have disappeared. -assert(s2 == """HOA: v1 +tc.assertEqual(s2, """HOA: v1 States: 1 Start: 0 AP: 2 "y" "z" diff --git a/tests/python/alternating.py b/tests/python/alternating.py index 7b3a5d713..5b38ca378 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2016-2017, 2021-2022 Laboratoire de Recherche +# et Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -20,6 +20,8 @@ import spot import buddy +from unittest import TestCase +tc = TestCase() aut = spot.make_twa_graph(spot._bdd_dict) @@ -38,9 +40,8 @@ aut.new_edge(2, 2, p1 | p2) tr = [(s, [[x for x in aut.univ_dests(i)] for i in aut.out(s)]) for s in range(3)] -print(tr) -assert [(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])] == tr -assert not aut.is_existential() +tc.assertEqual([(0, [[1, 2], [0, 1]]), (1, [[0, 2, 1]]), (2, [[2]])], tr) +tc.assertFalse(aut.is_existential()) received = False try: @@ -49,11 +50,10 @@ try: pass except RuntimeError: received = True -assert received +tc.assertTrue(received) h = aut.to_str('hoa') -print(h) -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 3 Start: 0 AP: 2 "p1" "p2" @@ -68,22 +68,20 @@ State: 1 [0&1] 0&2&1 State: 2 [0 | 1] 2 ---END--""" +--END--""") aut2 = spot.automaton(h) h2 = aut2.to_str('hoa') -print(h2) -assert h != h2 +tc.assertNotEqual(h, h2) # This will sort destination groups aut.merge_univ_dests() h = aut.to_str('hoa') -assert h == h2 +tc.assertEqual(h, h2) aut2.set_univ_init_state([0, 1]) h3 = aut2.to_str('hoa') -print(h3) -assert h3 == """HOA: v1 +tc.assertEqual(h3, """HOA: v1 States: 3 Start: 0&1 AP: 2 "p1" "p2" @@ -98,23 +96,22 @@ State: 1 [0&1] 0&1&2 State: 2 [0 | 1] 2 ---END--""" +--END--""") st = spot.states_and(aut, [0, 2]) st2 = spot.states_and(aut, [1, st]) st3 = spot.states_and(aut, [0, 1, 2]) -assert (st, st2, st3) == (3, 4, 5) +tc.assertEqual((st, st2, st3), (3, 4, 5)) received = False try: st4 = spot.states_and(aut, []) except RuntimeError: received = True -assert received +tc.assertTrue(received) h = aut.to_str('hoa') -print(h) -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 6 Start: 0 AP: 2 "p1" "p2" @@ -136,11 +133,10 @@ State: 4 [0&1] 0&1&2 State: 5 [0&1] 0&1&2 ---END--""" +--END--""") h = spot.split_edges(aut).to_str('hoa') -print(h) -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 6 Start: 0 AP: 2 "p1" "p2" @@ -168,7 +164,7 @@ State: 4 [0&1] 0&1&2 State: 5 [0&1] 0&1&2 ---END--""" +--END--""") # remove_univ_otf @@ -206,11 +202,11 @@ State: 2 --END--""" desalt = spot.remove_univ_otf(aut) -assert(desalt.to_str('hoa') == out) +tc.assertEqual(desalt.to_str('hoa'), out) -assert aut.num_states() == 3 -assert aut.num_edges() == 3 +tc.assertEqual(aut.num_states(), 3) +tc.assertEqual(aut.num_edges(), 3) aut.edge_storage(3).cond = buddy.bddfalse aut.purge_dead_states() -assert aut.num_states() == 1 -assert aut.num_edges() == 0 +tc.assertEqual(aut.num_states(), 1) +tc.assertEqual(aut.num_edges(), 0) diff --git a/tests/python/bdddict.py b/tests/python/bdddict.py index d6222b58f..b7b442b1f 100644 --- a/tests/python/bdddict.py +++ b/tests/python/bdddict.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019, 2021 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2019, 2021, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -17,8 +17,8 @@ # You should have received a copy of the GNU General Public License # along with this program. If not, see . -# Make sure we can leep track of BDD association in Python using bdd_dict, as -# discussed in issue #372. +# Make sure we can keep track of BDD association in Python using bdd_dict, as +# discussed in (deleted???) issue #372. # CPython use reference counting, so that automata are destructed # when we expect them to be. However other implementations like @@ -33,6 +33,8 @@ else: gc.collect() import spot +from unittest import TestCase +tc = TestCase() class bdd_holder: @@ -64,7 +66,7 @@ class bdd_holder3: def check_ok(): - assert type(bdict.varnum(spot.formula.ap("a"))) is int + tc.assertIs(type(bdict.varnum(spot.formula.ap("a"))), int) def check_nok(): @@ -123,7 +125,7 @@ debug("h2") h3 = bdd_holder3(h2) var = bdict.register_anonymous_variables(1, h3) debug("h3") -assert var == 2 +tc.assertEqual(var, 2) del h2 gcollect() debug("-h2") diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py index 3d3bb7894..95cc441b3 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 Laboratoire de Recherche et +# Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,11 +24,13 @@ import spot import buddy import sys +from unittest import TestCase +tc = TestCase() run = spot.translate('a & !b').accepting_run() b = run.prefix[0].label c = buddy.bdd_satone(b) -assert c != buddy.bddfalse +tc.assertNotEqual(c, buddy.bddfalse) res = [] while c != buddy.bddtrue: var = buddy.bdd_var(c) @@ -40,23 +42,23 @@ while c != buddy.bddtrue: res.append(var) c = h -assert res == [0, -1] +tc.assertEqual(res, [0, -1]) res2 = [] for i in run.aut.ap(): res2.append((str(i), run.aut.register_ap(i))) -assert str(res2) == "[('a', 0), ('b', 1)]" +tc.assertEqual(str(res2), "[('a', 0), ('b', 1)]") f = spot.bdd_to_formula(b) -assert f._is(spot.op_And) -assert f[0]._is(spot.op_ap) -assert f[1]._is(spot.op_Not) -assert f[1][0]._is(spot.op_ap) -assert str(f) == 'a & !b' +tc.assertTrue(f._is(spot.op_And)) +tc.assertTrue(f[0]._is(spot.op_ap)) +tc.assertTrue(f[1]._is(spot.op_Not)) +tc.assertTrue(f[1][0]._is(spot.op_ap)) +tc.assertEqual(str(f), 'a & !b') try: f = spot.bdd_to_formula(b, spot.make_bdd_dict()) sys.exit(2) except RuntimeError as e: - assert "not in the dictionary" in str(e) + tc.assertIn("not in the dictionary", str(e)) diff --git a/tests/python/bugdet.py b/tests/python/bugdet.py index 9e06e0db3..19434c967 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement +# de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -22,6 +22,8 @@ # sent to the Spot mailing list on 2016-10-31. import spot +from unittest import TestCase +tc = TestCase() a = spot.automaton(""" HOA: v1 @@ -80,12 +82,12 @@ State: 7 {0} # was fine. print("use_simulation=True") b1 = spot.tgba_determinize(b, False, True, True, True) -assert b1.num_states() == 5 +tc.assertEqual(b1.num_states(), 5) b1 = spot.remove_fin(spot.dualize(b1)) -assert not a.intersects(b1) +tc.assertFalse(a.intersects(b1)) print("\nuse_simulation=False") b2 = spot.tgba_determinize(b, False, True, False, True) -assert b2.num_states() == 5 +tc.assertEqual(b2.num_states(), 5) b2 = spot.remove_fin(spot.dualize(b2)) -assert not a.intersects(b2) +tc.assertFalse(a.intersects(b2)) diff --git a/tests/python/complement_semidet.py b/tests/python/complement_semidet.py index 5ab4557bc..da06749a3 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 Laboratoire de Recherche et Développement de +# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -19,6 +19,8 @@ import spot import buddy +from unittest import TestCase +tc = TestCase() def complement(aut): @@ -35,4 +37,4 @@ for aut in spot.automata( comp = complement(aut) semidet_comp = spot.complement_semidet(aut, True) - assert(comp.equivalent_to(semidet_comp)) + tc.assertTrue(comp.equivalent_to(semidet_comp)) diff --git a/tests/python/declenv.py b/tests/python/declenv.py index 868f6ca1d..3ab47736b 100644 --- a/tests/python/declenv.py +++ b/tests/python/declenv.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -21,6 +21,8 @@ # This file tests various error conditions on the twa API import spot +from unittest import TestCase +tc = TestCase() env = spot.declarative_environment() env.declare("a") @@ -28,26 +30,27 @@ env.declare("b") f1a = spot.parse_infix_psl("a U b") f1b = spot.parse_infix_psl("a U b", env) -assert not f1a.errors -assert not f1b.errors +tc.assertFalse(f1a.errors) +tc.assertFalse(f1b.errors) + # In the past, atomic propositions requires via different environments were # never equal, but this feature was never used and we changed that in Spot 2.0 # for the sake of simplicity. -assert f1a.f == f1b.f +tc.assertEqual(f1a.f, f1b.f) f2 = spot.parse_infix_psl("(a U b) U c", env) -assert f2.errors +tc.assertTrue(f2.errors) ostr = spot.ostringstream() f2.format_errors(ostr) err = ostr.str() -assert "unknown atomic proposition `c'" in err +tc.assertIn("unknown atomic proposition `c'", err) f3 = spot.parse_prefix_ltl("R a d", env) -assert f3.errors +tc.assertTrue(f3.errors) ostr = spot.ostringstream() f3.format_errors(ostr) err = ostr.str() -assert "unknown atomic proposition `d'" in err +tc.assertIn("unknown atomic proposition `d'", err) f4 = spot.parse_prefix_ltl("R a b", env) -assert not f4.errors +tc.assertFalse(f4.errors) diff --git a/tests/python/decompose_scc.py b/tests/python/decompose_scc.py index 5f6ad46cb..47741fb72 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 Laboratoire de Recherche et +# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() aut = spot.translate('(Ga -> Gb) W c') si = spot.scc_info(aut) @@ -26,10 +28,10 @@ si = spot.scc_info(aut) # if the generation of the automaton changes, so just scan # for it. rej = [j for j in range(si.scc_count()) if si.is_rejecting_scc(j)] -assert len(rej) == 1 +tc.assertEqual(len(rej), 1) s = spot.decompose_scc(si, rej[0]).to_str('hoa', '1.1') -assert (s == """HOA: v1.1 +tc.assertEqual(s, """HOA: v1.1 States: 3 Start: 0 AP: 3 "b" "a" "c" @@ -56,7 +58,8 @@ except RuntimeError: else: raise AssertionError -assert (spot.decompose_scc(si, 0, True).to_str('hoa', '1.1') == """HOA: v1.1 +tc.assertEqual(spot.decompose_scc(si, 0, True).to_str('hoa', '1.1'), +"""HOA: v1.1 States: 4 Start: 0 AP: 3 "b" "a" "c" @@ -81,7 +84,8 @@ State: 3 [1] 3 --END--""") -assert (spot.decompose_scc(si, 2, True).to_str('hoa', '1.1') == """HOA: v1.1 +tc.assertEqual(spot.decompose_scc(si, 2, True).to_str('hoa', '1.1'), +"""HOA: v1.1 States: 2 Start: 0 AP: 3 "b" "a" "c" @@ -103,4 +107,4 @@ try: except RuntimeError: pass else: - raise AssertionError + raise AssertionError("missing exception") diff --git a/tests/python/det.py b/tests/python/det.py index 03f07c096..36fa31ff3 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 Laboratoire de Recherche et Développement de +# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -19,6 +19,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() a = spot.translate('FGa | FGb') @@ -26,10 +28,10 @@ a = spot.translate('FGa | FGb') d = spot.tgba_determinize(a, False, True, True, True, None, -1, True) cld = list(d.get_original_classes()) -assert [0, 1, 2, 3, 3] == cld +tc.assertEqual([0, 1, 2, 3, 3], cld) e = spot.sbacc(d) -assert e.get_original_states() is None +tc.assertIsNone(e.get_original_states()) cle = list(e.get_original_classes()) -assert len(cle) == e.num_states() -assert set(cle) == set(cld) +tc.assertEqual(len(cle), e.num_states()) +tc.assertEqual(set(cle), set(cld)) diff --git a/tests/python/dualize.py b/tests/python/dualize.py index 81d2a2b23..b870e1e5e 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et +# Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -20,6 +20,8 @@ import spot import buddy +from unittest import TestCase +tc = TestCase() match_strings = [('is_buchi', 'is_co_buchi'), ('is_generalized_buchi', 'is_generalized_co_buchi'), @@ -79,19 +81,19 @@ def test_aut(aut, d=None): def test_complement(aut): - assert aut.is_deterministic() + tc.assertTrue(aut.is_deterministic()) d = spot.dualize(aut) s = spot.product_or(aut, d) - assert spot.dualize(s).is_empty() + tc.assertTrue(spot.dualize(s).is_empty()) def test_assert(a, d=None): t = test_aut(a, d) if not t[0]: - print (t[1]) - print (a.to_str('hoa')) - print (spot.dualize(a).to_str('hoa')) - assert False + print(t[1]) + print(a.to_str('hoa')) + print(spot.dualize(a).to_str('hoa')) + tc.assertTrue(t[0]) aut = spot.translate('a') @@ -101,7 +103,7 @@ test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 3 Start: 1 AP: 1 "a" @@ -117,7 +119,7 @@ State: 1 [!0] 2 State: 2 [t] 2 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -141,7 +143,7 @@ test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" @@ -161,7 +163,7 @@ State: 2 {0} [!1] 3 State: 3 [t] 3 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -186,7 +188,7 @@ test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 2 Start: 1 AP: 2 "a" "b" @@ -198,7 +200,7 @@ State: 0 [t] 0 State: 1 [!0 | !1] 0 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -219,10 +221,10 @@ State: 3 {1} --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 2 Start: 1 AP: 2 "a" "b" @@ -234,7 +236,7 @@ State: 0 [t] 0 State: 1 [!0 | !1] 0 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -255,10 +257,10 @@ State: 3 {0} --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 5 Start: 0 AP: 2 "a" "b" @@ -280,7 +282,7 @@ State: 3 {0} [t] 3 State: 4 [t] 4 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -302,10 +304,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" @@ -327,7 +329,7 @@ State: 2 [!0&!1] 0&2 State: 3 [t] 3 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -348,10 +350,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -362,7 +364,7 @@ properties: deterministic terminal --BODY-- State: 0 [t] 0 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -382,10 +384,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -396,7 +398,7 @@ properties: deterministic terminal --BODY-- State: 0 [t] 0 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -419,7 +421,7 @@ State: 2 dual = spot.dualize(aut) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -435,7 +437,7 @@ State: 1 {0} [t] 1 State: 2 [t] 2 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -456,10 +458,10 @@ State: 2 dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 2 Start: 0 AP: 1 "a" @@ -471,7 +473,7 @@ State: 0 [!0] 1 State: 1 {0} [t] 1 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -495,10 +497,10 @@ State: 3 {0} --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 3 Start: 0 AP: 1 "a" @@ -515,7 +517,7 @@ State: 1 [0] 2 State: 2 {0} [t] 2 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -536,10 +538,10 @@ State: 2 --END--""") dual = spot.dualize(aut) -assert dualtype(aut, dual) +tc.assertTrue(dualtype(aut, dual)) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 3 Start: 0 AP: 1 "a" @@ -555,14 +557,14 @@ State: 1 {0} [t] 0 State: 2 {1} [t] 0 ---END--""" +--END--""") aut = spot.translate('G!a R XFb') test_assert(aut) dual = spot.dualize(aut) h = dual.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 5 Start: 0 AP: 2 "a" "b" @@ -589,7 +591,7 @@ State: 3 {0} [0] 4 State: 4 [t] 4 ---END--""" +--END--""") opts = spot.option_map() opts.set('output', spot.randltlgenerator.LTL) diff --git a/tests/python/ecfalse.py b/tests/python/ecfalse.py index 36301914b..ccbaa2693 100644 --- a/tests/python/ecfalse.py +++ b/tests/python/ecfalse.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ import spot from buddy import bddfalse, bddtrue +from unittest import TestCase +tc = TestCase() a = spot.automaton(""" HOA: v1 @@ -43,8 +45,8 @@ for e in a.out(1): if e.dst == 0: e.cond = bddfalse -assert a.accepting_run() is None -assert a.is_empty() +tc.assertIsNone(a.accepting_run()) +tc.assertTrue(a.is_empty()) for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']: print(name) @@ -52,13 +54,13 @@ for name in ['SE05', 'CVWY90', 'GV04', 'Cou99(shy)', 'Cou99', 'Tau03']: res = ec.check() if res is not None: print(res.accepting_run()) - assert res is None + tc.assertIsNone(res) si = spot.scc_info(a) -assert si.scc_count() == 1 # only one accessible SCC +tc.assertEqual(si.scc_count(), 1) # only one accessible SCC a.set_init_state(0) si = spot.scc_info(a) -assert si.scc_count() == 2 +tc.assertEqual(si.scc_count(), 2) a = spot.automaton("""HOA: v1 States: 11 Start: 0 AP: 2 "a" "b" Acceptance: 8 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & ((Fin(4) & Inf(5)) | (Fin(6) & Inf(7))) @@ -71,16 +73,16 @@ State: 5 State: 6 State: 7 [!0&!1] 1 {4 6 7} [!0&!1] 2 {5 6} State: 8 [!0&!1] 2 {4} State: 9 [!0&!1] 2 {0 4} [!0&!1] 4 {3 4} State: 10 --END-- """) r = a.accepting_run() -assert r is not None -assert r.replay(spot.get_cout()) +tc.assertIsNotNone(r) +tc.assertTrue(r.replay(spot.get_cout())) for e in a.out(7): if e.dst == 2: e.cond = bddfalse s = a.accepting_run() -assert s is not None -assert s.replay(spot.get_cout()) +tc.assertIsNotNone(s) +tc.assertTrue(s.replay(spot.get_cout())) for e in a.out(2): if e.dst == 1: e.cond = bddfalse s = a.accepting_run() -assert s is None +tc.assertIsNone(s) diff --git a/tests/python/except.py b/tests/python/except.py index 178e419b4..8674721c9 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -24,6 +24,8 @@ import spot import buddy +from unittest import TestCase +tc = TestCase() def report_missing_exception(): @@ -35,7 +37,7 @@ aut.set_acceptance(spot.acc_cond("parity min even 4")) try: spot.iar(aut) except RuntimeError as e: - assert 'iar() expects Rabin-like or Streett-like input' in str(e) + tc.assertIn('iar() expects Rabin-like or Streett-like input', str(e)) else: report_missing_exception() @@ -43,7 +45,7 @@ alt = spot.dualize(spot.translate('FGa | FGb')) try: spot.tgba_determinize(alt) except RuntimeError as e: - assert 'tgba_determinize() does not support alternation' in str(e) + tc.assertIn('tgba_determinize() does not support alternation', str(e)) else: report_missing_exception() @@ -52,18 +54,18 @@ aps = aut.ap() rem = spot.remove_ap() rem.add_ap('"a"=0,b') aut = rem.strip(aut) -assert aut.ap() == aps[2:] +tc.assertEqual(aut.ap(), aps[2:]) try: rem.add_ap('"a=0,b') except ValueError as e: - assert """missing closing '"'""" in str(e) + tc.assertIn("""missing closing '"'""", str(e)) else: report_missing_exception() try: rem.add_ap('a=0=b') except ValueError as e: - assert """unexpected '=' at position 3""" in str(e) + tc.assertIn("""unexpected '=' at position 3""", str(e)) else: report_missing_exception() @@ -73,7 +75,7 @@ for meth in ('scc_has_rejecting_cycle', 'is_inherently_weak_scc', try: getattr(spot, meth)(si, 20) except ValueError as e: - assert "invalid SCC number" in str(e) + tc.assertIn("invalid SCC number", str(e)) else: report_missing_exception() @@ -89,14 +91,15 @@ si = spot.scc_info(alt) try: si.determine_unknown_acceptance() except RuntimeError as e: - assert "scc_info::determine_unknown_acceptance() does not supp" in str(e) + tc.assertIn("scc_info::determine_unknown_acceptance() does not supp", + str(e)) else: report_missing_exception() try: alt.set_init_state(999) except ValueError as e: - assert "set_init_state()" in str(e) + tc.assertIn("set_init_state()", str(e)) else: report_missing_exception() @@ -107,7 +110,7 @@ alt.set_init_state(u) try: alt.set_init_state(u - 1) except ValueError as e: - assert "set_init_state()" in str(e) + tc.assertIn("set_init_state()", str(e)) else: report_missing_exception() @@ -116,21 +119,21 @@ r = spot.twa_run(aut) try: a = r.as_twa() except RuntimeError as e: - assert "empty cycle" in str(e) + tc.assertIn("empty cycle", str(e)) else: report_missing_exception() try: a = r.replay(spot.get_cout()) except RuntimeError as e: - assert "empty cycle" in str(e) + tc.assertIn("empty cycle", str(e)) else: report_missing_exception() try: a = r.reduce() except RuntimeError as e: - assert "empty cycle" in str(e) + tc.assertIn("empty cycle", str(e)) else: report_missing_exception() @@ -138,12 +141,12 @@ a = spot.translate('Fa') a = spot.to_generalized_rabin(a, False) r = a.accepting_run() r = r.reduce() -assert r.cycle[0].acc == spot.mark_t([1]) +tc.assertEqual(r.cycle[0].acc, spot.mark_t([1])) r.cycle[0].acc = spot.mark_t([0]) try: r.reduce(); except RuntimeError as e: - assert "expects an accepting cycle" in str(e) + tc.assertIn("expects an accepting cycle", str(e)) else: report_missing_exception() @@ -151,7 +154,7 @@ f = spot.formula('GF(a | Gb)') try: spot.gf_guarantee_to_ba(f, spot._bdd_dict) except RuntimeError as e: - assert "guarantee" in str(e) + tc.assertIn("guarantee", str(e)) else: report_missing_exception() @@ -159,7 +162,7 @@ f = spot.formula('FG(a | Fb)') try: spot.fg_safety_to_dca(f, spot._bdd_dict) except RuntimeError as e: - assert "safety" in str(e) + tc.assertIn("safety", str(e)) else: report_missing_exception() @@ -168,28 +171,28 @@ m = spot.mark_t([n - 1]) try: m = spot.mark_t([0]) << n except RuntimeError as e: - assert "Too many acceptance sets" in str(e) + tc.assertIn("Too many acceptance sets", str(e)) else: report_missing_exception() try: m.set(n) except RuntimeError as e: - assert "bit index is out of bounds" in str(e) + tc.assertIn("bit index is out of bounds", str(e)) else: report_missing_exception() try: m = spot.mark_t([0, n, 1]) except RuntimeError as e: - assert "Too many acceptance sets used. The limit is" in str(e) + tc.assertIn("Too many acceptance sets used. The limit is", str(e)) else: report_missing_exception() try: spot.complement_semidet(spot.translate('Gb R a', 'ba')) except RuntimeError as e: - assert "requires a semi-deterministic input" in str(e) + tc.assertIn("requires a semi-deterministic input", str(e)) else: report_missing_exception() @@ -197,52 +200,55 @@ try: spot.translate('F(G(a | !a) & ((b <-> c) W d))', 'det', 'any') except ValueError as e: s = str(e) - assert 'det' in s - assert 'any' in s + tc.assertIn('det', s) + tc.assertIn('any', s) else: report_missing_exception() a1 = spot.translate('FGa') a2 = spot.translate('Gb') -assert not spot.is_deterministic(a1) -assert spot.is_deterministic(a2) +tc.assertFalse(spot.is_deterministic(a1)) +tc.assertTrue(spot.is_deterministic(a2)) try: spot.product_xor(a1, a2) except RuntimeError as e: - assert "product_xor() only works with deterministic automata" in str(e) + tc.assertIn("product_xor() only works with deterministic automata", str(e)) else: report_missing_exception() try: spot.product_xor(a2, a1) except RuntimeError as e: - assert "product_xor() only works with deterministic automata" in str(e) + tc.assertIn("product_xor() only works with deterministic automata", str(e)) else: report_missing_exception() try: spot.product_xnor(a1, a2) except RuntimeError as e: - assert "product_xnor() only works with deterministic automata" in str(e) + tc.assertIn("product_xnor() only works with deterministic automata", str(e)) else: report_missing_exception() try: spot.product_xnor(a2, a1) except RuntimeError as e: - assert "product_xnor() only works with deterministic automata" in str(e) + tc.assertIn("product_xnor() only works with deterministic automata", str(e)) else: report_missing_exception() try: spot.solve_safety_game(a1) except RuntimeError as e: - assert "solve_safety_game(): arena should have true acceptance" in str(e) + tc.assertIn( + "solve_safety_game(): arena should have true acceptance", + str(e)) else: report_missing_exception() try: spot.solve_parity_game(a1) except RuntimeError as e: - assert "solve_parity_game(): arena must have max-odd acceptance condition" \ - in str(e) + tc.assertIn( + "solve_parity_game(): arena must have max-odd acceptance condition", + str(e)) else: report_missing_exception() @@ -250,16 +256,16 @@ else: try: spot.formula_Star(spot.formula("a"), 10, 333) except OverflowError as e: - assert "333" in str(e) - assert "254" in str(e) + tc.assertIn("333", str(e)) + tc.assertIn("254", str(e)) else: report_missing_exception() try: spot.formula_FStar(spot.formula("a"), 333, 400) except OverflowError as e: - assert "333" in str(e) - assert "254" in str(e) + tc.assertIn("333", str(e)) + tc.assertIn("254", str(e)) else: report_missing_exception() @@ -267,15 +273,15 @@ try: spot.formula_nested_unop_range(spot.op_F, spot.op_Or, 333, 400, spot.formula("a")) except OverflowError as e: - assert "333" in str(e) - assert "254" in str(e) + tc.assertIn("333", str(e)) + tc.assertIn("254", str(e)) else: report_missing_exception() try: spot.formula_FStar(spot.formula("a"), 50, 40) except OverflowError as e: - assert "reversed" in str(e) + tc.assertIn("reversed", str(e)) else: report_missing_exception() @@ -287,5 +293,41 @@ try: a.to_str() except RuntimeError as e: se = str(e) - assert "synthesis-outputs" in se - assert "unregistered proposition" in se + tc.assertIn("synthesis-outputs", se) + tc.assertIn("unregistered proposition", se) +else: + report_missing_exception() + + +a = spot.make_twa_graph() +s = a.new_state() +b = spot.formula_to_bdd("a & b", a.get_dict(), a) +a.new_edge(s, s, b, []) +try: + print(a.to_str('hoa')) +except RuntimeError as e: + tc.assertIn("unregistered atomic propositions", str(e)) +else: + report_missing_exception() + +a.register_aps_from_dict() +tc.assertEqual(a.to_str('hoa'), """HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[0&1] 0 +--END--""") + +try: + a.register_aps_from_dict() +except RuntimeError as e: + se = str(e) + tc.assertIn("register_aps_from_dict", se) + tc.assertIn("already registered", se) +else: + report_missing_exception() diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index 95241be9d..7075cf653 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -976,6 +976,62 @@ "print(ap) # print as a string\n", "display(ap) # LaTeX-style, for notebooks" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Converting to Suffix Operator Normal Form:" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\mathsf{G} (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{F} a)$" + ], + "text/plain": [ + "spot.formula(\"G({x[*]}[]-> Fa)\")" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathit{sonf\\_}_{0} \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathit{sonf\\_}_{1}))$" + ], + "text/plain": [ + "spot.formula(\"Gsonf_0 & G(!sonf_1 | Fa) & G(!sonf_0 | ({x[*]}[]-> sonf_1))\")" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "('sonf_0', 'sonf_1')" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "f = spot.formula('G({x*} []-> Fa)')\n", + "display(f)\n", + "\n", + "# In addition to the formula, returns a list of newly introduced APs\n", + "f, aps = spot.suffix_operator_normal_form(f, 'sonf_')\n", + "display(f)\n", + "display(aps)" + ] } ], "metadata": { diff --git a/tests/python/game.py b/tests/python/game.py index 9d77c153d..d7aec2f38 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 Laboratoire de Recherche et Développement de +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -19,6 +19,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() g = spot.automaton("""HOA: v1 States: 9 Start: 0 AP: 2 "a" "b" acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) properties: @@ -27,10 +29,10 @@ trans-labels explicit-labels state-acc spot-state-player: 0 1 0 1 0 1 {1} [0] 8 State: 3 {1} [1] 4 State: 4 {1} [0] 5 State: 5 {1} [0] 6 State: 6 {1} [1] 7 State: 7 State: 8 {1} [0] 2 --END--""") -assert spot.solve_parity_game(g) == False +tc.assertFalse(spot.solve_parity_game(g)) s = spot.highlight_strategy(g).to_str("HOA", "1.1") -assert s == """HOA: v1.1 +tc.assertEqual(s, """HOA: v1.1 States: 9 Start: 0 AP: 2 "a" "b" @@ -60,4 +62,4 @@ State: 6 {1} State: 7 State: 8 {1} [0] 2 ---END--""" +--END--""") diff --git a/tests/python/gen.py b/tests/python/gen.py index dd844741c..a9fed6890 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,63 +23,66 @@ import spot.gen as gen from sys import exit +from unittest import TestCase +tc = TestCase() k2 = gen.aut_pattern(gen.AUT_KS_NCA, 2) -assert k2.prop_state_acc() -assert k2.num_states() == 5 -assert k2.prop_universal().is_false() -assert k2.prop_inherently_weak().is_false() -assert k2.prop_stutter_invariant().is_false() -assert k2.prop_semi_deterministic().is_false() -assert k2.prop_deterministic().is_false() -assert k2.prop_terminal().is_false() +tc.assertTrue(k2.prop_state_acc()) +tc.assertEqual(k2.num_states(), 5) +tc.assertTrue(k2.prop_universal().is_false()) +tc.assertTrue(k2.prop_inherently_weak().is_false()) +tc.assertTrue(k2.prop_stutter_invariant().is_false()) +tc.assertTrue(k2.prop_semi_deterministic().is_false()) +tc.assertTrue(k2.prop_deterministic().is_false()) +tc.assertTrue(k2.prop_terminal().is_false()) # to_str is defined in the spot package, so this makes sure # the type returned by spot.gen.ks_nca() is the correct one. -assert 'to_str' in dir(k2) +tc.assertIn('to_str', dir(k2)) k3 = gen.aut_pattern(gen.AUT_L_NBA, 3) -assert k3.num_states() == 10 -assert k3.prop_state_acc() -assert k3.prop_universal().is_false() -assert k3.prop_inherently_weak().is_false() -assert k3.prop_stutter_invariant().is_false() -assert k3.prop_semi_deterministic().is_false() -assert k3.prop_deterministic().is_false() -assert k3.prop_terminal().is_false() +tc.assertEqual(k3.num_states(), 10) +tc.assertTrue(k3.prop_state_acc()) +tc.assertTrue(k3.prop_universal().is_false()) +tc.assertTrue(k3.prop_inherently_weak().is_false()) +tc.assertTrue(k3.prop_stutter_invariant().is_false()) +tc.assertTrue(k3.prop_semi_deterministic().is_false()) +tc.assertTrue(k3.prop_deterministic().is_false()) +tc.assertTrue(k3.prop_terminal().is_false()) -assert k2.get_dict() == k3.get_dict() +tc.assertEqual(k2.get_dict(), k3.get_dict()) try: gen.aut_pattern(gen.AUT_KS_NCA, 0) except RuntimeError as e: - assert 'positive argument' in str(e) + tc.assertIn('positive argument', str(e)) else: exit(2) f = gen.ltl_pattern(gen.LTL_AND_F, 3) -assert f.size() == 3 -assert gen.ltl_pattern_name(gen.LTL_AND_F) == "and-f" +tc.assertEqual(f.size(), 3) +tc.assertEqual(gen.ltl_pattern_name(gen.LTL_AND_F), "and-f") try: gen.ltl_pattern(1000, 3) except RuntimeError as e: - assert 'unsupported pattern' in str(e) + tc.assertIn('unsupported pattern', str(e)) else: exit(2) try: gen.ltl_pattern(gen.LTL_OR_G, -10) except RuntimeError as e: - assert 'or-g' in str(e) - assert 'positive' in str(e) + tc.assertIn('or-g', str(e)) + tc.assertIn('positive', str(e)) else: exit(2) -assert 40 == sum(p.size() for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5), - (gen.LTL_GH_Q, 3), - gen.LTL_EH_PATTERNS)) +tc.assertEqual(40, sum(p.size() + for p in gen.ltl_patterns((gen.LTL_OR_G, 1, 5), + (gen.LTL_GH_Q, 3), + gen.LTL_EH_PATTERNS))) -assert 32 == sum(p.num_states() - for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), - (gen.AUT_KS_NCA, 5))) +tc.assertEqual(32, sum(p.num_states() + for p in gen.aut_patterns((gen.AUT_L_NBA, 1, 3), + (gen.AUT_KS_NCA, 5)))) diff --git a/tests/python/genem.py b/tests/python/genem.py index 5da9ce85c..0c9d0809a 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,6 +22,8 @@ # are usable with methods from the spot package. import spot +from unittest import TestCase +tc = TestCase() a1 = spot.automaton(''' HOA: v1 name: "aut" States: 4 Start: 0 AP: 0 @@ -179,7 +181,7 @@ def generic_emptiness2_rec(aut): # Find some Fin set, we necessarily have one, otherwise the SCC # would have been found to be either rejecting or accepting. fo = acc.fin_one() - assert fo >= 0, acc + tc.assertTrue(fo >= 0, acc) for part in si.split_on_sets(scc, [fo]): if not generic_emptiness2(part): return False @@ -309,10 +311,10 @@ def run_bench(automata): + str(res3b)[0] + str(res3c)[0] + str(res3d)[0] + str(res4)[0] + str(res5)[0]) print(res) - assert res in ('TTTTTTTT', 'FFFFFFFF') + tc.assertIn(res, ('TTTTTTTT', 'FFFFFFFF')) if res == 'FFFFFFFF': run3 = spot.generic_accepting_run(aut) - assert run3.replay(spot.get_cout()) is True + tc.assertTrue(run3.replay(spot.get_cout())) run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360, act]) diff --git a/tests/python/implies.py b/tests/python/implies.py index 2e4e64ddd..24d74b720 100755 --- a/tests/python/implies.py +++ b/tests/python/implies.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2022 Laboratoire de Recherche et Développement # de l'EPITA. # # This file is part of Spot, a model checking library. @@ -19,6 +19,8 @@ import sys from buddy import * +from unittest import TestCase +tc = TestCase() bdd_init(10000, 10000) bdd_setvarnum(5) @@ -33,26 +35,26 @@ e = V[1] & V[2] & -V[3] & V[4] f = V[0] & -V[3] & V[4] g = -V[0] | V[1] -assert(bdd_implies(b, a)) -assert(not bdd_implies(a, b)) -assert(not bdd_implies(c, a)) -assert(bdd_implies(a, d)) -assert(bdd_implies(b, d)) -assert(bdd_implies(c, d)) -assert(bdd_implies(d, d)) -assert(not bdd_implies(e, d)) -assert(not bdd_implies(d, e)) -assert(not bdd_implies(f, e)) -assert(not bdd_implies(e, f)) -assert(bdd_implies(bddfalse, f)) -assert(not bdd_implies(bddtrue, f)) -assert(bdd_implies(f, bddtrue)) -assert(not bdd_implies(f, bddfalse)) -assert(bdd_implies(a, g)) +tc.assertTrue(bdd_implies(b, a)) +tc.assertFalse(bdd_implies(a, b)) +tc.assertFalse(bdd_implies(c, a)) +tc.assertTrue(bdd_implies(a, d)) +tc.assertTrue(bdd_implies(b, d)) +tc.assertTrue(bdd_implies(c, d)) +tc.assertTrue(bdd_implies(d, d)) +tc.assertFalse(bdd_implies(e, d)) +tc.assertFalse(bdd_implies(d, e)) +tc.assertFalse(bdd_implies(f, e)) +tc.assertFalse(bdd_implies(e, f)) +tc.assertTrue(bdd_implies(bddfalse, f)) +tc.assertFalse(bdd_implies(bddtrue, f)) +tc.assertTrue(bdd_implies(f, bddtrue)) +tc.assertFalse(bdd_implies(f, bddfalse)) +tc.assertTrue(bdd_implies(a, g)) a = (-V[2] & (-V[1] | V[0])) | (-V[0] & V[1] & V[2]) b = V[1] | -V[2] -assert(bdd_implies(a, b)) +tc.assertTrue(bdd_implies(a, b)) # Cleanup all BDD variables before calling bdd_done(), otherwise # bdd_delref will be called after bdd_done() and this is unsafe in diff --git a/tests/python/intrun.py b/tests/python/intrun.py index c86c6d643..e3b708a95 100644 --- a/tests/python/intrun.py +++ b/tests/python/intrun.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() # This issue was reported by Florian Renkin. The reduce() call used in # intersecting_run() was bogus, and could incorrectly reduce a word @@ -34,5 +36,5 @@ trans-labels explicit-labels trans-acc complete properties: deterministic State: 3 [t] 1 {1 2} State: 4 [!0&1] 4 {2} [!0&!1] 3 {2} [0] 2 {0 2} --END--""") r = b.intersecting_run(spot.complement(a)); c = spot.twa_word(r).as_automaton() -assert c.intersects(b) -assert not c.intersects(a) +tc.assertTrue(c.intersects(b)) +tc.assertFalse(c.intersects(a)) diff --git a/tests/python/kripke.py b/tests/python/kripke.py index f3ce218b2..fa92b3fa9 100644 --- a/tests/python/kripke.py +++ b/tests/python/kripke.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,6 +19,9 @@ import spot import buddy +from unittest import TestCase +tc = TestCase() + bdict = spot.make_bdd_dict() k = spot.make_kripke_graph(bdict) p1 = buddy.bdd_ithvar(k.register_ap("p1")) @@ -51,25 +54,25 @@ State: [0&1] 1 "0" State: [!0&!1] 2 "2" 2 1 --END--""" -assert hoa == k.to_str('HOA') -assert k.num_states() == 3 -assert k.num_edges() == 5 +tc.assertEqual(hoa, k.to_str('HOA')) +tc.assertEqual(k.num_states(), 3) +tc.assertEqual(k.num_edges(), 5) res = [] for e in k.out(s1): res.append((e.src, e.dst)) -assert res == [(1, 0), (1, 2)] +tc.assertEqual(res, [(1, 0), (1, 2)]) res = [] for e in k.edges(): res.append((e.src, e.dst)) -assert res == [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)] +tc.assertEqual(res, [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)]) res = [] for s in k.states(): res.append(s.cond()) -assert res == [cond1, cond2, cond3] +tc.assertEqual(res, [cond1, cond2, cond3]) -assert k.states()[0].cond() == cond1 -assert k.states()[1].cond() == cond2 -assert k.states()[2].cond() == cond3 +tc.assertEqual(k.states()[0].cond(), cond1) +tc.assertEqual(k.states()[1].cond(), cond2) +tc.assertEqual(k.states()[2].cond(), cond3) diff --git a/tests/python/langmap.py b/tests/python/langmap.py index 6fd860986..723a5c0d5 100644 --- a/tests/python/langmap.py +++ b/tests/python/langmap.py @@ -1,6 +1,6 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017, 2020 Laboratoire de Recherche et Développement -# de l'Epita (LRDE) +# Copyright (C) 2016, 2017, 2020, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE) # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ import spot import sys +from unittest import TestCase +tc = TestCase() def hstates(txt): @@ -31,13 +33,10 @@ def hstates(txt): def test(f, opt, expected): aut = spot.translate(f, *opt, 'deterministic') v = spot.language_map(aut) - assert len(v) == aut.num_states() + tc.assertEqual(len(v), aut.num_states()) spot.highlight_languages(aut) l = hstates(aut.to_str('hoa', '1.1')) - if l != expected: - print('for {}\nexpected: {}\n but got: {}'.format(f, expected, l), - file=sys.stderr) - exit(1) + tc.assertEqual(l, expected) test('GF(a) & GFb & c', ['Buchi', 'SBAcc'], '1 0 2 0 3 0') @@ -50,6 +49,6 @@ test('Xa', ['Buchi', 'SBAcc'], '') try: test('FGa', ['Buchi'], '') except RuntimeError as e: - assert 'language_map only works with deterministic automata'in str(e) + tc.assertIn('language_map only works with deterministic automata', str(e)) else: exit(1) diff --git a/tests/python/ltl2tgba.py b/tests/python/ltl2tgba.py index 25fff4566..913c557be 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 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2014-2016, 2021-2022 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -98,7 +98,7 @@ if f: elif taa_opt: a = concrete = spot.ltl_to_taa(f, dict) else: - assert "unspecified translator" + raise RuntimeError("unspecified translator") if wdba: a = spot.ensure_digraph(a) @@ -117,7 +117,7 @@ if f: elif output == 6: spot.print_lbtt(cout, a) else: - assert "unknown output option" + raise RuntimeError("unknown output option") if degeneralize_opt: del degeneralized @@ -137,4 +137,6 @@ del dict # not necessary in other implementations. from platform import python_implementation if python_implementation() == 'CPython': - assert spot.fnode_instances_check() + from unittest import TestCase + tc = TestCase() + tc.assertTrue(spot.fnode_instances_check()) diff --git a/tests/python/ltlf.py b/tests/python/ltlf.py index 5676a2a1b..b13432d3e 100644 --- a/tests/python/ltlf.py +++ b/tests/python/ltlf.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de # l'Epita # # This file is part of Spot, a model checking library. @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() lcc = spot.language_containment_checker() @@ -43,5 +45,5 @@ for f in formulas: f4 = spot.formula_And([spot.from_ltlf(f2), cst]) print("{}\t=>\t{}".format(f1, f3)) print("{}\t=>\t{}".format(f2, f4)) - assert lcc.equal(f3, f4) + tc.assertTrue(lcc.equal(f3, f4)) print() diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index 98562743c..208e0c321 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 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2009-2012, 2014-2017, 2019, 2021-2022 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -22,6 +22,8 @@ import sys import spot +from unittest import TestCase +tc = TestCase() e = spot.default_environment.instance() @@ -41,11 +43,11 @@ for str1, isl in l: pf = spot.parse_infix_psl(str2, e) if pf.format_errors(spot.get_cout()): sys.exit(1) - assert isl == pf.f.is_leaf() + tc.assertEqual(isl, pf.f.is_leaf()) del pf -assert spot.formula('a').is_leaf() -assert spot.formula('0').is_leaf() +tc.assertTrue(spot.formula('a').is_leaf()) +tc.assertTrue(spot.formula('0').is_leaf()) for str1 in ['a * b', 'a xor b', 'a <-> b']: pf = spot.parse_infix_boolean(str1, e, False) @@ -66,21 +68,21 @@ for (x, op) in [('a* <-> b*', "`<->'"), ('a*[=2]', "[=...]"), ('a*[->2]', "[->...]")]: f5 = spot.parse_infix_sere(x) - assert f5.errors + tc.assertTrue(f5.errors) ostr = spot.ostringstream() f5.format_errors(ostr) err = ostr.str() - assert "not a Boolean expression" in err - assert op in err - assert "SERE" in err + tc.assertIn("not a Boolean expression", err) + tc.assertIn(op, err) + tc.assertIn("SERE", err) del f5 f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]') -assert not f6.errors +tc.assertFalse(f6.errors) del f6 f6 = spot.parse_infix_sere('-') -assert f6.errors +tc.assertTrue(f6.errors) del f6 for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), @@ -150,12 +152,12 @@ for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), ('{"X}', "missing closing brace"), ]: f7 = spot.parse_infix_psl(x) - assert f7.errors + tc.assertTrue(f7.errors) ostr = spot.ostringstream() f7.format_errors(ostr) err = ostr.str() print(err) - assert msg in err + tc.assertIn(msg, err) del f7 for (x, msg) in [('a&', "missing right operand for \"and operator\""), @@ -174,12 +176,12 @@ for (x, msg) in [('a&', "missing right operand for \"and operator\""), ('!', "missing right operand for \"not operator\""), ]: f8 = spot.parse_infix_boolean(x) - assert f8.errors + tc.assertTrue(f8.errors) ostr = spot.ostringstream() f8.format_errors(ostr) err = ostr.str() print(err) - assert msg in err + tc.assertIn(msg, err) del f8 for (x, msg) in [('a->', "missing right operand for \"implication operator\""), @@ -191,12 +193,12 @@ for (x, msg) in [('a->', "missing right operand for \"implication operator\""), ]: f9 = spot.parse_infix_psl(x, spot.default_environment.instance(), False, True) - assert f9.errors + tc.assertTrue(f9.errors) ostr = spot.ostringstream() f9.format_errors(ostr) err = ostr.str() print(err) - assert msg in err + tc.assertIn(msg, err) del f9 # force GC before fnode_instances_check(), unless it's CPython @@ -205,15 +207,15 @@ if python_implementation() != 'CPython': import gc gc.collect() -assert spot.fnode_instances_check() +tc.assertTrue(spot.fnode_instances_check()) f = spot.formula_F(2, 4, spot.formula_ap("a")) -assert f == spot.formula("XX(a | X(a | X(a)))") +tc.assertEqual(f, spot.formula("XX(a | X(a | X(a)))")) f = spot.formula_G(2, 4, spot.formula_ap("a")) -assert f == spot.formula("XX(a & X(a & X(a)))") +tc.assertEqual(f, spot.formula("XX(a & X(a & X(a)))")) f = spot.formula_X(2, spot.formula_ap("a")) -assert f == spot.formula("XX(a)") +tc.assertEqual(f, spot.formula("XX(a)")) f = spot.formula_G(2, spot.formula_unbounded(), spot.formula_ap("a")) -assert f == spot.formula("XXG(a)") +tc.assertEqual(f, spot.formula("XXG(a)")) f = spot.formula_F(2, spot.formula_unbounded(), spot.formula_ap("a")) -assert f == spot.formula("XXF(a)") +tc.assertEqual(f, spot.formula("XXF(a)")) diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index 7b88f07dc..c21c3b7f1 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 Laboratoire de +# Copyright (C) 2009, 2010, 2012, 2015, 2018, 2021-2022 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systemes Répartis Coopératifs (SRC), Université Pierre @@ -22,6 +22,8 @@ import spot import sys +from unittest import TestCase +tc = TestCase() # Some of the tests here assume timely destructor calls, as they occur # in the the reference-counted CPython implementation. Other @@ -35,13 +37,13 @@ b = spot.formula.ap('b') c = spot.formula.ap('c') c2 = spot.formula.ap('c') -assert c == c2 +tc.assertEqual(c, c2) op = spot.formula.And([a, b]) op2 = spot.formula.And([op, c]) op3 = spot.formula.And([a, c, b]) -assert op2 == op3 +tc.assertEqual(op2, op3) # The symbol for a subformula which hasn't been cloned is better # suppressed, so we don't attempt to reuse it elsewhere. @@ -52,12 +54,12 @@ sys.stdout.write('op2 = %s\n' % str(op2)) del a, b, c2 sys.stdout.write('op3 = %s\n' % str(op3)) -assert op2 == op3 +tc.assertEqual(op2, op3) op4 = spot.formula.Or([op2, op3]) sys.stdout.write('op4 = %s\n' % str(op4)) -assert op4 == op2 +tc.assertEqual(op4, op2) del op2, op3, op4 @@ -78,10 +80,11 @@ f5 = spot.formula.Xor(F, c) del a, b, c, T, F, f1, f2, f4, f5 if is_cpython: - assert spot.fnode_instances_check() + tc.assertTrue(spot.fnode_instances_check()) # ---------------------------------------------------------------------- -assert str([str(x) for x in spot.formula('a &b & c')]) == "['a', 'b', 'c']" +tc.assertEqual(str([str(x) for x in spot.formula('a &b & c')]), + "['a', 'b', 'c']") def switch_g_f(x): @@ -93,7 +96,7 @@ def switch_g_f(x): f = spot.formula('GFa & XFGb & Fc & G(a | b | Fd)') -assert str(switch_g_f(f)) == 'FGa & XGFb & Gc & F(a | b | Gd)' +tc.assertEqual(str(switch_g_f(f)), 'FGa & XGFb & Gc & F(a | b | Gd)') x = 0 @@ -105,7 +108,7 @@ def count_g(f): f.traverse(count_g) -assert x == 3 +tc.assertEqual(x, 3) # ---------------------------------------------------------------------- @@ -121,14 +124,14 @@ LBT for shell: echo {f:lq} | ... Default for CSV: ...,{f:c},... Wring, centered: {f:w:~^50}""".format(f=formula) -assert res == """\ +tc.assertEqual(res, """\ Default output: a U (b U "$strange[0]=name") Spin syntax: a U (b U ($strange[0]=name)) (Spin syntax): (a) U ((b) U ($strange[0]=name)) Default for shell: echo 'a U (b U "$strange[0]=name")' | ... LBT for shell: echo 'U "a" U "b" "$strange[0]=name"' | ... Default for CSV: ...,"a U (b U ""$strange[0]=name"")",... -Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~""" +Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~""") opt = spot.tl_simplifier_options(False, True, True, @@ -144,9 +147,8 @@ for (input, output) in [('(a&b)<->b', 'b->(a&b)'), ('b xor (!(a&b))', 'b->(a&b)'), ('!b xor (a&b)', 'b->(a&b)')]: f = spot.tl_simplifier(opt).simplify(input) - print(input, f, output) - assert(f == output) - assert(spot.are_equivalent(input, output)) + tc.assertEqual(f, output) + tc.assertTrue(spot.are_equivalent(input, output)) def myparse(input): @@ -157,7 +159,7 @@ def myparse(input): # This used to fail, because myparse would return a pointer # to pf.f inside the destroyed pf. -assert myparse('a U b') == spot.formula('a U b') +tc.assertEqual(myparse('a U b'), spot.formula('a U b')) -assert spot.is_liveness('a <-> GFb') -assert not spot.is_liveness('a & GFb') +tc.assertTrue(spot.is_liveness('a <-> GFb')) +tc.assertFalse(spot.is_liveness('a & GFb')) diff --git a/tests/python/mealy.py b/tests/python/mealy.py index da71d1bfb..71c7739f9 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -19,6 +19,8 @@ # along with this program. If not, see . import spot, buddy +from unittest import TestCase +tc = TestCase() # Testing Sat-based approach @@ -42,8 +44,8 @@ spot.set_state_players(a, [False,True,False,True,False,True]) spot.set_synthesis_outputs(a, o1&o2) b = spot.minimize_mealy(a) -assert(list(spot.get_state_players(b)).count(False) == 2) -assert(spot.is_split_mealy_specialization(a, b)) +tc.assertEqual(list(spot.get_state_players(b)).count(False), 2) +tc.assertTrue(spot.is_split_mealy_specialization(a, b)) test_auts = [ ("""HOA: v1 @@ -371,21 +373,21 @@ for (mealy_str, nenv_min) in test_auts: elif aap.ap_name().startswith("i"): ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name())) else: - assert("""Aps must start with either "i" or "o".""") + raise AssertionError("""Aps must start with either "i" or "o".""") spot.set_synthesis_outputs(mealy, outs) mealy_min_ks = spot.minimize_mealy(mealy, -1) n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)]) - assert(n_e == nenv_min) - assert(spot.is_split_mealy_specialization(mealy, mealy_min_ks)) + tc.assertEqual(n_e, nenv_min) + tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_ks)) # Test un- and resplit tmp = spot.unsplit_2step(mealy_min_ks) mealy_min_rs = spot.split_2step(tmp, spot.get_synthesis_outputs(tmp), False) - assert(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True)) - assert(spot.are_equivalent(mealy_min_ks, mealy_min_rs)) + tc.assertTrue(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True)) + tc.assertTrue(spot.are_equivalent(mealy_min_ks, mealy_min_rs)) # Testing bisimulation (with output assignment) @@ -515,15 +517,15 @@ spot.set_synthesis_outputs(aut, & buddy.bdd_ithvar( aut.register_ap("u02alarm29control0f1d2alarm29turn2off1b"))) min_equiv = spot.reduce_mealy(aut, False) -assert min_equiv.num_states() == 6 -assert spot.are_equivalent(min_equiv, aut) +tc.assertEqual(min_equiv.num_states(), 6) +tc.assertTrue(spot.are_equivalent(min_equiv, aut)) # Build an automaton that recognizes a subset of the language of the original # automaton min_sub = spot.reduce_mealy(aut, True) -assert min_sub.num_states() == 5 +tc.assertEqual(min_sub.num_states(), 5) prod = spot.product(spot.complement(aut), min_sub) -assert spot.generic_emptiness_check(prod) +tc.assertTrue(spot.generic_emptiness_check(prod)) aut = spot.automaton(""" HOA: v1 @@ -564,7 +566,7 @@ State: 0 # An example that shows that we should not build a tree when we use inclusion. res = spot.reduce_mealy(aut, True) -assert res.to_str() == exp +tc.assertEqual(res.to_str(), exp) aut = spot.automaton(""" HOA: v1 @@ -608,4 +610,4 @@ State: 1 --END--""" res = spot.reduce_mealy(aut, True) -assert res.to_str() == exp +tc.assertEqual(res.to_str(), exp) diff --git a/tests/python/merge.py b/tests/python/merge.py index c56d8f309..893916953 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et +# Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() aut = spot.automaton(""" HOA: v1 @@ -39,7 +41,7 @@ State: 2 out = spot.simplify_acceptance(aut) hoa = out.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -54,8 +56,8 @@ State: 1 [1] 2 {0} State: 2 [1] 0 ---END--""" -assert spot.are_equivalent(out, aut) +--END--""") +tc.assertTrue(spot.are_equivalent(out, aut)) aut = spot.automaton("""HOA: v1 States: 3 @@ -75,7 +77,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -90,7 +92,7 @@ State: 1 [1] 2 {0} State: 2 [1] 0 ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -111,7 +113,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -126,7 +128,7 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -146,7 +148,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -161,7 +163,7 @@ State: 1 [1] 2 {1} State: 2 [1] 0 {0} ---END--""" +--END--""") aut = spot.automaton(""" HOA: v1 @@ -182,7 +184,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -197,7 +199,7 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -217,7 +219,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -232,7 +234,7 @@ State: 1 {0} [1] 2 State: 2 {0} [1] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -252,7 +254,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -267,7 +269,7 @@ State: 1 {0} [1] 2 State: 2 {0} [1] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -287,7 +289,7 @@ State: 2 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -301,7 +303,7 @@ State: 1 {1} [1] 2 State: 2 [1] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 4 @@ -335,7 +337,7 @@ State: 3 {1 3} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 4 Start: 0 AP: 2 "a" "b" @@ -364,7 +366,7 @@ State: 3 {1} [0&!1] 0 [!0&1] 3 [0&1] 2 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -388,7 +390,7 @@ State: 2 out = spot.simplify_acceptance(aut) hoa = out.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" @@ -406,8 +408,8 @@ State: 1 State: 2 [0] 2 {0} [!0] 1 {0} ---END--""" -assert spot.are_equivalent(out, aut) +--END--""") +tc.assertTrue(spot.are_equivalent(out, aut)) aut = spot.automaton("""HOA: v1 States: 4 @@ -435,7 +437,7 @@ State: 3 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 4 Start: 0 AP: 2 "p0" "p1" @@ -457,7 +459,7 @@ State: 3 [0&1] 0 {1} [0&!1] 3 {1 2} [!0] 1 {3} ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 1 @@ -475,7 +477,7 @@ State: 0 {1 2} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 1 Start: 0 AP: 2 "p0" "p1" @@ -486,7 +488,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 2 @@ -506,7 +508,7 @@ State: 1 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -519,7 +521,7 @@ State: 0 [!0] 1 {2} State: 1 [t] 1 {1 2} ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 1 @@ -536,7 +538,7 @@ State: 0 {0 1 3} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 1 Start: 0 AP: 2 "p0" "p1" @@ -547,7 +549,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 2 @@ -568,7 +570,7 @@ State: 1 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -583,7 +585,7 @@ State: 0 State: 1 [0] 1 [!0] 0 {1} ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 2 @@ -602,7 +604,7 @@ State: 1 {1} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -615,7 +617,7 @@ State: 0 [t] 1 State: 1 [t] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -636,7 +638,7 @@ State: 2 {2} spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" @@ -650,7 +652,7 @@ State: 1 {0} [t] 1 State: 2 {2} [t] 1 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -672,7 +674,7 @@ State: 2 {1 2 3} out = spot.simplify_acceptance(aut) hoa = out.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p1" @@ -687,8 +689,8 @@ State: 1 {1} [t] 2 State: 2 {0 1} [t] 1 ---END--""" -assert spot.are_equivalent(out, aut) +--END--""") +tc.assertTrue(spot.are_equivalent(out, aut)) aut = spot.automaton("""HOA: v1 States: 2 @@ -708,7 +710,7 @@ State: 1 spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 2 Start: 0 AP: 2 "p0" "p1" @@ -722,7 +724,7 @@ State: 0 State: 1 [0] 1 [!0] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -740,7 +742,7 @@ State: 2 --END--""") spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -755,7 +757,7 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -773,7 +775,7 @@ State: 2 --END--""") spot.simplify_acceptance_here(aut) hoa = aut.to_str('hoa') -assert hoa == """HOA: v1 +tc.assertEqual(hoa, """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -788,4 +790,4 @@ State: 1 [1] 2 State: 2 [1] 0 ---END--""" +--END--""") diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py index e55bdabf2..4e97abe23 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, 2021 Laboratoire de Recherche et Développement de +# Copyright (C) 2020-2022 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -20,12 +20,14 @@ import spot +from unittest import TestCase +tc = TestCase() aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a" Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""") -assert aut.num_edges() == 2 +tc.assertEqual(aut.num_edges(), 2) aut.merge_edges() -assert aut.num_edges() == 1 +tc.assertEqual(aut.num_edges(), 1) aut = spot.automaton(""" HOA: v1 @@ -44,15 +46,15 @@ State: 1 [0 | 1] 1 [0&!1] 1 {0} --END--""") -assert aut.num_edges() == 5 +tc.assertEqual(aut.num_edges(), 5) aut.merge_edges() -assert aut.num_edges() == 5 -assert not spot.is_deterministic(aut) +tc.assertEqual(aut.num_edges(), 5) +tc.assertFalse(spot.is_deterministic(aut)) aut = spot.split_edges(aut) -assert aut.num_edges() == 9 +tc.assertEqual(aut.num_edges(), 9) aut.merge_edges() -assert aut.num_edges() == 5 -assert spot.is_deterministic(aut) +tc.assertEqual(aut.num_edges(), 5) +tc.assertTrue(spot.is_deterministic(aut)) aut = spot.automaton(""" HOA: v1 @@ -74,15 +76,15 @@ State: 2 [0] 1 --END--""") aut.merge_states() -assert aut.num_edges() == 4 -assert aut.num_states() == 2 -assert spot.is_deterministic(aut) -assert aut.prop_complete() +tc.assertEqual(aut.num_edges(), 4) +tc.assertEqual(aut.num_states(), 2) +tc.assertTrue(spot.is_deterministic(aut)) +tc.assertTrue(aut.prop_complete()) aut.merge_states() -assert aut.num_edges() == 4 -assert aut.num_states() == 2 -assert spot.is_deterministic(aut) -assert aut.prop_complete() +tc.assertEqual(aut.num_edges(), 4) +tc.assertEqual(aut.num_states(), 2) +tc.assertTrue(spot.is_deterministic(aut)) +tc.assertTrue(aut.prop_complete()) aa = spot.automaton(""" diff --git a/tests/python/misc-ec.py b/tests/python/misc-ec.py index d1234bd69..85d4aaa47 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 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2017, 2020, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,6 +18,9 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() + aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'Buchi', 'SBAcc') ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut) n = 0 @@ -27,7 +30,7 @@ while True: break print(res.accepting_run()) n += 1 -assert n == 2 +tc.assertEqual(n, 2) for name in ['SE05', 'CVWY90', 'GV04']: aut = spot.translate("GFa && GFb") @@ -35,13 +38,13 @@ for name in ['SE05', 'CVWY90', 'GV04']: ec = spot.make_emptiness_check_instantiator(name)[0].instantiate(aut) print(ec.check().accepting_run()) except RuntimeError as e: - assert "Büchi or weak" in str(e) + tc.assertIn("Büchi or weak", str(e)) aut = spot.translate("a", 'monitor') try: ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) except RuntimeError as e: - assert "at least one" in str(e) + tc.assertIn("at least one", str(e)) aut = spot.translate("a", 'ba') ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) diff --git a/tests/python/optionmap.py b/tests/python/optionmap.py index 667ef0b19..ad526f510 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 Laboratoire de Recherche et Développement -# de l'EPITA. +# Copyright (C) 2010, 2012, 2018, 2022 Laboratoire de Recherche et +# Développement de l'EPITA. # Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -21,65 +21,67 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() o = spot.option_map() res = o.parse_options("optA, opta=2M, optb =4 ; optB = 7\ , optC= 10") -assert not res +tc.assertFalse(res) -assert o.get('optA') == 1 -assert o.get('opta') == 2*1024*1024 -assert o.get('optb') == 4 -assert o.get('optB') == 7 -assert o.get('optC') == 10 -assert o.get('none') == 0 -assert o.get('none', 16) == 16 +tc.assertEqual(o.get('optA'), 1) +tc.assertEqual(o.get('opta'), 2*1024*1024) +tc.assertEqual(o.get('optb'), 4) +tc.assertEqual(o.get('optB'), 7) +tc.assertEqual(o.get('optC'), 10) +tc.assertEqual(o.get('none'), 0) +tc.assertEqual(o.get('none', 16), 16) o.set('optb', 40) -assert o.get('optb') == 40 +tc.assertEqual(o.get('optb'), 40) res = o.parse_options("!optA !optb optC, !optB") -assert not res -assert o.get('optA') == 0 -assert o.get('opta') == 2*1024*1024 -assert o.get('optb') == 0 -assert o.get('optB') == 0 -assert o.get('optC') == 1 +tc.assertFalse(res) +tc.assertEqual(o.get('optA'), 0) +tc.assertEqual(o.get('opta'), 2*1024*1024) +tc.assertEqual(o.get('optb'), 0) +tc.assertEqual(o.get('optB'), 0) +tc.assertEqual(o.get('optC'), 1) res = o.parse_options("!") -assert res == "!" +tc.assertEqual(res, "!") res = o.parse_options("foo, !opt = 1") -assert res == "!opt = 1" +tc.assertEqual(res, "!opt = 1") res = o.parse_options("foo=3, opt == 1") -assert res == "opt == 1" +tc.assertEqual(res, "opt == 1") res = o.parse_options("foo=3opt == 1") -assert res == "3opt == 1" +tc.assertEqual(res, "3opt == 1") aut1 = spot.translate('GF(a <-> XXa)', 'det') -assert aut1.num_states() == 4 +tc.assertEqual(aut1.num_states(), 4) aut2 = spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') -assert aut2.num_states() == 9 +tc.assertEqual(aut2.num_states(), 9) try: spot.translate('GF(a <-> XXa)', 'det', xargs='foobar=1') except RuntimeError as e: - assert "option 'foobar' was not used" in str(e) + tc.assertIn("option 'foobar' was not used", str(e)) else: raise RuntimeError("missing exception") try: spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=0') except RuntimeError as e: - assert "option 'gf-guarantee' was not used" in str(e) + tc.assertIn("option 'gf-guarantee' was not used", str(e)) else: raise RuntimeError("missing exception") try: spot.translate('GF(a <-> XXa)').postprocess('det', xargs='gf-guarantee=x') except RuntimeError as e: - assert "failed to parse option at: 'gf-guarantee=x'" in str(e) + tc.assertIn("failed to parse option at: 'gf-guarantee=x'", str(e)) else: raise RuntimeError("missing exception") diff --git a/tests/python/origstate.py b/tests/python/origstate.py index 0ca013889..15a7ab0ad 100644 --- a/tests/python/origstate.py +++ b/tests/python/origstate.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2015, 2017, 2022 Laboratoire de Recherche et +# Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ import spot from sys import exit +from unittest import TestCase +tc = TestCase() aut = spot.automaton(""" HOA: v1 @@ -38,7 +40,7 @@ State: 1 """) aut2 = spot.degeneralize(aut) -assert aut2.to_str() == """HOA: v1 +tc.assertEqual(aut2.to_str(), """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -56,10 +58,10 @@ State: 1 [1] 2 State: 2 {0} [1] 2 ---END--""" +--END--""") aut2.copy_state_names_from(aut) -assert aut2.to_str() == """HOA: v1 +tc.assertEqual(aut2.to_str(), """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -77,7 +79,7 @@ State: 1 "0#0" [1] 2 State: 2 "1#1" {0} [1] 2 ---END--""" +--END--""") aut2.set_init_state(2) aut2.purge_unreachable_states() @@ -93,16 +95,16 @@ properties: deterministic State: 0 "1#1" {0} [1] 0 --END--""" -assert aut2.to_str() == ref +tc.assertEqual(aut2.to_str(), ref) # This makes sure that the original-states vector has also been renamed. aut2.copy_state_names_from(aut) -assert aut2.to_str() == ref +tc.assertEqual(aut2.to_str(), ref) aut2 = spot.degeneralize(aut) aut2.release_named_properties() try: aut2.copy_state_names_from(aut) except RuntimeError as e: - assert "state does not exist in source automaton" in str(e) + tc.assertIn("state does not exist in source automaton", str(e)) else: exit(1) diff --git a/tests/python/otfcrash.py b/tests/python/otfcrash.py index 69acbcb1a..8e30cb501 100644 --- a/tests/python/otfcrash.py +++ b/tests/python/otfcrash.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2018, 2022 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -23,6 +23,8 @@ import spot.aux import tempfile import shutil import sys +from unittest import TestCase +tc = TestCase() spot.ltsmin.require('divine') @@ -51,4 +53,4 @@ system async; p = spot.otf_product(k, a) return p.is_empty() - assert(modelcheck('X "R.found"', m) == True) + tc.assertTrue(modelcheck('X "R.found"', m)) diff --git a/tests/python/parity.py b/tests/python/parity.py index b0389c40e..6ced51c40 100644 --- a/tests/python/parity.py +++ b/tests/python/parity.py @@ -19,36 +19,38 @@ # 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) -assert max_even_5 == spot.acc_code.parity_max_even(5) -assert max_even_5 == spot.acc_code.parity_max(False, 5) +tc.assertEqual(max_even_5, spot.acc_code.parity_max_even(5)) +tc.assertEqual(max_even_5, spot.acc_code.parity_max(False, 5)) min_even_5 = spot.acc_code.parity(False, False, 5) -assert min_even_5 == spot.acc_code.parity_min_even(5) -assert min_even_5 == spot.acc_code.parity_min(False, 5) +tc.assertEqual(min_even_5, spot.acc_code.parity_min_even(5)) +tc.assertEqual(min_even_5, spot.acc_code.parity_min(False, 5)) max_odd_5 = spot.acc_code.parity(True, True, 5) -assert max_odd_5 == spot.acc_code.parity_max_odd(5) -assert max_odd_5 == spot.acc_code.parity_max(True, 5) +tc.assertEqual(max_odd_5, spot.acc_code.parity_max_odd(5)) +tc.assertEqual(max_odd_5, spot.acc_code.parity_max(True, 5)) min_odd_5 = spot.acc_code.parity(False, True, 5) -assert min_odd_5 == spot.acc_code.parity_min_odd(5) -assert min_odd_5 == spot.acc_code.parity_min(True, 5) +tc.assertEqual(min_odd_5, spot.acc_code.parity_min_odd(5)) +tc.assertEqual(min_odd_5, spot.acc_code.parity_min(True, 5)) for f in ('FGa', 'GFa & GFb & FGc', 'XXX(a U b)'): a1 = spot.translate(f, 'parity') - assert a1.acc().is_parity() + tc.assertTrue(a1.acc().is_parity()) a2 = spot.translate(f).postprocess('parity') - assert a2.acc().is_parity() + tc.assertTrue(a2.acc().is_parity()) a3 = spot.translate(f, 'det').postprocess('parity', 'colored') - assert a3.acc().is_parity() - assert spot.is_colored(a3) + tc.assertTrue(a3.acc().is_parity()) + tc.assertTrue(spot.is_colored(a3)) a = spot.translate('GFa & GFb') try: spot.change_parity_here(a, spot.parity_kind_same, spot.parity_style_even) except RuntimeError as e: - assert 'input should have parity acceptance' in str(e) + tc.assertIn('input should have parity acceptance', str(e)) else: exit(2) @@ -64,7 +66,7 @@ State: 0 --END-- """) spot.cleanup_parity_here(a) -assert a.to_str() == """HOA: v1 +tc.assertEqual(a.to_str(), """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -75,7 +77,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""" +--END--""") a = spot.automaton(""" HOA: v1 @@ -89,7 +91,7 @@ State: 0 --END-- """) spot.cleanup_parity_here(a) -assert a.to_str() == """HOA: v1 +tc.assertEqual(a.to_str(), """HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -100,7 +102,7 @@ properties: deterministic --BODY-- State: 0 [t] 0 ---END--""" +--END--""") a = spot.automaton("""HOA: v1 States: 3 @@ -120,39 +122,39 @@ State: 2 try: spot.get_state_players(a) except RuntimeError as e: - assert "not a game" in str(e) + tc.assertIn("not a game", str(e)) else: report_missing_exception() try: spot.set_state_player(a, 1, True) except RuntimeError as e: - assert "Can only" in str(e) + tc.assertIn("Can only", str(e)) else: report_missing__exception() spot.set_state_players(a, (False, True, False)) -assert spot.get_state_player(a, 0) == False -assert spot.get_state_player(a, 1) == True -assert spot.get_state_player(a, 2) == False +tc.assertEqual(spot.get_state_player(a, 0), False) +tc.assertEqual(spot.get_state_player(a, 1), True) +tc.assertEqual(spot.get_state_player(a, 2), False) try: spot.set_state_players(a, [True, False, False, False]) except RuntimeError as e: - assert "many owners as states" in str(e) + tc.assertIn("many owners as states", str(e)) else: report_missing_exception() try: spot.get_state_player(a, 4) except RuntimeError as e: - assert "invalid state number" in str(e) + tc.assertIn("invalid state number", str(e)) else: report_missing_exception() try: spot.set_state_player(a, 4, True) except RuntimeError as e: - assert "invalid state number" in str(e) + tc.assertIn("invalid state number", str(e)) else: report_missing_exception() @@ -168,4 +170,4 @@ oi.erase() # postprocess used to call reduce_parity that did not # work correctly on automata with deleted edges. sm = a.postprocess("gen", "small") -assert sm.num_states() == 3 +tc.assertEqual(sm.num_states(), 3) diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py index cbcacb183..038b33a19 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 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2012, 2014, 2015, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ import os import spot +from unittest import TestCase +tc = TestCase() contents = ''' HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi @@ -34,7 +36,7 @@ out.close() a = spot.parse_aut(filename, spot.make_bdd_dict()) -assert not a.errors +tc.assertFalse(a.errors) spot.print_dot(spot.get_cout(), a.aut) diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 02150d375..12bc9e39a 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 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2019, 2020, 2021, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -23,6 +23,8 @@ import spot +from unittest import TestCase +tc = TestCase() a, b, d, f = spot.automata(""" HOA: v1 @@ -73,19 +75,19 @@ State: 1 --END-- """) -assert spot.is_partially_degeneralizable(a) == [0, 1] +tc.assertEqual(spot.is_partially_degeneralizable(a), [0, 1]) da = spot.partial_degeneralize(a, [0, 1]) -assert da.equivalent_to(a) -assert da.num_states() == 2 +tc.assertTrue(da.equivalent_to(a)) +tc.assertEqual(da.num_states(), 2) -assert spot.is_partially_degeneralizable(b) == [0, 1] +tc.assertEqual(spot.is_partially_degeneralizable(b), [0, 1]) db = spot.partial_degeneralize(b, [0, 1]) -assert db.equivalent_to(b) -assert db.num_states() == 3 +tc.assertTrue(db.equivalent_to(b)) +tc.assertEqual(db.num_states(), 3) db.copy_state_names_from(b) dbhoa = db.to_str('hoa') -assert dbhoa == """HOA: v1 +tc.assertEqual(dbhoa, """HOA: v1 States: 3 Start: 0 AP: 1 "p0" @@ -99,28 +101,28 @@ State: 1 "0#0" {0 1} [0] 2 State: 2 "1#0" {1} [0] 1 ---END--""" +--END--""") c = spot.automaton("randaut -A'(Fin(0)&Inf(1)&Inf(2))|Fin(2)' 1 |") -assert spot.is_partially_degeneralizable(c) == [1, 2] +tc.assertEqual(spot.is_partially_degeneralizable(c), [1, 2]) dc = spot.partial_degeneralize(c, [1, 2]) -assert dc.equivalent_to(c) -assert str(dc.get_acceptance()) == '(Fin(0) & Inf(2)) | Fin(1)' +tc.assertTrue(dc.equivalent_to(c)) +tc.assertEqual(str(dc.get_acceptance()), '(Fin(0) & Inf(2)) | Fin(1)') -assert spot.is_partially_degeneralizable(d) == [] +tc.assertEqual(spot.is_partially_degeneralizable(d), []) dd = spot.partial_degeneralize(d, []) -assert dd.equivalent_to(d) -assert dd.num_states() == 1 -assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)' +tc.assertTrue(dd.equivalent_to(d)) +tc.assertEqual(dd.num_states(), 1) +tc.assertEqual(str(dd.get_acceptance()), 'Inf(1) & Fin(0)') e = spot.dualize(b) de = spot.partial_degeneralize(e, [0, 1]) -assert de.equivalent_to(e) -assert de.num_states() == 4 +tc.assertTrue(de.equivalent_to(e)) +tc.assertEqual(de.num_states(), 4) de.copy_state_names_from(e) dehoa = de.to_str('hoa') -assert dehoa == """HOA: v1 +tc.assertEqual(dehoa, """HOA: v1 States: 4 Start: 0 AP: 1 "p0" @@ -140,18 +142,18 @@ State: 2 "3#0" State: 3 "2#0" [0] 1 {0} [!0] 2 ---END--""" +--END--""") -assert spot.is_partially_degeneralizable(de) == [] +tc.assertEqual(spot.is_partially_degeneralizable(de), []) df = spot.partial_degeneralize(f, [0, 1]) df.equivalent_to(f) -assert str(df.acc()) == '(1, Fin(0))' +tc.assertEqual(str(df.acc()), '(1, Fin(0))') try: df = spot.partial_degeneralize(f, [0, 1, 2]) except RuntimeError as e: - assert 'partial_degeneralize(): {0,1,2} does not' in str(e) + tc.assertIn('partial_degeneralize(): {0,1,2} does not', str(e)) else: raise RuntimeError("missing exception") @@ -165,13 +167,13 @@ State: 2 [0&!1&2] 3 {1 4 9} State: 3 [0&!1&2] 4 {0 1 5 9} State: 4 [!0&!1&2] 1 State: 7 [0&!1&!2] 0 {4 7} --END--""") daut5 = spot.degeneralize_tba(aut5) -assert daut5.equivalent_to(aut5) +tc.assertTrue(daut5.equivalent_to(aut5)) sets = list(range(aut5.num_sets())) -assert spot.is_partially_degeneralizable(aut5) == sets +tc.assertEqual(spot.is_partially_degeneralizable(aut5), sets) pdaut5 = spot.partial_degeneralize(aut5, sets) -assert pdaut5.equivalent_to(aut5) -assert daut5.num_states() == 9 -assert pdaut5.num_states() == 8 +tc.assertTrue(pdaut5.equivalent_to(aut5)) +tc.assertEqual(daut5.num_states(), 9) +tc.assertEqual(pdaut5.num_states(), 8) aut6 = spot.automaton("""HOA: v1 States: 6 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: generalized-Buchi 3 Acceptance: 3 Inf(0)&Inf(1)&Inf(2) properties: @@ -180,13 +182,13 @@ trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [0&1&!2] 5 {1} State: 4 [!0&1&!2] 0 {1 2} [0&!1&!2] 3 {0} State: 5 [!0&1&2] 1 --END-- """) daut6 = spot.degeneralize_tba(aut6) -assert daut6.equivalent_to(aut6) +tc.assertTrue(daut6.equivalent_to(aut6)) sets = list(range(aut6.num_sets())) -assert spot.is_partially_degeneralizable(aut6) == sets +tc.assertEqual(spot.is_partially_degeneralizable(aut6), sets) pdaut6 = spot.partial_degeneralize(aut6, sets) -assert pdaut6.equivalent_to(aut6) -assert daut6.num_states() == 8 -assert pdaut6.num_states() == 8 +tc.assertTrue(pdaut6.equivalent_to(aut6)) +tc.assertEqual(daut6.num_states(), 8) +tc.assertEqual(pdaut6.num_states(), 8) aut7 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" @@ -197,13 +199,13 @@ State: 0 [0&!1&2] 1 {2 3} State: 1 [0&!1&2] 0 {0 2} [0&!1&!2] 6 State: 2 [!0&!1&!2] 3 State: 5 [0&1&!2] 0 [!0&1&2] 7 State: 6 [0&1&2] 2 {1} State: 7 [!0&!1&2] 0 {0} [!0&1&!2] 4 --END--""") daut7 = spot.degeneralize_tba(aut7) -assert daut7.equivalent_to(aut7) +tc.assertTrue(daut7.equivalent_to(aut7)) sets = list(range(aut7.num_sets())) -assert spot.is_partially_degeneralizable(aut7) == sets +tc.assertEqual(spot.is_partially_degeneralizable(aut7), sets) pdaut7 = spot.partial_degeneralize(aut7, sets) -assert pdaut7.equivalent_to(aut7) -assert daut7.num_states() == 10 -assert pdaut7.num_states() == 10 +tc.assertTrue(pdaut7.equivalent_to(aut7)) +tc.assertEqual(daut7.num_states(), 10) +tc.assertEqual(pdaut7.num_states(), 10) aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4) @@ -213,19 +215,19 @@ State: 0 [!0&1&!2] 7 {0} State: 1 [!0&1&2] 1 {4} [0&!1&2] 6 {1 2} State: 2 5 [!0&1&!2] 0 {1 3} State: 6 [0&1&2] 4 [0&1&!2] 6 State: 7 [!0&!1&!2] 1 --END--""") daut8 = spot.degeneralize_tba(aut8) -assert daut8.equivalent_to(aut8) +tc.assertTrue(daut8.equivalent_to(aut8)) sets = list(range(aut8.num_sets())) -assert spot.is_partially_degeneralizable(aut8) == sets +tc.assertEqual(spot.is_partially_degeneralizable(aut8), sets) pdaut8 = spot.partial_degeneralize(aut8, sets) -assert pdaut8.equivalent_to(aut8) -assert daut8.num_states() == 22 -assert pdaut8.num_states() == 9 +tc.assertTrue(pdaut8.equivalent_to(aut8)) +tc.assertEqual(daut8.num_states(), 22) +tc.assertEqual(pdaut8.num_states(), 9) aut9 = spot.dualize(aut8) pdaut9 = spot.partial_degeneralize(aut9, sets) -assert pdaut9.equivalent_to(aut9) +tc.assertTrue(pdaut9.equivalent_to(aut9)) # one more state than aut9, because dualize completed the automaton. -assert pdaut9.num_states() == 10 +tc.assertEqual(pdaut9.num_states(), 10) aut10 = spot.automaton("""HOA: v1 States: 3 @@ -242,10 +244,10 @@ State: 2 [0] 0 {1} [!0] 1 --END--""") -assert spot.is_partially_degeneralizable(aut10) == [0, 1] +tc.assertEqual(spot.is_partially_degeneralizable(aut10), [0, 1]) pdaut10 = spot.partial_degeneralize(aut10, [0, 1]) -assert pdaut10.equivalent_to(aut10) -assert pdaut10.to_str() == """HOA: v1 +tc.assertTrue(pdaut10.equivalent_to(aut10)) +tc.assertEqual(pdaut10.to_str(), """HOA: v1 States: 3 Start: 0 AP: 1 "p0" @@ -260,7 +262,7 @@ State: 1 State: 2 [0] 0 {1} [!0] 1 ---END--""" +--END--""") aut11 = spot.automaton("""HOA: v1 States: 3 @@ -277,10 +279,10 @@ State: 2 [0] 0 {1} [!0] 1 --END--""") -assert spot.is_partially_degeneralizable(aut11) == [0, 1] +tc.assertEqual(spot.is_partially_degeneralizable(aut11), [0, 1]) pdaut11 = spot.partial_degeneralize(aut11, [0, 1]) -assert pdaut11.equivalent_to(aut11) -assert pdaut11.to_str() == """HOA: v1 +tc.assertTrue(pdaut11.equivalent_to(aut11)) +tc.assertEqual(pdaut11.to_str(), """HOA: v1 States: 3 Start: 0 AP: 1 "p0" @@ -295,7 +297,7 @@ State: 1 State: 2 [0] 0 {2} [!0] 1 ---END--""" +--END--""") aut12 = spot.automaton("""HOA: v1 States: 3 @@ -313,24 +315,24 @@ State: 2 [0] 0 [!0] 1 {3} --END--""") -assert spot.is_partially_degeneralizable(aut12) == [0,1] +tc.assertEqual(spot.is_partially_degeneralizable(aut12), [0,1]) aut12b = spot.partial_degeneralize(aut12, [0,1]) aut12c = spot.partial_degeneralize(aut12b, [1,2]) -assert aut12c.equivalent_to(aut12) -assert aut12c.num_states() == 9 +tc.assertTrue(aut12c.equivalent_to(aut12)) +tc.assertEqual(aut12c.num_states(), 9) aut12d = spot.partial_degeneralize(aut12, [0,1,3]) aut12e = spot.partial_degeneralize(aut12d, [0,1]) -assert aut12e.equivalent_to(aut12) -assert aut12e.num_states() == 9 +tc.assertTrue(aut12e.equivalent_to(aut12)) +tc.assertEqual(aut12e.num_states(), 9) aut12f = spot.partial_degeneralize(aut12) -assert aut12f.equivalent_to(aut12) -assert aut12f.num_states() == 9 +tc.assertTrue(aut12f.equivalent_to(aut12)) +tc.assertEqual(aut12f.num_states(), 9) # Check handling of original-states dot = aut12f.to_str('dot', 'd') -assert dot == """digraph "" { +tc.assertEqual(dot, """digraph "" { rankdir=LR label="Inf(2) | (Inf(1) & Fin(0))\\n[Rabin-like 2]" labelloc="t" @@ -367,10 +369,10 @@ assert dot == """digraph "" { 8 -> 4 [label="p0\\n{1,2}"] 8 -> 7 [label="p0"] } -""" +""") aut12g = spot.partial_degeneralize(aut12f) -assert aut12f == aut12g +tc.assertEqual(aut12f, aut12g) aut13 = spot.automaton("""HOA: v1 States: 2 @@ -390,8 +392,8 @@ State: 1 [!0&!1&2&3] 1 {0 2} --END--""") aut13g = spot.partial_degeneralize(aut13) -assert aut13g.equivalent_to(aut13) -assert aut13g.num_states() == 3 +tc.assertTrue(aut13g.equivalent_to(aut13)) +tc.assertEqual(aut13g.num_states(), 3) aut14 = spot.automaton("""HOA: v1 @@ -412,8 +414,8 @@ State: 1 --END-- """) aut14g = spot.partial_degeneralize(aut14) -assert aut14g.equivalent_to(aut14) -assert aut14g.num_states() == 3 +tc.assertTrue(aut14g.equivalent_to(aut14)) +tc.assertEqual(aut14g.num_states(), 3) # Extracting an SCC from this large automaton will produce an automaton A in # which original-states refers to states larger than those in A. Some version @@ -439,4 +441,4 @@ State: 10 [!0&1] 4 [0&1] 8 [!0&!1] 10 {0 1 2 3 5} [0&!1] 13 {1 2 3} State: 11 si = spot.scc_info(aut15) aut15b = si.split_on_sets(2, [])[0]; d aut15c = spot.partial_degeneralize(aut15b) -assert aut15c.equivalent_to(aut15b) +tc.assertTrue(aut15c.equivalent_to(aut15b)) diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py index 098bafb26..4d00b4dae 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 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2016-2017, 2019-2020, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() # make sure that we are not allowed to build the product of two automata with # different dictionaries. @@ -94,14 +96,14 @@ State: 60 40 38 60 68 State: 61 40 41 57 61 State: 62 40 59 44 62 State: State: 70 40 59 57 70 State: 71 40 63 57 71 State: 72 40 69 57 72 --END-- ''') res = spot.product(left, right) -assert res.num_states() == 977 -assert res.num_edges() == 8554 +tc.assertEqual(res.num_states(), 977) +tc.assertEqual(res.num_edges(), 8554) res = spot.product(left, right, spot.output_aborter(1000, 6000)) -assert res is None +tc.assertIsNone(res) res = spot.product(left, right, spot.output_aborter(900, 9000)) -assert res is None +tc.assertIsNone(res) res = spot.product(left, right, spot.output_aborter(1000, 9000)) -assert res is not None +tc.assertIsNotNone(res) a, b = spot.automata("""HOA: v1 States: 1 Start: 0 AP: 0 acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete @@ -110,7 +112,7 @@ properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 properties: trans-labels explicit-labels state-acc complete properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 --END--""") out = spot.product(a, b).to_str() -assert out == """HOA: v1 +tc.assertEqual(out, """HOA: v1 States: 1 Start: 0 AP: 0 @@ -120,9 +122,9 @@ properties: trans-labels explicit-labels state-acc deterministic properties: stutter-invariant terminal --BODY-- State: 0 ---END--""" +--END--""") out = spot.product_susp(a, b).to_str() -assert out == """HOA: v1 +tc.assertEqual(out, """HOA: v1 States: 1 Start: 0 AP: 0 @@ -132,4 +134,4 @@ properties: trans-labels explicit-labels state-acc deterministic properties: stutter-invariant terminal --BODY-- State: 0 ---END--""" +--END--""") diff --git a/tests/python/randgen.py b/tests/python/randgen.py index 094ddcb3f..32762d02e 100755 --- a/tests/python/randgen.py +++ b/tests/python/randgen.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2015, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,9 +18,11 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() o = spot.option_map() g = spot.randltlgenerator(0, o) -assert str(g.next()) == '1' -assert str(g.next()) == '0' -assert str(g.next()) == 'None' +tc.assertEqual(str(g.next()), '1') +tc.assertEqual(str(g.next()), '0') +tc.assertEqual(str(g.next()), 'None') diff --git a/tests/python/relabel.py b/tests/python/relabel.py index 5a4a370eb..0de668b12 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 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2015, 2017-2019, 2022 Laboratoire de Recherche et +# Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() f = spot.formula('GF(a & b) -> (FG(a & b) & Gc)') m = spot.relabeling_map() @@ -26,19 +28,18 @@ res = "" for old, new in m.items(): res += "#define {} {}\n".format(old, new) res += str(g) -print(res) -assert(res == """#define p0 a & b +tc.assertEqual(res, """#define p0 a & b #define p1 c GFp0 -> (FGp0 & Gp1)""") h = spot.relabel_apply(g, m) -assert h == f +tc.assertEqual(h, f) autg = g.translate() spot.relabel_here(autg, m) -assert str(autg.ap()) == \ - '(spot.formula("a"), spot.formula("b"), spot.formula("c"))' -assert spot.isomorphism_checker.are_isomorphic(autg, f.translate()) +tc.assertEqual(str(autg.ap()), \ + '(spot.formula("a"), spot.formula("b"), spot.formula("c"))') +tc.assertTrue(spot.isomorphism_checker.are_isomorphic(autg, f.translate())) a = spot.formula('a') u = spot.formula('a U b') @@ -46,11 +47,11 @@ m[a] = u try: spot.relabel_here(autg, m) except RuntimeError as e: - assert "new labels" in str(e) + tc.assertIn("new labels", str(e)) m = spot.relabeling_map() m[u] = a try: spot.relabel_here(autg, m) except RuntimeError as e: - assert "old labels" in str(e) + tc.assertIn("old labels", str(e)) diff --git a/tests/python/remfin.py b/tests/python/remfin.py index 20115a14f..ffff3e22a 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 Laboratoire de Recherche et Développement de -# l'Epita +# Copyright (C) 2015-2018, 2020, 2022 Laboratoire de Recherche et +# Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ import spot +from unittest import TestCase +tc = TestCase() # This test used to trigger an assertion (or a segfault) # in scc_filter_states(). @@ -41,7 +43,7 @@ State: 2 aut.prop_inherently_weak(True) aut = spot.dualize(aut) aut1 = spot.scc_filter_states(aut) -assert(aut1.to_str('hoa') == """HOA: v1 +tc.assertEqual(aut1.to_str('hoa'), """HOA: v1 States: 2 Start: 0 AP: 1 "a" @@ -56,17 +58,17 @@ State: 1 [t] 1 --END--""") -assert(aut.scc_filter_states().to_str() == aut1.to_str()) -assert(aut1.get_name() == None) +tc.assertEqual(aut.scc_filter_states().to_str(), aut1.to_str()) +tc.assertIsNone(aut1.get_name()) aut1.set_name("test me") -assert(aut1.get_name() == "test me") +tc.assertEqual(aut1.get_name(), "test me") # The method is the same as the function a = spot.translate('true', 'low', 'any') -assert(a.prop_universal().is_maybe()) -assert(a.prop_unambiguous().is_maybe()) -assert(a.is_deterministic() == True) -assert(a.is_unambiguous() == True) +tc.assertTrue(a.prop_universal().is_maybe()) +tc.assertTrue(a.prop_unambiguous().is_maybe()) +tc.assertTrue(a.is_deterministic()) +tc.assertTrue(a.is_unambiguous()) a = spot.automaton(""" HOA: v1 @@ -92,4 +94,4 @@ State: 2 """) b = spot.remove_fin(a) size = (b.num_states(), b.num_edges()) -assert size == (5, 13); +tc.assertEqual(size, (5, 13)) diff --git a/tests/python/removeap.py b/tests/python/removeap.py index 7a9268c85..ba656ac89 100644 --- a/tests/python/removeap.py +++ b/tests/python/removeap.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019 Laboratoire de Recherche et Développement +# Copyright (C) 2019, 2022 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,16 +18,18 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() aut = spot.translate('a U (c & Gb)') -assert not spot.is_terminal_automaton(aut) -assert aut.prop_terminal().is_false() +tc.assertFalse(spot.is_terminal_automaton(aut)) +tc.assertTrue(aut.prop_terminal().is_false()) rem = spot.remove_ap() rem.add_ap("b") aut = rem.strip(aut) -assert not aut.prop_terminal().is_false() -assert spot.is_terminal_automaton(aut) -assert aut.prop_terminal().is_true() +tc.assertFalse(aut.prop_terminal().is_false()) +tc.assertTrue(spot.is_terminal_automaton(aut)) +tc.assertTrue(aut.prop_terminal().is_true()) aut = rem.strip(aut) -assert aut.prop_terminal().is_true() +tc.assertTrue(aut.prop_terminal().is_true()) diff --git a/tests/python/rs_like.py b/tests/python/rs_like.py index 7b4ee75cf..669af5885 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 Laboratoire de Recherche et Développement +# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() a = spot.vector_rs_pair() @@ -30,12 +32,13 @@ mall = spot.mark_t() def test_rs(acc, rs, expected_res, expected_pairs): res, p = getattr(acc, 'is_' + rs + '_like')() - assert res == expected_res + tc.assertEqual(res, expected_res) if expected_res: expected_pairs.sort() p = sorted(p) for a, b in zip(p, expected_pairs): - assert a.fin == b.fin and a.inf == b.inf + tc.assertEqual(a.fin, b.fin) + tc.assertEqual(a.inf, b.inf) def switch_pairs(pairs): diff --git a/tests/python/satmin.py b/tests/python/satmin.py index 2d28dd405..f9fa466f8 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 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2015, 2020, 2021, 2022 Laboratoire de Recherche et +# Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -18,232 +18,234 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() aut = spot.translate('GFa & GFb', 'Buchi', 'SBAcc') -assert aut.num_sets() == 1 -assert aut.num_states() == 3 -assert aut.is_deterministic() +tc.assertEqual(aut.num_sets(), 1) +tc.assertEqual(aut.num_states(), 3) +tc.assertTrue(aut.is_deterministic()) min1 = spot.sat_minimize(aut, acc='Rabin 1') -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_langmap=True) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=0) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=1) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=2) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1, sat_incr_steps=50) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=-1) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=0) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=1) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=2) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2, sat_incr_steps=50) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_naive=True) -assert min1.num_sets() == 2 -assert min1.num_states() == 2 +tc.assertEqual(min1.num_sets(), 2) +tc.assertEqual(min1.num_states(), 2) min2 = spot.sat_minimize(aut, acc='Streett 2') -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_langmap=True) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=0) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=1) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=2) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1, sat_incr_steps=50) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=-1) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=0) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=1) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=2) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2, sat_incr_steps=50) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min2 = spot.sat_minimize(aut, acc='Streett 2', sat_naive=True) -assert min2.num_sets() == 4 -assert min2.num_states() == 1 +tc.assertEqual(min2.num_sets(), 4) +tc.assertEqual(min2.num_states(), 1) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_langmap=True) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=1) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=1, sat_incr_steps=0) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=1, sat_incr_steps=1) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=1, sat_incr_steps=2) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=1, sat_incr_steps=50) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2, sat_incr_steps=-1) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2, sat_incr_steps=0) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2, sat_incr_steps=1) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2, sat_incr_steps=2) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_incr=2, sat_incr_steps=50) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, sat_naive=True) -assert min3.num_sets() == 4 -assert min3.num_states() == 3 +tc.assertEqual(min3.num_sets(), 4) +tc.assertEqual(min3.num_states(), 3) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_langmap=True) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=0) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=1) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=2) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=1, sat_incr_steps=50) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=-1) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=0) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=1) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=2) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_incr=2, sat_incr_steps=50) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_naive=True) -assert min4.num_sets() == 3 -assert min4.num_states() == 2 +tc.assertEqual(min4.num_sets(), 3) +tc.assertEqual(min4.num_states(), 2) aut = spot.translate('GFa') -assert aut.num_sets() == 1 -assert aut.num_states() == 1 -assert aut.is_deterministic() +tc.assertEqual(aut.num_sets(), 1) +tc.assertEqual(aut.num_states(), 1) +tc.assertTrue(aut.is_deterministic()) out = spot.sat_minimize(aut, state_based=True) -assert out.num_states() == 2 +tc.assertEqual(out.num_states(), 2) out = spot.sat_minimize(aut, state_based=True, max_states=1) -assert out is None +tc.assertTrue(out is None) diff --git a/tests/python/sbacc.py b/tests/python/sbacc.py index 445845dbc..22d937014 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 Laboratoire de Recherche et +# Copyright (C) 2017-2018, 2021, 2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -18,13 +18,15 @@ # along with this program. If not, see . import spot -aut = spot.translate('GFa') -assert aut.num_states() == 1 -assert not aut.prop_state_acc().is_true() -aut = spot.sbacc(aut) -assert aut.num_states() == 2 -assert aut.prop_state_acc().is_true() +from unittest import TestCase +tc = TestCase() +aut = spot.translate('GFa') +tc.assertEqual(aut.num_states(), 1) +tc.assertFalse(aut.prop_state_acc().is_true()) +aut = spot.sbacc(aut) +tc.assertEqual(aut.num_states(), 2) +tc.assertTrue(aut.prop_state_acc().is_true()) aut = spot.automaton("""HOA: v1 States: 3 @@ -48,7 +50,7 @@ s = spot.sbacc(aut) s.copy_state_names_from(aut) h = s.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -59,7 +61,7 @@ State: 0 "0" [0] 1 State: 1 "2" {1} [t] 1 ---END--""" +--END--""") aut = spot.automaton("""HOA: v1 States: 3 @@ -83,7 +85,7 @@ d = spot.degeneralize(aut) d.copy_state_names_from(aut) h = d.to_str('hoa') -assert h == """HOA: v1 +tc.assertEqual(h, """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -95,4 +97,4 @@ State: 0 "0#0" [0] 1 State: 1 "2#0" {0} [t] 1 ---END--""" +--END--""") diff --git a/tests/python/sccfilter.py b/tests/python/sccfilter.py index 6edd33e9f..7728b70a6 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 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -22,6 +22,8 @@ # Major) import spot +from unittest import TestCase +tc = TestCase() a = spot.automaton(""" HOA: v1.1 @@ -43,7 +45,7 @@ State: 1 "bar" --END-- """) -assert (spot.scc_filter(a, True).to_str('hoa', '1.1') == """HOA: v1.1 +tc.assertEqual(spot.scc_filter(a, True).to_str('hoa', '1.1'), """HOA: v1.1 States: 2 Start: 0 AP: 1 "a" diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py index 0ac645726..f8ade7e4b 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et +# Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() a = spot.translate('(Ga -> Gb) W c') @@ -26,11 +28,11 @@ try: si = spot.scc_info(a, 10) exit(2) except RuntimeError as e: - assert "initial state does not exist" in str(e) + tc.assertIn("initial state does not exist", str(e)) si = spot.scc_info(a) n = si.scc_count() -assert n == 4 +tc.assertEqual(n, 4) acc = 0 rej = 0 @@ -39,24 +41,24 @@ for i in range(n): acc += si.is_accepting_scc(i) rej += si.is_rejecting_scc(i) triv += si.is_trivial(i) -assert acc == 3 -assert rej == 1 -assert triv == 0 +tc.assertEqual(acc, 3) +tc.assertEqual(rej, 1) +tc.assertEqual(triv, 0) for scc in si: acc -= scc.is_accepting() rej -= scc.is_rejecting() triv -= scc.is_trivial() -assert acc == 0 -assert rej == 0 -assert triv == 0 +tc.assertEqual(acc, 0) +tc.assertEqual(rej, 0) +tc.assertEqual(triv, 0) l0 = si.states_of(0) l1 = si.states_of(1) l2 = si.states_of(2) l3 = si.states_of(3) l = sorted(list(l0) + list(l1) + list(l2) + list(l3)) -assert l == [0, 1, 2, 3, 4] +tc.assertEqual(l, [0, 1, 2, 3, 4]) i = si.initial() todo = [i] @@ -73,14 +75,14 @@ while todo: if s not in seen: seen.add(s) todo.append(s) -assert seen == {0, 1, 2, 3} -assert trans == [(0, 0), (0, 1), (0, 2), (0, 3), - (2, 0), (2, 1), (2, 2), (2, 4), - (3, 3), (4, 1), (4, 4), (1, 1)] -assert transi == [(0, 0, 1), (0, 2, 3), (2, 0, 6), - (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)] +tc.assertEqual(seen, {0, 1, 2, 3}) +tc.assertEqual(trans, [(0, 0), (0, 1), (0, 2), (0, 3), + (2, 0), (2, 1), (2, 2), (2, 4), + (3, 3), (4, 1), (4, 4), (1, 1)]) +tc.assertEqual(transi, [(0, 0, 1), (0, 2, 3), (2, 0, 6), + (2, 2, 8), (3, 3, 10), (4, 4, 12), (1, 1, 5)]) -assert not spot.is_weak_automaton(a, si) +tc.assertFalse(spot.is_weak_automaton(a, si)) a = spot.automaton(""" @@ -107,8 +109,8 @@ State: 3 """) si = spot.scc_info(a) si.determine_unknown_acceptance() -assert si.scc_count() == 2 -assert si.is_accepting_scc(0) -assert not si.is_rejecting_scc(0) -assert si.is_rejecting_scc(1) -assert not si.is_accepting_scc(1) +tc.assertEqual(si.scc_count(), 2) +tc.assertTrue(si.is_accepting_scc(0)) +tc.assertFalse(si.is_rejecting_scc(0)) +tc.assertTrue(si.is_rejecting_scc(1)) +tc.assertFalse(si.is_accepting_scc(1)) diff --git a/tests/python/sccsplit.py b/tests/python/sccsplit.py index 9095a1a29..4a1781475 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement +# de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,6 +19,9 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() + aut = spot.translate('GF(a <-> Xa) & GF(b <-> XXb)') si = spot.scc_info(aut) @@ -27,4 +30,4 @@ for aut2 in si.split_on_sets(0, [0]): # This call to to_str() used to fail because split_on_sets had not # registered the atomic propositions of aut s += aut2.to_str() -assert spot.automaton(s).num_states() == 8 +tc.assertEqual(spot.automaton(s).num_states(), 8) diff --git a/tests/python/semidet.py b/tests/python/semidet.py index 856b3b7d2..9072f5917 100644 --- a/tests/python/semidet.py +++ b/tests/python/semidet.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2017, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() formulas = [('(Gp0 | Fp1) M 1', False, True), ('(!p1 U p1) U X(!p0 -> Fp1)', False, True), @@ -31,9 +33,9 @@ for f, isd, issd in formulas: aut = spot.translate(f) # The formula with isd=True, issd=True is the only one # for which both properties are already set. - assert (aut.prop_deterministic().is_maybe() or - aut.prop_semi_deterministic().is_maybe() or - isd == issd) + tc.assertTrue(aut.prop_deterministic().is_maybe() or + aut.prop_semi_deterministic().is_maybe() or + isd == issd) spot.check_determinism(aut) - assert aut.prop_deterministic() == isd - assert aut.prop_semi_deterministic() == issd + tc.assertEqual(aut.prop_deterministic(), isd) + tc.assertEqual(aut.prop_semi_deterministic(), issd) diff --git a/tests/python/setacc.py b/tests/python/setacc.py index 8d20b6a49..7246bf5cc 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2016, 2018, 2021, 2022 Laboratoire de Recherche et +# Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,54 +19,56 @@ # along with this program. If not, see . 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")) -assert(a.prop_state_acc() == True) +tc.assertTrue(a.prop_state_acc()) a.set_acceptance(1, spot.acc_code("Fin(0)")) -assert(a.prop_state_acc() == spot.trival.maybe()) +tc.assertEqual(a.prop_state_acc(), spot.trival.maybe()) # Some tests for used_inf_fin_sets(), which return a pair of mark_t. (inf, fin) = a.get_acceptance().used_inf_fin_sets() -assert inf == [] -assert fin == [0] +tc.assertEqual(inf, []) +tc.assertEqual(fin, [0]) (inf, fin) = spot.acc_code("(Fin(0)|Inf(1))&Fin(2)&Inf(0)").used_inf_fin_sets() -assert inf == [0, 1] -assert fin == [0, 2] +tc.assertEqual(inf, [0, 1]) +tc.assertEqual(fin, [0, 2]) # is_rabin_like() returns (bool, [(inf, fin), ...]) (b, v) = spot.acc_cond("(Fin(0)&Inf(1))|(Fin(2)&Inf(0))").is_rabin_like() -assert b == True -assert len(v) == 2 -assert v[0].fin == [0] -assert v[0].inf == [1] -assert v[1].fin == [2] -assert v[1].inf == [0] +tc.assertTrue(b) +tc.assertEqual(len(v), 2) +tc.assertEqual(v[0].fin, [0]) +tc.assertEqual(v[0].inf, [1]) +tc.assertEqual(v[1].fin, [2]) +tc.assertEqual(v[1].inf, [0]) (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_rabin_like() -assert b == False -assert len(v) == 0 +tc.assertFalse(b) +tc.assertEqual(len(v), 0) (b, v) = spot.acc_cond("(Fin(0)|Inf(1))&(Fin(2)|Inf(0))").is_streett_like() -assert b == True -assert repr(v) == \ - '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))' +tc.assertTrue(b) +tc.assertEqual(repr(v), \ + '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))') v2 = (spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0])) -assert v == v2 +tc.assertEqual(v, v2) acc = spot.acc_cond("generalized-Rabin 1 2") (b, v) = acc.is_generalized_rabin() -assert b == True -assert v == (2,) +tc.assertTrue(b) +tc.assertEqual(v, (2,)) (b, v) = acc.is_generalized_streett() -assert b == False -assert v == () +tc.assertFalse(b) +tc.assertEqual(v, ()) (b, v) = acc.is_streett_like() -assert b == True +tc.assertTrue(b) ve = (spot.rs_pair([0], []), spot.rs_pair([], [1]), spot.rs_pair([], [2])) -assert v == ve -assert acc.name() == "generalized-Rabin 1 2" +tc.assertEqual(v, ve) +tc.assertEqual(acc.name(), "generalized-Rabin 1 2") # At the time of writting, acc_cond does not yet recognize # "generalized-Streett", as there is no definition for that in the HOA format, @@ -74,23 +76,23 @@ assert acc.name() == "generalized-Rabin 1 2" # being a generalized-Streett. See issue #249. acc = spot.acc_cond("Inf(0)|Fin(1)|Fin(2)") (b, v) = acc.is_generalized_streett() -assert b == True -assert v == (2,) +tc.assertTrue(b) +tc.assertEqual(v, (2,)) (b, v) = acc.is_generalized_rabin() -assert b == False -assert v == () +tc.assertFalse(b) +tc.assertEqual(v, ()) # FIXME: We should have a way to disable the following output, as it is not # part of HOA v1. -assert acc.name() == "generalized-Streett 1 2" +tc.assertEqual(acc.name(), "generalized-Streett 1 2") # issue #469. This test is meaningful only if Spot is compiled with # --enable-max-accsets=64 or more. try: m = spot.mark_t([33]) - assert m.lowest() == m + tc.assertEqual(m.lowest(), m) n = spot.mark_t([33,34]) - assert n.lowest() == m + tc.assertEqual(n.lowest(), m) except RuntimeError as e: if "Too many acceptance sets used." in str(e): pass @@ -102,24 +104,24 @@ except RuntimeError as e: from gc import collect acc = spot.translate('a').acc() collect() -assert acc == spot.acc_cond('Inf(0)') +tc.assertEqual(acc, spot.acc_cond('Inf(0)')) acc = spot.translate('b').get_acceptance() collect() -assert acc == spot.acc_code('Inf(0)') +tc.assertEqual(acc, spot.acc_code('Inf(0)')) c = spot.acc_cond('Fin(0)&Fin(1)&(Inf(2)|Fin(3))') m1 = c.fin_unit() m2 = c.inf_unit() -assert m1 == [0,1] -assert m2 == [] +tc.assertEqual(m1, [0,1]) +tc.assertEqual(m2, []) c = spot.acc_cond('Inf(0)&Inf(1)&(Inf(2)|Fin(3))') m1 = c.fin_unit() m2 = c.inf_unit() -assert m1 == [] -assert m2 == [0,1] +tc.assertEqual(m1, []) +tc.assertEqual(m2, [0,1]) c = spot.acc_cond('Inf(0)&Inf(1)|(Inf(2)|Fin(3))') m1 = c.fin_unit() m2 = c.inf_unit() -assert m1 == [] -assert m2 == [] +tc.assertEqual(m1, []) +tc.assertEqual(m2, []) diff --git a/tests/python/setxor.py b/tests/python/setxor.py index 7cd1e5da1..2fe69cd99 100755 --- a/tests/python/setxor.py +++ b/tests/python/setxor.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -# de l'EPITA. +# Copyright (C) 2010, 2011, 2022 Laboratoire de Recherche et +# Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ import sys from buddy import * +from unittest import TestCase +tc = TestCase() bdd_init(10000, 10000) bdd_setvarnum(5) @@ -29,18 +31,18 @@ a = V[0] & -V[1] & V[2] & -V[3] b = V[0] & V[1] & V[2] & -V[3] c = -V[0] & V[1] & -V[2] & -V[3] -assert(c == bdd_setxor(a, b)) -assert(c == bdd_setxor(b, a)) -assert(a == bdd_setxor(b, c)) -assert(a == bdd_setxor(c, b)) -assert(b == bdd_setxor(a, c)) -assert(b == bdd_setxor(c, a)) +tc.assertEqual(c, bdd_setxor(a, b)) +tc.assertEqual(c, bdd_setxor(b, a)) +tc.assertEqual(a, bdd_setxor(b, c)) +tc.assertEqual(a, bdd_setxor(c, b)) +tc.assertEqual(b, bdd_setxor(a, c)) +tc.assertEqual(b, bdd_setxor(c, a)) d = V[1] & V[2] & -V[3] & V[4] e = V[0] & V[1] & -V[2] & -V[3] & V[4] -assert(e == bdd_setxor(a, d)) -assert(e == bdd_setxor(d, a)) +tc.assertEqual(e, bdd_setxor(a, d)) +tc.assertEqual(e, bdd_setxor(d, a)) # Cleanup all BDD variables before calling bdd_done(), otherwise # bdd_delref will be called after bdd_done() and this is unsafe in diff --git a/tests/python/simplacc.py b/tests/python/simplacc.py index e742d69a4..50dc2d74a 100644 --- a/tests/python/simplacc.py +++ b/tests/python/simplacc.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() auts = list(spot.automata(""" @@ -70,19 +72,19 @@ explicit-labels trans-acc deterministic --BODY-- State: 0 [0&!1] 0 {2 3} res = [] for a in auts: b = spot.simplify_acceptance(a) - assert b.equivalent_to(a) + tc.assertTrue(b.equivalent_to(a)) res.append(str(b.get_acceptance())) c = spot.simplify_acceptance(b) - assert b.get_acceptance() == c.get_acceptance() + tc.assertEqual(b.get_acceptance(), c.get_acceptance()) a.set_acceptance(a.num_sets(), a.get_acceptance().complement()) b = spot.simplify_acceptance(a) - assert b.equivalent_to(a) + tc.assertTrue(b.equivalent_to(a)) res.append(str(b.get_acceptance())) c = spot.simplify_acceptance(b) - assert b.get_acceptance() == c.get_acceptance() + tc.assertEqual(b.get_acceptance(), c.get_acceptance()) -assert res == [ +tc.assertEqual(res, [ 'Inf(0)', 'Fin(0)', 'Inf(1) & Fin(0)', @@ -101,4 +103,4 @@ assert res == [ '(Inf(0) | Fin(2)) & Inf(1)', '(Fin(2) & (Inf(1) | Fin(0))) | (Inf(0)&Inf(2))', '(Inf(2) | (Fin(1) & Inf(0))) & (Fin(0)|Fin(2))', - ] + ]) diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 6c2ca8bc3..b0b62267d 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-2021 Laboratoire de Recherche +# Copyright (C) 2015, 2017-2018, 2020-2022 Laboratoire de Recherche # et Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -19,6 +19,8 @@ import spot from sys import exit +from unittest import TestCase +tc = TestCase() # CPython use reference counting, so that automata are destructed # when we expect them to be. However other implementations like @@ -48,7 +50,7 @@ State: 1 """) aut2 = spot.simulation(aut) -assert aut2.to_str() == """HOA: v1 +tc.assertEqual(aut2.to_str(), """HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" @@ -59,10 +61,10 @@ properties: deterministic --BODY-- State: 0 {0} [t] 0 ---END--""" +--END--""") aut2.copy_state_names_from(aut) -assert aut2.to_str() == """HOA: v1 +tc.assertEqual(aut2.to_str(), """HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" @@ -73,7 +75,7 @@ properties: deterministic --BODY-- State: 0 "[0,1]" {0} [t] 0 ---END--""" +--END--""") del aut del aut2 @@ -82,7 +84,7 @@ gcollect() aut = spot.translate('GF((p0 -> Gp0) R p1)') daut = spot.tgba_determinize(aut, True) -assert daut.to_str() == """HOA: v1 +tc.assertEqual(daut.to_str(), """HOA: v1 States: 3 Start: 0 AP: 2 "p1" "p0" @@ -106,7 +108,7 @@ State: 2 "{₀[0]₀}{₁[1]₁}" [!0&1] 2 [0&!1] 0 {0} [0&1] 1 {2} ---END--""" +--END--""") del aut del daut @@ -129,7 +131,7 @@ State: 1 """) daut = spot.tgba_determinize(aut, True) -assert daut.to_str() == """HOA: v1 +tc.assertEqual(daut.to_str(), """HOA: v1 States: 12 Start: 0 AP: 2 "a" "b" @@ -185,18 +187,18 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" [!0&1] 2 {0} [0&!1] 6 {0} [0&1] 9 {0} ---END--""" +--END--""") a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)') a = spot.degeneralize_tba(a) -assert a.num_states() == 8 +tc.assertEqual(a.num_states(), 8) b = spot.simulation(a) -assert b.num_states() == 3 +tc.assertEqual(b.num_states(), 3) b.set_init_state(1) b.purge_unreachable_states() b.copy_state_names_from(a) -assert b.to_str() == """HOA: v1 +tc.assertEqual(b.to_str(), """HOA: v1 States: 1 Start: 0 AP: 2 "p0" "p1" @@ -208,7 +210,7 @@ properties: deterministic stutter-invariant State: 0 "[1,7]" [1] 0 [!1] 0 {0} ---END--""" +--END--""") aut = spot.automaton('''HOA: v1 States: 12 @@ -267,7 +269,7 @@ State: 11 [0&!1] 6 {0} [0&1] 9 {0} --END--''') -assert spot.reduce_iterated(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1 States: 9 Start: 0 AP: 2 "a" "b" @@ -308,7 +310,7 @@ State: 8 [0&!1] 4 {0} [!0&1] 6 [0&1] 7 ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 States: 6 @@ -332,7 +334,7 @@ State: 4 State: 5 [0] 5 --END--''') -assert spot.reduce_iterated(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_iterated(aut).to_str(), '''HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -347,7 +349,7 @@ State: 1 [0] 2 State: 2 [1] 2 ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 States: 5 @@ -374,7 +376,7 @@ State: 4 [0&1&!2&3] 4 {0} --END--''') -assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1 States: 5 Start: 0 AP: 4 "p0" "p2" "p3" "p1" @@ -395,7 +397,7 @@ State: 3 [0&!1&2&3] 3 {1} State: 4 [0&!1&2&3] 4 {0} ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 States: 2 @@ -410,7 +412,7 @@ State: 0 State: 1 [0] 0 --END--''') -assert spot.reduce_direct_sim(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_direct_sim(aut).to_str(), '''HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" @@ -418,7 +420,7 @@ Acceptance: 2 Fin(0) & Fin(1) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 name: "(p1 U p2) U p3" @@ -445,7 +447,7 @@ State: 3 [1] 1 [0&!1] 3 --END--''') -assert spot.reduce_direct_cosim_sba(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_direct_cosim_sba(aut).to_str(), '''HOA: v1 States: 4 Start: 0 AP: 3 "p2" "p3" "p1" @@ -468,7 +470,7 @@ State: 2 State: 3 [0] 1 [!0&2] 3 ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 States: 4 @@ -488,7 +490,7 @@ State: 2 State: 3 {0} [1] 3 --END--''') -assert spot.reduce_direct_cosim(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_direct_cosim(aut).to_str(), '''HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -502,9 +504,9 @@ State: 1 [1] 2 State: 2 {0} [1] 2 ---END--''' +--END--''') -assert spot.reduce_direct_sim_sba(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_direct_sim_sba(aut).to_str(), '''HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -516,7 +518,7 @@ State: 0 [0] 1 State: 1 {0} [1] 1 ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 States: 3 @@ -532,7 +534,7 @@ State: 1 State: 2 {0} [0] 2 --END--''') -assert spot.reduce_iterated_sba(aut).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_iterated_sba(aut).to_str(), '''HOA: v1 States: 1 Start: 0 AP: 1 "a" @@ -542,7 +544,7 @@ properties: deterministic --BODY-- State: 0 {0} [0] 0 ---END--''' +--END--''') aut = spot.automaton('''HOA: v1 States: 30 @@ -630,7 +632,7 @@ State: 28 State: 29 [0&!1&!2&!3] 29 --END--''') -assert spot.reduce_iterated(a).to_str() == '''HOA: v1 +tc.assertEqual(spot.reduce_iterated(a).to_str(), '''HOA: v1 States: 8 Start: 0 AP: 2 "p0" "p1" @@ -669,7 +671,7 @@ State: 7 [!1] 1 {0} [0&1] 5 [1] 7 ---END--''' +--END--''') # issue #452 @@ -707,4 +709,4 @@ State: 8 [@p] 3 {0 1} --END--""") aut = spot.simulation(aut) -assert aut.num_states() == 1 +tc.assertEqual(aut.num_states(), 1) diff --git a/tests/python/sonf.py b/tests/python/sonf.py new file mode 100644 index 000000000..40af758b0 --- /dev/null +++ b/tests/python/sonf.py @@ -0,0 +1,43 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020, 2022 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot +from unittest import TestCase +tc = TestCase() + +formulas = """\ +{x[*]}[]-> F({y[*]}<>-> GFz) +<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17))) +{{true} || {[*0]}}[]-> (false) +{{p14} & {{p0}[*]}}[]-> (p11) +{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18))))) +""" + +for f1 in formulas.splitlines(): + f1 = spot.formula(f1) + a1 = spot.translate(f1) + + f2, aps = spot.suffix_operator_normal_form(f1, 'sonf_') + a2 = spot.translate(f2) + rm = spot.remove_ap() + for ap in aps: + rm.add_ap(ap) + a2 = rm.strip(a2) + + tc.assertTrue(spot.are_equivalent(a1, a2)) diff --git a/tests/python/split.py b/tests/python/split.py index adab5a931..b916f494f 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2021 Laboratoire de Recherche et +# Copyright (C) 2018-2022 Laboratoire de Recherche et # Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -19,6 +19,8 @@ import spot import buddy +from unittest import TestCase +tc = TestCase() # CPython use reference counting, so that automata are destructed # when we expect them to be. However other implementations like @@ -51,16 +53,17 @@ def do_split(f, out_list): return aut, s aut, s = do_split('(FG !a) <-> (GF b)', ['b']) -assert equiv(aut, spot.unsplit_2step(s)) +tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) del aut del s gcollect() aut, s = do_split('GFa && GFb', ['b']) -assert equiv(aut, spot.unsplit_2step(s)) -# FIXME see below -# assert str_diff("""HOA: v1 +tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) +# FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable +# we should investigate this. See Issue #502. +# tc.assertEqual("""HOA: v1 # States: 3 # Start: 0 # AP: 2 "a" "b" @@ -86,10 +89,11 @@ del s gcollect() aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['ack']) -assert equiv(aut, spot.unsplit_2step(s)) +tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) + # FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable -# we should investigate this -# assert s.to_str() == """HOA: v1 +# we should investigate this. See Issue #502. +# tc.assertEqual(s.to_str(), """HOA: v1 # States: 9 # Start: 0 # AP: 4 "ack" "req" "go" "grant" @@ -122,7 +126,7 @@ assert equiv(aut, spot.unsplit_2step(s)) # [!0] 1 # State: 8 {0} # [!3] 2 -# --END--""" +# --END--""") del aut del s @@ -131,4 +135,4 @@ gcollect() aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \ && g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))', ['g_0', 'g_1']) -assert equiv(aut, spot.unsplit_2step(s)) +tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) diff --git a/tests/python/streett_totgba.py b/tests/python/streett_totgba.py index 1c0bfc13e..8a18defbc 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2017-2018, 2021-2022 Laboratoire de Recherche et +# Développement de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -22,7 +22,8 @@ import spot import os import shutil import sys - +from unittest import TestCase +tc = TestCase() def tgba(a): if not a.is_existential(): @@ -33,11 +34,11 @@ def tgba(a): def test_aut(aut): stgba = tgba(aut) - assert stgba.equivalent_to(aut) + tc.assertTrue(stgba.equivalent_to(aut)) os.environ["SPOT_STREETT_CONV_MIN"] = '1' sftgba = tgba(aut) del os.environ["SPOT_STREETT_CONV_MIN"] - assert stgba.equivalent_to(sftgba) + tc.assertTrue(stgba.equivalent_to(sftgba)) slike = spot.simplify_acceptance(aut) @@ -45,8 +46,7 @@ def test_aut(aut): os.environ["SPOT_STREETT_CONV_MIN"] = "1" slftgba = tgba(slike) del os.environ["SPOT_STREETT_CONV_MIN"] - assert sltgba.equivalent_to(slftgba) - + tc.assertTrue(sltgba.equivalent_to(slftgba)) if shutil.which('ltl2dstar') is None: sys.exit(77) diff --git a/tests/python/streett_totgba2.py b/tests/python/streett_totgba2.py index 852eff0af..5ff97a369 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 Laboratoire de Recherche et Développement de -# l'EPITA. +# Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement +# de l'EPITA. # # This file is part of Spot, a model checking library. # @@ -19,6 +19,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() # Issue 316 a = spot.automaton(""" @@ -60,11 +62,11 @@ State: 7 {1 3 4} """) tgba = spot.streett_to_generalized_buchi(a) -assert tgba.acc().is_generalized_buchi() +tc.assertTrue(tgba.acc().is_generalized_buchi()) ba = spot.simplify_acceptance(a) -assert ba.acc().is_buchi() +tc.assertTrue(ba.acc().is_buchi()) nba = spot.dualize(ba.postprocess('generic', 'deterministic')) ntgba = spot.dualize(tgba.postprocess('generic', 'deterministic')) -assert not ba.intersects(ntgba) -assert not tgba.intersects(nba) +tc.assertFalse(ba.intersects(ntgba)) +tc.assertFalse(tgba.intersects(nba)) diff --git a/tests/python/stutter.py b/tests/python/stutter.py index dafb03b7e..05c28fda9 100644 --- a/tests/python/stutter.py +++ b/tests/python/stutter.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019-2021 Laboratoire de Recherche et Développement de +# Copyright (C) 2019-2022 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -23,6 +23,8 @@ import spot +from unittest import TestCase +tc = TestCase() def explain_stut(f): @@ -45,20 +47,20 @@ def explain_stut(f): # Test from issue #388 w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc') -assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}' -assert str(w2) == 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}' +tc.assertEqual(str(w1), 'a & !b & !c; cycle{!a & b & !c}') +tc.assertEqual(str(w2), 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}') # Test from issue #401 w1, w2 = explain_stut('G({x} |-> ({x[+]} <>-> ({Y1[+]} <>=> Y2)))') -assert str(w1) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}' -assert str(w2) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}' +tc.assertEqual(str(w1), 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}') +tc.assertEqual(str(w2), 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}') # Related to issue #401 as well. sl() and sl2() should upgrade # the t acceptance condition into inf(0). pos = spot.translate('Xa & XXb') w = pos.accepting_word().as_automaton() -assert w.acc().is_t() +tc.assertTrue(w.acc().is_t()) a = spot.sl2(w) -assert a.acc().is_buchi() +tc.assertTrue(a.acc().is_buchi()) a = spot.sl(w) -assert a.acc().is_buchi() +tc.assertTrue(a.acc().is_buchi()) diff --git a/tests/python/sum.py b/tests/python/sum.py index 7e2e74220..1f7c6e0a1 100644 --- a/tests/python/sum.py +++ b/tests/python/sum.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017-2019 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et +# Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -20,6 +20,8 @@ import spot import sys import itertools +from unittest import TestCase +tc = TestCase() # make sure that we are not allowed to build the sum of two automata with # different dictionaries. @@ -65,8 +67,8 @@ for p in zip(phi1, phi2): p0orp1 = spot.formula.Or(p) a1ora2 = spot.remove_alternation(spot.sum(a1, a2), True) - assert p0orp1.equivalent_to(a1ora2) + tc.assertTrue(p0orp1.equivalent_to(a1ora2)) p0andp1 = spot.formula.And(p) a1anda2 = spot.remove_alternation(spot.sum_and(a1, a2), True) - assert p0andp1.equivalent_to(a1anda2) + tc.assertTrue(p0andp1.equivalent_to(a1anda2)) diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py index 59022624c..e1a88650a 100644 --- a/tests/python/synthesis.py +++ b/tests/python/synthesis.py @@ -18,6 +18,8 @@ # 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. @@ -25,11 +27,11 @@ for i in range(0, 2): gi = spot.synthesis_info() gi.s = spot.synthesis_info.algo_LAR game = spot.ltl_to_game("(Ga) <-> (Fb)", ["b"], gi) - assert not spot.solve_game(game) + tc.assertFalse(spot.solve_game(game)) # A game can have only inputs game = spot.ltl_to_game("GFa", []) -assert(game.to_str() == """HOA: v1 +tc.assertEqual(game.to_str(), """HOA: v1 States: 3 Start: 0 AP: 1 "a" diff --git a/tests/python/toparity.py b/tests/python/toparity.py index df226ebe4..37e111f9b 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-2021 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -21,6 +21,8 @@ import spot from itertools import zip_longest from buddy import bddfalse +from unittest import TestCase +tc = TestCase() # Tests for the new version of to_parity @@ -114,17 +116,16 @@ def test(aut, expected_num_states=[], full=True): if opt is not None and opt.parity_prefix is False: # Reduce the number of colors to help are_equivalent spot.reduce_parity_here(p1) - assert spot.are_equivalent(aut, p1) + tc.assertTrue(spot.are_equivalent(aut, p1)) if expected_num is not None: - # print(p1.num_states(), expected_num) - assert p1.num_states() == expected_num + tc.assertEqual(p1.num_states(), expected_num) if full and opt is not None: # Make sure passing opt is the same as setting # each argument individually p2 = spot.to_parity(aut, opt) - assert p2.num_states() == p1st - assert p2.num_edges() == p1ed - assert p2.num_sets() == p1se + tc.assertEqual(p2.num_states(), p1st) + tc.assertEqual(p2.num_edges(), p1ed) + tc.assertEqual(p2.num_sets(), p1se) test(spot.automaton("""HOA: v1 name: "(FGp0 & ((XFp0 & F!p1) | F(Gp1 & XG!p0))) | G(F!p0 & (XFp0 | F!p1) & @@ -351,7 +352,7 @@ State: 0 [!0&!1] 0 --END--""") p = spot.to_parity_old(a, True) -assert spot.are_equivalent(a, p) +tc.assertTrue(spot.are_equivalent(a, p)) test(a) a = spot.automaton(""" @@ -363,8 +364,8 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} 4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END-- """) p = spot.to_parity_old(a, True) -assert p.num_states() == 22 -assert spot.are_equivalent(a, p) +tc.assertEqual(p.num_states(), 22) +tc.assertTrue(spot.are_equivalent(a, p)) test(a, [8, 6, 6, 6, 6, 6, 6, 6]) # Force a few edges to false, to make sure to_parity() is OK with that. @@ -377,22 +378,22 @@ for e in a.out(3): e.cond = bddfalse break p = spot.to_parity_old(a, True) -assert p.num_states() == 22 -assert spot.are_equivalent(a, p) +tc.assertEqual(p.num_states(), 22) +tc.assertTrue(spot.are_equivalent(a, p)) test(a, [7, 6, 6, 6, 6, 6, 6, 6]) for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") p = spot.to_parity_old(d, True) - assert spot.are_equivalent(p, d) + tc.assertTrue(spot.are_equivalent(p, d)) for f in spot.randltl(5, 2000): n = spot.translate(f) p = spot.to_parity_old(n, True) - assert spot.are_equivalent(n, p) + tc.assertTrue(spot.are_equivalent(n, p)) # Issue #390. a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) -assert a.equivalent_to(b) +tc.assertTrue(a.equivalent_to(b)) test(a, [7, 7, 3, 7, 7, 7, 3, 3]) diff --git a/tests/python/toweak.py b/tests/python/toweak.py index b2d908037..23dcf66fa 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 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et +# Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() phi1 = """GFb X(!b | GF!a) @@ -33,7 +35,7 @@ b | (a & XF(b R a)) | (!a & XG(!b U !a))""" def test_phi(phi): a = spot.translate(phi, 'GeneralizedBuchi', 'SBAcc') res = spot.to_weak_alternating(spot.dualize(a)) - assert res.equivalent_to(spot.formula.Not(spot.formula(phi))) + tc.assertTrue(res.equivalent_to(spot.formula.Not(spot.formula(phi)))) for p in phi1.split('\n'): @@ -83,4 +85,4 @@ State: 6 --END-- """) a2 = spot.to_weak_alternating(a2) -assert a2.equivalent_to(phi2) +tc.assertTrue(a2.equivalent_to(phi2)) diff --git a/tests/python/tra2tba.py b/tests/python/tra2tba.py index b303c010b..354ced630 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-2021 Laboratoire de Recherche +# Copyright (C) 2016-2018, 2020-2022 Laboratoire de Recherche # et Développement de l'Epita # # This file is part of Spot, a model checking library. @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() # CPython use reference counting, so that automata are destructed # when we expect them to be. However other implementations like @@ -57,7 +59,7 @@ State: 1 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 2. aut = spot.automaton(""" @@ -97,7 +99,7 @@ State: 2 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 3. aut = spot.automaton(""" @@ -128,7 +130,7 @@ State: 0 --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 4. aut = spot.automaton(""" @@ -168,7 +170,7 @@ State: 2 {0} --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 5. aut = spot.automaton(""" @@ -214,7 +216,7 @@ State: 3 {0} --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 6. aut = spot.automaton(""" @@ -257,7 +259,7 @@ State: 2 {0} --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 7. aut = spot.automaton(""" @@ -292,7 +294,7 @@ State: 1 {0} --END--""" res = spot.remove_fin(aut) -assert(res.to_str('hoa') == exp) +tc.assertEqual(res.to_str('hoa'), exp) # Test 8. aut = spot.automaton(""" @@ -372,9 +374,9 @@ State: 7 res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) # Test 9. aut = spot.automaton(""" @@ -411,9 +413,9 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) # Test 10. aut = spot.automaton(""" @@ -453,9 +455,9 @@ State: 2 {0} res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) # Test 11. aut = spot.automaton(""" @@ -493,9 +495,9 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) # Different order for rabin_to_buchi_if_realizable() due to merge_edges() not # being called. This is on purpose: the edge order should match exactly the @@ -518,9 +520,9 @@ State: 1 --END--""" res = spot.rabin_to_buchi_if_realizable(aut) if is_cpython: - assert(res.to_str('hoa') == exp2) + tc.assertEqual(res.to_str('hoa'), exp2) else: - assert(res.equivalent_to(spot.automaton(exp2))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp2))) # Test 12. aut = spot.automaton(""" @@ -565,9 +567,9 @@ State: 3 {0} res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) # Test 13. aut = spot.automaton(""" @@ -615,9 +617,9 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) # rabin_to_buchi_if_realizable() does not call merge_edges() on purpose: the # edge order should match exactly the original automaton. @@ -644,9 +646,9 @@ State: 1 res = spot.rabin_to_buchi_if_realizable(aut) if is_cpython: - assert(res.to_str('hoa') == exp2) + tc.assertEqual(res.to_str('hoa'), exp2) else: - assert(res.equivalent_to(spot.automaton(exp2))) + tc.assertTrue(res.equivalent_to(spot.automaton(exp2))) # Test 14. aut = spot.automaton(""" @@ -681,7 +683,7 @@ State: 1 res = spot.remove_fin(aut) if is_cpython: - assert(res.to_str('hoa') == exp) + tc.assertEqual(res.to_str('hoa'), exp) else: - assert(res.equivalent_to(spot.automaton(exp))) -assert spot.rabin_to_buchi_if_realizable(aut) is None + tc.assertTrue(res.equivalent_to(spot.automaton(exp))) +tc.assertIsNone(spot.rabin_to_buchi_if_realizable(aut)) diff --git a/tests/python/trival.py b/tests/python/trival.py index 8fcf6a1fa..ea844e29c 100644 --- a/tests/python/trival.py +++ b/tests/python/trival.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2018, 2022 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -18,30 +18,32 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() v1 = spot.trival() v2 = spot.trival(False) v3 = spot.trival(True) v4 = spot.trival_maybe() -assert v1 != v2 -assert v1 != v3 -assert v2 != v3 -assert v2 == spot.trival(spot.trival.no_value) -assert v2 != spot.trival(spot.trival.yes_value) -assert v4 != v2 -assert v4 != v3 -assert v2 == False -assert True == v3 -assert v2 != True -assert False != v3 -assert v4 == spot.trival_maybe() -assert v4 == spot.trival(spot.trival.maybe_value) -assert v3 -assert -v2 -assert not -v1 -assert not v1 -assert not -v3 +tc.assertNotEqual(v1, v2) +tc.assertNotEqual(v1, v3) +tc.assertNotEqual(v2, v3) +tc.assertEqual(v2, spot.trival(spot.trival.no_value)) +tc.assertNotEqual(v2, spot.trival(spot.trival.yes_value)) +tc.assertNotEqual(v4, v2) +tc.assertNotEqual(v4, v3) +tc.assertEqual(v2, False) +tc.assertEqual(True, v3) +tc.assertNotEqual(v2, True) +tc.assertNotEqual(False, v3) +tc.assertEqual(v4, spot.trival_maybe()) +tc.assertEqual(v4, spot.trival(spot.trival.maybe_value)) +tc.assertTrue(v3) +tc.assertTrue(-v2) +tc.assertFalse(-v1) +tc.assertFalse(v1) +tc.assertFalse(-v3) for u in (v1, v2, v3): for v in (v1, v2, v3): - assert (u & v) == -(-u | -v) + tc.assertEqual((u & v), -(-u | -v)) diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index b8834b211..1ebcb8ac5 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2021 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2017, 2021-2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -22,6 +22,8 @@ import spot from buddy import bddtrue, bddfalse +from unittest import TestCase +tc = TestCase() aut = spot.make_twa_graph(spot.make_bdd_dict()) @@ -29,98 +31,98 @@ try: print(aut.to_str()) exit(2) except RuntimeError as e: - assert "no state" in str(e) + tc.assertIn("no state", str(e)) try: aut.set_init_state(2) except ValueError as e: - assert "nonexisting" in str(e) + tc.assertIn("nonexisting", str(e)) try: aut.set_univ_init_state([2, 1]) except ValueError as e: - assert "nonexisting" in str(e) + tc.assertIn("nonexisting", str(e)) aut.new_states(3) aut.set_init_state(2) -assert aut.get_init_state_number() == 2 +tc.assertEqual(aut.get_init_state_number(), 2) aut.set_univ_init_state([2, 1]) -assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) +tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number()))) try: aut.get_init_state() except RuntimeError as e: s = str(e) - assert "abstract interface" in s and "alternating automata" in s + tc.assertIn("abstract interface" in s and "alternating automata", s) cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all()) -assert aut.to_str() == cpy.to_str() +tc.assertEqual(aut.to_str(), cpy.to_str()) all = aut.set_buchi() -assert aut.to_str() != cpy.to_str() +tc.assertNotEqual(aut.to_str(), cpy.to_str()) cpy = spot.make_twa_graph(aut, spot.twa_prop_set.all()) aut.new_acc_edge(0, 1, bddtrue, True) -assert aut.num_edges() == 1 + cpy.num_edges() +tc.assertEqual(aut.num_edges(), 1 + cpy.num_edges()) aut.prop_universal(True) aut.set_name("some name") cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False, False, False, False)) -assert cpy.prop_universal() != aut.prop_universal() -assert cpy.prop_universal() == spot.trival.maybe() -assert cpy.get_name() == None +tc.assertNotEqual(cpy.prop_universal(), aut.prop_universal()) +tc.assertEqual(cpy.prop_universal(), spot.trival.maybe()) +tc.assertEqual(cpy.get_name(), None) cpy = spot.make_twa_graph(aut, spot.twa_prop_set(False, False, False, False, False, False), True) -assert cpy.get_name() == "some name" +tc.assertEqual(cpy.get_name(), "some name") from copy import copy cpy = copy(aut) -assert aut.to_str() == cpy.to_str() +tc.assertEqual(aut.to_str(), cpy.to_str()) cpy.set_init_state(1) -assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) -assert cpy.get_init_state_number() == 1 -assert cpy.get_name() == "some name" +tc.assertEqual([2, 1], list(aut.univ_dests(aut.get_init_state_number()))) +tc.assertEqual(cpy.get_init_state_number(), 1) +tc.assertEqual(cpy.get_name(), "some name") try: s = aut.state_acc_sets(0) except RuntimeError as e: - assert "state-based acceptance" in str(e) + tc.assertIn("state-based acceptance", str(e)) try: s = aut.state_is_accepting(0) except RuntimeError as e: - assert "state-based acceptance" in str(e) + tc.assertIn("state-based acceptance", str(e)) aut.prop_state_acc(True) -assert aut.state_acc_sets(0) == all -assert aut.state_is_accepting(0) == True +tc.assertEqual(aut.state_acc_sets(0), all) +tc.assertEqual(aut.state_is_accepting(0), True) aut.set_init_state(0) aut.purge_unreachable_states() i = aut.get_init_state() -assert aut.state_is_accepting(i) == True +tc.assertEqual(aut.state_is_accepting(i), True) it = aut.succ_iter(i) it.first() -assert aut.edge_number(it) == 1 -assert aut.state_number(it.dst()) == 1 -assert aut.edge_storage(it).src == 0 -assert aut.edge_storage(1).src == 0 -assert aut.edge_data(it).cond == bddtrue -assert aut.edge_data(1).cond == bddtrue +tc.assertEqual(aut.edge_number(it), 1) +tc.assertEqual(aut.state_number(it.dst()), 1) +tc.assertEqual(aut.edge_storage(it).src, 0) +tc.assertEqual(aut.edge_storage(1).src, 0) +tc.assertEqual(aut.edge_data(it).cond, bddtrue) +tc.assertEqual(aut.edge_data(1).cond, bddtrue) aut.release_iter(it) aut.purge_dead_states() i = aut.get_init_state() -assert aut.state_is_accepting(i) == False +tc.assertEqual(aut.state_is_accepting(i), False) aut = spot.translate('FGa') # Kill the edge between state 0 and 1 -assert aut.edge_storage(2).src == 0 -assert aut.edge_storage(2).dst == 1 +tc.assertEqual(aut.edge_storage(2).src, 0) +tc.assertEqual(aut.edge_storage(2).dst, 1) aut.edge_data(2).cond = bddfalse -assert aut.num_edges() == 3 -assert aut.num_states() == 2 +tc.assertEqual(aut.num_edges(), 3) +tc.assertEqual(aut.num_states(), 2) aut.purge_dead_states() -assert aut.num_edges() == 1 -assert aut.num_states() == 1 +tc.assertEqual(aut.num_edges(), 1) +tc.assertEqual(aut.num_states(), 1) diff --git a/tests/python/zlktree.py b/tests/python/zlktree.py index df8fd86f0..e1b0c9e7b 100644 --- a/tests/python/zlktree.py +++ b/tests/python/zlktree.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2021, 2022 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -18,6 +18,8 @@ # along with this program. If not, see . import spot +from unittest import TestCase +tc = TestCase() a = spot.automaton("""HOA: v1 States: 5 Start: 0 AP: 2 "p0" "p1" Acceptance: 4 Inf(3) | Fin(3) properties: trans-labels explicit-labels @@ -25,8 +27,8 @@ trans-acc --BODY-- State: 0 [!0&!1] 3 [!0&!1] 4 State: 1 [!0&!1] 4 {3} [0&!1] 0 {2} [!0&1] 1 {2} State: 2 [!0&1] 0 {0 2} [!0&!1] 1 State: 3 [!0&1] 2 State: 4 [0&!1] 3 --END--""") b = spot.zielonka_tree_transform(a) -assert spot.are_equivalent(a, b) -assert b.acc().is_buchi() +tc.assertTrue(spot.are_equivalent(a, b)) +tc.assertTrue(b.acc().is_buchi()) def report_missing_exception(): raise RuntimeError("missing exception") @@ -45,95 +47,96 @@ State: 2 [0&1] 8 {3} [0&1] 2 {1} [!0&1] 4 {3 4} [!0&!1] 3 {2 5} State: [!0&!1] 2 {5} [!0&!1] 0 {3} [!0&!1] 5 --END--""") aa = spot.acd(a) try: - assert aa.has_rabin_shape() + tc.assertTrue(aa.has_rabin_shape()) except RuntimeError as e: - assert 'CHECK_RABIN' in str(e) + tc.assertIn('CHECK_RABIN', str(e)) else: report_missing_exception() try: - assert not aa.has_streett_shape() + tc.assertFalse(aa.has_streett_shape()) except RuntimeError as e: - assert 'CHECK_STREETT' in str(e) + tc.assertIn('CHECK_STREETT', str(e)) else: report_missing_exception() try: - assert not aa.has_parity_shape() + tc.assertFalse(aa.has_parity_shape()) except RuntimeError as e: - assert 'CHECK_PARITY' in str(e) + tc.assertIn('CHECK_PARITY', str(e)) else: report_missing_exception() aa = spot.acd(a, spot.acd_options_CHECK_RABIN) -assert aa.has_rabin_shape() -assert aa.node_count() == 13 +tc.assertTrue(aa.has_rabin_shape()) +tc.assertEqual(aa.node_count(), 13) try: - assert not aa.has_streett_shape() + tc.assertFalse(aa.has_streett_shape()) except RuntimeError as e: - assert 'CHECK_STREETT' in str(e) + tc.assertIn('CHECK_STREETT', str(e)) else: report_missing_exception() try: - assert aa.has_parity_shape() + tc.assertTrue(aa.has_parity_shape()) except RuntimeError as e: - assert 'CHECK_PARITY' in str(e) + tc.assertIn('CHECK_PARITY', str(e)) else: report_missing_exception() aa = spot.acd(a, (spot.acd_options_CHECK_PARITY | spot.acd_options_ABORT_WRONG_SHAPE)) -assert aa.has_rabin_shape() -assert not aa.has_streett_shape() -assert not aa.has_parity_shape() -assert aa.node_count() == 0 +tc.assertTrue(aa.has_rabin_shape()) +tc.assertFalse(aa.has_streett_shape()) +tc.assertFalse(aa.has_parity_shape()) +tc.assertEqual(aa.node_count(), 0) + try: aa.first_branch(0) except RuntimeError as e: - assert 'ABORT_WRONG_SHAPE' in str(e) + tc.assertIn('ABORT_WRONG_SHAPE', str(e)) else: report_missing_exception() try: aa.step(0, 0) except RuntimeError as e: - assert 'incorrect branch number' in str(e) + tc.assertIn('incorrect branch number', str(e)) else: report_missing_exception() try: aa.node_acceptance(0) except RuntimeError as e: - assert 'unknown node' in str(e) + tc.assertIn('unknown node', str(e)) else: report_missing_exception() try: aa.edges_of_node(0) except RuntimeError as e: - assert 'unknown node' in str(e) + tc.assertIn('unknown node', str(e)) else: report_missing_exception() try: aa.node_level(0) except RuntimeError as e: - assert 'unknown node' in str(e) + tc.assertIn('unknown node', str(e)) else: report_missing_exception() a = spot.translate('true') a.set_acceptance(spot.acc_cond('f')) b = spot.acd_transform(a) -assert a.equivalent_to(b) +tc.assertTrue(a.equivalent_to(b)) a = spot.translate('true') a.set_acceptance(spot.acc_cond('f')) b = spot.zielonka_tree_transform(a) -assert a.equivalent_to(b) +tc.assertTrue(a.equivalent_to(b)) a = spot.automaton("""HOA: v1 name: "^ G F p0 G F p1" States: 5 Start: 2 AP: 2 "a" "b" acc-name: Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) | @@ -144,8 +147,8 @@ complete properties: deterministic --BODY-- State: 0 {0} [!0&!1] 0 2} [!0&!1] 1 [0&!1] 4 [!0&1] 3 [0&1] 2 State: 4 {0 3} [!0&!1] 0 [0&!1] 4 [!0&1] 3 [0&1] 2 --END--""") b = spot.acd_transform_sbacc(a, True) -assert str(b.acc()) == '(3, Fin(0) & (Inf(1) | Fin(2)))' -assert a.equivalent_to(b) +tc.assertEqual(str(b.acc()), '(3, Fin(0) & (Inf(1) | Fin(2)))') +tc.assertTrue(a.equivalent_to(b)) b = spot.acd_transform_sbacc(a, False) -assert str(b.acc()) == '(2, Fin(0) & Inf(1))' -assert a.equivalent_to(b) +tc.assertEqual(str(b.acc()), '(2, Fin(0) & Inf(1))') +tc.assertTrue(a.equivalent_to(b)) diff --git a/tests/run.in b/tests/run.in index d14bf52a9..7eaa7732c 100755 --- a/tests/run.in +++ b/tests/run.in @@ -104,18 +104,21 @@ export srcdir case $1 in *.ipynb) - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + PYTHONPATH=$pypath:$PYTHONPATH \ + DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ PYTHONIOENCODING=utf-8:surrogateescape \ exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";; *.py) - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + PYTHONPATH=$pypath:$PYTHONPATH \ + DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ exec $PREFIXCMD @PYTHON@ "$@";; *.test) exec sh -x "$@";; *.pl) exec $PERL "$@";; *python*|*jupyter*|*pypy*) - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ + PYTHONPATH=$pypath:$PYTHONPATH \ + DYLD_LIBRARY_PATH=$modpath:$DYLD_LIBRARY_PATH \ exec $PREFIXCMD "$@";; *) echo "Unknown extension" >&2 diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 8f157014d..85ef359b0 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2022 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -392,6 +392,27 @@ for dir in "${INCDIR-..}" "${INCDIR-..}/../bin" "${INCDIR-..}/../tests"; do done || : # Make sure sh does not abort when read exits with false. done +# Rules for Python tests +for dir in "${INCDIR-..}/../tests"; do + + find "$dir" -name "*.py" -a -type f -a -print | + while read file; do + fail=false + + # Strip comments. + sed 's,[ ]*#.*,,' < $file > $tmp + + $GREP '[ ]$' $tmp && + diag 'Trailing whitespace.' + + $GREP -E '([ ]|^)assert[ (]' $tmp && + diag "replace assert keywords by unittest assertion tests" + + $fail && echo "$file" >>failures.style + done || : # Make sure sh does not abort when read exits with false. +done + + if test -f failures.style; then echo "The following files contain style errors:" cat failures.style