Factor the %-formating machinery.
* src/misc/formater.hh: New file. * src/misc/Makefile.am: Add it. * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: Use it.
This commit is contained in:
Alexandre Duret-Lutz
parent
62af20d39f
commit
a303c8603c
4 changed files with 256 additions and 120 deletions
|
|
@ -1,4 +1,4 @@
|
|||
## Copyright (C) 2011 Laboratoire de Recherche et Développement
|
||||
## Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
|
||||
## de l'Epita (LRDE).
|
||||
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
|
|
@ -37,6 +37,7 @@ misc_HEADERS = \
|
|||
casts.hh \
|
||||
escape.hh \
|
||||
fixpool.hh \
|
||||
formater.hh \
|
||||
freelist.hh \
|
||||
hash.hh \
|
||||
hashfunc.hh \
|
||||
|
|
|
|||
195
src/misc/formater.hh
Normal file
195
src/misc/formater.hh
Normal file
|
|
@ -0,0 +1,195 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012 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 2 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 Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#ifndef SPOT_SRC_MISC_FORMATER_HH
|
||||
#define SPOT_SRC_MISC_FORMATER_HH
|
||||
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
#include <vector>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class printable
|
||||
{
|
||||
public:
|
||||
~printable()
|
||||
{
|
||||
}
|
||||
virtual void
|
||||
print(std::ostream&, const char*) const = 0;
|
||||
};
|
||||
|
||||
|
||||
template <class T>
|
||||
class printable_value: public printable
|
||||
{
|
||||
protected:
|
||||
T val_;
|
||||
public:
|
||||
operator T() const
|
||||
{
|
||||
return val_;
|
||||
}
|
||||
|
||||
printable_value&
|
||||
operator=(const T& new_val)
|
||||
{
|
||||
val_ = new_val;
|
||||
return *this;
|
||||
}
|
||||
|
||||
virtual void
|
||||
print(std::ostream& os, const char*) const
|
||||
{
|
||||
os << val_;
|
||||
}
|
||||
};
|
||||
|
||||
/// The default callback simply writes "%c".
|
||||
class printable_id: public printable
|
||||
{
|
||||
public:
|
||||
virtual void
|
||||
print(std::ostream& os, const char* x) const
|
||||
{
|
||||
os << '%' << *x;
|
||||
}
|
||||
};
|
||||
|
||||
/// Called by default for "%%" and "%\0".
|
||||
class printable_percent: public printable
|
||||
{
|
||||
public:
|
||||
virtual void
|
||||
print(std::ostream& os, const char*) const
|
||||
{
|
||||
os << '%';
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
class formater
|
||||
{
|
||||
printable_id id;
|
||||
printable_percent percent;
|
||||
public:
|
||||
|
||||
formater()
|
||||
: has_(256), call_(256, &id)
|
||||
{
|
||||
call_['%'] = call_[0] = &percent;
|
||||
}
|
||||
|
||||
/// Collect the %-sequences occurring in \a fmt.
|
||||
void
|
||||
prime(const char* fmt)
|
||||
{
|
||||
for (const char* pos = fmt; *pos; ++pos)
|
||||
if (*pos == '%')
|
||||
{
|
||||
char c = *++pos;
|
||||
has_[c] = true;
|
||||
if (!c)
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
/// Collect the %-sequences occurring in \a fmt.
|
||||
void
|
||||
prime(const std::string& fmt)
|
||||
{
|
||||
prime(fmt.c_str());
|
||||
}
|
||||
|
||||
/// Whether %c occurred in the primed formats.
|
||||
bool
|
||||
has(char c) const
|
||||
{
|
||||
return has_[c];
|
||||
}
|
||||
|
||||
/// Declare a callback function for %c.
|
||||
void
|
||||
declare(char c, const printable* f)
|
||||
{
|
||||
call_[c] = f;
|
||||
}
|
||||
|
||||
/// Remember where to output any string.
|
||||
void
|
||||
set_output(std::ostream& output)
|
||||
{
|
||||
output_ = &output;
|
||||
}
|
||||
|
||||
/// Expand the %-sequences in \a fmt, write the result on \a output_.
|
||||
std::ostream&
|
||||
format(const char* fmt)
|
||||
{
|
||||
for (const char* pos = fmt; *pos; ++pos)
|
||||
if (*pos != '%')
|
||||
{
|
||||
*output_ << *pos;
|
||||
}
|
||||
else
|
||||
{
|
||||
char c = *++pos;
|
||||
call_[c]->print(*output_, pos);
|
||||
if (!c)
|
||||
break;
|
||||
}
|
||||
return *output_;
|
||||
}
|
||||
|
||||
/// Expand the %-sequences in \a fmt, write the result on \a output.
|
||||
std::ostream&
|
||||
format(std::ostream& output, const char* fmt)
|
||||
{
|
||||
set_output(output);
|
||||
return format(fmt);
|
||||
}
|
||||
|
||||
/// Expand the %-sequences in \a fmt, write the result on \a output_.
|
||||
std::ostream&
|
||||
format(const std::string& fmt)
|
||||
{
|
||||
return format(fmt.c_str());
|
||||
}
|
||||
|
||||
/// Expand the %-sequences in \a fmt, write the result on \a output.
|
||||
std::ostream&
|
||||
format(std::ostream& output, const std::string& fmt)
|
||||
{
|
||||
return format(output, fmt.c_str());
|
||||
}
|
||||
|
||||
private:
|
||||
std::vector<bool> has_;
|
||||
std::vector<const printable*> call_;
|
||||
protected:
|
||||
std::ostream* output_;
|
||||
const char* pos_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_SRC_MISC_FORMATER_HH
|
||||
|
|
@ -133,151 +133,68 @@ namespace spot
|
|||
return s;
|
||||
}
|
||||
|
||||
namespace
|
||||
void printable_formula::print(std::ostream& os, const char*) const
|
||||
{
|
||||
enum what {
|
||||
Formula = 1, // %f
|
||||
States = 2, // %s
|
||||
Edges = 4, // %e
|
||||
Trans = 8, // %t
|
||||
Acc = 16, // %a
|
||||
Scc = 32, // %S
|
||||
Nondetstates = 64, // %n
|
||||
Deterministic = 128 // %d
|
||||
};
|
||||
}
|
||||
ltl::to_string(val_, os);
|
||||
};
|
||||
|
||||
stat_printer::stat_printer(std::ostream& os, const char* format)
|
||||
: os_(os), format_(format)
|
||||
: format_(format)
|
||||
{
|
||||
needed_ = 0;
|
||||
// scan the format for needed statistics
|
||||
for (const char* pos = format; *pos; ++pos)
|
||||
if (*pos == '%')
|
||||
{
|
||||
switch (*++pos)
|
||||
{
|
||||
case 'f':
|
||||
needed_ |= Formula;
|
||||
break;
|
||||
case 's':
|
||||
needed_ |= States;
|
||||
break;
|
||||
case 'e':
|
||||
needed_ |= Edges;
|
||||
break;
|
||||
case 't':
|
||||
needed_ |= Trans;
|
||||
break;
|
||||
case 'a':
|
||||
needed_ |= Acc;
|
||||
break;
|
||||
case 'S':
|
||||
needed_ |= Scc;
|
||||
break;
|
||||
case 'n':
|
||||
needed_ |= Nondetstates;
|
||||
break;
|
||||
case 'd':
|
||||
needed_ |= Deterministic;
|
||||
break;
|
||||
case '%':
|
||||
break;
|
||||
case 0:
|
||||
--pos;
|
||||
break;
|
||||
}
|
||||
}
|
||||
declare('a', &acc_);
|
||||
declare('d', &deterministic_);
|
||||
declare('e', &edges_);
|
||||
declare('f', &form_);
|
||||
declare('n', &nondetstates_);
|
||||
declare('s', &states_);
|
||||
declare('S', &scc_);
|
||||
declare('t', &trans_);
|
||||
set_output(os);
|
||||
prime(format);
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
stat_printer::print(const tgba* aut,
|
||||
const ltl::formula* f)
|
||||
{
|
||||
unsigned states = 0;
|
||||
unsigned edges = 0;
|
||||
unsigned trans = 0;
|
||||
unsigned acc = 0;
|
||||
unsigned scc = 0;
|
||||
unsigned nondetstates = 0;
|
||||
unsigned deterministic = 0;
|
||||
form_ = f;
|
||||
|
||||
if (needed_ & Trans)
|
||||
if (has('t'))
|
||||
{
|
||||
tgba_sub_statistics s = sub_stats_reachable(aut);
|
||||
states = s.states;
|
||||
edges = s.transitions;
|
||||
trans = s.sub_transitions;
|
||||
states_ = s.states;
|
||||
edges_ = s.transitions;
|
||||
trans_ = s.sub_transitions;
|
||||
}
|
||||
else if (needed_ & (States | Edges))
|
||||
else if (has('s') || has('e'))
|
||||
{
|
||||
tgba_sub_statistics s = sub_stats_reachable(aut);
|
||||
states = s.states;
|
||||
edges = s.transitions;
|
||||
states_ = s.states;
|
||||
edges_ = s.transitions;
|
||||
}
|
||||
if (needed_ & Acc)
|
||||
acc = aut->number_of_acceptance_conditions();
|
||||
|
||||
if (needed_ & Scc)
|
||||
if (has('a'))
|
||||
acc_ = aut->number_of_acceptance_conditions();
|
||||
|
||||
if (has('S'))
|
||||
{
|
||||
scc_map m(aut);
|
||||
m.build_map();
|
||||
scc = m.scc_count();
|
||||
scc_ = m.scc_count();
|
||||
}
|
||||
|
||||
if (needed_ & Nondetstates)
|
||||
if (has('n'))
|
||||
{
|
||||
nondetstates = count_nondet_states(aut);
|
||||
deterministic = (nondetstates == 0);
|
||||
nondetstates_ = count_nondet_states(aut);
|
||||
deterministic_ = (nondetstates_ == 0);
|
||||
}
|
||||
else if (needed_ & Deterministic)
|
||||
else if (has('d'))
|
||||
{
|
||||
// This is more efficient than calling count_nondet_state().
|
||||
deterministic = is_deterministic(aut);
|
||||
deterministic_ = is_deterministic(aut);
|
||||
}
|
||||
|
||||
for (const char* format = format_; *format; ++format)
|
||||
if (*format != '%')
|
||||
os_ << *format;
|
||||
else
|
||||
switch (*++format)
|
||||
{
|
||||
case 'a':
|
||||
os_ << acc;
|
||||
break;
|
||||
case 'e':
|
||||
os_ << edges;
|
||||
break;
|
||||
case 'f':
|
||||
assert(f);
|
||||
ltl::to_string(f, os_);
|
||||
break;
|
||||
case 'd':
|
||||
os_ << deterministic;
|
||||
break;
|
||||
case 'n':
|
||||
os_ << nondetstates;
|
||||
break;
|
||||
case 's':
|
||||
os_ << states;
|
||||
break;
|
||||
case 'S':
|
||||
os_ << scc;
|
||||
break;
|
||||
case 't':
|
||||
os_ << trans;
|
||||
break;
|
||||
case 0:
|
||||
--format;
|
||||
// fall through
|
||||
case '%':
|
||||
os_ << '%';
|
||||
break;
|
||||
default:
|
||||
os_ << '%' << *format;
|
||||
break;
|
||||
}
|
||||
return os_;
|
||||
return format(format_);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@
|
|||
|
||||
#include "tgba/tgba.hh"
|
||||
#include <iosfwd>
|
||||
#include "misc/formater.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -53,12 +54,27 @@ namespace spot
|
|||
/// \brief Compute subended statistics for an automaton.
|
||||
tgba_sub_statistics sub_stats_reachable(const tgba* g);
|
||||
|
||||
|
||||
class printable_formula: public printable_value<const ltl::formula*>
|
||||
{
|
||||
public:
|
||||
printable_formula&
|
||||
operator=(const ltl::formula* new_val)
|
||||
{
|
||||
val_ = new_val;
|
||||
return *this;
|
||||
}
|
||||
|
||||
virtual void
|
||||
print(std::ostream& os, const char*) const;
|
||||
};
|
||||
|
||||
/// \brief prints various statistics about a TGBA
|
||||
///
|
||||
/// This object can be configured to display various statistics
|
||||
/// about a TGBA. Some %-sequence of characters are interpreted in
|
||||
/// the format string, and replaced by the corresponding statistics.
|
||||
class stat_printer
|
||||
class stat_printer: protected formater
|
||||
{
|
||||
public:
|
||||
stat_printer(std::ostream& os, const char* format);
|
||||
|
|
@ -71,9 +87,16 @@ namespace spot
|
|||
print(const tgba* aut, const ltl::formula* f = 0);
|
||||
|
||||
private:
|
||||
std::ostream& os_;
|
||||
const char* format_;
|
||||
unsigned needed_;
|
||||
|
||||
printable_formula form_;
|
||||
printable_value<unsigned> states_;
|
||||
printable_value<unsigned> edges_;
|
||||
printable_value<unsigned> trans_;
|
||||
printable_value<unsigned> acc_;
|
||||
printable_value<unsigned> scc_;
|
||||
printable_value<unsigned> nondetstates_;
|
||||
printable_value<unsigned> deterministic_;
|
||||
};
|
||||
|
||||
/// @}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue