Commit d12b2cd5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

honor SPOT_BDD_TRACE

* spot/priv/bddalloc.cc: Add hooks on request.
* bin/man/spot-x.x, NEWS: Document the envvar.
parent 361b44e5
......@@ -150,6 +150,10 @@ New in spot 2.3.5.dev (not yet released)
- spot::sbacc() is now able to work on alternating automata.
- If the SPOT_BDD_TRACE envorinment variable is set, statistics
about BDD garbage collection and table resizing are shown.
Python:
- The 'spot.gen' package exports the functions from libspotgen.
......
......@@ -39,6 +39,11 @@ This naive method tries to reduce the size of the automaton one state at a
time. Note that it restarts all the encoding each time.
[ENVIRONMENT VARIABLES]
.TP
\fBSPOT_BDD_TRACE\fR
If this variable is set to any value, statistics about BDD garbage
collection and resizing will be output on standard error.
.TP
\fBSPOT_DEFAULT_FORMAT\fR
Set to a value of \fBdot\fR or \fBhoa\fR to override the default
......
// -*- coding: utf-8 -*-
// Copyright (C) 2007, 2011, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2007, 2011, 2014, 2015, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
......@@ -22,6 +22,8 @@
#include <bddx.h>
#include <cassert>
#include <cstdlib>
#include <ctime>
#include "spot/priv/bddalloc.hh"
namespace spot
......@@ -29,6 +31,37 @@ namespace spot
bool bdd_allocator::initialized = false;
static void show_bdd_stats()
{
bddStat s;
bdd_stats(&s);
std::cerr << "spot: BDD stats: produced=" << s.produced
<< " nodenum=" << s.nodenum
<< " freenodes=" << s.freenodes
<< " (" << (s.freenodes * 100 / s.nodenum)
<< "%) minfreenodes=" << s.minfreenodes
<< "% varnum=" << s.varnum
<< " cachesize=" << s.cachesize
<< " hashsize=" << s.hashsize
<< " gbcnum=" << s.gbcnum
<< '\n';
}
static void resize_handler(int oldsize, int newsize)
{
std::cerr << "spot: BDD resize "
<< oldsize << " -> " << newsize << '\n';
}
static void gbc_handler(int pre, bddGbcStat *s)
{
if (!pre)
std::cerr << "spot: BDD GC #" << s->num
<< " in " << ((float)s->time)/CLOCKS_PER_SEC << "s / "
<< ((float)s->sumtime)/CLOCKS_PER_SEC << "s total\n";
show_bdd_stats();
}
bdd_allocator::bdd_allocator()
{
initialize();
......@@ -49,14 +82,25 @@ namespace spot
// the library is solving. It would be nice to allow users
// to tune this. By the meantime, we take the typical values
// for large examples advocated by the BuDDy manual.
bdd_init(1000000, 10000);
bdd_init(1 << 19, 2);
bdd_setcacheratio(40);
bdd_setvarnum(2);
// When the node table is full, add 2**19 nodes; this requires 10MB.
bdd_setmaxincrease(1 << 19);
// Disable the default GC handler. (Note that this will only be
// done if Buddy is initialized by Spot. Otherwise we prefer not
// to overwrite a handler that might have been set by the user.)
bdd_gbc_hook(nullptr);
// When the node time is full, add 500000 nodes, i.e., 10MB.
bdd_setmaxincrease(500000);
if (getenv("SPOT_BDD_TRACE"))
{
bdd_gbc_hook(gbc_handler);
bdd_resize_hook(resize_handler);
std::cerr << "spot: BDD package initialized\n";
show_bdd_stats();
}
else
{
bdd_gbc_hook(nullptr);
}
}
void
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment