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

dtgbasat: replace tgba_explicit_number by tgba_digraph

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh,
src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh: Use tgba_digraph
and modernize syntax slightly.
parent ee087b59
...@@ -666,23 +666,23 @@ namespace spot ...@@ -666,23 +666,23 @@ namespace spot
return std::make_pair(d.nvars, nclauses.nb_clauses()); return std::make_pair(d.nvars, nclauses.nb_clauses());
} }
static tgba_explicit_number* static tgba_digraph*
sat_build(const satsolver::solution& solution, dict& satdict, sat_build(const satsolver::solution& solution, dict& satdict,
const tgba* aut, bool state_based) const tgba* aut, bool state_based)
{ {
bdd_dict* autdict = aut->get_dict(); auto autdict = aut->get_dict();
tgba_explicit_number* a = new tgba_explicit_number(autdict); auto a = new tgba_digraph(autdict);
autdict->register_all_variables_of(aut, a); autdict->register_all_variables_of(aut, a);
const ltl::formula* t = ltl::constant::true_instance(); const ltl::formula* t = ltl::constant::true_instance();
bdd acc = bdd_ithvar(autdict->register_acceptance_variable(t, a)); bdd acc = bdd_ithvar(autdict->register_acceptance_variable(t, a));
a->set_acceptance_conditions(acc); a->set_acceptance_conditions(acc);
for (int s = 1; s < satdict.cand_size; ++s) auto& g = a->get_graph();
a->add_state(s); g.new_states(satdict.cand_size);
state_explicit_number::transition* last_aut_trans = 0; unsigned last_aut_trans = -1U;
const transition* last_sat_trans = 0; const transition* last_sat_trans = nullptr;
#if DEBUG #if DEBUG
std::fstream out("dtba-sat.dbg", std::fstream out("dtba-sat.dbg",
...@@ -694,11 +694,8 @@ namespace spot ...@@ -694,11 +694,8 @@ namespace spot
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::set<int> acc_states; std::set<int> acc_states;
std::set<src_cond> seen_trans; std::set<src_cond> seen_trans;
for (satsolver::solution::const_iterator i = solution.begin(); for (int v: solution)
i != solution.end(); ++i)
{ {
int v = *i;
if (v < 0) // FIXME: maybe we can have (v < NNN)? if (v < 0) // FIXME: maybe we can have (v < NNN)?
continue; continue;
...@@ -714,17 +711,19 @@ namespace spot ...@@ -714,17 +711,19 @@ namespace spot
if (seen_trans.insert(src_cond(t->second.src, if (seen_trans.insert(src_cond(t->second.src,
t->second.cond)).second) t->second.cond)).second)
{ {
last_aut_trans = a->create_transition(t->second.src, bdd accept = bddfalse;
t->second.dst);
last_aut_trans->condition = t->second.cond;
last_sat_trans = &t->second;
dout << v << '\t' << t->second << \n";
// Mark the transition as accepting if the source is. // Mark the transition as accepting if the source is.
if (state_based if (state_based
&& acc_states.find(t->second.src) != acc_states.end()) && acc_states.find(t->second.src) != acc_states.end())
last_aut_trans->acceptance_conditions = acc; accept = acc;
last_aut_trans = g.new_transition(t->second.src - 1,
t->second.dst -1,
t->second.cond,
accept);
last_sat_trans = &t->second;
dout << v << '\t' << t->second << \n";
} }
} }
else else
...@@ -738,7 +737,7 @@ namespace spot ...@@ -738,7 +737,7 @@ namespace spot
assert(!state_based); assert(!state_based);
// This assumes that the SAT solvers output // This assumes that the SAT solvers output
// variables in increasing order. // variables in increasing order.
last_aut_trans->acceptance_conditions = acc; g.trans_data(last_aut_trans).acc = acc;
} }
else if (state_based) else if (state_based)
{ {
...@@ -754,53 +753,37 @@ namespace spot ...@@ -754,53 +753,37 @@ namespace spot
} }
#if DEBUG #if DEBUG
dout << "--- state_pair variables ---\n"; dout << "--- state_pair variables ---\n";
for (std::map<state_pair, int>::const_iterator pit = for (auto pit: satdict.prodid)
satdict.prodid.begin(); pit != satdict.prodid.end(); ++pit) if (positive.find(pit.second) != positive.end())
if (positive.find(pit->second) != positive.end()) dout << pit.second << '\t' << pit.first << "C\n";
dout << pit->second << '\t' << pit->first << "C\n";
else else
dout << -pit->second << "\t¬" << pit->first << "C\n"; dout << -pit.second << "\t¬" << pit.first << "C\n";
dout << "--- pathid_cand variables ---\n"; dout << "--- pathid_cand variables ---\n";
for (std::map<path, int>::const_iterator pit = for (auto pit: satdict.pathid_cand)
satdict.pathid_cand.begin(); if (positive.find(pit.second) != positive.end())
pit != satdict.pathid_cand.end(); ++pit) dout << pit.second << '\t' << pit.first << "C\n";
if (positive.find(pit->second) != positive.end())
dout << pit->second << '\t' << pit->first << "C\n";
else else
dout << -pit->second << "\t¬" << pit->first << "C\n"; dout << -pit.second << "\t¬" << pit.first << "C\n";
dout << "--- pathid_ref variables ---\n"; dout << "--- pathid_ref variables ---\n";
for (std::map<path, int>::const_iterator pit = for (auto pit: satdict.pathid_ref)
satdict.pathid_ref.begin(); if (positive.find(pit.second) != positive.end())
pit != satdict.pathid_ref.end(); ++pit) dout << pit.second << '\t' << pit.first << "R\n";
if (positive.find(pit->second) != positive.end())
dout << pit->second << '\t' << pit->first << "R\n";
else else
dout << -pit->second << "\t¬" << pit->first << "C\n"; dout << -pit.second << "\t¬" << pit.first << "C\n";
dout << "--- pathcand variables ---\n";
for (std::map<state_pair, int>::const_iterator pit =
satdict.pathcand.begin();
pit != satdict.pathcand.end(); ++pit)
if (positive.find(pit->second) != positive.end())
dout << pit->second << '\t' << pit->first << "C\n";
else
dout << -pit->second << "\t¬" << pit->first << "C\n";
#endif #endif
a->merge_transitions(); a->merge_transitions();
return a; return a;
} }
} }
tgba_explicit_number* tgba_digraph*
dtba_sat_synthetize(const tgba* a, int target_state_number, dtba_sat_synthetize(const tgba* a, int target_state_number,
bool state_based) bool state_based)
{ {
if (target_state_number == 0) if (target_state_number == 0)
return 0; return nullptr;
trace << "dtba_sat_synthetize(..., states = " << target_state_number trace << "dtba_sat_synthetize(..., states = " << target_state_number
<< ", state_based = " << state_based << ")\n"; << ", state_based = " << state_based << ")\n";
dict d; dict d;
...@@ -817,7 +800,7 @@ namespace spot ...@@ -817,7 +800,7 @@ namespace spot
solution = solver.get_solution(); solution = solver.get_solution();
t.stop("solve"); t.stop("solve");
tgba_explicit_number* res = 0; tgba_digraph* res = nullptr;
if (!solution.second.empty()) if (!solution.second.empty())
res = sat_build(solution.second, d, a, state_based); res = sat_build(solution.second, d, a, state_based);
...@@ -853,17 +836,17 @@ namespace spot ...@@ -853,17 +836,17 @@ namespace spot
return res; return res;
} }
tgba_explicit_number* tgba_digraph*
dtba_sat_minimize(const tgba* a, bool state_based) dtba_sat_minimize(const tgba* a, bool state_based)
{ {
int n_states = stats_reachable(a).states; int n_states = stats_reachable(a).states;
tgba_explicit_number* prev = 0; tgba_digraph* prev = nullptr;
for (;;) for (;;)
{ {
tgba_explicit_number* next = tgba_digraph* next =
dtba_sat_synthetize(prev ? prev : a, --n_states, state_based); dtba_sat_synthetize(prev ? prev : a, --n_states, state_based);
if (next == 0) if (!next)
break; break;
else else
n_states = stats_reachable(next).states; n_states = stats_reachable(next).states;
...@@ -874,19 +857,19 @@ namespace spot ...@@ -874,19 +857,19 @@ namespace spot
return prev; return prev;
} }
tgba_explicit_number* tgba_digraph*
dtba_sat_minimize_dichotomy(const tgba* a, bool state_based) dtba_sat_minimize_dichotomy(const tgba* a, bool state_based)
{ {
int max_states = stats_reachable(a).states - 1; int max_states = stats_reachable(a).states - 1;
int min_states = 1; int min_states = 1;
tgba_explicit_number* prev = 0; tgba_digraph* prev = nullptr;
while (min_states <= max_states) while (min_states <= max_states)
{ {
int target = (max_states + min_states) / 2; int target = (max_states + min_states) / 2;
tgba_explicit_number* next = tgba_digraph* next =
dtba_sat_synthetize(prev ? prev : a, target, state_based); dtba_sat_synthetize(prev ? prev : a, target, state_based);
if (next == 0) if (!next)
{ {
min_states = target + 1; min_states = target + 1;
} }
......
// -*- coding: utf-8 -*- // -*- 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. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_DTBASAT_HH #ifndef SPOT_TGBAALGOS_DTBASAT_HH
# define SPOT_TGBAALGOS_DTBASAT_HH # define SPOT_TGBAALGOS_DTBASAT_HH
#include "tgba/tgbaexplicit.hh" #include "tgba/tgbagraph.hh"
namespace spot namespace spot
{ {
...@@ -40,7 +40,7 @@ namespace spot ...@@ -40,7 +40,7 @@ namespace spot
/// ///
/// If no equivalent deterministic TBA with \a target_state_number /// If no equivalent deterministic TBA with \a target_state_number
/// states is found, a null pointer /// states is found, a null pointer
SPOT_API tgba_explicit_number* SPOT_API tgba_digraph*
dtba_sat_synthetize(const tgba* a, int target_state_number, dtba_sat_synthetize(const tgba* a, int target_state_number,
bool state_based = false); bool state_based = false);
...@@ -50,7 +50,7 @@ namespace spot ...@@ -50,7 +50,7 @@ namespace spot
/// number of states, and returns the last successfully built TBA. /// number of states, and returns the last successfully built TBA.
/// ///
/// If no smaller TBA exist, this returns a null pointer. /// If no smaller TBA exist, this returns a null pointer.
SPOT_API tgba_explicit_number* SPOT_API tgba_digraph*
dtba_sat_minimize(const tgba* a, bool state_based = false); dtba_sat_minimize(const tgba* a, bool state_based = false);
/// \brief Attempt to minimize a deterministic TBA with a SAT solver. /// \brief Attempt to minimize a deterministic TBA with a SAT solver.
...@@ -59,7 +59,7 @@ namespace spot ...@@ -59,7 +59,7 @@ namespace spot
/// find the minimum number of states using a binary search. /// find the minimum number of states using a binary search.
// //
/// If no smaller TBA exist, this returns a null pointer. /// If no smaller TBA exist, this returns a null pointer.
SPOT_API tgba_explicit_number* SPOT_API tgba_digraph*
dtba_sat_minimize_dichotomy(const tgba* a, bool state_based = false); dtba_sat_minimize_dichotomy(const tgba* a, bool state_based = false);
} }
......
...@@ -841,21 +841,23 @@ namespace spot ...@@ -841,21 +841,23 @@ namespace spot
return std::make_pair(d.nvars, nclauses.nb_clauses()); return std::make_pair(d.nvars, nclauses.nb_clauses());
} }
static tgba_explicit_number* static tgba_digraph*
sat_build(const satsolver::solution& solution, dict& satdict, sat_build(const satsolver::solution& solution, dict& satdict,
const tgba* aut, bool state_based) const tgba* aut, bool state_based)
{ {
bdd_dict* autdict = aut->get_dict(); auto autdict = aut->get_dict();
tgba_explicit_number* a = new tgba_explicit_number(autdict); auto a = new tgba_digraph(autdict);
autdict->register_all_variables_of(aut, a); autdict->register_all_variables_of(aut, a);
autdict->unregister_all_typed_variables(bdd_dict::acc, aut); autdict->unregister_all_typed_variables(bdd_dict::acc, aut);
a->set_acceptance_conditions(satdict.all_cand_acc.back()); a->set_acceptance_conditions(satdict.all_cand_acc.back());
for (int s = 1; s < satdict.cand_size; ++s) auto& g = a->get_graph();
a->add_state(s); g.new_states(satdict.cand_size);
state_explicit_number::transition* last_aut_trans = 0; // Last transition set in the automaton.
const transition* last_sat_trans = 0; unsigned last_aut_trans = -1U;
// Last transition read from the SAT result.
const transition* last_sat_trans = nullptr;
#if DEBUG #if DEBUG
std::fstream out("dtgba-sat.dbg", std::fstream out("dtgba-sat.dbg",
...@@ -867,11 +869,8 @@ namespace spot ...@@ -867,11 +869,8 @@ namespace spot
dout << "--- transition variables ---\n"; dout << "--- transition variables ---\n";
std::map<int, bdd> state_acc; std::map<int, bdd> state_acc;
std::set<src_cond> seen_trans; std::set<src_cond> seen_trans;
for (satsolver::solution::const_iterator i = solution.begin(); for (int v: solution)
i != solution.end(); ++i)
{ {
int v = *i;
if (v < 0) // FIXME: maybe we can have (v < NNN)? if (v < 0) // FIXME: maybe we can have (v < NNN)?
continue; continue;
...@@ -887,20 +886,21 @@ namespace spot ...@@ -887,20 +886,21 @@ namespace spot
if (seen_trans.insert(src_cond(t->second.src, if (seen_trans.insert(src_cond(t->second.src,
t->second.cond)).second) t->second.cond)).second)
{ {
last_aut_trans = a->create_transition(t->second.src, bdd acc = bddfalse;
t->second.dst);
last_aut_trans->condition = t->second.cond;
last_sat_trans = &t->second;
dout << v << '\t' << t->second << \n";
if (state_based) if (state_based)
{ {
std::map<int, bdd>::const_iterator i = auto i = state_acc.find(t->second.src);
state_acc.find(t->second.src);
if (i != state_acc.end()) if (i != state_acc.end())
last_aut_trans->acceptance_conditions = i->second; acc = i->second;
} }
last_aut_trans = g.new_transition(t->second.src - 1,
t->second.dst - 1,
t->second.cond,
acc);
last_sat_trans = &t->second;
dout << v << '\t' << t->second << \n";
} }
} }
else else
...@@ -919,7 +919,7 @@ namespace spot ...@@ -919,7 +919,7 @@ namespace spot
ta->second.dst == last_sat_trans->dst) ta->second.dst == last_sat_trans->dst)
{ {
assert(!state_based); assert(!state_based);
last_aut_trans->acceptance_conditions |= ta->second.acc; g.trans_data(last_aut_trans).acc |= ta->second.acc;
} }
else if (state_based) else if (state_based)
{ {
...@@ -930,11 +930,9 @@ namespace spot ...@@ -930,11 +930,9 @@ namespace spot
} }
#if DEBUG #if DEBUG
dout << "--- pathid variables ---\n"; dout << "--- pathid variables ---\n";
for (std::map<path, int>::const_iterator pit = for (auto pit: satdict.pathid)
satdict.pathid.begin(); if (positive.find(pit.second) != positive.end())
pit != satdict.pathid.end(); ++pit) dout << pit.second << '\t' << pit.first << "C\n";
if (positive.find(pit->second) != positive.end())
dout << pit->second << '\t' << pit->first << "C\n";
#endif #endif
a->merge_transitions(); a->merge_transitions();
...@@ -943,12 +941,12 @@ namespace spot ...@@ -943,12 +941,12 @@ namespace spot
} }
} }
tgba_explicit_number* tgba_digraph*
dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number, dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number,
int target_state_number, bool state_based) int target_state_number, bool state_based)
{ {
if (target_state_number == 0) if (target_state_number == 0)
return 0; return nullptr;
trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number
<< ", states = " << target_state_number << ", states = " << target_state_number
<< ", state_based = " << state_based << ")\n"; << ", state_based = " << state_based << ")\n";
...@@ -968,7 +966,7 @@ namespace spot ...@@ -968,7 +966,7 @@ namespace spot
solution = solver.get_solution(); solution = solver.get_solution();
t.stop("solve"); t.stop("solve");
tgba_explicit_number* res = 0; tgba_digraph* res = nullptr;
if (!solution.second.empty()) if (!solution.second.empty())
res = sat_build(solution.second, d, a, state_based); res = sat_build(solution.second, d, a, state_based);
...@@ -1004,19 +1002,19 @@ namespace spot ...@@ -1004,19 +1002,19 @@ namespace spot
return res; return res;
} }
tgba_explicit_number* tgba_digraph*
dtgba_sat_minimize(const tgba* a, unsigned target_acc_number, dtgba_sat_minimize(const tgba* a, unsigned target_acc_number,
bool state_based) bool state_based)
{ {
int n_states = stats_reachable(a).states; int n_states = stats_reachable(a).states;
tgba_explicit_number* prev = 0; tgba_digraph* prev = nullptr;
for (;;) for (;;)
{ {
tgba_explicit_number* next = tgba_digraph* next =
dtgba_sat_synthetize(prev ? prev : a, target_acc_number, dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
--n_states, state_based); --n_states, state_based);
if (next == 0) if (!next)
break; break;
else else
n_states = stats_reachable(next).states; n_states = stats_reachable(next).states;
...@@ -1026,21 +1024,21 @@ namespace spot ...@@ -1026,21 +1024,21 @@ namespace spot
return prev; return prev;
} }
tgba_explicit_number* tgba_digraph*
dtgba_sat_minimize_dichotomy(const tgba* a, unsigned target_acc_number, dtgba_sat_minimize_dichotomy(const tgba* a, unsigned target_acc_number,
bool state_based) bool state_based)
{ {
int max_states = stats_reachable(a).states - 1; int max_states = stats_reachable(a).states - 1;
int min_states = 1; int min_states = 1;
tgba_explicit_number* prev = 0; tgba_digraph* prev = nullptr;
while (min_states <= max_states) while (min_states <= max_states)
{ {
int target = (max_states + min_states) / 2; int target = (max_states + min_states) / 2;
tgba_explicit_number* next = tgba_digraph* next =
dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target, dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target,
state_based); state_based);
if (next == 0) if (!next)
{ {
min_states = target + 1; min_states = target + 1;
} }
......
// -*- coding: utf-8 -*- // -*- 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. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
#ifndef SPOT_TGBAALGOS_DTGBASAT_HH #ifndef SPOT_TGBAALGOS_DTGBASAT_HH
# define SPOT_TGBAALGOS_DTGBASAT_HH # define SPOT_TGBAALGOS_DTGBASAT_HH
#include "tgba/tgbaexplicit.hh" #include "tgba/tgbagraph.hh"
namespace spot namespace spot
{ {
...@@ -44,7 +44,7 @@ namespace spot ...@@ -44,7 +44,7 @@ namespace spot
/// acceptance sets and target_state_number states that is /// acceptance sets and target_state_number states that is
/// equivalent to \a a. If no such TGBA is found, a null pointer is /// equivalent to \a a. If no such TGBA is found, a null pointer is
/// returned. /// returned.
SPOT_API tgba_explicit_number* SPOT_API tgba_digraph*
dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number, dtgba_sat_synthetize(const tgba* a, unsigned target_acc_number,
int target_state_number,