From c0eeea2c5fc41719be98a5efa0390153089f6118 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Gillard?= Date: Fri, 3 Feb 2017 14:37:32 +0100 Subject: [PATCH] autfilt: Add '--decompose-scc' option See #172. * bin/autfilt.cc: Add option. * tests/core/strength.test: Remove ambiguity with '--decompose-strength'. * NEWS: Mention it. * tests/core/scc.test: Test it. --- NEWS | 5 +++ bin/autfilt.cc | 27 +++++++++++++++ tests/core/scc.test | 72 +++++++++++++++++++++++++++++++++++++++- tests/core/strength.test | 14 ++++---- 4 files changed, 110 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 4a583c01b..a86212c0f 100644 --- a/NEWS +++ b/NEWS @@ -21,6 +21,11 @@ New in spot 2.3.1 (2017-02-20) Kupferman & Rosenberg [MoChArt'10] are recognizable by deterministic Büchi automata with at least 2^2^n states. + - autfilt has a new transformation: --decompose-scc, which allows + decomposition of automata through their accepting SCCs. + A demonstration of this feature via the Python bindings + can be found at https://spot.lrde.epita.fr/ipynb/decompose.html + Library: - spot::twa_run::as_twa() has an option to preserve state names. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 3142dcf84..a48871867 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -88,6 +88,7 @@ enum { OPT_COMPLEMENT_ACC, OPT_COUNT, OPT_DECOMPOSE_STRENGTH, + OPT_DECOMPOSE_SCC, OPT_DESTUT, OPT_DNF_ACC, OPT_EDGES, @@ -295,6 +296,8 @@ static const argp_option options[] = { "decompose-strength", OPT_DECOMPOSE_STRENGTH, "t|w|s", 0, "extract the (t) terminal, (w) weak, or (s) strong part of an automaton" " (letters may be combined to combine more strengths in the output)", 0 }, + { "decompose-scc", OPT_DECOMPOSE_SCC, "N", 0, "keep only the Nth accepting" + " SCC as accepting", 0 }, { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0, "if any of those APs occur in the automaton, restrict all edges to " "ensure two of them may not be true at the same time. Use this option " @@ -469,6 +472,7 @@ static bool opt_clean_acc = false; static bool opt_complement = false; static bool opt_complement_acc = false; static char* opt_decompose_strength = nullptr; +static int opt_decompose_scc = -1; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -564,6 +568,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_DECOMPOSE_STRENGTH: opt_decompose_strength = arg; break; + case OPT_DECOMPOSE_SCC: + opt_decompose_scc = to_pos_int(arg); + break; case OPT_DESTUT: opt_destut = true; break; @@ -1188,6 +1195,26 @@ namespace return 0; } + if (opt_decompose_scc != -1) + { + spot::scc_info si(aut); + unsigned scc_num = 0; + + for (; scc_num < si.scc_count(); ++scc_num) + { + if (si.is_accepting_scc(scc_num)) + { + if (!opt_decompose_scc) + break; + --opt_decompose_scc; + } + } + + aut = decompose_scc(si, scc_num); + if (!aut) + return 0; + } + if (opt_sat_minimize) { aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc); diff --git a/tests/core/scc.test b/tests/core/scc.test index b464778fe..dee6d9564 100755 --- a/tests/core/scc.test +++ b/tests/core/scc.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2015 Laboratoire de Recherche et Developpement de +# Copyright (C) 2009, 2015, 2017 Laboratoire de Recherche et Developpement de # l'Epita # # This file is part of Spot, a model checking library. @@ -33,3 +33,73 @@ EOF run 0 ltl2tgba --low --any --stats='%f,%e,%s,%c' -F formulas/1 >out cat out diff out formulas + +ltl2tgba 'a W b' > aut + +cat >ref< out +cat out +diff out ref + +cat >ref< out +cat out +diff out ref + +autfilt --decompose-scc=2 -F aut 2>stderr && exit 1 +[ $? -eq 2 ] +grep "out of bounds" stderr + +# always satisfied acceptance +ltl2tgba 'Ga R b | Gc R b' > aut + +cat >ref< out +cat out +diff out ref diff --git a/tests/core/strength.test b/tests/core/strength.test index bc7a7598e..880eca1f0 100755 --- a/tests/core/strength.test +++ b/tests/core/strength.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Developpement +# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Developpement # de l'Epita # # This file is part of Spot, a model checking library. @@ -221,12 +221,12 @@ EOF diff out expected -run 0 $autfilt -H --decompose=t in | tee out.t -run 0 $autfilt -H --decompose=w in | tee out.w -run 0 $autfilt -H --decompose=s in | tee out.s -run 0 $autfilt -H --decompose=tw in | tee out.tw -run 0 $autfilt -H --decompose=ws in | tee out.ws -run 0 $autfilt -H --decompose=tws in | tee out.tws +run 0 $autfilt -H --decompose-strength=t in | tee out.t +run 0 $autfilt -H --decompose-strength=w in | tee out.w +run 0 $autfilt -H --decompose-strength=s in | tee out.s +run 0 $autfilt -H --decompose-strength=tw in | tee out.tw +run 0 $autfilt -H --decompose-strength=ws in | tee out.ws +run 0 $autfilt -H --decompose-strength=tws in | tee out.tws echo '/******************************/' > sep cat out.t sep out.w sep out.s sep out.tw sep out.ws sep out.tws > out