statistic.hpp

Go to the documentation of this file.

/****************************************************************************/
/*                                                                          */
/* This file is part of libDDD, a library for manipulation of DDD and SDD.  */
/*                                                                          */
/*     Copyright (C) 2001-2008 Yann Thierry-Mieg, Jean-Michel Couvreur      */
/*                             and Denis Poitrenaud                         */
/*                                                                          */
/*     This program is free software; you can redistribute it and/or modify */
/*     it under the terms of the GNU Lesser General Public License as       */
/*     published by the Free Software Foundation; either version 3 of the   */
/*     License, or (at your option) any later version.                      */
/*     This program 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 LEsserGeneral Public License for more details.                   */
/*                                                                          */
/* You should have received a copy of the GNU Lesser General Public License */
/*     along with this program; if not, write to the Free Software          */
/*Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA */
/*                                                                          */
/****************************************************************************/
 
#include <iostream>
#include <string>
#include "ddd/SDD.h"
#include "ddd/DDD.h"
 
 
 
typedef enum {CSV, LATEX} OutputType;
 
class Statistic {
        long double nb_Stat;
        long double DDD_size;
        long double SDD_size;
        long double DDD_peak_size;
        long double SDD_peak_size;
        double total_time;
        size_t memory;
        double nbHom;
        double nbShom;
        double ddd_cache;
        double sdd_cache;
        bool isPureDDD;
        OutputType style;
        std::string stat_name;
 
        size_t shom_cache;
 
        bool show_peak;
        void load (const SDD & s);
        void load (const DDD & s);
public:
 
  Statistic (const SDD & s, const std::string & name, OutputType style=LATEX, bool show_peak = true);
  Statistic (const DDD & s, const std::string & name, OutputType style=LATEX, bool show_peak = true);
 
  void print_header (std::ostream & os);
 
  void print_trailer (std::ostream & os, bool withLegend=true);
 
  void print_line (std::ostream &os);
 
  void print_table (std::ostream & os);
 
  void print_legend (std::ostream & os);
 
  void setStyle (OutputType style);
 
  double getTime() const { return total_time; }
  long double getNbStates () const { return nb_Stat; }
  
};