alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: do not use remove_fin anymore

Browse source 
* bin/ltlcross.cc: Since is_empty() now works with arbitrary
acceptance conditions, calling remove_fin() is not necessary anymore.
* tests/core/ltlcrossce.test: Adjust.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-09 14:55:51 +01:00
parent addaf7f5b0
commit 4e99518da7
3 changed files with 35 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -21,6 +21,10 @@ New in spot 2.8.6.dev (not yet released)
conjunctions of Inf, or disjunction of Fin that appears in
arbitrary conditions.
- ltlcross is now using the generic emptiness check procedure
introduced in Spot 2.7, as opposed to removing Fin acceptance
before using a classical emptiness check.
- ltlcross learned a --save-inclusion-products=FILENAME option. Its
use cases are probably quite limited. We use that to generate
benchmarks for our generic emptiness check procedure.

89
bin/ltlcross.cc
View file

@ -1264,6 +1264,33 @@ namespace
unalt(neg, i, 'N');
}
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
const char* prefix, const char* suffix)
{
if (!x[i])
return;
unsigned before = x[i]->num_sets();
cleanup_acceptance_here(x[i]);
unsigned after = x[i]->num_sets();
if (verbose && before != after)
{
if (print_first)
{
std::cerr << "info: removing unused sets...\n";
print_first = false;
}
std::cerr << "info: " << prefix << i
<< suffix << '\t' << before << " sets -> "
<< after << " sets\n";
}
};
for (size_t i = 0; i < m; ++i)
{
tmp(pos, i, " P", " ");
tmp(neg, i, " N", " ");
}
// Complement
if (!no_complement)
{
@ -1324,67 +1351,11 @@ namespace
}
}
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
const char* prefix, const char* suffix)
{
if (!x[i])
return;
if (x[i]->acc().uses_fin_acceptance())
{
if (verbose)
{
if (print_first)
{
std::cerr <<
"info: getting rid of any Fin acceptance...\n";
print_first = false;
}
std::cerr << "info:\t" << prefix << i
<< suffix << "\t(";
printsize(x[i]);
std::cerr << ") ->";
}
try
{
x[i] = remove_fin(x[i]);
}
catch (const std::runtime_error& err)
{
if (verbose)
std::cerr << " failed (" << err.what() << ")\n";
else
std::cerr << "info: preprocessing "
<< prefix << i << suffix
<< " failed (" << err.what() << ")\n";
x[i] = nullptr;
}
if (verbose && x[i])
{
std::cerr << " (";
printsize(x[i]);
std::cerr << ")\n";
}
}
else
{
// Remove useless sets nonetheless.
cleanup_acceptance_here(x[i]);
}
};
for (size_t i = 0; i < m; ++i)
{
tmp(pos, i, " P", " ");
tmp(neg, i, " N", " ");
tmp(comp_pos, i, "Comp(P", ")");
tmp(comp_neg, i, "Comp(N", ")");
}
if (smallest_pos_ref >= 0)
{
// Recompute the smallest references now, because removing
// alternation and Fin acceptance might have changed the
// sizes.
// Recompute the smallest references now, because
// removing alternation and useless acceptance sets
// might have changed the sizes.
smallest_pos_ref = smallest_ref(pos);
smallest_neg_ref = smallest_ref(neg);

3
tests/core/ltlcrossce.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013, 2016, 2019 Laboratoire de Recherche et
# Copyright (C) 2013, 2016, 2019, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -95,7 +95,6 @@ test `grep '^error:' errors | wc -l` = 4
run 1 ltlcross --verbose -D -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \
"ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
cat errors
test `grep 'info: Comp(' errors | wc -l` = 3
grep 'error: P0\*N1 is nonempty' errors
grep 'error: P1\*N0 is nonempty' errors
grep 'error: P1\*N1 is nonempty' errors