stats: preparatory change of the implementation of %c
This now holds the scc_info while processing the %c sequence, so that using options we will soon be able to specify which SCC to count. * spot/twaalgos/stats.hh, spot/twaalgos/stats.cc (printable_scc_info): New class. (state_printer): Use it for %c. * spot/misc/formater.hh: Add move assignment. * bin/common_aoutput.hh, bin/common_aoutput.cc: Use printable_scc_info for %C. * tests/core/format.test: Add a quick test case to make sure nothing changed.
This commit is contained in:
parent
70de1328d8
commit
4f0a630dbc
6 changed files with 47 additions and 5 deletions
|
|
@ -406,7 +406,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
|
||||||
haut_acc_ = haut->aut->acc().num_sets();
|
haut_acc_ = haut->aut->acc().num_sets();
|
||||||
|
|
||||||
if (has('C'))
|
if (has('C'))
|
||||||
haut_scc_ = spot::scc_info(haut->aut).scc_count();
|
haut_scc_.automaton(haut->aut);
|
||||||
|
|
||||||
if (has('N'))
|
if (has('N'))
|
||||||
{
|
{
|
||||||
|
|
@ -471,6 +471,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
|
||||||
// automata are built.
|
// automata are built.
|
||||||
output_aut_ = nullptr;
|
output_aut_ = nullptr;
|
||||||
input_aut_ = nullptr;
|
input_aut_ = nullptr;
|
||||||
|
haut_scc_.reset();
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -111,7 +111,7 @@ private:
|
||||||
spot::printable_value<unsigned> haut_edges_;
|
spot::printable_value<unsigned> haut_edges_;
|
||||||
spot::printable_value<unsigned> haut_trans_;
|
spot::printable_value<unsigned> haut_trans_;
|
||||||
spot::printable_value<unsigned> haut_acc_;
|
spot::printable_value<unsigned> haut_acc_;
|
||||||
spot::printable_value<unsigned> haut_scc_;
|
spot::printable_scc_info haut_scc_;
|
||||||
spot::printable_value<unsigned> haut_deterministic_;
|
spot::printable_value<unsigned> haut_deterministic_;
|
||||||
spot::printable_value<unsigned> haut_nondetstates_;
|
spot::printable_value<unsigned> haut_nondetstates_;
|
||||||
spot::printable_value<unsigned> haut_complete_;
|
spot::printable_value<unsigned> haut_complete_;
|
||||||
|
|
|
||||||
|
|
@ -71,6 +71,13 @@ namespace spot
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
printable_value&
|
||||||
|
operator=(T&& new_val)
|
||||||
|
{
|
||||||
|
val_ = std::move(new_val);
|
||||||
|
return *this;
|
||||||
|
}
|
||||||
|
|
||||||
virtual void
|
virtual void
|
||||||
print(std::ostream& os, const char*) const override
|
print(std::ostream& os, const char*) const override
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -123,6 +123,12 @@ namespace spot
|
||||||
print_psl(os, val_);
|
print_psl(os, val_);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
void printable_scc_info::print(std::ostream& os, const char*) const
|
||||||
|
{
|
||||||
|
os << val_->scc_count();
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
stat_printer::stat_printer(std::ostream& os, const char* format)
|
stat_printer::stat_printer(std::ostream& os, const char* format)
|
||||||
: format_(format)
|
: format_(format)
|
||||||
{
|
{
|
||||||
|
|
@ -167,8 +173,12 @@ namespace spot
|
||||||
if (has('a'))
|
if (has('a'))
|
||||||
acc_ = aut->num_sets();
|
acc_ = aut->num_sets();
|
||||||
|
|
||||||
|
// %S was renamed to %c in Spot 1.2, so that autfilt could use %S
|
||||||
|
// and %s to designate the state numbers in input and output
|
||||||
|
// automate. We still recognize %S an obsolete and undocumented
|
||||||
|
// alias for %c, if it is not overridden by a subclass.
|
||||||
if (has('c') || has('S'))
|
if (has('c') || has('S'))
|
||||||
scc_ = scc_info(aut).scc_count();
|
scc_.automaton(aut);
|
||||||
|
|
||||||
if (has('n'))
|
if (has('n'))
|
||||||
{
|
{
|
||||||
|
|
@ -193,7 +203,9 @@ namespace spot
|
||||||
gen_acc_ = os.str();
|
gen_acc_ = os.str();
|
||||||
}
|
}
|
||||||
|
|
||||||
return format(format_);
|
auto& os = format(format_);
|
||||||
|
scc_.reset(); // Make sure we do not hold a pointer to the automaton
|
||||||
|
return os;
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -23,6 +23,7 @@
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
||||||
#include <spot/twa/twa.hh>
|
#include <spot/twa/twa.hh>
|
||||||
|
#include <spot/twaalgos/sccinfo.hh>
|
||||||
#include <iosfwd>
|
#include <iosfwd>
|
||||||
#include <spot/misc/formater.hh>
|
#include <spot/misc/formater.hh>
|
||||||
|
|
||||||
|
|
@ -69,6 +70,24 @@ namespace spot
|
||||||
print(std::ostream& os, const char*) const override;
|
print(std::ostream& os, const char*) const override;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
class SPOT_API printable_scc_info final:
|
||||||
|
public spot::printable
|
||||||
|
{
|
||||||
|
std::unique_ptr<scc_info> val_;
|
||||||
|
public:
|
||||||
|
void automaton(const const_twa_graph_ptr& aut)
|
||||||
|
{
|
||||||
|
val_ = std::unique_ptr<scc_info>(new scc_info(aut));
|
||||||
|
}
|
||||||
|
|
||||||
|
void reset()
|
||||||
|
{
|
||||||
|
val_ = nullptr;
|
||||||
|
}
|
||||||
|
|
||||||
|
void print(std::ostream& os, const char* pos) const override;
|
||||||
|
};
|
||||||
|
|
||||||
/// \brief prints various statistics about a TGBA
|
/// \brief prints various statistics about a TGBA
|
||||||
///
|
///
|
||||||
/// This object can be configured to display various statistics
|
/// This object can be configured to display various statistics
|
||||||
|
|
@ -95,7 +114,7 @@ namespace spot
|
||||||
printable_value<unsigned> edges_;
|
printable_value<unsigned> edges_;
|
||||||
printable_value<unsigned> trans_;
|
printable_value<unsigned> trans_;
|
||||||
printable_value<unsigned> acc_;
|
printable_value<unsigned> acc_;
|
||||||
printable_value<unsigned> scc_;
|
printable_scc_info scc_;
|
||||||
printable_value<unsigned> nondetstates_;
|
printable_value<unsigned> nondetstates_;
|
||||||
printable_value<unsigned> deterministic_;
|
printable_value<unsigned> deterministic_;
|
||||||
printable_value<unsigned> complete_;
|
printable_value<unsigned> complete_;
|
||||||
|
|
|
||||||
|
|
@ -56,3 +56,6 @@ test "$out" = "cycle{a},cycle{!a}"
|
||||||
test "0,1,0,1" = "`ltl2tgba FGa | autfilt -D --stats='%D,%d,%P,%p'`"
|
test "0,1,0,1" = "`ltl2tgba FGa | autfilt -D --stats='%D,%d,%P,%p'`"
|
||||||
test "0,0,0,1" = "`ltl2tgba FGa | autfilt -C --stats='%D,%d,%P,%p'`"
|
test "0,0,0,1" = "`ltl2tgba FGa | autfilt -C --stats='%D,%d,%P,%p'`"
|
||||||
test "1,0" = "`ltl2tgba FGa | autfilt -D --stats='%N,%n'`"
|
test "1,0" = "`ltl2tgba FGa | autfilt -D --stats='%N,%n'`"
|
||||||
|
|
||||||
|
test "4" = "`ltl2tgba '(Ga -> Gb)W c' --stats=%c`"
|
||||||
|
test "4,5" = "`ltl2tgba '(Ga -> Gb)W c' | autfilt -C --stats=%C,%c`"
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue