alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Introduce simplify_mealy

Browse source 
Convenience function dispatching to
minimize_mealy and reduce_mealy.
Change tests accordingly

* spot/twaalgos/mealy_machine.cc,
  spot/twaalgos/mealy_machine.hh: Here
* bin/ltlsynt.cc: Use simplify
* spot/twaalgos/synthesis.cc,
  spot/twaalgos/synthesis.hh: Remove
 minimization, Update options
* tests/core/ltlsynt.test,
  tests/python/synthesis.ipynb,
  tests/python/_synthesis.ipynb: Adapt
This commit is contained in:
Philipp Schlehuber-Caissier 2022-03-18 15:27:46 +01:00
parent 86de4d4052
commit 97fc3f6c0b
8 changed files with 901 additions and 327 deletions
Download patch file Download diff file Expand all files Collapse all files

167
spot/twaalgos/mealy_machine.cc
View file

@ -135,11 +135,12 @@ namespace spot
if (!is_mealy(m))
return false;
if (m->get_named_prop<region_t>("state-player") == nullptr)
if (!m->get_named_prop<region_t>("state-player"))
{
trace << "is_split_mealy(): Split mealy machine must define the named "
"property \"state-player\"!\n";
}
auto sp = get_state_players(m);
if (sp.size() != m->num_states())
@ -1027,6 +1028,28 @@ namespace
std::pair<const_twa_graph_ptr, unsigned>
reorganize_mm(const_twa_graph_ptr mm, const std::vector<bool>& sp)
{
// Check if the twa_graph already has the correct form
{
auto sp = get_state_players(mm);
// All player states mus be at the end
bool is_ok = true;
bool seen_player = false;
for (const auto& p : sp)
{
if (seen_player & !p)
{
is_ok = false;
break;
}
seen_player |= p;
}
if (is_ok)
return {mm,
mm->num_states()
- std::accumulate(sp.begin(), sp.end(), 0)};
}
// We actually need to generate a new graph with the correct
// form
// Purge unreachable and reorganize the graph
std::vector<unsigned> renamed(mm->num_states(), -1u);
const unsigned n_old = mm->num_states();
@ -3607,7 +3630,7 @@ namespace spot
twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm,
int premin)
{
assert(is_split_mealy(mm));
assert(is_mealy(mm));
stopwatch sw;
sw.start();
@ -3615,38 +3638,33 @@ namespace spot
if ((premin < -1) || (premin > 1))
throw std::runtime_error("premin has to be -1, 0 or 1");
auto orig_spref = get_state_players(mm);
// Check if finite traces exist
// If so, deactivate fast minimization
// todo : this is overly conservative
// If unreachable states have no outgoing edges we do not care
// but testing this as well starts to be expensive...
if (premin != -1
&& [&]()
{
for (unsigned s = 0; s < mm->num_states(); ++s)
{
auto eit = mm->out(s);
if (eit.begin() == eit.end())
return true;
}
return false;
}())
premin = -1;
auto do_premin = [&]()->const_twa_graph_ptr
{
if (premin == -1)
return mm;
{
if (!mm->get_named_prop<region_t>("state-player"))
return split_2step(mm, false);
else
return mm;
}
else
{
bool is_split = mm->get_named_prop<region_t>("state-player");
// We have a split machine -> unsplit then resplit,
// as reduce mealy works on separated
auto mms = unsplit_mealy(mm);
reduce_mealy_here(mms, premin == 1);
split_separated_mealy_here(mms);
return mms;
twa_graph_ptr mms;
if (is_split)
{
auto mmi = unsplit_2step(mm);
reduce_mealy_here(mmi, premin == 1);
split_separated_mealy_here(mmi);
return mmi;
}
else
{
auto mms = reduce_mealy(mm, premin == 1);
return split_2step(mms, false);
}
}
};
@ -3689,9 +3707,13 @@ namespace spot
auto early_exit = [&]()
{
// Always keep machines split
assert(is_split_mealy_specialization(mm, mmw));
if (mm->get_named_prop<region_t>("state-player"))
assert(is_split_mealy_specialization(mm, mmw));
else
assert(is_split_mealy_specialization(split_2step(mm, false),
mmw));
return std::const_pointer_cast<twa_graph>(mmw);
};
};
// If the partial solution has the same number of
// states as the original automaton -> we are done
@ -3897,4 +3919,91 @@ namespace spot
return p;
}
void
simplify_mealy_here(twa_graph_ptr& m, int minimize_lvl,
bool split_out)
{
auto si = synthesis_info();
si.minimize_lvl = minimize_lvl;
return simplify_mealy_here(m, si, split_out);
}
void
simplify_mealy_here(twa_graph_ptr& m, synthesis_info& si,
bool split_out)
{
const auto minimize_lvl = si.minimize_lvl;
assert(is_mealy(m)
&& "simplify_mealy_here(): m is not a mealy machine!");
if (minimize_lvl < 0 || 5 < minimize_lvl)
throw std::runtime_error("simplify_mealy_here(): minimize_lvl "
"must be between 0 and 5.");
stopwatch sw;
if (si.bv)
sw.start();
bool is_separated = false;
if (0 < minimize_lvl && minimize_lvl < 3)
{
// unsplit if necessary
if (m->get_named_prop<region_t>("state-player"))
{
m = unsplit_mealy(m);
is_separated = true;
}
reduce_mealy_here(m, minimize_lvl == 2);
}
else if (3 <= minimize_lvl)
m = minimize_mealy(m, minimize_lvl - 4);
// Convert to demanded output format
bool is_split = m->get_named_prop<region_t>("state-player");
if (minimize_lvl == 0)
{
if (is_split && !split_out)
m = unsplit_mealy(m);
else if (!is_split && split_out)
m = split_2step(m, false);
}
else if (0 < minimize_lvl && minimize_lvl < 3 && split_out)
{
if (is_separated)
split_separated_mealy_here(m);
else
m = split_2step(m, false);
}
else if (3 <= minimize_lvl && !split_out)
m = unsplit_mealy(m);
if (si.bv)
{
if (si.verbose_stream)
*si.verbose_stream << "simplification took " << sw.stop()
<< " seconds\n";
si.bv->simplify_strat_time += sw.stop();
auto n_s_env = 0u;
auto n_e_env = 0u;
if (auto sp = m->get_named_prop<region_t>("state-player"))
{
n_s_env = sp->size() - std::accumulate(sp->begin(),
sp->end(),
0u);
std::for_each(m->edges().begin(), m->edges().end(),
[&n_e_env, &sp](const auto& e)
{
n_e_env += (*sp)[e.src];
});
}
else
{
n_s_env = m->num_states();
n_e_env = m->num_edges();
}
si.bv->nb_simpl_strat_states += n_s_env;
si.bv->nb_simpl_strat_edges += n_e_env;
}
}
}

23
spot/twaalgos/mealy_machine.hh
View file

@ -23,6 +23,9 @@
namespace spot
{
// Forward decl
struct synthesis_info;
/// todo
/// Comment je faire au mieux pour expliquer mealy dans les doc
@ -104,7 +107,7 @@ namespace spot
bool output_assignment = false);
/// @}
/// \brief Minimizes a split (in)completely specified mealy machine
/// \brief Minimizes an (in)completely specified mealy machine
/// The approach is described in \todo TACAS
/// \param premin Use reduce_mealy before applying the
/// main algorithm if demanded AND
@ -138,4 +141,22 @@ namespace spot
SPOT_API twa_graph_ptr
mealy_product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \brief Convenience function to call minimize_mealy or reduce_mealy.
/// Uses the same convention as ltlsynt for \a minimize_lvl:
/// 0: no reduction
/// 1: bisimulation based reduction
/// 2: bisimulation with output assignment
/// 3: SAT minimization
/// 4: 1 then 3
/// 5: 2 then 3
/// Minimizes the given machine \a m inplace, the parameter
/// \a split_out defines whether it is split or not
SPOT_API void
simplify_mealy_here(twa_graph_ptr& m, int minimize_lvl,
bool split_out);
SPOT_API void
simplify_mealy_here(twa_graph_ptr& m, synthesis_info& si,
bool split_out);
}

26
spot/twaalgos/synthesis.cc
View file

@ -1051,22 +1051,25 @@ namespace spot
if (!get_state_winner(arena, arena->get_init_state_number()))
return nullptr;
// If we use minimizations 0,1 or 2 -> unsplit
const bool do_unsplit = gi.minimize_lvl < 3;
auto m = apply_strategy(arena, do_unsplit, false);
auto m = apply_strategy(arena, false, false);
m->prop_universal(true);
if ((0 < gi.minimize_lvl) && (gi.minimize_lvl < 3))
reduce_mealy_here(m, gi.minimize_lvl == 2);
else if (gi.minimize_lvl >= 3)
m = minimize_mealy(m, gi.minimize_lvl - 4);
if (gi.bv)
{
auto sp = get_state_players(m);
auto n_s_env = sp.size() - std::accumulate(sp.begin(),
sp.end(),
0u);
auto n_e_env = 0u;
std::for_each(m->edges().begin(), m->edges().end(),
[&n_e_env, &sp](const auto& e)
{
n_e_env += sp[e.src];
});
gi.bv->strat2aut_time += sw.stop();
gi.bv->nb_strat_states += m->num_states();
gi.bv->nb_strat_edges += m->num_edges();
gi.bv->nb_strat_states += n_s_env;
gi.bv->nb_strat_edges += n_e_env;
}
assert(is_mealy(m));
@ -1200,7 +1203,8 @@ namespace spot
{
*vs << "direct strategy was found.\n"
<< "direct strat has " << strat->num_states()
<< " states and " << strat->num_sets() << " colors\n";
<< " states, " << strat->num_edges()
<< " edges and " << strat->num_sets() << " colors\n";
}
return mealy_like{
mealy_like::realizability_code::REALIZABLE_REGULAR,

3
spot/twaalgos/synthesis.hh
View file

@ -96,11 +96,14 @@ namespace spot
double paritize_time = 0.0;
double solve_time = 0.0;
double strat2aut_time = 0.0;
double simplify_strat_time = 0.0;
double aig_time = 0.0;
unsigned nb_states_arena = 0;
unsigned nb_states_arena_env = 0;
unsigned nb_strat_states = 0;
unsigned nb_strat_edges = 0;
unsigned nb_simpl_strat_states = 0;
unsigned nb_simpl_strat_edges = 0;
unsigned nb_latches = 0;
unsigned nb_gates = 0;
bool realizable = false;