safra: Edges to accepting SCC are accepting
* src/twaalgos/safra.cc, src/twaalgos/safra.hh: Implement optimisation. Update function calls with new API. * src/tests/safra.cc, src/tests/safra.test: Use new API.
This commit is contained in:
Alexandre Lewkowicz
Alexandre Duret-Lutz
parent
f29de22b8a
commit
e8c428d0a3
4 changed files with 120 additions and 49 deletions
|
|
@ -20,14 +20,14 @@
|
|||
#include <iostream>
|
||||
#include <cstring>
|
||||
|
||||
#include "ltlparse/public.hh" // ltl::parse
|
||||
#include "parseaut/public.hh"
|
||||
#include "twa/twagraph.hh"
|
||||
#include "twaalgos/degen.hh"
|
||||
#include "twaalgos/dot.hh" // print_dot
|
||||
#include "twaalgos/hoa.hh" // print_hoa
|
||||
#include "twaalgos/safra.hh"
|
||||
#include "twaalgos/translate.hh"
|
||||
#include "hoaparse/public.hh"
|
||||
#include "ltlparse/public.hh"
|
||||
#include "twaalgos/dotty.hh"
|
||||
#include "twaalgos/hoa.hh"
|
||||
#include "twaalgos/degen.hh"
|
||||
|
||||
|
||||
int help()
|
||||
|
|
@ -37,11 +37,14 @@ int help()
|
|||
std::cerr << "\t--hoa file.hoa\tinput file has hoa format\n";
|
||||
std::cerr << "\t-p\tpretty print states\n";
|
||||
std::cerr << "\t-H\toutput hoa format\n";
|
||||
std::cerr << "\t-b\treduce result using bisimulation\n";
|
||||
std::cerr << "\t--emit_scc\ttransitions to accpting scc are accepting\n";
|
||||
return 1;
|
||||
}
|
||||
|
||||
int main(int argc, char* argv[])
|
||||
{
|
||||
bool emit_scc = false;
|
||||
bool sim = false;
|
||||
bool in_hoa = false;
|
||||
bool in_ltl = false;
|
||||
|
|
@ -77,6 +80,8 @@ int main(int argc, char* argv[])
|
|||
pretty_print = true;
|
||||
else if (!strncmp(argv[i], "-b", 2))
|
||||
sim = true;
|
||||
else if (!strncmp(argv[i], "--emit_scc", 2))
|
||||
emit_scc = true;
|
||||
}
|
||||
|
||||
if (!input)
|
||||
|
|
@ -88,33 +93,32 @@ int main(int argc, char* argv[])
|
|||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f =
|
||||
spot::ltl::parse(input, pel, spot::ltl::default_environment::instance(),
|
||||
false);
|
||||
spot::ltl::parse_infix_psl(input, pel);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, input, pel))
|
||||
return 2;
|
||||
spot::translator trans(dict);
|
||||
trans.set_pref(spot::postprocessor::Deterministic);
|
||||
auto tmp = trans.run(f);
|
||||
res = spot::tgba_determinisation(tmp, sim, pretty_print);
|
||||
res = spot::tgba_determinisation(tmp, sim, pretty_print, emit_scc);
|
||||
f->destroy();
|
||||
}
|
||||
else if (in_hoa)
|
||||
{
|
||||
spot::hoa_parse_error_list pel;
|
||||
auto aut = spot::hoa_parse(input, pel, dict);
|
||||
if (spot::format_hoa_parse_errors(std::cerr, input, pel))
|
||||
spot::parse_aut_error_list pel;
|
||||
auto aut = spot::parse_aut(input, pel, dict);
|
||||
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
||||
return 2;
|
||||
res = tgba_determinisation(aut->aut, sim, pretty_print);
|
||||
res = tgba_determinisation(aut->aut, sim, pretty_print, emit_scc);
|
||||
}
|
||||
res->merge_transitions();
|
||||
res->merge_edges();
|
||||
|
||||
if (out_hoa)
|
||||
{
|
||||
spot::hoa_reachable(std::cout, res, "t");
|
||||
spot::print_hoa(std::cout, res, "t");
|
||||
std::cout << std::endl;
|
||||
}
|
||||
else if (out_dot)
|
||||
spot::dotty_reachable(std::cout, res);
|
||||
spot::print_dot(std::cout, res);
|
||||
else
|
||||
assert(false);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ EOF
|
|||
|
||||
cat >out.exp << EOF
|
||||
HOA: v1
|
||||
States: 6
|
||||
States: 5
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Buchi
|
||||
|
|
@ -101,9 +101,9 @@ State: 1
|
|||
[0&1] 2
|
||||
[!0&1] 3 {0}
|
||||
State: 2
|
||||
[0&1] 1 {0}
|
||||
[!0&1] 3 {0}
|
||||
[0&!1] 4
|
||||
[0&1] 5
|
||||
State: 3
|
||||
[0&!1] 0
|
||||
[0&1] 2
|
||||
|
|
@ -111,15 +111,52 @@ State: 3
|
|||
State: 4
|
||||
[0] 1 {0}
|
||||
[!0&1] 3 {0}
|
||||
State: 5
|
||||
[0] 1 {0}
|
||||
[!0&1] 3 {0}
|
||||
--END--
|
||||
EOF
|
||||
|
||||
run 0 ../safra --hoa double_b.hoa -H > out.hoa
|
||||
diff out.hoa out.exp
|
||||
|
||||
# Test emit_scc optim
|
||||
cat > out.exp << EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc deterministic
|
||||
--BODY--
|
||||
State: 0 "{₀0₀}"
|
||||
[0] 1 {0}
|
||||
State: 1 "{₀0 1₀}"
|
||||
[0] 1 {0}
|
||||
[!0&1] 2 {0}
|
||||
State: 2 "{₀1₀}"
|
||||
[1] 2 {0}
|
||||
[0&!1] 2
|
||||
--END--
|
||||
EOF
|
||||
|
||||
cat > in.hoa << EOF
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 1 Inf(0)
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 0 {0}
|
||||
[0] 1
|
||||
State: 1
|
||||
[1] 1 {0}
|
||||
[0] 1
|
||||
--END--
|
||||
EOF
|
||||
|
||||
run 0 ../safra --hoa in.hoa --emit_scc -p -H > out.hoa
|
||||
diff out.hoa out.exp
|
||||
|
||||
# Formulas from bench/dtgbasat/formulas
|
||||
cat >formulae <<EOF
|
||||
X((a M F((!c & !b) | (c & b))) W (G!c U b))
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@
|
|||
|
||||
#include "safra.hh"
|
||||
#include "twaalgos/degen.hh"
|
||||
#include "twaalgos/sccinfo.hh"
|
||||
#include "twaalgos/simulation.hh"
|
||||
|
||||
namespace spot
|
||||
|
|
@ -141,7 +142,7 @@ namespace spot
|
|||
{
|
||||
assert(max_acc < 32);
|
||||
unsigned mask = (1 << max_acc) - 1;
|
||||
for (auto& t: aut->transitions())
|
||||
for (auto& t: aut->edges())
|
||||
{
|
||||
t.acc &= mask;
|
||||
}
|
||||
|
|
@ -166,26 +167,30 @@ namespace spot
|
|||
}
|
||||
|
||||
}
|
||||
auto
|
||||
|
||||
void
|
||||
safra_state::compute_succs(const const_twa_graph_ptr& aut,
|
||||
const std::vector<unsigned>& bddnums,
|
||||
std::unordered_map<bdd,
|
||||
std::pair<unsigned, unsigned>,
|
||||
bdd_hash>& deltas) const -> succs_t
|
||||
bdd_hash>& deltas,
|
||||
succs_t& res) const
|
||||
{
|
||||
succs_t res;
|
||||
// Given a bdd returns index of associated safra_state in res
|
||||
std::map<unsigned, unsigned> bdd2num;
|
||||
for (auto& node: nodes_)
|
||||
{
|
||||
for (auto& t: aut->out(node.first))
|
||||
{
|
||||
// deltas precalculate all transitions in edge t
|
||||
auto p = deltas[t.cond];
|
||||
for (unsigned j = p.first; j < p.second; ++j)
|
||||
{
|
||||
auto i = bdd2num.insert(std::make_pair(bddnums[j], res.size()));
|
||||
unsigned idx;
|
||||
if (!i.second)
|
||||
// No new state added, so get pre-existing state whichi is an
|
||||
// index in the vector of safra states (res)
|
||||
idx = i.first->second;
|
||||
else
|
||||
{
|
||||
|
|
@ -203,9 +208,17 @@ namespace spot
|
|||
for (auto& s: res)
|
||||
{
|
||||
safra_state& tmp = s.first;
|
||||
tmp.ungreenify_last_brace();
|
||||
s.first.color_ = tmp.finalize_construction();
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
void safra_state::ungreenify_last_brace()
|
||||
{
|
||||
// Step A4: For a brace to emit green it must surround other braces.
|
||||
// Hence, the last brace cannot emit green as it is the most inside brace.
|
||||
for (auto& n: nodes_)
|
||||
is_green_[n.second.back()] = false;
|
||||
}
|
||||
|
||||
unsigned safra_state::finalize_construction()
|
||||
|
|
@ -218,7 +231,7 @@ namespace spot
|
|||
{
|
||||
if (nb_braces_[i] == 0)
|
||||
{
|
||||
// It is impossible to emit red == -1 as those transitions would
|
||||
// It is impossible to emit red == -1 as those edges would
|
||||
// lead us in a sink states which are not created here.
|
||||
assert(i >= 1);
|
||||
red = std::min(red, 2 * i - 1);
|
||||
|
|
@ -301,12 +314,10 @@ namespace spot
|
|||
unsigned dst, const acc_cond::mark_t acc)
|
||||
{
|
||||
std::vector<node_helper::brace_t> copy = braces;
|
||||
// TODO handle multiple accepting sets
|
||||
if (acc.count())
|
||||
{
|
||||
assert(acc.has(0) && acc.count() == 1 &&
|
||||
"Only one TBA are accepted at the moment");
|
||||
// Accepting transition generate new braces: step A1
|
||||
assert(acc.has(0) && acc.count() == 1 && "Only one TBA are accepted");
|
||||
// Accepting edge generate new braces: step A1
|
||||
copy.emplace_back(nb_braces_.size());
|
||||
// nb_braces_ gets updated later so put 0 for now
|
||||
nb_braces_.emplace_back(0);
|
||||
|
|
@ -333,9 +344,6 @@ namespace spot
|
|||
// After inserting new node, update the brace count per node
|
||||
for (auto b: i.first->second)
|
||||
++nb_braces_[b];
|
||||
// Step A4: For a brace to emit green it must surround other braces.
|
||||
// Hence, the last brace cannot emit green as it is the most inside brace.
|
||||
is_green_[i.first->second.back()] = false;
|
||||
}
|
||||
|
||||
// Called only to initialize first state
|
||||
|
|
@ -367,16 +375,32 @@ namespace spot
|
|||
return nodes_ < other.nodes_;
|
||||
}
|
||||
|
||||
// All edge going into an accepting SCC are marked as accepting
|
||||
// This helps safra make fewer trees as we immediately see the accepting
|
||||
// edge and don't create useless states
|
||||
void
|
||||
emit_accepting_scc(twa_graph_ptr& aut, scc_info& scc)
|
||||
{
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
unsigned src_scc = scc.scc_of(e.src);
|
||||
unsigned dst_scc = scc.scc_of(e.dst);
|
||||
if (src_scc == dst_scc)
|
||||
continue;
|
||||
if (scc.is_accepting_scc(dst_scc))
|
||||
e.acc |= 1;
|
||||
}
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation,
|
||||
bool pretty_print)
|
||||
bool pretty_print, bool emit_scc)
|
||||
{
|
||||
// Degeneralize
|
||||
const_twa_graph_ptr aut;
|
||||
if (a->acc().is_generalized_buchi())
|
||||
aut = spot::degeneralize_tba(a);
|
||||
else
|
||||
aut = a;
|
||||
twa_graph_ptr aut = spot::degeneralize_tba(a);
|
||||
scc_info scc = scc_info(aut);
|
||||
if (emit_scc)
|
||||
emit_accepting_scc(aut, scc);
|
||||
|
||||
|
||||
bdd allap = bddtrue;
|
||||
|
|
@ -384,7 +408,7 @@ namespace spot
|
|||
typedef std::set<bdd, bdd_less_than> sup_map;
|
||||
sup_map sup;
|
||||
// Record occurrences of all guards
|
||||
for (auto& t: aut->transitions())
|
||||
for (auto& t: aut->edges())
|
||||
sup.emplace(t.cond);
|
||||
for (auto& i: sup)
|
||||
allap &= bdd_support(i);
|
||||
|
|
@ -398,7 +422,7 @@ namespace spot
|
|||
// Used to convert large bdd to indexes
|
||||
std::unordered_map<bdd, std::pair<unsigned, unsigned>, bdd_hash> deltas;
|
||||
std::vector<unsigned> bddnums;
|
||||
for (auto& t: aut->transitions())
|
||||
for (auto& t: aut->edges())
|
||||
{
|
||||
auto it = deltas.find(t.cond);
|
||||
if (it == deltas.end())
|
||||
|
|
@ -428,7 +452,7 @@ namespace spot
|
|||
});
|
||||
|
||||
// Given a safra_state get its associated state in output automata.
|
||||
// Required to create new transitions from 2 safra-state
|
||||
// Required to create new edges from 2 safra-state
|
||||
power_set seen;
|
||||
safra_state init(aut->get_init_state_number(), true);
|
||||
unsigned num = res->new_state();
|
||||
|
|
@ -437,13 +461,14 @@ namespace spot
|
|||
std::deque<safra_state> todo;
|
||||
todo.push_back(init);
|
||||
unsigned sets = 0;
|
||||
using succs_t = safra_state::succs_t;
|
||||
succs_t succs;
|
||||
while (!todo.empty())
|
||||
{
|
||||
using succs_t = safra_state::succs_t;
|
||||
safra_state curr = todo.front();
|
||||
unsigned src_num = seen.find(curr)->second;
|
||||
todo.pop_front();
|
||||
succs_t succs = curr.compute_succs(aut, bddnums, deltas);
|
||||
curr.compute_succs(aut, bddnums, deltas, succs);
|
||||
for (auto s: succs)
|
||||
{
|
||||
auto i = seen.find(s.first);
|
||||
|
|
@ -461,15 +486,16 @@ namespace spot
|
|||
}
|
||||
if (s.first.color_ != -1U)
|
||||
{
|
||||
res->new_transition(src_num, dst_num, num2bdd[s.second],
|
||||
res->new_edge(src_num, dst_num, num2bdd[s.second],
|
||||
{s.first.color_});
|
||||
// We only care about green acc
|
||||
if (s.first.color_ % 2 == 0)
|
||||
sets = std::max(s.first.color_ + 1, sets);
|
||||
}
|
||||
else
|
||||
res->new_transition(src_num, dst_num, num2bdd[s.second]);
|
||||
res->new_edge(src_num, dst_num, num2bdd[s.second]);
|
||||
}
|
||||
succs.clear();
|
||||
}
|
||||
remove_dead_acc(res, sets);
|
||||
res->set_acceptance(sets, acc_cond::acc_code::parity(false, false, sets));
|
||||
|
|
|
|||
|
|
@ -47,11 +47,14 @@ namespace spot
|
|||
safra_state(unsigned state_number, bool init_state = false);
|
||||
// Given a certain transition_label, compute all the successors of that
|
||||
// label, and return that new node.
|
||||
succs_t compute_succs(const const_twa_graph_ptr& aut,
|
||||
void compute_succs(const const_twa_graph_ptr& aut,
|
||||
const std::vector<unsigned>& bddnums,
|
||||
std::unordered_map<bdd,
|
||||
std::pair<unsigned, unsigned>,
|
||||
bdd_hash>& deltas) const;
|
||||
bdd_hash>& deltas,
|
||||
succs_t& res) const;
|
||||
// The outermost brace of each node cannot be green
|
||||
void ungreenify_last_brace();
|
||||
// Used when creating the list of successors
|
||||
// A new intermediate node is created with src's braces and with dst as id
|
||||
// A merge is done if dst already existed in *this
|
||||
|
|
@ -74,5 +77,6 @@ namespace spot
|
|||
SPOT_API twa_graph_ptr
|
||||
tgba_determinisation(const const_twa_graph_ptr& aut,
|
||||
bool bisimulation = false,
|
||||
bool pretty_print = false);
|
||||
bool pretty_print = false,
|
||||
bool emit_scc = false);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue