diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 7500274a2b98e039db46d9333d91586bbfeed5b7..78a38c197f1be4519070cdfe48243746ceb295d6 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -737,6 +737,26 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) { + if (aut_i->num_sets() + aut_j->num_sets() + > 8 * sizeof(spot::acc_cond::mark_t::value_t)) + { + // Report the skipped test if both automata are not + // complemented, or the --verbose option is used, + if (!verbose && (icomp || jcomp)) + return false; + std::cerr << "info: building "; + if (icomp) + std::cerr << "Comp(N" << i << ')'; + else + std::cerr << 'P' << i; + if (jcomp) + std::cerr << "*Comp(P" << j << ')'; + else + std::cerr << "*N" << j; + std::cerr << " requires more acceptance sets than supported\n"; + return false; + } + auto prod = spot::product(aut_i, aut_j); if (verbose) diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index bf8fdba51febe35b67207938745fc2c3d98d6bf4..6f97d3f20016624fdb88772459f4ac4764154d11 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -215,6 +215,7 @@ TESTS_twa = \ dra2dba.test \ unambig.test \ ltlcross4.test \ + ltl3dra.test \ ltl2dstar.test \ ltl2dstar2.test \ ltl2dstar3.test \ diff --git a/src/tests/ltl3dra.test b/src/tests/ltl3dra.test new file mode 100755 index 0000000000000000000000000000000000000000..a1a8ad3216c7749e779b28e15f20eb0a1f40a710 --- /dev/null +++ b/src/tests/ltl3dra.test @@ -0,0 +1,37 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 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 . + +# Do some quick translations to make sure the neverclaims produced by +# spot actually look correct! We do that by parsing them via ltlcross. +# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed. + +. ./defs +set -e + +# Skip this test if ltl3dra is not installed. +(ltl3dra -v) || exit 77 + +# This used to crash ltlcross because the number of +# acceptance sets generated was to high. +../../bin/ltlcross '../../bin/ltl2tgba' 'ltl3dra' -f '(<>((((p0) && +(!(<>(p2)))) || ((!(p0)) && (<>(p2)))) U ((<>(((p0) && (!([](((!(p1)) +&& ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1)) +&& ([](p3))) || ((p1) && (!([](p3))))))))) && (((p0) && (!(<>(p2)))) +|| ((!(p0)) && (<>(p2)))))))'