acd: add ORDER_HEURISTIC for state-based ACD-transform

* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Add the
acd_options::ORDER_HEURISTIC and use it by default in
acd_transform_sbacc().
* spot/misc/bitvect.hh (bitvect::count, bitvect::add_common): New
methods.
* tests/python/zlktree.ipynb: Adjust examples and discuss this
heuristic.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-24 20:39:47 +02:00
parent 70ede35702
commit fea0be96c1
4 changed files with 1655 additions and 554 deletions

View file

@ -167,6 +167,11 @@ namespace spot
/// shape that is tested. When that happens, node_count() is set
/// to 0.
ABORT_WRONG_SHAPE = 4,
/// Order the children of a node by decreasing size of the number
/// of states they would introduce if that child appears as the
/// last child of an "ACD" round in the state-based version of the
/// ACD output.
ORDER_HEURISTIC = 8,
};
#ifndef SWIG
@ -407,13 +412,15 @@ namespace spot
/// optimal transition-based output (optimal in the sense of least
/// number of duplicated states), while the acd_tansform_sbacc() variant
/// produces state-based output from transition-based input and without
/// any optimality claim.
/// any optimality claim. The \a order_heuristics argument, enabled
/// by default activates the ORDER_HEURISTICS option of the ACD.
/// @{
SPOT_API
twa_graph_ptr acd_transform(const const_twa_graph_ptr& aut,
bool colored = false);
SPOT_API
twa_graph_ptr acd_transform_sbacc(const const_twa_graph_ptr& aut,
bool colored = false);
bool colored = false,
bool order_heuristic = true);
/// @}
}