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

bin: --stats=%x to count atomic propositions

Browse source 
* bin/common_aoutput.cc, bin/common_aoutput.hh: Implement %x and %X.
* tests/core/remprop.test: Test them.
* NEWS: Mention them.
This commit is contained in:
Alexandre Duret-Lutz 2017-02-28 14:06:26 +01:00
parent 0f7008d98c
commit 6c218e4828
4 changed files with 26 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -1,6 +1,10 @@
New in spot 2.3.1.dev (not yet released)
Nothing yet.
Tools:
- In tools that output automata the number of atomic propositions
can be output using --stats=%x (output automaton) or --stats=%X
(input automaton).
New in spot 2.3.1 (2017-02-20)

16
bin/common_aoutput.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -193,6 +193,8 @@ static const argp_option io_options[] =
"wall-clock time elapsed in seconds (excluding parsing)", 0 },
{ "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"one word accepted by the automaton", 0 },
{ "%X, %x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of atomic propositions declared in the automaton", 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@ -228,6 +230,8 @@ static const argp_option o_options[] =
"number of transitions", 0 },
{ "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance sets", 0 },
{ "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of acceptance sets", 0 },
{ "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"acceptance condition (in HOA syntax)", 0 },
{ "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@ -250,6 +254,8 @@ static const argp_option o_options[] =
"wall-clock time elapsed in seconds (excluding parsing)", 0 },
{ "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"one word accepted by the output automaton", 0 },
{ "%x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"number of atomic propositions declared in the automaton", 0 },
{ "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
"a single %", 0 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }
@ -361,6 +367,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format,
declare('S', &haut_states_);
declare('T', &haut_trans_);
declare('W', &haut_word_);
declare('X', &haut_ap_size_);
}
declare('<', &csv_prefix_);
declare('>', &csv_suffix_);
@ -372,6 +379,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format,
declare('h', &output_aut_);
declare('m', &aut_name_);
declare('w', &aut_word_);
declare('x', &aut_ap_size_);
}
std::ostream&
@ -467,6 +475,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
haut_word_.val().clear();
}
}
if (has('X'))
haut_ap_size_ = haut->aut->ap().size();
}
if (has('m'))
@ -490,6 +500,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
aut_word_.val().clear();
}
}
if (has('x'))
aut_ap_size_ = aut->ap().size();
auto& res = this->spot::stat_printer::print(aut, f, run_time);
// Make sure we do not store the automaton until the next one is

6
bin/common_aoutput.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -144,6 +144,8 @@ private:
spot::printable_value<unsigned> haut_edges_;
spot::printable_value<unsigned> haut_trans_;
spot::printable_value<unsigned> haut_acc_;
spot::printable_value<unsigned> haut_ap_size_;
spot::printable_value<unsigned> aut_ap_size_;
spot::printable_scc_info haut_scc_;
spot::printable_value<unsigned> haut_deterministic_;
spot::printable_value<unsigned> haut_nondetstates_;

5
tests/core/remprop.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -47,6 +47,7 @@ EOF
cat >expected <<EOF
HOA: v1
name: "3->1"
States: 4
Start: 0
AP: 1 "c"
@ -68,7 +69,7 @@ State: 3
--END--
EOF
run 0 autfilt -H --remove-ap=a,b automaton >out
run 0 autfilt -H --remove-ap=a,b --name='%X->%x' automaton >out
cat out
diff out expected