Commit ead04cb1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

dtgbacomp: Rewrite using tgba_digraph instead of tgba_explicit_number

* src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh: Rewrite.
Also prefer simple loops over reachiter.
* src/tgbatest/det.test: Adjust.
parent 0909c2fe
......@@ -19,124 +19,87 @@
#include "dtgbacomp.hh"
#include "ltlast/constant.hh"
#include "reachiter.hh"
#include "dupexp.hh"
namespace spot
{
namespace
tgba_digraph* dtgba_complement(const tgba* aut)
{
class dtgbacomp_iter: public tgba_reachable_iterator_depth_first_stack
{
bdd orig_acc_;
bdd all_neg_;
bdd acc_;
bdd_dict* dict_;
tgba_explicit_number* out_;
int num_acc_;
// Clone the original automaton.
tgba_digraph* res = tgba_dupexp_dfs(aut);
typedef state_explicit_number::transition trans;
public:
dtgbacomp_iter(const tgba* a)
: tgba_reachable_iterator_depth_first_stack(a),
dict_(a->get_dict()),
out_(new tgba_explicit_number(dict_))
{
dict_->register_all_variables_of(a, out_);
orig_acc_ = a->all_acceptance_conditions();
all_neg_ = a->neg_acceptance_conditions();
num_acc_ = a->number_of_acceptance_conditions();
auto dict = res->get_dict();
// Register one acceptance condition for the result.
int accvar = dict_->register_acceptance_variable
(ltl::constant::true_instance(), out_);
acc_ = bdd_ithvar(accvar);
out_->set_acceptance_conditions(acc_);
}
bdd oldaccs = aut->all_acceptance_conditions();
bdd oldnegs = aut->neg_acceptance_conditions();
tgba_explicit_number*
result()
{
return out_;
}
// We will modify res in place, and the resulting
// automaton will only have one acceptance set.
dict->unregister_all_typed_variables(bdd_dict::acc, res);
bdd theacc =
bdd_ithvar(dict->register_acceptance_variable
(ltl::constant::true_instance(), res));
res->set_acceptance_conditions(theacc);
void
end()
{
out_->merge_transitions();
// create a sink state if needed.
if (out_->has_state(0))
{
trans* t = out_->create_transition(0, 0);
t->condition = bddtrue;
t->acceptance_conditions = acc_;
}
}
unsigned num_acc = aut->number_of_acceptance_conditions();
unsigned n = res->num_states();
// We will duplicate the automaton as many times as we have
// acceptance sets, and we need one extra sink state.
res->new_states(num_acc * n + 1);
unsigned sink = res->num_states() - 1;
// The sink state has an accepting self-loop.
res->new_transition(sink, sink, bddtrue, theacc);
void process_state(const state*, int n,
tgba_succ_iterator* i)
for (unsigned src = 0; src < n; ++src)
{
// add a transition to a sink state if the state is not complete.
bdd all = bddtrue;
if (i->first())
do
all -= i->current_condition();
while (i->next());
if (all != bddfalse)
// Keep track of all conditions on transition leaving state
// SRC, so we can complete it.
bdd missingcond = bddtrue;
for (auto& t: res->out(src))
{
trans* t = out_->create_transition(n, 0);
t->condition = all;
}
}
void
process_link(const state*, int in,
const state*, int out,
const tgba_succ_iterator* si)
{
assert(in > 0);
assert(out > 0);
bdd a = si->current_acceptance_conditions();
if (t.dst >= n) // Ignore transition we added.
break;
missingcond -= t.cond;
bdd curacc = t.acc;
// The original transition must not accept anymore.
t.acc = bddfalse;
// Transition that were fully accepting are never cloned.
if (curacc == oldaccs)
continue;
// Save t.cond and t.dst as the reference to t
// is invalided by calls to new_transition().
unsigned dst = t.dst;
bdd cond = t.cond;
// We want all acceptance bdd variable to appear in curacc.
if (curacc == bddfalse)
curacc = oldnegs;
// Positive states represent a non-accepting copy of the
// original automaton.
trans* t1 = out_->create_transition(in, out);
t1->condition = si->current_condition();
// Negative states encode NUM_ACC_ copies of the automaton.
// In each copy transitions labeled by one of the acceptance
// set have been removed, and all the remaining transitions
// are now accepting.
// For each state S, we have NUM_ACC_ additional copies
// labeled S*-NUM_ACC, S*-NUM_ACC+1, ... S*-NUM_ACC+(NUM_ACC-1),
if (a != orig_acc_)
{
bool backlink = on_stack(out);
int add = 0;
if (a == bddfalse)
a = all_neg_;
// Iterate over all the acceptance conditions in 'a'.
bdd ac = a;
while (ac != bddtrue)
// Iterate over all the acceptance conditions in 'curacc',
// an duplicate it each each clone for which it does not
// belong to the acceptance set.
unsigned add = 0;
while (curacc != bddtrue)
{
bdd h = bdd_high(ac);
add += n;
bdd h = bdd_high(curacc);
if (h == bddfalse)
{
trans* t2 = out_->create_transition(in * -num_acc_ + add,
out * -num_acc_ + add);
t2->condition = si->current_condition();
t2->acceptance_conditions = acc_;
// Clone the transition
res->new_transition(src + add, dst + add, cond, theacc);
assert(dst + add < sink);
// Using `t' is disallowed from now on as it is a
// reference to a transition that may have been
// reallocated.
if (backlink)
{
// Since we are closing a cycle, add
// a non-deterministic transition from
// the original automaton to this copy.
trans* t3 =
out_->create_transition(in, out * -num_acc_ + add);
t3->condition = si->current_condition();
}
ac = bdd_low(ac);
// At least one transition per cycle should have a
// nondeterministic copy from the original clone.
// We use state numbers to select it, as any cycle
// is guaranteed to have at least one transition
// with dst <= src. FIXME: Computing a feedback
// arc set would be better.
if (dst <= src)
res->new_transition(src, dst + add, cond);
curacc = bdd_low(curacc);
}
else
{
......@@ -148,26 +111,21 @@ namespace spot
// branch is false. In that case we take the HIGH
// branch to enumerate all the remaining negated
// variables.
bdd tmp = bdd_low(ac);
bdd tmp = bdd_low(curacc);
if (tmp != bddfalse)
ac = tmp;
curacc = tmp;
else
ac = h;
curacc = h;
}
++add;
}
assert(add == num_acc_);
assert(add == num_acc * n);
}
// Complete the original automaton.
if (missingcond != bddfalse)
res->new_transition(src, sink, missingcond);
}
};
} // anonymous
tgba_explicit_number* dtgba_complement(const tgba* aut)
{
dtgbacomp_iter dci(aut);
dci.run();
return dci.result();
res->merge_transitions();
// FIXME: Remove unreachable states.
return res;
}
}
......@@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_DTGBACOMP_HH
# define SPOT_TGBAALGOS_DTGBACOMP_HH
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbagraph.hh"
namespace spot
{
......@@ -30,7 +30,7 @@ namespace spot
/// to be complete. Acceptance can be transition-based, or
/// state-based. The resulting automaton is very unlikely to be
/// deterministic.
SPOT_API tgba_explicit_number*
SPOT_API tgba_digraph*
dtgba_complement(const tgba* aut);
}
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Développement
# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -72,21 +72,22 @@ EOF
# FIXME: we should improve this output
cat >ex.tgba <<'EOF'
acc = "1";
"0", "1", "a",;
"0", "0", "!a",;
"0", "3", "!a",;
"1", "2", "a",;
"1", "1", "!a",;
"1", "-1", "!a",;
"2", "3", "a",;
"2", "1", "!a",;
"2", "-1", "!a",;
"-1", "-1", "!a", "1";
"3", "3", "a",;
"3", "-3", "a",;
"3", "1", "!a",;
"3", "-1", "!a",;
"-3", "-3", "a", "1";
"-3", "-1", "!a", "1";
"1", "0", "!a",;
"1", "3", "!a",;
"3", "3", "!a", "1";
"2", "2", "a",;
"2", "0", "!a",;
"2", "5", "a",;
"2", "3", "!a",;
"5", "5", "a", "1";
"5", "3", "!a", "1";
EOF
run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba
diff out.tgba ex.tgba
......@@ -96,15 +97,15 @@ cat >ex.tgba <<EOF
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1"]
1 [label="0"]
1 -> 2 [label="1\n"]
2 [label="2"]
2 [label="1"]
2 -> 2 [label="1\n"]
2 -> 3 [label="!a\n"]
2 -> 4 [label="!b\n"]
3 [label="-4"]
3 [label="3"]
3 -> 3 [label="!a\n{Acc[1]}"]
4 [label="-3"]
4 [label="5"]
4 -> 4 [label="!b\n{Acc[1]}"]
}
EOF
......
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