Commit c0eeea2c authored by Clément Gillard's avatar Clément Gillard

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.
parent 164135d3
......@@ -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.
......
......@@ -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<bool> 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);
......
#!/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<<EOF
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1 {0}
[t] 1
--END--
EOF
run 0 autfilt --decompose-scc=0 -F aut> out
cat out
diff out ref
cat >ref<<EOF
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
--BODY--
State: 0 {0}
[0&!1] 0
--END--
EOF
run 0 autfilt --decompose-scc=1 -F aut> 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<<EOF
HOA: v1
States: 2
Start: 0
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0&2] 1
[0] 0
State: 1 {0}
[2] 1
--END--
EOF
run 0 autfilt --decompose-scc=1 -F aut> out
cat out
diff out ref
#!/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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment