bin: handle thousands of output files

Fixes #534.  Test case is only on next branch.

* bin/common_file.hh, bin/common_file.cc: Make it possible
to reopen a closed file.
* bin/common_output.cc, bin/common_aoutput.cc: Add a heuristic
to decide when to close files.
* NEWS: Mention the issue.
This commit is contained in:
Alexandre Duret-Lutz 2023-07-24 16:56:24 +02:00
parent adca03a30a
commit bd1809f758
5 changed files with 67 additions and 1 deletions

View file

@ -636,7 +636,27 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
auto [it, b] = outputfiles.try_emplace(fname, nullptr);
if (b)
it->second.reset(new output_file(fname.c_str()));
else
// reopen if the file has been closed; see below
it->second->reopen_for_append(fname);
out = &it->second->ostream();
// If we have opened fewer than 10 files, we keep them all open
// to avoid wasting time on open/close calls.
//
// However we cannot keep all files open, especially in
// scenarios were we use thousands of files only once. To keep
// things simple, we only close the previous file if it is not
// the current output. This way we still save the close/open
// cost when consecutive automata are sent to the same file.
static output_file* previous = nullptr;
static const std::string* previous_name = nullptr;
if (previous
&& outputfiles.size() > 10
&& &previous->ostream() != out)
previous->close(*previous_name);
previous = it->second.get();
previous_name = &it->first;
}
// Output it.