Commit d2068bb1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sbacc: improve using SCCs and common marks

* spot/twaalgos/sbacc.cc: Here.
* tests/core/parseaut.test, tests/python/automata.ipynb: Adjust.
* tests/core/sbacc.test: Likewise + more tests.
* NEWS: Mention it.
parent d271dfd5
......@@ -117,6 +117,12 @@ New in spot 2.0.3a (not yet released)
the corresponding properties of the automaton as a side-effect of
their check.
* the sbacc() function, used by "ltl2tgba -S" and "autfilt -S" to
convert automata to state-based acceptance, learned some tricks
(using SCCs, pulling accepting marks common to all outgoing edges,
and pushing acceptance marks common to all incoming edges) to
reduce the number of additional states needed.
* language_containment_checker now has default values for all
parameters of its constructor.
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
......@@ -21,6 +21,7 @@
#include <map>
#include <utility>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sccinfo.hh>
namespace spot
{
......@@ -29,6 +30,26 @@ namespace spot
if (old->prop_state_acc())
return old;
scc_info si(old);
unsigned ns = old->num_states();
acc_cond::mark_t all = old->acc().all_sets();
std::vector<acc_cond::mark_t> common_in(ns, all);
std::vector<acc_cond::mark_t> common_out(ns, all);
std::vector<acc_cond::mark_t> one_in(ns, 0U);
for (auto& e: old->edges())
if (si.scc_of(e.src) == si.scc_of(e.dst))
{
common_in[e.dst] &= e.acc;
common_out[e.src] &= e.acc;
one_in[e.dst] = e.acc;
}
for (unsigned s = 0; s < ns; ++s)
common_out[s] |= common_in[s];
for (auto& e: old->edges())
if (si.scc_of(e.src) == si.scc_of(e.dst))
one_in[e.dst] = (e.acc - common_out[e.src]);
auto res = make_twa_graph(old->get_dict());
res->copy_ap_of(old);
res->copy_acceptance_of(old);
......@@ -54,28 +75,39 @@ namespace spot
return p.first->second;
};
// Find any edge going into the initial state, and use its
// acceptance as mark.
acc_cond::mark_t init_acc = 0U;
unsigned old_init = old->get_init_state_number();
for (auto& t: old->edges())
if (t.dst == old_init)
{
init_acc = t.acc;
break;
}
acc_cond::mark_t init_acc = 0U;
if (!si.is_rejecting_scc(si.scc_of(old_init)))
// Use any edge going into the initial state to set the first
// acceptance mark.
init_acc = one_in[old_init] | common_out[init_acc];
res->set_init_state(new_state(old_init, init_acc));
while (!todo.empty())
{
auto one = todo.back();
todo.pop_back();
unsigned scc_src = si.scc_of(one.first.first);
bool maybe_accepting = !si.is_rejecting_scc(scc_src);
for (auto& t: old->out(one.first.first))
res->new_edge(one.second,
new_state(t.dst, t.acc),
t.cond,
one.first.second);
{
unsigned scc_dst = si.scc_of(t.dst);
acc_cond::mark_t acc = 0U;
bool dst_acc = si.is_accepting_scc(scc_dst);
if (maybe_accepting && scc_src == scc_dst)
acc = t.acc - common_out[t.src];
else if (dst_acc)
// We enter a new accepting SCC. Use any edge going into
// t.dst from this SCC to set the initial acceptance mark.
acc = one_in[t.dst];
if (dst_acc)
acc |= common_out[t.dst];
common_out[t.dst];
res->new_edge(one.second, new_state(t.dst, acc),
t.cond, one.first.second);
}
}
res->merge_edges();
return res;
}
}
......@@ -1755,14 +1755,14 @@ State: 0
1 0 2 2 1 0 2 2 1 0 2 2 1 0 2 2
State: 1
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
State: 2
2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5
State: 3 {0}
2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5
State: 4 {1}
2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5
State: 5 {0 1}
2 2 2 2 3 3 3 3 4 4 4 4 5 5 5 5
State: 2 {0 1}
3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2
State: 3
3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2
State: 4 {0}
3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2
State: 5 {1}
3 3 3 3 4 4 4 4 5 5 5 5 2 2 2 2
--END--
EOF
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -37,26 +37,26 @@ Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0 {0 1}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 1
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 2 {1}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 3 {0}
[0&1] 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 0 {0}
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 1 {0 1}
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 2
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
State: 3 {1}
[0&!1] 0
[0&1] 1
[!0&!1] 2
[!0&1] 3
--END--
EOF
......@@ -91,9 +91,9 @@ properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {1}
[0] 1
State: 1
State: 1 {0}
[0] 2
State: 2 {0}
State: 2 {0 1}
[0] 0
--END--
EOF
......@@ -124,4 +124,8 @@ EOF
diff out.hoa expected
randltl --weak-fairness -n 20 2 |
ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O"
ltlcross "$ltl2tgba -DH %f >%O" \
"$ltl2tgba -S %f >%O" \
"$ltl2tgba -H %f | $autfilt -H >%O"
test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s`
This diff is collapsed.
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