diff --git a/NEWS b/NEWS index e57846bef..b4d8a42d5 100644 --- a/NEWS +++ b/NEWS @@ -31,6 +31,8 @@ New in spot 2.9.6.dev (not yet released) --sbacc (an alias for --state-based-acceptance) cannot be abbreviated as --sba anymore. + - autfilt learned a --kill-states=NUM[,NUM...] option. + Library: - Historically, Spot labels automata by Boolean formulas over @@ -176,6 +178,10 @@ New in spot 2.9.6.dev (not yet released) - twa_graph::merge_edges() had its two passes swapped. Doing so improves the determinism of some automata. + - twa_graph::kill_state(num) is a new method that removes the + outgoing edge of some state. It can be used together with + purge_dead_states() to remove selected states. + Python: - Bindings for functions related to games. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index d9c842074..cef86c26c 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -130,6 +130,7 @@ enum { OPT_IS_VERY_WEAK, OPT_IS_WEAK, OPT_KEEP_STATES, + OPT_KILL_STATES, OPT_MASK_ACC, OPT_MERGE, OPT_NONDET_STATES, @@ -297,6 +298,9 @@ static const argp_option options[] = { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0, "only keep specified states. The first state will be the new "\ "initial state. Implies --remove-unreachable-states.", 0 }, + { "kill-states", OPT_KILL_STATES, "NUM[,NUM...]", 0, + "mark the specified states as dead (no successor), and remove" + " them. Implies --remove-dead-states.", 0 }, { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0, "put the acceptance condition in Disjunctive Normal Form", 0 }, { "streett-like", OPT_STREETT_LIKE, nullptr, 0, @@ -656,6 +660,7 @@ static spot::acc_cond::mark_t opt_partial_degen = {}; static spot::acc_cond::mark_t opt_mask_acc = {}; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; +static std::vector opt_kill_states = {}; static bool opt_simpl_acc = false; static bool opt_simplify_exclusive_ap = false; static bool opt_rem_dead = false; @@ -1019,6 +1024,19 @@ parse_opt(int key, char* arg, struct argp_state*) } break; } + case OPT_KILL_STATES: + { + std::vector values = to_longs(arg); + for (auto res : values) + { + if (res < 0) + error(2, 0, "state ids should be non-negative:" + " --kill-states=%ld", res); + opt_kill_states.push_back(res); + } + opt_rem_dead = true; + break; + } case OPT_MERGE: opt_merge = true; break; @@ -1527,6 +1545,13 @@ namespace else if (opt_instut == 2) aut = spot::sl2_inplace(std::move(aut)); + if (!opt_kill_states.empty()) + { + unsigned ns = aut->num_states(); + for (unsigned s: opt_kill_states) + if (s < ns) + aut->kill_state(s); + } if (!opt_keep_states.empty()) aut = mask_keep_accessible_states(aut, opt_keep_states, opt_keep_states_initial); diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index c19585b69..bdce9587d 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -822,6 +822,35 @@ namespace spot set_named_prop("state-names", names.release()); } + void twa_graph::kill_state(unsigned state) + { + auto t = g_.out_iteraser(state); + while (t) + t.erase(); + // A complete automaton is unlikely to stay + // complete after killing a state. + if (prop_complete().is_true()) + prop_complete(trival::maybe()); + prop_stutter_invariant(trival::maybe()); + // Many properties are preserved by state removal, and may even + // become true if they were false before and the appropriate + // states are removed. + if (prop_universal().is_false()) + prop_universal(trival::maybe()); + if (prop_inherently_weak().is_false()) + prop_inherently_weak(trival::maybe()); + if (prop_weak().is_false()) + prop_weak(trival::maybe()); + if (prop_very_weak().is_false()) + prop_very_weak(trival::maybe()); + if (prop_terminal().is_false()) + prop_terminal(trival::maybe()); + if (prop_unambiguous().is_false()) + prop_unambiguous(trival::maybe()); + if (prop_semi_deterministic().is_false()) + prop_semi_deterministic(trival::maybe()); + } + void twa_graph::dump_storage_as_dot(std::ostream& out, const char* opt) const { diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 072a0d04c..77ca9284a 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -726,6 +726,15 @@ namespace spot ///@} #endif // SWIG + /// \brief Make a state dead. + /// + /// A state is dead if it has no successors. So this function + /// simply erases all edges leaving \a state. + /// + /// It can be used together with purge_dead_states() to remove a + /// set of states from an automaton. + void kill_state(unsigned state); + /// \brief Print the data structures used to represent the /// automaton in dot's format. /// diff --git a/tests/core/maskkeep.test b/tests/core/maskkeep.test index 1188c1b67..56a6c4ac0 100755 --- a/tests/core/maskkeep.test +++ b/tests/core/maskkeep.test @@ -100,14 +100,38 @@ State: 1 --END-- EOF +cat >expect5 <output diff output expect3 run 0 autfilt --keep-states=0,9999,1,2 input1 -H >output diff output expect3 +run 0 autfilt --kill-states=99,3 input1 -H >output +diff output expect3 run 0 autfilt --keep-states=1,2,0 input1 -H >output diff output expect4 +run 0 autfilt --kill-states=1,2 --kill-states=0 input1 -H >output +diff output expect5 +run 0 autfilt --kill-states=0 input1 -H >output +diff output expect5 + +# make sure the complete property is reset +ltl2tgba 'GF(a<->Xa)' | autfilt --kill-state=1 | grep -v complete + # Errors run 2 autfilt --keep-states=a3 input1 2> error cat error @@ -115,3 +139,10 @@ grep 'failed to parse' error run 2 autfilt --keep-states=3-2 input1 2> error cat error grep 'non-negative: --keep-states' error + +run 2 autfilt --kill-states=a3 input1 2> error +cat error +grep 'failed to parse' error +run 2 autfilt --kill-states=3-2 input1 2> error +cat error +grep 'non-negative: --kill-states' error