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

tgba_digraph: add a copy constructor, and obsolete dupexp

* src/tgba/tgbagraph.hh, src/tgba/tgbagraph.cc: Add a copy constructor,
and some method to purge unreachable states.
* src/graph/graph.hh (defrag_states): Erase transition of removed
states.
* src/tgbaalgos/complete.cc, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/simulation.cc,
src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2tgba.cc: Adjust to use make_tgba_digraph() instead
of tgba_dupexp_dfs() or tgba_dupexp_bfs().
* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Use
make_tgba_digraph() when possible.
* src/tgbatest/det.test, src/tgbatest/sim.test: Adjust expected results.
parent 971788fd
......@@ -656,8 +656,18 @@ namespace spot
for (state s = 0; s < send; ++s)
{
state dst = newst[s];
if (dst == s || dst == -1U)
if (dst == s)
continue;
if (dst == -1U)
{
// This is an erased state. Mark all its transitions as
// dead (i.e., t.next_succ should point to t for each of
// them).
auto t = states_[s].succ;
while (t)
std::swap(t, transitions_[t].next_succ);
continue;
}
states_[dst] = std::move(states_[s]);
}
states_.resize(used_states);
......
......@@ -62,6 +62,40 @@ namespace spot
g_.defrag();
}
void tgba_digraph::purge_unreachable_states()
{
unsigned num_states = g_.num_states();
if (num_states == 0)
return;
std::vector<unsigned> seen(num_states, 0);
std::vector<unsigned> todo;
todo.reserve(num_states);
todo.push_back(init_number_);
seen[init_number_] = 1;
auto todo_pos = todo.begin();
while (todo_pos != todo.end())
{
for (auto& t: g_.out(*todo_pos))
if (!seen[t.dst])
{
seen[t.dst] = 1;
todo.push_back(t.dst);
}
++todo_pos;
}
// Now renumber each used state.
unsigned current = 0;
for (auto& v: seen)
if (!v)
v = -1U;
else
v = current++;
if (current == seen.size())
return; // No useless state.
init_number_ = seen[init_number_];
g_.defrag_states(std::move(seen), current);
}
void tgba_digraph::purge_dead_states()
{
unsigned num_states = g_.num_states();
......
......@@ -25,6 +25,7 @@
#include "graph/ngraph.hh"
#include "tgba/bdddict.hh"
#include "tgba/tgba.hh"
#include "tgbaalgos/dupexp.hh"
#include "misc/bddop.hh"
#include <sstream>
......@@ -170,6 +171,14 @@ namespace spot
{
}
explicit tgba_digraph(const const_tgba_digraph_ptr& other)
: tgba(other->get_dict()),
g_(other->g_), init_number_(other->init_number_)
{
copy_acceptance_conditions_of(other);
copy_ap_of(other);
}
virtual ~tgba_digraph()
{
get_dict()->unregister_all_my_variables(this);
......@@ -228,7 +237,7 @@ namespace spot
set_init_state(state_number(s));
}
virtual graph_t::state get_init_state_number() const
graph_t::state get_init_state_number() const
{
if (num_states() == 0)
const_cast<graph_t&>(g_).new_state();
......@@ -391,6 +400,9 @@ namespace spot
/// Remove all states without successors.
void purge_dead_states();
/// Remove all unreachable states.
void purge_unreachable_states();
bool state_is_accepting(unsigned s) const
{
assert(has_state_based_acc());
......@@ -412,6 +424,21 @@ namespace spot
{
return std::make_shared<tgba_digraph>(dict);
}
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut)
{
return std::make_shared<tgba_digraph>(aut);
}
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut)
{
auto p = std::dynamic_pointer_cast<const tgba_digraph>(aut);
if (p)
return std::make_shared<tgba_digraph>(p);
else
return tgba_dupexp_dfs(aut);
}
}
#endif // SPOT_TGBA_TGBAGRAPH_HH
......@@ -18,7 +18,6 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "complete.hh"
#include "dupexp.hh"
namespace spot
{
......@@ -105,7 +104,12 @@ namespace spot
tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut)
{
tgba_digraph_ptr res = tgba_dupexp_dfs(aut);
auto res = make_tgba_digraph(aut);
res->prop_copy(aut,
true, // state based
true, // single acc
true, // inherently_weak
true); // deterministic
tgba_complete_here(res);
return res;
}
......
......@@ -25,7 +25,6 @@
#include "minimize.hh"
#include "simulation.hh"
#include "safety.hh"
#include "dupexp.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh"
......
......@@ -18,7 +18,6 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "dtgbacomp.hh"
#include "dupexp.hh"
#include "sccinfo.hh"
namespace spot
......@@ -26,9 +25,12 @@ namespace spot
tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_ptr& aut)
{
// Clone the original automaton.
tgba_digraph_ptr res = tgba_dupexp_dfs(aut);
auto res = make_tgba_digraph(aut);
res->prop_copy(aut,
false, // state based
false, // single acc
false, // inherently_weak
false); // deterministic
// Copy the old acceptance condition before we replace it.
acc_cond oldacc = aut->acc(); // Copy it!
......@@ -36,6 +38,9 @@ namespace spot
// automaton will only have one acceptance set.
// This changes aut->acc();
res->set_single_acceptance_set();
// The resulting automaton is weak.
res->prop_inherently_weak();
res->prop_state_based_acc();
unsigned num_sets = oldacc.num_sets();
unsigned n = res->num_states();
......@@ -108,8 +113,7 @@ namespace spot
tgba_digraph_ptr dtgba_complement_weak(const const_tgba_ptr& aut)
{
// Clone the original automaton.
tgba_digraph_ptr res = tgba_dupexp_dfs(aut);
auto res = make_tgba_digraph(aut);
res->prop_copy(aut,
true, // state based
true, // single acc
......
......@@ -21,10 +21,12 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "dupexp.hh"
#include "tgba/tgbagraph.hh"
#include <sstream>
#include <string>
#include <map>
#include "reachiter.hh"
#include "dotty.hh"
namespace spot
{
......@@ -119,6 +121,20 @@ namespace spot
tgba_digraph_ptr
tgba_dupexp_dfs(const const_tgba_ptr& aut, std::vector<const state*>& rel)
{
auto aa = std::dynamic_pointer_cast<const spot::tgba_digraph>(aut);
if (aa)
{
aa->get_init_state_number(); // Create an initial state if needed.
auto res = make_tgba_digraph(aa);
unsigned ns = aa->num_states();
rel.reserve(ns);
// The state numbers are common to both automata, but
// the state pointers are to the older one.
for (unsigned n = 0; n < ns; ++n)
rel.push_back(aa->state_from_number(n));
return res;
}
dupexp_iter_save<tgba_reachable_iterator_depth_first> di(aut, rel);
di.run();
return di.result();
......
......@@ -23,7 +23,10 @@
#ifndef SPOT_TGBAALGOS_DUPEXP_HH
# define SPOT_TGBAALGOS_DUPEXP_HH
# include "tgba/tgbagraph.hh"
# include "misc/common.hh"
# include "tgba/fwd.hh"
# include "tgba/tgba.hh"
# include <vector>
namespace spot
{
......
......@@ -256,7 +256,6 @@ namespace spot
scc_info_.reset(new scc_info(a_));
old_a_ = a_;
// Replace all the acceptance conditions by their complements.
// (In the case of Cosimulation, we also flip the transitions.)
{
......@@ -298,6 +297,8 @@ namespace spot
else
t.acc = acc;
}
if (Cosimulation)
a_->set_init_state(old_a_->get_init_state_number());
}
size_a_ = ns;
}
......@@ -435,7 +436,7 @@ namespace spot
// When we Cosimulate, we add a special flag to differentiate
// the initial state from the other.
if (Cosimulation && src == 0)
if (Cosimulation && src == a_->get_init_state_number())
res |= bdd_initial;
return res;
......@@ -696,6 +697,8 @@ namespace spot
}
}
res->purge_unreachable_states();
delete gb;
res->prop_copy(original_,
false, // state-based acc forced below
......@@ -835,6 +838,8 @@ namespace spot
bdd res = bddfalse;
unsigned scc = scc_info_->scc_of(src);
if (scc == -1U) // Unreachable
return bddfalse;
bool sccacc = scc_info_->is_accepting_scc(scc);
for (auto& t: a_->out(src))
......@@ -1353,12 +1358,13 @@ namespace spot
direct_simulation<true, Sba> cosimul(res);
res = cosimul.run();
next.set_size(res);
if (Sba)
res = scc_filter_states(res);
else
res = scc_filter(res, false);
next.set_size(res);
}
while (prev != next);
return res;
......
......@@ -29,7 +29,6 @@
#include "tgbaalgos/sccfilter.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/dupexp.hh"
void
syntax(char* prog)
......@@ -93,8 +92,8 @@ main(int argc, char** argv)
if (fpos->is_ltl_formula())
{
auto apos = scc_filter(spot::tgba_dupexp_dfs(ltl_to_taa(fpos, d)));
auto aneg = scc_filter(spot::tgba_dupexp_dfs(ltl_to_taa(fneg, d)));
auto apos = scc_filter(make_tgba_digraph(ltl_to_taa(fpos, d)));
auto aneg = scc_filter(make_tgba_digraph(ltl_to_taa(fneg, d)));
if (!spot::product(apos, aneg)->is_empty())
{
std::cerr << "non-empty intersection between pos and neg (TAA)\n";
......
......@@ -103,9 +103,9 @@ digraph G {
2 -> 2 [label="1"]
2 -> 3 [label="!a"]
2 -> 4 [label="!b"]
3 [label="3"]
3 [label="3", peripheries=2]
3 -> 3 [label="!a\n{0}"]
4 [label="4"]
4 [label="4", peripheries=2]
4 -> 4 [label="!b\n{0}"]
}
EOF
......
......@@ -31,7 +31,6 @@
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/emptiness.hh"
void
......@@ -103,7 +102,7 @@ main(int argc, char** argv)
{
auto a = spot::ltl_to_taa(f, d);
aut[0] = a;
aut[1] = spot::degeneralize_tba(spot::tgba_dupexp_bfs(a));
aut[1] = spot::degeneralize_tba(spot::make_tgba_digraph(a));
}
{
auto a = spot::ltl_to_tgba_fm(f, d);
......
......@@ -324,7 +324,7 @@ spot::tgba_digraph_ptr ensure_digraph(const spot::tgba_ptr& a)
auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
if (aa)
return aa;
return spot::tgba_dupexp_dfs(a);
return spot::make_tgba_digraph(a);
}
int
......
......@@ -35,8 +35,8 @@ run 0 ../ltl2tgba -X -RDCS -b in.tgba > out.tgba
cat >expected.tgba <<EOF
acc = "0";
"0", "3", "b",;
"3", "3", "a", "0";
"0", "1", "b",;
"1", "1", "a", "0";
EOF
diff out.tgba expected.tgba
......@@ -44,8 +44,8 @@ diff out.tgba expected.tgba
run 0 ../ltl2tgba -RDCIS -b XXXXGFa > out.tgba
cat >expected.tgba <<EOF
acc = "a";
"0", "0", "a", "a";
acc = "0";
"0", "0", "a", "0";
"0", "0", "!a",;
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