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

Add option -k to ltl2tgba

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2008-12-05 11:21:38 +01:00
parent d1ca1e31aa
commit d5235c6901
4 changed files with 30 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2008-12-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbatest/ltl2tgba.cc (-k): New option that calls
stats_reachable(a).dump().
* src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh:
Add tgba_statistics::dump().
2008-08-29 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* bench/gspn-ssp/tools/modelgen-create: Remove and fold into ...

11
src/tgbaalgos/stats.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -19,6 +19,7 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <iostream>
#include "tgba/tgba.hh"
#include "stats.hh"
#include "reachiter.hh"
@ -53,6 +54,14 @@ namespace spot
};
} // anonymous
std::ostream& tgba_statistics::dump(std::ostream& out) const
{
out << "transitions: " << transitions << std::endl;
out << "states: " << states << std::endl;
return out;
}
tgba_statistics
stats_reachable(const tgba* g)
{

5
src/tgbaalgos/stats.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2004, 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -23,6 +23,7 @@
# define SPOT_TGBAALGOS_STATS_HH
#include "tgba/tgba.hh"
#include <iosfwd>
namespace spot
{
@ -34,6 +35,8 @@ namespace spot
{
unsigned transitions;
unsigned states;
std::ostream& dump(std::ostream& out) const;
};
/// \brief Compute statistics for an automaton.

9
src/tgbatest/ltl2tgba.cc
View file

@ -89,6 +89,8 @@ syntax(char* prog)
<< std::endl
<< " -G graph the accepting run seen as an automaton "
<< " (requires -e)" << std::endl
<< " -k display statistics on the TGBA instead of dumping it"
<< std::endl
<< " -L fair-loop approximation (implies -f)" << std::endl
<< " -m try to reduce accepting runs, in a second pass"
<< std::endl
@ -318,6 +320,10 @@ main(int argc, char** argv)
{
graph_run_tgba_opt = true;
}
else if (!strcmp(argv[formula_index], "-k"))
{
output = 9;
}
else if (!strcmp(argv[formula_index], "-L"))
{
fair_loop_approx = true;
@ -723,6 +729,9 @@ main(int argc, char** argv)
spot::never_claim_reachable(std::cout, s, f);
break;
}
case 9:
stats_reachable(a).dump(std::cout);
break;
default:
assert(!"unknown output option");
}