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

Renaming and clean up

Browse source 
"Strategy" was used for mealy machines and game strategies a like.
Introduced the notion of mealy machine in three different flavors:
mealy machine: twa_graph with synthesis-outputs
separated mealy machine: mealy machine and all transitions
have conditions of the form (bdd over inputs)&(bdd over outputs)
split mealy machine: mealy machine that alternates between
env and player states. Needs state-players

* bin/ltlsynt.cc: renaming
* python/spot/impl.i: Add vector for const_twa_graph_ptr
* spot/twaalgos/aiger.cc,
spot/twaalgos/aiger.hh: Adapting functions
* spot/twaalgos/mealy_machine.cc,
spot/twaalgos/mealy_machine.hh: Add test functions and
propagate properties correctly. Adjust for names
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Removing unnecessary functions
and adapt to new names
* tests/python/aiger.py,
tests/python/_mealy.ipynb,
tests/python/mealy.py,
tests/python/synthesis.ipynb: Adjust
This commit is contained in:
philipp 2021-11-04 00:24:17 +01:00
parent 6ebe3d7447
commit 98ebbea17e
12 changed files with 3376 additions and 3038 deletions
Download patch file Download diff file Expand all files Collapse all files

108
bin/ltlsynt.cc
View file

@ -36,6 +36,7 @@
#include <spot/twaalgos/game.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/mealy_machine.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/translate.hh>
@ -344,7 +345,7 @@ namespace
auto sub_f = sub_form.begin();
auto sub_o = sub_outs_str.begin();
std::vector<spot::strategy_like_t> strategies;
std::vector<spot::mealy_like> mealy_machines;
auto print_game = want_game ?
[](const spot::twa_graph_ptr& game)->void
@ -359,27 +360,27 @@ namespace
for (; sub_f != sub_form.end(); ++sub_f, ++sub_o)
{
spot::strategy_like_t strat
spot::mealy_like m_like
{
spot::strategy_like_t::realizability_code::UNKNOWN,
spot::mealy_like::realizability_code::UNKNOWN,
nullptr,
bddfalse
};
// If we want to print a game,
// we never use the direct approach
if (!want_game)
strat =
m_like =
spot::try_create_direct_strategy(*sub_f, *sub_o, *gi);
switch (strat.success)
switch (m_like.success)
{
case spot::strategy_like_t::realizability_code::UNREALIZABLE:
case spot::mealy_like::realizability_code::UNREALIZABLE:
{
std::cout << "UNREALIZABLE" << std::endl;
safe_tot_time();
return 1;
}
case spot::strategy_like_t::realizability_code::UNKNOWN:
case spot::mealy_like::realizability_code::UNKNOWN:
{
auto arena = spot::ltl_to_game(*sub_f, *sub_o, *gi);
if (gi->bv)
@ -404,55 +405,75 @@ namespace
// only if we need it
if (!opt_real)
{
spot::strategy_like_t sl;
sl.success =
spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR;
sl.strat_like = spot::create_strategy(arena, *gi);
sl.glob_cond = bddfalse;
strategies.push_back(sl);
spot::mealy_like ml;
ml.success =
spot::mealy_like::realizability_code::REALIZABLE_REGULAR;
ml.mealy_like =
spot::solved_game_to_separated_mealy(arena, *gi);
ml.glob_cond = bddfalse;
mealy_machines.push_back(ml);
}
break;
}
case spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR:
case spot::mealy_like::realizability_code::REALIZABLE_REGULAR:
{
// the direct approach yielded a strategy
// which can now be minimized
// We minimize only if we need it
assert(strat.strat_like && "Expected success but found no strat!");
assert(m_like.mealy_like && "Expected success but found no mealy!");
if (!opt_real)
{
spot::stopwatch sw_min;
sw_min.start();
unsigned simplify = gi->minimize_lvl;
bool do_split = 3 <= simplify;
if (do_split)
strat.strat_like =
split_2step(strat.strat_like,
spot::get_synthesis_outputs(strat.strat_like),
spot::stopwatch sw_direct;
sw_direct.start();
if ((0 < gi->minimize_lvl) && (gi->minimize_lvl < 3))
// Uses reduction or not,
// both work with mealy machines (non-separated)
reduce_mealy_here(m_like.mealy_like, gi->minimize_lvl == 2);
auto delta = sw_direct.stop();
sw_direct.start();
// todo better algo here?
m_like.mealy_like =
split_2step(m_like.mealy_like,
spot::get_synthesis_outputs(m_like.mealy_like),
false);
minimize_strategy_here(strat.strat_like, simplify);
if (do_split)
strat.strat_like = spot::unsplit_2step(strat.strat_like);
auto delta = sw_min.stop();
if (gi->bv)
gi->bv->split_time += sw_direct.stop();
sw_direct.start();
if (gi->minimize_lvl >= 3)
{
sw_direct.start();
// actual minimization, works on split mealy
m_like.mealy_like = minimize_mealy(m_like.mealy_like,
gi->minimize_lvl - 4);
delta = sw_direct.stop();
}
// Unsplit to have separated mealy
m_like.mealy_like = unsplit_mealy(m_like.mealy_like);
if (gi->bv)
gi->bv->strat2aut_time += delta;
if (gi->verbose_stream)
*gi->verbose_stream << "final strategy has "
<< strat.strat_like->num_states()
<< m_like.mealy_like->num_states()
<< " states and "
<< strat.strat_like->num_edges()
<< m_like.mealy_like->num_edges()
<< " edges\n"
<< "minimization took " << delta
<< " seconds\n";
}
SPOT_FALLTHROUGH;
}
case spot::strategy_like_t::realizability_code::REALIZABLE_DTGBA:
case spot::mealy_like::realizability_code::REALIZABLE_DTGBA:
if (!opt_real)
strategies.push_back(strat);
mealy_machines.push_back(m_like);
break;
default:
error(2, 0, "unexpected success code during strategy generation "
error(2, 0, "unexpected success code during mealy machine generation "
"(please send bug report)");
}
}
@ -472,8 +493,9 @@ namespace
}
// If we reach this line
// a strategy was found for each subformula
assert(strategies.size() == sub_form.size()
&& "Strategies are missing");
assert(mealy_machines.size() == sub_form.size()
&& "There are subformula for which no mealy like object"
"has been created.");
spot::aig_ptr saig = nullptr;
spot::twa_graph_ptr tot_strat = nullptr;
@ -485,7 +507,7 @@ namespace
spot::stopwatch sw2;
if (gi->bv)
sw2.start();
saig = spot::strategies_to_aig(strategies, opt_print_aiger,
saig = spot::mealy_machines_to_aig(mealy_machines, opt_print_aiger,
input_aps,
sub_outs_str);
if (gi->bv)
@ -507,14 +529,14 @@ namespace
else
{
assert(std::all_of(
strategies.begin(), strategies.end(),
[](const auto& sl)
{return sl.success ==
spot::strategy_like_t::realizability_code::REALIZABLE_REGULAR; })
&& "ltlsynt: Can not handle TGBA as strategy.");
tot_strat = strategies.front().strat_like;
for (size_t i = 1; i < strategies.size(); ++i)
tot_strat = spot::product(tot_strat, strategies[i].strat_like);
mealy_machines.begin(), mealy_machines.end(),
[](const auto& ml)
{return ml.success ==
spot::mealy_like::realizability_code::REALIZABLE_REGULAR; })
&& "ltlsynt: Cannot handle TGBA as strategy.");
tot_strat = mealy_machines.front().mealy_like;
for (size_t i = 1; i < mealy_machines.size(); ++i)
tot_strat = spot::product(tot_strat, mealy_machines[i].mealy_like);
printer.print(tot_strat, timer_printer_dummy);
}

3
python/spot/impl.i
View file

@ -461,6 +461,8 @@ static void handle_any_exception()
%include <spot/misc/trival.hh>
%implicitconv std::vector<spot::formula>;
%implicitconv std::vector<spot::twa_graph_ptr>;
%implicitconv std::vector<spot::const_twa_graph_ptr>;
%implicitconv spot::formula;
%implicitconv std::vector<bool>;
@ -670,6 +672,7 @@ def state_is_accepting(self, src) -> "bool":
%template(scc_info_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_all>;
%template(scc_info_inner_scc_edges) spot::internal::scc_edges<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data> const, spot::internal::keep_inner_scc>;
%template(vector_twa_graph) std::vector<spot::twa_graph_ptr>;
%template(vector_const_twa_graph) std::vector<spot::const_twa_graph_ptr>;
%include <spot/twaalgos/strength.hh>
%include <spot/twaalgos/sccfilter.hh>
%include <spot/twaalgos/stats.hh>

197
spot/twaalgos/aiger.cc
View file

@ -34,6 +34,7 @@
#include <spot/twa/twagraph.hh>
#include <spot/misc/bddlt.hh>
#include <spot/misc/minato.hh>
#include <spot/twaalgos/mealy_machine.hh>
#include <spot/twaalgos/synthesis.hh>
#define STR(x) #x
@ -1201,12 +1202,20 @@ namespace spot
};
std::vector<bdd> outbddvec;
outbddvec.reserve(output_names_.size());
for (auto& ao : output_names_)
outbddvec.push_back(bdd_ithvar(aut->register_ap(ao)));
// Also register the ins
for (auto& ai : input_names_)
aut->register_ap(ai);
// Set the named prop
set_synthesis_outputs(aut,
std::accumulate(outbddvec.begin(), outbddvec.end(),
(bdd) bddtrue,
[](const bdd& b1, const bdd& b2) -> bdd
{return b1 & b2; }));
std::vector<bdd> outcondbddvec;
for (auto ov : outputs_)
outcondbddvec.push_back(aigvar2bdd(ov));
@ -1387,8 +1396,6 @@ namespace
{
assert(e.cond != bddfalse);
bdd bout = bdd_exist(e.cond, all_inputs);
assert(((bout & bdd_existcomp(e.cond, all_inputs)) == e.cond) &&
"Precondition (in) & (out) == cond violated");
// low is good, dc is ok, high is bad
this_outc[astrat.first->edge_number(e)] =
bdd_satoneshortest(bout, 0, 1, 5);
@ -1447,9 +1454,9 @@ namespace
const std::vector<std::string>& unused_ins = {},
const std::vector<std::string>& unused_outs = {})
{
// The aiger circuit cannot encode the acceptance condition
// Test that the acceptance condition is true
for (auto&& astrat : strat_vec)
// The aiger circuit can currently noly encode separated mealy machines
for (const auto& astrat : strat_vec)
if (!astrat.first->acc().is_t())
{
std::cerr << "Acc cond must be true not " << astrat.first->acc()
@ -1457,6 +1464,10 @@ namespace
throw std::runtime_error("Cannot turn automaton into "
"aiger circuit");
}
// This checks the acc again, but does more and is to
// costly for non-debug mode
assert(std::all_of(strat_vec.begin(), strat_vec.end(),
[](const auto& p){ return is_separated_mealy(p.first); }));
// get the propositions
std::vector<std::string> input_names;
@ -1840,56 +1851,40 @@ namespace spot
{
aig_ptr
strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode)
mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode)
{
if (!aut)
throw std::runtime_error("aut cannot be null");
if (!m)
throw std::runtime_error("mealy_machine_to_aig(): "
"m cannot be null");
return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode);
return auts_to_aiger({{m, get_synthesis_outputs(m)}}, mode);
}
aig_ptr
strategies_to_aig(const std::vector<const_twa_graph_ptr>& strat_vec,
const char *mode)
mealy_machine_to_aig(const mealy_like& m, const char* mode)
{
std::for_each(strat_vec.begin()+1, strat_vec.end(),
[usedbdd = strat_vec.at(0)->get_dict()](const auto& s)
{
if (usedbdd != s->get_dict())
throw std::runtime_error("All strategies have to "
"share a bdd_dict!\n");
});
if (m.success != mealy_like::realizability_code::REALIZABLE_REGULAR)
throw std::runtime_error("mealy_machine_to_aig(): "
"Can only handle regular mealy machine, TBD");
std::vector<std::pair<const_twa_graph_ptr, bdd>> new_vec;
new_vec.reserve(strat_vec.size());
bdd all_outputs = bddtrue;
for (auto& astrat : strat_vec)
{
bdd this_outputs = get_synthesis_outputs(astrat);
// Check if outs do not overlap
if (bdd_and(bdd_not(this_outputs), all_outputs) == bddfalse)
throw std::runtime_error("\"outs\" of strategies are not "
"distinct!.\n");
all_outputs &= this_outputs;
new_vec.emplace_back(astrat, this_outputs);
}
return auts_to_aiger(new_vec, mode);
return mealy_machine_to_aig(m.mealy_like, mode);
}
aig_ptr
strategy_to_aig(const twa_graph_ptr &aut, const char *mode,
mealy_machine_to_aig(const twa_graph_ptr &m, const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::string>& outs)
{
if (!aut)
throw std::runtime_error("aut cannot be null");
if (!m)
throw std::runtime_error("mealy_machine_to_aig(): "
"m cannot be null");
// Make sure ins and outs are disjoint
{
std::vector<std::string> all_ap = ins;
all_ap.insert(all_ap.end(), outs.begin(), outs.end());
check_double_names(all_ap, "Atomic propositions appears in input "
check_double_names(all_ap, "mealy_machine_to_aig(): "
"Atomic propositions appears in input "
"and output propositions; ");
}
// Check if there exist outs or ins that are not used by the
@ -1900,7 +1895,7 @@ namespace spot
std::vector<std::string> unused_ins;
{
std::set<std::string> used_aps;
for (const auto& f : aut->ap())
for (const auto& f : m->ap())
used_aps.insert(f.ap_name());
for (const auto& ao : outs)
if (!used_aps.count(ao))
@ -1910,25 +1905,90 @@ namespace spot
unused_ins.push_back(ai);
}
// todo Some additional checks?
return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode,
return auts_to_aiger({{m, get_synthesis_outputs(m)}}, mode,
unused_ins, unused_outs);
}
aig_ptr
mealy_machine_to_aig(mealy_like& m, const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::string>& outs)
{
if (m.success != mealy_like::realizability_code::REALIZABLE_REGULAR)
throw std::runtime_error("mealy_machine_to_aig(): "
"Can only handle regular mealy machine, TBD");
return mealy_machine_to_aig(m.mealy_like, mode, ins, outs);
}
aig_ptr
mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
const char *mode)
{
std::for_each(m_vec.begin()+1, m_vec.end(),
[usedbdd = m_vec.at(0)->get_dict()](const auto& s)
{
if (usedbdd != s->get_dict())
throw std::runtime_error("mealy_machines_to_aig(): "
"All machines have to "
"share a bdd_dict!\n");
});
std::vector<std::pair<const_twa_graph_ptr, bdd>> new_vec;
new_vec.reserve(m_vec.size());
bdd all_outputs = bddtrue;
for (auto& am : m_vec)
{
bdd this_outputs = get_synthesis_outputs(am);
// Check if outs do not overlap
if (bdd_and(bdd_not(this_outputs), all_outputs) == bddfalse)
throw std::runtime_error("mealy_machines_to_aig(): "
"\"outs\" of the machines are not "
"distinct!.\n");
all_outputs &= this_outputs;
new_vec.emplace_back(am, this_outputs);
}
return auts_to_aiger(new_vec, mode);
}
aig_ptr
mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
const char *mode)
{
if (std::any_of(m_vec.cbegin(), m_vec.cend(),
[](const auto& m)
{return m.success !=
mealy_like::realizability_code::REALIZABLE_REGULAR; }))
throw std::runtime_error("mealy_machines_to_aig(): "
"Can only handle regular mealy machine for "
"the moment, TBD");
auto new_vec = std::vector<const_twa_graph_ptr>();
new_vec.reserve(m_vec.size());
std::transform(m_vec.cbegin(), m_vec.cend(),
std::back_inserter(new_vec),
[](const auto& m){return m.mealy_like; });
return mealy_machines_to_aig(new_vec, mode);
}
// Note: This ignores the named property
aig_ptr
strategies_to_aig(const std::vector<twa_graph_ptr>& strat_vec,
mealy_machines_to_aig(const std::vector<twa_graph_ptr>& m_vec,
const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::vector<std::string>>& outs)
{
if (strat_vec.size() != outs.size())
throw std::runtime_error("Expected as many outs as strategies!\n");
if (m_vec.size() != outs.size())
throw std::runtime_error("mealy_machines_to_aig(): "
"Expected as many outs as strategies!\n");
std::for_each(strat_vec.begin()+1, strat_vec.end(),
[usedbdd = strat_vec.at(0)->get_dict()](auto&& it)
std::for_each(m_vec.begin()+1, m_vec.end(),
[usedbdd = m_vec.at(0)->get_dict()](auto&& it)
{
if (usedbdd != it->get_dict())
throw std::runtime_error("All strategies have to "
throw std::runtime_error("mealy_machines_to_aig(): "
"All strategies have to "
"share a bdd_dict!\n");
});
@ -1944,17 +2004,17 @@ namespace spot
}
std::vector<std::pair<const_twa_graph_ptr, bdd>> new_vec;
new_vec.reserve(strat_vec.size());
new_vec.reserve(m_vec.size());
std::set<std::string> used_aps;
for (size_t i = 0; i < strat_vec.size(); ++i)
for (size_t i = 0; i < m_vec.size(); ++i)
{
for (const auto& f : strat_vec[i]->ap())
for (const auto& f : m_vec[i]->ap())
used_aps.insert(f.ap_name());
// todo Some additional checks?
new_vec.emplace_back(strat_vec[i],
get_synthesis_outputs(strat_vec[i]));
new_vec.emplace_back(m_vec[i],
get_synthesis_outputs(m_vec[i]));
}
// Check if there exist outs or ins that are not used by the
@ -1975,15 +2035,15 @@ namespace spot
}
aig_ptr
strategies_to_aig(const std::vector<strategy_like_t>& strat_vec,
const char *mode,
mealy_machines_to_aig(const std::vector<mealy_like>& strat_vec,
const char* mode,
const std::vector<std::string>& ins,
const std::vector<std::vector<std::string>>& outs)
{
// todo extend to TGBA and possibly others
const unsigned ns = strat_vec.size();
std::vector<twa_graph_ptr> strategies;
strategies.reserve(ns);
std::vector<twa_graph_ptr> m_machines;
m_machines.reserve(ns);
std::vector<std::vector<std::string>> outs_used;
outs_used.reserve(ns);
@ -1991,27 +2051,28 @@ namespace spot
{
switch (strat_vec[i].success)
{
case strategy_like_t::realizability_code::UNREALIZABLE:
throw std::runtime_error("strategies_to_aig(): Partial strat is "
"not feasible!");
case strategy_like_t::realizability_code::UNKNOWN:
throw std::runtime_error("strategies_to_aig(): Partial strat has "
"unknown status!");
case strategy_like_t::realizability_code::REALIZABLE_REGULAR:
case mealy_like::realizability_code::UNREALIZABLE:
throw std::runtime_error("mealy_machines_to_aig(): One of the "
"mealy like machines is not realizable.");
case mealy_like::realizability_code::UNKNOWN:
throw std::runtime_error("mealy_machines_to_aig(): One of the"
"mealy like objects has "
"status \"unkwnown\"");
case mealy_like::realizability_code::REALIZABLE_REGULAR:
{
strategies.push_back(strat_vec[i].strat_like);
m_machines.push_back(strat_vec[i].mealy_like);
outs_used.push_back(outs[i]);
break;
}
case strategy_like_t::realizability_code::REALIZABLE_DTGBA:
throw std::runtime_error("strategies_to_aig(): TGBA not "
"yet supported.");
case mealy_like::realizability_code::REALIZABLE_DTGBA:
throw std::runtime_error("mealy_machines_to_aig(): TGBA not "
"yet supported - TBD");
default:
throw std::runtime_error("strategies_to_aig(): Unknown "
throw std::runtime_error("mealy_machines_to_aig(): Unknown "
"success identifier.");
}
}
return strategies_to_aig(strategies, mode, ins, outs_used);
return mealy_machines_to_aig(m_machines, mode, ins, outs_used);
}
std::ostream &
@ -2073,7 +2134,7 @@ namespace spot
print_aiger(std::ostream& os, const const_twa_graph_ptr& aut,
const char* mode)
{
print_aiger(os, strategy_to_aig(aut, mode));
print_aiger(os, mealy_machine_to_aig(aut, mode));
return os;
}
}

26
spot/twaalgos/aiger.hh
View file

@ -36,7 +36,7 @@
namespace spot
{
// Forward for synthesis
struct strategy_like_t;
struct mealy_like;
class aig;
@ -415,8 +415,8 @@ namespace spot
};
/// \ingroup synthesis
/// \brief Convert a strategy into an aig relying on the transformation
/// described by \a mode.
/// \brief Convert a mealy (like) machine into an aig relying on
/// the transformation described by \a mode.
/// \param mode This param has to be of the form
/// `ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2]`
/// Where `ite` means encoded via if-then-else normal form,
@ -437,9 +437,16 @@ namespace spot
/// outs are guaranteed to appear in the aiger circuit.
///@{
SPOT_API aig_ptr
strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode);
mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode);
SPOT_API aig_ptr
strategy_to_aig(const twa_graph_ptr& aut, const char *mode,
mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::string>& outs);
SPOT_API aig_ptr
mealy_machine_to_aig(const mealy_like& m, const char* mode);
SPOT_API aig_ptr
mealy_machine_to_aig(mealy_like& m, const char *mode,
const std::vector<std::string>& ins,
const std::vector<std::string>& outs);
///@}
@ -459,15 +466,18 @@ namespace spot
/// guaranteed to appear in the aiger circuit.
/// @{
SPOT_API aig_ptr
strategies_to_aig(const std::vector<const_twa_graph_ptr>& strat_vec,
mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
const char* mode);
SPOT_API aig_ptr
strategies_to_aig(const std::vector<twa_graph_ptr>& strat_vec,
mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
const char* mode);
SPOT_API aig_ptr
mealy_machines_to_aig(const std::vector<twa_graph_ptr>& m_vec,
const char* mode,
const std::vector<std::string>& ins,
const std::vector<std::vector<std::string>>& outs);
SPOT_API aig_ptr
strategies_to_aig(const std::vector<strategy_like_t>& strat_vec,
mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
const char* mode,
const std::vector<std::string>& ins,
const std::vector<std::vector<std::string>>& outs);

461
spot/twaalgos/mealy_machine.cc
View file

@ -33,6 +33,7 @@
#include <spot/misc/timer.hh>
#include <spot/misc/minato.hh>
#include <spot/twaalgos/game.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/synthesis.hh>
#include <picosat/picosat.h>
@ -52,11 +53,245 @@
# define dotimeprint while (0) std::cerr
#endif
namespace
{
bool is_deterministic_(const std::vector<bdd>& ins)
{
const unsigned n_ins = ins.size();
for (unsigned idx1 = 0; idx1 < n_ins - 1; ++idx1)
for (unsigned idx2 = idx1 + 1; idx2 < n_ins; ++idx2)
if (bdd_have_common_assignment(ins[idx1], ins[idx2]))
return false;
return true;
}
}
namespace spot
{
bool
is_mealy(const const_twa_graph_ptr& m)
{
if (!m->acc().is_t())
{
trace << "is_mealy(): Mealy machines must have "
"true acceptance condition.\n";
return false;
}
if (!m->get_named_prop<bdd>("synthesis-outputs"))
{
trace << "is_mealy(): \"synthesis-outputs\" not found!\n";
return false;
}
return true;
}
bool
is_separated_mealy(const const_twa_graph_ptr& m)
{
if (!is_mealy(m))
return false;
auto outs = get_synthesis_outputs(m);
for (const auto& e : m->edges())
if ((bdd_exist(e.cond, outs) & bdd_existcomp(e.cond, outs)) != e.cond)
{
trace << "is_separated_mealy_machine(): Edge number "
<< m->edge_number(e) << " from " << e.src << " to " << e.dst
<< " with " << e.cond << " is not separated!\n";
return false;
}
return true;
}
bool
is_split_mealy(const const_twa_graph_ptr& m)
{
if (!is_mealy(m))
return false;
if (m->get_named_prop<region_t>("state-player") == nullptr)
{
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())
{
trace << "\"state-player\" has not the same size as the "
"automaton!\n";
return false;
}
if (sp[m->get_init_state_number()])
{
trace << "is_split_mealy(): Initial state must be owned by env!\n";
return false;
}
auto outs = get_synthesis_outputs(m);
for (const auto& e : m->edges())
{
if (sp[e.src] == sp[e.dst])
{
trace << "is_split_mealy(): Edge number "
<< m->edge_number(e) << " from " << e.src << " to " << e.dst
<< " is not alternating!\n";
return false;
}
if (sp[e.src] && (bdd_exist(e.cond, outs) != bddtrue))
{
trace << "is_split_mealy(): Edge number "
<< m->edge_number(e) << " from " << e.src << " to " << e.dst
<< " depends on inputs, but should be labeled by outputs!\n";
return false;
}
if (!sp[e.src] && (bdd_existcomp(e.cond, outs) != bddtrue))
{
trace << "is_split_mealy(): Edge number "
<< m->edge_number(e) << " from " << e.src << " to " << e.dst
<< " depends on outputs, but should be labeled by inputs!\n";
return false;
}
}
return true;
}
bool
is_input_deterministic_mealy(const const_twa_graph_ptr& m)
{
if (!is_mealy(m))
return false;
const unsigned N = m->num_states();
auto sp_ptr = m->get_named_prop<region_t>("state-player");
// Unsplit mealy -> sp_ptr == nullptr
if (sp_ptr && !is_split_mealy(m))
return false;
auto outs = get_synthesis_outputs(m);
std::vector<bdd> ins;
for (unsigned s = 0; s < N; ++s)
{
if (sp_ptr && (*sp_ptr)[s])
continue;
ins.clear();
for (const auto& e : m->out(s))
ins.push_back(sp_ptr ? e.cond
: bdd_exist(e.cond, outs));
if (!is_deterministic_(ins))
{
trace << "is_input_deterministic_mealy(): State number "
<< s << " is not input determinisc!\n";
return false;
}
}
return true;
}
void
split_separated_mealy_here(const twa_graph_ptr& m)
{
assert(is_mealy(m));
auto output_bdd = get_synthesis_outputs(m);
struct dst_cond_color_t
{
std::pair<unsigned, int> dst_cond;
acc_cond::mark_t color;
};
auto hasher = [](const dst_cond_color_t& dcc) noexcept
{
return dcc.color.hash() ^ pair_hash()(dcc.dst_cond);
};
auto equal = [](const dst_cond_color_t& dcc1,
const dst_cond_color_t& dcc2) noexcept
{
return (dcc1.dst_cond == dcc2.dst_cond)
&& (dcc1.color == dcc2.color);
};
std::unordered_map<dst_cond_color_t, unsigned,
decltype(hasher),
decltype(equal)> player_map(m->num_edges(),
hasher, equal);
auto get_ps = [&](unsigned dst, const bdd& ocond,
acc_cond::mark_t color)
{
dst_cond_color_t key{std::make_pair(dst, ocond.id()),
color};
auto [it, inserted] =
player_map.try_emplace(key, m->num_states());
if (!inserted)
return it->second;
unsigned ns = m->new_state();
assert(ns == it->second);
m->new_edge(ns, dst, ocond, color);
return ns;
};
unsigned ne = m->edge_vector().size();
for (unsigned eidx = 1; eidx < ne; ++eidx)
{
const auto& e = m->edge_storage(eidx);
if (e.next_succ == eidx) // dead edge
continue;
bdd incond = bdd_exist(e.cond, output_bdd);
bdd outcond = bdd_existcomp(e.cond, output_bdd);
assert(((incond&outcond) == e.cond) && "Precondition violated");
// Create new state and trans
// this may invalidate "e".
unsigned new_dst = get_ps(e.dst, outcond, e.acc);
// redirect
auto& e2 = m->edge_storage(eidx);
e2.dst = new_dst;
e2.cond = incond;
}
auto* sp_ptr = m->get_or_set_named_prop<region_t>("state-player");
sp_ptr->resize(m->num_states());
std::fill(sp_ptr->begin(), sp_ptr->end(), false);
for (const auto& eit : player_map)
(*sp_ptr)[eit.second] = true;
//Done
}
twa_graph_ptr
split_separated_mealy(const const_twa_graph_ptr& m)
{
assert(is_mealy((m)));
auto m2 = make_twa_graph(m, twa::prop_set::all());
m2->copy_acceptance_of(m);
set_synthesis_outputs(m2, get_synthesis_outputs(m));
split_separated_mealy_here(m2);
return m2;
}
twa_graph_ptr
unsplit_mealy(const const_twa_graph_ptr& m)
{
assert(is_split_mealy(m));
return unsplit_2step(m);
}
}
namespace
{
// Anonymous for minimize_mealy_fast
// Anonymous for reduce_mealy
using namespace spot;
// Used to get the signature of the state.
@ -478,84 +713,33 @@ namespace
namespace spot
{
twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm,
bool use_inclusion)
twa_graph_ptr reduce_mealy(const const_twa_graph_ptr& mm,
bool output_assignment)
{
bool orig_is_split = true;
bdd* outsptr = nullptr;
bdd outs = bddfalse;
assert(is_mealy(mm));
if (mm->get_named_prop<std::vector<bool>>("state-player"))
throw std::runtime_error("reduce_mealy(): "
"Only works on unsplit machines.\n");
twa_graph_ptr mmc;
if (mm->get_named_prop<std::vector<bool>>("state-player") != nullptr)
{
outsptr = mm->get_named_prop<bdd>("synthesis-outputs");
assert(outsptr && "If the original strat is split, "
"we need \"synthesis-outputs\".");
outs = *outsptr;
mmc = unsplit_2step(mm);
}
else
{
mmc = make_twa_graph(mm, twa::prop_set::all());
auto mmc = make_twa_graph(mm, twa::prop_set::all());
mmc->copy_ap_of(mm);
mmc->copy_acceptance_of(mm);
orig_is_split = false;
}
set_synthesis_outputs(mmc, get_synthesis_outputs(mm));
minimize_mealy_fast_here(mmc, use_inclusion);
// Split if the initial aut was split
if (orig_is_split)
{
mmc = split_2step(mmc, outs, false);
bool orig_init_player =
mm->get_named_prop<std::vector<bool>>("state-player")
->at(mm->get_init_state_number());
alternate_players(mmc, orig_init_player, false);
}
// Try to set outputs
if (outsptr)
mmc->set_named_prop("synthesis-outputs", new bdd(outs));
reduce_mealy_here(mmc, output_assignment);
assert(is_mealy(mmc));
return mmc;
}
void minimize_mealy_fast_here(twa_graph_ptr& mm, bool use_inclusion)
void reduce_mealy_here(twa_graph_ptr& mm, bool output_assignment)
{
bool orig_is_split = false;
bdd* outsptr = nullptr;
bdd outs = bddfalse;
auto sp_ptr = mm->get_named_prop<std::vector<bool>>("state-player");
bool init_player = sp_ptr ? sp_ptr->at(mm->get_init_state_number())
: false;
assert(is_mealy(mm));
// Only consider infinite runs
mm->purge_dead_states();
if (mm->get_named_prop<std::vector<bool>>("state-player") != nullptr)
{
// Check if done
if (std::count(sp_ptr->begin(), sp_ptr->end(), false) == 1)
return;
outsptr = mm->get_named_prop<bdd>("synthesis-outputs");
assert(outsptr && "If the original strat is split, "
"we need \"synthesis-outputs\".");
outs = *outsptr;
init_player =
mm->get_named_prop<std::vector<bool>>("state-player")->at(
mm->get_init_state_number());
mm = unsplit_2step(mm);
orig_is_split = true;
}
else
// Check if done
if (mm->num_states() == 1)
return;
auto repr = get_repres(mm, use_inclusion);
auto repr = get_repres(mm, output_assignment);
if (repr[0] == -1U)
return;
@ -580,12 +764,7 @@ namespace spot
}
}
mm->purge_unreachable_states();
if (orig_is_split)
{
mm = split_2step(mm, outs, false);
alternate_players(mm, init_player, false);
mm->set_named_prop("synthesis-outputs", new bdd(outs));
}
assert(is_mealy(mm));
}
}
@ -639,7 +818,7 @@ namespace
template <class CONT, class PRED>
size_t find_first_index_of(const CONT& c, PRED pred)
{
size_t s = c.size();
const size_t s = c.size();
for (unsigned i = 0; i < s; ++i)
if (pred(c[i]))
return i;
@ -874,8 +1053,8 @@ namespace
std::vector<bool> spnew(n_new, true);
std::fill(spnew.begin(), spnew.begin()+n_env, false);
omm->set_named_prop("state-player",
new std::vector<bool>(std::move(spnew)));
set_state_players(omm, std::move(spnew));
set_synthesis_outputs(omm, get_synthesis_outputs(mm));
// Make sure we have a proper strategy,
// that is each player state has only one successor
@ -1217,7 +1396,7 @@ namespace
#ifdef TRACE
trace << "We found " << n_group << " groups.\n";
for (unsigned s = 0; s < n_env; ++s)
trace << s << " : " << which_group[s] << '\n';
trace << s << " : " << which_group.at(s) << '\n';
#endif
return std::make_pair(n_group, which_group);
}
@ -1640,7 +1819,7 @@ namespace
split_mmw->get_graph().chain_edges_();
#ifdef TRACE
trace << "Orig split aut\n";
print_hoa(std::cerr, split_mmw) << '\n';
print_hoa(std::cerr, mmw) << '\n';
{
auto ss = make_twa_graph(split_mmw, twa::prop_set::all());
for (unsigned group = 0; group < red.n_groups; ++group)
@ -1652,10 +1831,9 @@ namespace
bdd_ithvar(ss->register_ap("g"+std::to_string(group)
+"e"+std::to_string(i))));
}
const unsigned ns = ss->num_states();
for (unsigned s = 0; s < ns; ++s)
for (unsigned s = 0; s < n_env; ++s)
{
if (red.which_group[s] != group)
if (red.which_group.at(s) != group)
continue;
for (auto& e : ss->out(s))
e.cond =
@ -1676,8 +1854,8 @@ namespace
for (const auto& idx_vec : red.bisim_letters[i])
trace << red.minimal_letters_vec[i][idx_vec.front()].id() << '\n';
trace << "ids in the edge of the group\n";
for (unsigned s = 0; s < split_mmw->num_states(); ++s)
if (red.which_group[s] == i)
for (unsigned s = 0; s < n_env; ++s)
if (red.which_group.at(s) == i)
for (const auto& e : split_mmw->out(s))
trace << e.src << "->" << e.dst << ':' << e.cond.id() << '\n';
}
@ -2763,57 +2941,7 @@ namespace
return gmm2cond;
}
void cstr_unsplit(twa_graph_ptr& minmach,
const reduced_alphabet_t& red,
const std::vector<std::pair<unsigned,
std::vector<bool>>>&
x_in_class,
std::unordered_map<iaj_t, bdd,
decltype(iaj_hash),
decltype(iaj_eq)>& used_ziaj_map)
{
const unsigned n_groups = red.n_groups;
// For each minimal letter, create the (input) condition that it represents
// This has to be created for each minimal letters
// and might be shared between alphabets
std::vector<std::vector<bdd>> gmm2cond
= comp_represented_cond(red);
// Use a new map to reduce the number of edges created
// iaj.i: src_class or 0
// iaj.a: id of out condition
// iaj.j: dst_class
std::unordered_map<iaj_t, bdd,
decltype(iaj_hash), decltype(iaj_eq)>
edge_map(2*used_ziaj_map.size(), iaj_hash, iaj_eq);
for (unsigned group = 0; group < n_groups; ++group)
{
edge_map.clear();
// Attention the a in used_ziaj corresponds to the index
for (const auto& [iaj, outcond] : used_ziaj_map)
{
if (x_in_class[iaj.i].first != group)
continue;
const bdd& repr_cond = gmm2cond[group].at(iaj.a);
// Check if there already exists a suitable edge
auto [itedge, inserted] =
edge_map.try_emplace({iaj.i, (unsigned) outcond.id(), iaj.j},
repr_cond);
if (!inserted)
itedge->second |= repr_cond;
}
// Create the actual edges
for (const auto& ep : edge_map)
minmach->new_edge(ep.first.i, ep.first.j,
ep.second & bdd_from_int((int) ep.first.a));
}
}
void cstr_keep_split(twa_graph_ptr& minmach,
void cstr_split_mealy(twa_graph_ptr& minmach,
const reduced_alphabet_t& red,
const std::vector<std::pair<unsigned,
std::vector<bool>>>&
@ -2895,11 +3023,10 @@ namespace
}
// Set the state-player
std::vector<bool> sp(minmach->num_states(), true);
auto* sp = new std::vector<bool>(minmach->num_states(), true);
for (unsigned i = 0; i < n_env_states; ++i)
sp[i] = false;
minmach->set_named_prop("state-player",
new std::vector<bool>(std::move(sp)));
(*sp)[i] = false;
minmach->set_named_prop("state-player", sp);
}
// This function refines the sat constraints in case the
@ -3185,7 +3312,6 @@ namespace
const reduced_alphabet_t& red,
const part_sol_t& psol,
const unsigned n_env,
bool keep_split,
stopwatch& sw)
{
const auto& psolv = psol.psol;
@ -3432,10 +3558,7 @@ namespace
continue; //retry
}
if (keep_split)
cstr_keep_split(minmach, red, x_in_class, used_ziaj_map);
else
cstr_unsplit(minmach, red, x_in_class, used_ziaj_map);
cstr_split_mealy(minmach, red, x_in_class, used_ziaj_map);
// todo: What is the impact of chosing one of the possibilities
minmach->set_init_state(init_class_v.front());
@ -3447,26 +3570,17 @@ namespace
namespace spot
{
twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm,
int premin, bool keep_split)
int premin)
{
assert(is_split_mealy(mm));
stopwatch sw;
sw.start();
if ((premin < -1) || (premin > 1))
throw std::runtime_error("premin has to be -1, 0 or 1");
if (!mm->acc().is_t())
throw std::runtime_error("Mealy machine needs true acceptance!\n");
auto orig_spref = get_state_players(mm);
if (orig_spref.size() != mm->num_states())
throw std::runtime_error("Inconsistent \"state-player\"");
if (std::any_of(mm->edges().begin(), mm->edges().end(),
[&](const auto& e){return orig_spref[e.src]
== orig_spref[e.dst]; }))
throw std::runtime_error("Arena is not alternating!");
// Check if finite traces exist
// If so, deactivate fast minimization
@ -3491,10 +3605,18 @@ namespace spot
if (premin == -1)
return mm;
else
return minimize_mealy_fast(mm, premin == 1);
{
// 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;
}
};
const_twa_graph_ptr mmw = do_premin();
assert(is_split_mealy(mmw));
dotimeprint << "Done premin " << sw.stop() << '\n';
// 0 -> "Env" next is input props
@ -3508,6 +3630,7 @@ namespace spot
// second black : player-states
unsigned n_env = -1u;
std::tie(mmw, n_env) = reorganize_mm(mmw, spref);
assert(is_split_mealy(mmw));
#ifdef TRACE
print_hoa(std::cerr, mmw);
#endif
@ -3530,15 +3653,9 @@ namespace spot
auto early_exit = [&]()
{
if (keep_split)
// Always keep machines split
assert(is_split_mealy_specialization(mm, mmw));
return std::const_pointer_cast<twa_graph>(mmw);
else
{
auto mmw_u = unsplit_2step(mmw);
// todo correct unsplit to avoid this
mmw_u->purge_unreachable_states();
return mmw_u;
}
};
// If the partial solution has the same number of
@ -3576,7 +3693,6 @@ namespace spot
minmachine = try_build_min_machine(mm_pb, mmw,
reduced_alphabet,
partsol, n_env,
keep_split,
sw);
dotimeprint << "Done try_build " << n_classes
<< " - " << sw.stop() << '\n';
@ -3591,35 +3707,32 @@ namespace spot
// Set state players!
if (!minmachine)
return early_exit();
// Try to set outputs
if (bdd* outptr = mm->get_named_prop<bdd>("synthesis-outputs"))
minmachine->set_named_prop("synthesis-outputs", new bdd(*outptr));
set_synthesis_outputs(minmachine, get_synthesis_outputs(mm));
dotimeprint << "Done minimizing - " << minmachine->num_states()
<< " - " << sw.stop() << '\n';
assert(is_split_mealy_specialization(mm, minmachine));
return minmachine;
}
}
namespace spot
{
bool is_mealy_specialization(const_twa_graph_ptr left,
bool is_split_mealy_specialization(const_twa_graph_ptr left,
const_twa_graph_ptr right,
bool verbose)
{
assert(is_split_mealy(left));
assert(is_split_mealy(right));
auto& spl = get_state_players(left);
auto& spr = get_state_players(right);
const unsigned initl = left->get_init_state_number();
const unsigned initr = right->get_init_state_number();
if (spl[initl])
throw std::runtime_error("left: Mealy machine must have an "
"environment controlled initial state.");
if (spr[initr])
throw std::runtime_error("right: Mealy machine must have an "
"environment controlled initial state.");
#ifndef NDEBUG
// todo
auto check_out = [](const const_twa_graph_ptr& aut,
const auto& sp)
{

117
spot/twaalgos/mealy_machine.hh
View file

@ -23,48 +23,109 @@
namespace spot
{
/// \brief Minimizes an (in)completely specified mealy machine
/// todo
/// Comment je faire au mieux pour expliquer mealy dans les doc
/// \brief Checks whether or not the automaton is a mealy machine
///
/// \param m The automaton to be verified
/// \note A mealy machine must have the named property \"synthesis-outputs\"
/// and have a \"true\" as acceptance condition
SPOT_API bool
is_mealy(const const_twa_graph_ptr& m);
/// \brief Checks whether or not the automaton is a separated mealy machine
///
/// \param m The automaton to be verified
/// \note A separated mealy machine is a mealy machine machine with all
/// transitions having the form (in)&(out) where in[out] is a bdd over
/// input[output] propositions of m
SPOT_API bool
is_separated_mealy(const const_twa_graph_ptr& m);
/// \brief Checks whether or not the automaton is a split mealy machine
///
/// \param m The automaton to be verified
/// \note A split mealy machine is a mealy machine machine with the named
/// property \"state-player\". Moreover the underlying automaton
/// must be alternating between the player and the env. Transitions
/// leaving env[player] states can only be labeled by
/// input[output] propositions.
SPOT_API bool
is_split_mealy(const const_twa_graph_ptr& m);
/// \brief Checks whether or not a mealy machine is input deterministic
///
/// \param m The automaton to be verified
/// \note works all mealy machines, no matter whether they are split
/// or separated or neither of neither of them.
/// \note A machine is input deterministic if none of the states
/// has two outgoing transitions that can agree on a assignement
/// of the input propositions.
SPOT_API bool
is_input_deterministic_mealy(const const_twa_graph_ptr& m);
/// \brief make each transition in a separated mealy machine a
/// 2-step transition.
///
/// \param m separated mealy machine to be split
/// \return returns the equivalent split mealy machine if not done inplace
/// @{
SPOT_API twa_graph_ptr
split_separated_mealy(const const_twa_graph_ptr& m);
SPOT_API void
split_separated_mealy_here(const twa_graph_ptr& m);
/// @}
/// \brief the inverse of split_separated_mealy
SPOT_API twa_graph_ptr
unsplit_mealy(const const_twa_graph_ptr& m);
/// \brief reduce an (in)completely specified mealy machine
/// Based on signature inclusion or equality. This is not guaranteed
/// to find the minimal number of states but is usually faster.
/// This also comes at another drawback:
/// All applicable sequences have to be infinite. Finite
/// traces are disregarded
/// \Note The graph does not have to be split into env and player
/// states as for minimize_mealy
SPOT_API
void minimize_mealy_fast_here(twa_graph_ptr& mm,
bool use_inclusion = false);
/// \param mm The mealy machine to be minimized, has to be unsplit
/// \param output_assignment Whether or not to use output assignment
/// \return A specialization of \c mm. Note that if mm is separated,
/// the returned machine is separated as well.
/// \note See todo TACAS22 Effective reductions of mealy machines
/// @{
SPOT_API twa_graph_ptr
reduce_mealy(const const_twa_graph_ptr& mm,
bool output_assignment = false);
/// \brief Like minimize_mealy_fast_here
SPOT_API
twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm,
bool use_inclusion = false);
SPOT_API void
reduce_mealy_here(twa_graph_ptr& mm,
bool output_assignment = false);
/// @}
/// \brief Minimizes an (in)completely specified mealy machine
/// The approach is basically described in \cite abel2015memin
/// \param premin Use minimize_mealy_fast before applying the
/// \brief Minimizes a split (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
/// the original machine has no finite trace.
/// -1 : Do not use;
/// 0 : Use without inclusion;
/// 1 : Use with inclusion
/// \param keep_split Whether or not to keep the automaton states
/// partitioned into player and env states
/// \pre Graph must be split into env states and player states,
/// such that they alternate. Edges leaving env states must be labeled
/// with input proposition and edges leaving player states must be
/// labeled with output propositions.
SPOT_API
twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm,
int premin = -1,
bool keep_split = true);
/// 0 : Use without output assignment;
/// 1 : Use with output assignment
/// \return Returns a split mealy machines which is a minimal
/// speciliazation of the original machine
SPOT_API twa_graph_ptr
minimize_mealy(const const_twa_graph_ptr& mm, int premin = -1);
/// \brief Test if the mealy machine \a right is a specialization of
/// the mealy machine \a left. That is all input sequences valid for left
/// \brief Test if the split mealy machine \a right is a specialization of
/// the split mealy machine \a left.
///
/// That is all input sequences valid for left
/// must be applicable for right and the induced sequence of output signals
/// of right must imply the ones of left
SPOT_API bool is_mealy_specialization(const_twa_graph_ptr left,
SPOT_API bool
is_split_mealy_specialization(const_twa_graph_ptr left,
const_twa_graph_ptr right,
bool verbose = false);
}

832
spot/twaalgos/synthesis.cc
View file

@ -39,6 +39,7 @@
// Helper function/structures for split_2step
namespace{
using namespace spot;
// Computes and stores the restriction
// of each cond to the input domain and the support
// This is useful as it avoids recomputation
@ -47,9 +48,9 @@ namespace{
struct small_cacher_t
{
//e to e_in and support
std::unordered_map<bdd, std::pair<bdd, bdd>, spot::bdd_hash> cond_hash_;
std::unordered_map<bdd, std::pair<bdd, bdd>, bdd_hash> cond_hash_;
void fill(const spot::const_twa_graph_ptr& aut, bdd output_bdd)
void fill(const const_twa_graph_ptr& aut, bdd output_bdd)
{
cond_hash_.reserve(aut->num_edges()/5+1);
// 20% is about lowest number of different edge conditions
@ -79,28 +80,28 @@ namespace{
// of the state.
struct e_info_t
{
e_info_t(const spot::twa_graph::edge_storage_t& e,
e_info_t(const twa_graph::edge_storage_t& e,
const small_cacher_t& sm)
: dst(e.dst),
econd(e.cond),
einsup(sm[e.cond]),
acc(e.acc)
{
pre_hash = (spot::wang32_hash(dst)
^ std::hash<spot::acc_cond::mark_t>()(acc))
* spot::fnv<size_t>::prime;
pre_hash = (wang32_hash(dst)
^ std::hash<acc_cond::mark_t>()(acc))
* fnv<size_t>::prime;
}
inline size_t hash() const
{
return spot::wang32_hash(spot::bdd_hash()(econdout)) ^ pre_hash;
return wang32_hash(bdd_hash()(econdout)) ^ pre_hash;
}
unsigned dst;
bdd econd;
mutable bdd econdout;
std::pair<bdd, bdd> einsup;
spot::acc_cond::mark_t acc;
acc_cond::mark_t acc;
size_t pre_hash;
};
// We define an order between the edges to avoid creating multiple
@ -129,6 +130,313 @@ namespace{
< std::tie(rhs->dst, rhs->acc, r_id);
}
}less_info_ptr;
// Improved apply strat, that reduces the number of edges/states
// while keeping the needed edge-properties
// Note, this only deals with deterministic strategies
// Note, assumes that env starts playing
twa_graph_ptr
apply_strategy(const twa_graph_ptr& arena,
bool unsplit, bool keep_acc)
{
const auto& win = get_state_winners(arena);
const auto& strat = get_strategy(arena);
const auto& sp = get_state_players(arena);
auto outs = get_synthesis_outputs(arena);
if (!win[arena->get_init_state_number()])
throw std::runtime_error("Player does not win initial state, strategy "
"is not applicable");
assert((sp[arena->get_init_state_number()] == false)
&& "Env needs to have first turn!");
assert(std::none_of(arena->edges().begin(), arena->edges().end(),
[&sp](const auto& e)
{ bool same_player = sp.at(e.src) == sp.at(e.dst);
if (same_player)
std::cerr << e.src << " and " << e.dst << " belong to same "
<< "player, arena not alternating!\n";
return same_player; }));
auto strat_split = make_twa_graph(arena->get_dict());
strat_split->copy_ap_of(arena);
if (keep_acc)
strat_split->copy_acceptance_of(arena);
else
strat_split->acc().set_acceptance(acc_cond::acc_code::t());
std::stack<unsigned> todo;
todo.push(arena->get_init_state_number());
struct dca{
unsigned dst;
unsigned condvar;
acc_cond::mark_t acc;
};
struct dca_hash
{
size_t operator()(const dca& d) const noexcept
{
return pair_hash()(std::make_pair(d.dst, d.condvar))
^ wang32_hash(d.acc.hash());
}
};
struct dca_equal
{
bool operator()(const dca& d1, const dca& d2) const noexcept
{
return std::tie(d1.dst, d1.condvar, d1.acc)
== std::tie(d2.dst, d2.condvar, d2.acc);
}
};
//env dst + player cond + acc -> p stat
std::unordered_map<dca,
unsigned,
dca_hash,
dca_equal> p_map;
constexpr unsigned unseen_mark = std::numeric_limits<unsigned>::max();
std::vector<unsigned> env_map(arena->num_states(), unseen_mark);
strat_split->set_init_state(strat_split->new_state());
env_map[arena->get_init_state_number()] =
strat_split->get_init_state_number();
// The states in the new graph are qualified local
// Get a local environment state
auto get_sel = [&](unsigned s)
{
if (SPOT_UNLIKELY(env_map[s] == unseen_mark))
env_map[s] = strat_split->new_state();
return env_map[s];
};
// local dst
// Check if there exists already a local player state
// that has the same dst, cond and (if keep_acc is true) acc
auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc)
{
dca d{dst, (unsigned) cond.id(), acc};
auto it = p_map.find(d);
if (it != p_map.end())
return it->second;
unsigned ns = strat_split->new_state();
p_map[d] = ns;
strat_split->new_edge(ns, dst, cond, acc);
return ns;
};
while (!todo.empty())
{
unsigned src_env = todo.top();
unsigned src_envl = get_sel(src_env);
todo.pop();
// All env edges
for (const auto& e_env : arena->out(src_env))
{
// Get the corresponding strat
const auto& e_strat = arena->edge_storage(strat[e_env.dst]);
// Check if already explored
if (env_map[e_strat.dst] == unseen_mark)
todo.push(e_strat.dst);
unsigned dst_envl = get_sel(e_strat.dst);
// The new env edge, player is constructed automatically
auto used_acc = keep_acc ? e_strat.acc : acc_cond::mark_t({});
strat_split->new_edge(src_envl,
get_spl(dst_envl, e_strat.cond, used_acc),
e_env.cond, used_acc);
}
}
// All states exists, we can try to further merge them
// Specialized merge
std::vector<bool> spnew(strat_split->num_states(), false);
for (const auto& p : p_map)
spnew[p.second] = true;
// Sorting edges in place
auto comp_edge = [](const auto& e1, const auto& e2)
{
return std::tuple(e1.dst, e1.acc, e1.cond.id())
< std::tuple(e2.dst, e2.acc, e2.cond.id());
};
// todo, replace with sort_edges_of_ in graph
auto sort_edges_of =
[&, &split_graph = strat_split->get_graph()](unsigned s)
{
static std::vector<unsigned> edge_nums;
edge_nums.clear();
auto eit = strat_split->out(s);
const auto eit_e = eit.end();
// 0 Check if it is already sorted
if (std::is_sorted(eit.begin(), eit_e, comp_edge))
return false; // No change
// 1 Get all edges numbers and sort them
std::transform(eit.begin(), eit_e, std::back_inserter(edge_nums),
[&](const auto& e)
{ return strat_split->edge_number(e); });
std::sort(edge_nums.begin(), edge_nums.end(),
[&](unsigned ne1, unsigned ne2)
{ return comp_edge(strat_split->edge_storage(ne1),
strat_split->edge_storage(ne2)); });
// 2 Correct the order
auto& sd = split_graph.state_storage(s);
sd.succ = edge_nums.front();
sd.succ_tail = edge_nums.back();
const unsigned n_edges_p = edge_nums.size()-1;
for (unsigned i = 0; i < n_edges_p; ++i)
split_graph.edge_storage(edge_nums[i]).next_succ = edge_nums[i+1];
split_graph.edge_storage(edge_nums.back()).next_succ = 0; //terminal
// All nicely chained
return true;
};
auto merge_edges_of = [&](unsigned s)
{
// Call this after sort edges of
// Mergeable edges are nicely chained
bool changed = false;
auto eit = strat_split->out_iteraser(s);
unsigned idx_last = strat_split->edge_number(*eit);
++eit;
while (eit)
{
auto& e_last = strat_split->edge_storage(idx_last);
if (std::tie(e_last.dst, e_last.acc)
== std::tie(eit->dst, eit->acc))
{
//Same dest and acc -> or condition
e_last.cond |= eit->cond;
eit.erase();
changed = true;
}
else
{
idx_last = strat_split->edge_number(*eit);
++eit;
}
}
return changed;
};
auto merge_able = [&](unsigned s1, unsigned s2)
{
auto eit1 = strat_split->out(s1);
auto eit2 = strat_split->out(s2);
// Note: No self-loops here
return std::equal(eit1.begin(), eit1.end(),
eit2.begin(), eit2.end(),
[](const auto& e1, const auto& e2)
{
return std::tuple(e1.dst, e1.acc, e1.cond.id())
== std::tuple(e2.dst, e2.acc, e2.cond.id());
});
};
const unsigned n_sstrat = strat_split->num_states();
std::vector<unsigned> remap(n_sstrat, -1u);
bool changed_any;
std::vector<unsigned> to_check;
to_check.reserve(n_sstrat);
// First iteration -> all env states are candidates
for (unsigned i = 0; i < n_sstrat; ++i)
if (!spnew[i])
to_check.push_back(i);
while (true)
{
changed_any = false;
std::for_each(to_check.begin(), to_check.end(),
[&](unsigned s){ sort_edges_of(s); merge_edges_of(s); });
// Check if we can merge env states
for (unsigned s1 : to_check)
for (unsigned s2 = 0; s2 < n_sstrat; ++s2)
{
if (spnew[s2] || (s1 == s2))
continue; // Player state or s1 == s2
if ((remap[s2] < s2))
continue; //s2 is already remapped
if (merge_able(s1, s2))
{
changed_any = true;
if (s1 < s2)
remap[s2] = s1;
else
remap[s1] = s2;
break;
}
}
if (!changed_any)
break;
// Redirect changed targets and set possibly mergeable states
to_check.clear();
for (auto& e : strat_split->edges())
if (remap[e.dst] != -1u)
{
e.dst = remap[e.dst];
to_check.push_back(e.src);
assert(spnew[e.src]);
}
// Now check the player states
// We can skip sorting -> only one edge
// todo change when multistrat
changed_any = false;
for (unsigned s1 : to_check)
for (unsigned s2 = 0; s2 < n_sstrat; ++s2)
{
if (!spnew[s2] || (s1 == s2))
continue; // Env state or s1 == s2
if ((remap[s2] < s2))
continue; //s2 is already remapped
if (merge_able(s1, s2))
{
changed_any = true;
if (s1 < s2)
remap[s2] = s1;
else
remap[s1] = s2;
break;
}
}
if (!changed_any)
break;
// Redirect changed targets and set possibly mergeable states
to_check.clear();
for (auto& e : strat_split->edges())
if (remap[e.dst] != -1u)
{
e.dst = remap[e.dst];
to_check.push_back(e.src);
assert(!spnew[e.src]);
}
}
// Defrag and alternate
if (remap[strat_split->get_init_state_number()] != -1u)
strat_split->set_init_state(remap[strat_split->get_init_state_number()]);
unsigned st = 0;
for (auto& s: remap)
if (s == -1U)
s = st++;
else
s = -1U;
strat_split->defrag_states(remap, st);
alternate_players(strat_split, false, false);
// What we do now depends on whether we unsplit or not
if (unsplit)
{
auto final = unsplit_2step(strat_split);
set_synthesis_outputs(final, outs);
return final;
}
set_synthesis_outputs(strat_split, outs);
return strat_split;
}
}
namespace spot
@ -142,7 +450,7 @@ namespace spot
split->copy_acceptance_of(aut);
split->new_states(aut->num_states());
split->set_init_state(aut->get_init_state_number());
split->set_named_prop<bdd>("synthesis-output", new bdd(output_bdd));
split->set_named_prop<bdd>("synthesis-outputs", new bdd(output_bdd));
auto [is_unsat, unsat_mark] = aut->acc().unsat_mark();
if (!is_unsat && complete_env)
@ -318,89 +626,13 @@ namespace spot
if (sink_env != -1u)
owner->at(sink_env) = false;
split->set_named_prop("state-player", owner);
split->set_named_prop("synthesis-outputs",
new bdd(output_bdd));
// Done
return split;
}
void
split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd)
{
struct dst_cond_color_t
{
std::pair<unsigned, int> dst_cond;
acc_cond::mark_t color;
};
auto hasher = [](const dst_cond_color_t& dcc) noexcept
{
return dcc.color.hash() ^ pair_hash()(dcc.dst_cond);
};
auto equal = [](const dst_cond_color_t& dcc1,
const dst_cond_color_t& dcc2) noexcept
{
return (dcc1.dst_cond == dcc2.dst_cond)
&& (dcc1.color == dcc2.color);
};
std::unordered_map<dst_cond_color_t, unsigned,
decltype(hasher),
decltype(equal)> player_map(aut->num_edges(),
hasher, equal);
auto get_ps = [&](unsigned dst, const bdd& ocond,
acc_cond::mark_t color)
{
dst_cond_color_t key{std::make_pair(dst, ocond.id()),
color};
auto [it, inserted] =
player_map.try_emplace(key, aut->num_states());
if (!inserted)
return it->second;
unsigned ns = aut->new_state();
assert(ns == it->second);
aut->new_edge(ns, dst, ocond, color);
return ns;
};
unsigned ne = aut->edge_vector().size();
for (unsigned eidx = 1; eidx < ne; ++eidx)
{
const auto& e = aut->edge_storage(eidx);
if (e.next_succ == eidx) // dead edge
continue;
bdd incond = bdd_exist(e.cond, output_bdd);
bdd outcond = bdd_existcomp(e.cond, output_bdd);
assert(((incond&outcond) == e.cond) && "Precondition violated");
// Create new state and trans
// this may invalidate "e".
unsigned new_dst = get_ps(e.dst, outcond, e.acc);
// redirect
auto& e2 = aut->edge_storage(eidx);
e2.dst = new_dst;
e2.cond = incond;
}
auto* sp_ptr =
aut->get_or_set_named_prop<std::vector<bool>>("state-player");
sp_ptr->resize(aut->num_states());
std::fill(sp_ptr->begin(), sp_ptr->end(), false);
for (auto& eit : player_map)
(*sp_ptr)[eit.second] = true;
//Done
}
twa_graph_ptr
split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd)
{
auto aut2 = make_twa_graph(aut, twa::prop_set::all());
aut2->copy_acceptance_of(aut);
aut2->set_named_prop<bdd>("synthesis-output", new bdd(output_bdd));
split_2step_fast_here(aut2, output_bdd);
return aut2;
}
twa_graph_ptr
unsplit_2step(const const_twa_graph_ptr& aut)
{
@ -453,321 +685,6 @@ namespace spot
return out;
}
// Improved apply strat, that reduces the number of edges/states
// while keeping the needed edge-properties
// Note, this only deals with deterministic strategies
// Note, assumes that env starts playing
spot::twa_graph_ptr
apply_strategy(const spot::twa_graph_ptr& arena,
bool unsplit, bool keep_acc)
{
const auto& win = get_state_winners(arena);
const auto& strat = get_strategy(arena);
const auto& sp = get_state_players(arena);
auto outs = get_synthesis_outputs(arena);
if (!win[arena->get_init_state_number()])
throw std::runtime_error("Player does not win initial state, strategy "
"is not applicable");
assert((sp[arena->get_init_state_number()] == false)
&& "Env needs to have first turn!");
assert(std::none_of(arena->edges().begin(), arena->edges().end(),
[&sp](const auto& e)
{ bool same_player = sp.at(e.src) == sp.at(e.dst);
if (same_player)
std::cerr << e.src << " and " << e.dst << " belong to same "
<< "player, arena not alternating!\n";
return same_player; }));
auto strat_split = spot::make_twa_graph(arena->get_dict());
strat_split->copy_ap_of(arena);
if (keep_acc)
strat_split->copy_acceptance_of(arena);
std::stack<unsigned> todo;
todo.push(arena->get_init_state_number());
struct dca{
unsigned dst;
unsigned condvar;
acc_cond::mark_t acc;
};
struct dca_hash
{
size_t operator()(const dca& d) const noexcept
{
return pair_hash()(std::make_pair(d.dst, d.condvar))
^ wang32_hash(d.acc.hash());
}
};
struct dca_equal
{
bool operator()(const dca& d1, const dca& d2) const noexcept
{
return std::tie(d1.dst, d1.condvar, d1.acc)
== std::tie(d2.dst, d2.condvar, d2.acc);
}
};
//env dst + player cond + acc -> p stat
std::unordered_map<dca,
unsigned,
dca_hash,
dca_equal> p_map;
constexpr unsigned unseen_mark = std::numeric_limits<unsigned>::max();
std::vector<unsigned> env_map(arena->num_states(), unseen_mark);
strat_split->set_init_state(strat_split->new_state());
env_map[arena->get_init_state_number()] =
strat_split->get_init_state_number();
// The states in the new graph are qualified local
// Get a local environment state
auto get_sel = [&](unsigned s)
{
if (SPOT_UNLIKELY(env_map[s] == unseen_mark))
env_map[s] = strat_split->new_state();
return env_map[s];
};
// local dst
// Check if there exists already a local player state
// that has the same dst, cond and (if keep_acc is true) acc
auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc)
{
dca d{dst, (unsigned) cond.id(), acc};
auto it = p_map.find(d);
if (it != p_map.end())
return it->second;
unsigned ns = strat_split->new_state();
p_map[d] = ns;
strat_split->new_edge(ns, dst, cond, acc);
return ns;
};
while (!todo.empty())
{
unsigned src_env = todo.top();
unsigned src_envl = get_sel(src_env);
todo.pop();
// All env edges
for (const auto& e_env : arena->out(src_env))
{
// Get the corresponding strat
const auto& e_strat = arena->edge_storage(strat[e_env.dst]);
// Check if already explored
if (env_map[e_strat.dst] == unseen_mark)
todo.push(e_strat.dst);
unsigned dst_envl = get_sel(e_strat.dst);
// The new env edge, player is constructed automatically
auto used_acc = keep_acc ? e_strat.acc : acc_cond::mark_t({});
strat_split->new_edge(src_envl,
get_spl(dst_envl, e_strat.cond, used_acc),
e_env.cond, used_acc);
}
}
// All states exists, we can try to further merge them
// Specialized merge
std::vector<bool> spnew(strat_split->num_states(), false);
for (const auto& p : p_map)
spnew[p.second] = true;
// Sorting edges in place
auto comp_edge = [](const auto& e1, const auto& e2)
{
return std::tuple(e1.dst, e1.acc, e1.cond.id())
< std::tuple(e2.dst, e2.acc, e2.cond.id());
};
auto sort_edges_of =
[&, &split_graph = strat_split->get_graph()](unsigned s)
{
static std::vector<unsigned> edge_nums;
edge_nums.clear();
auto eit = strat_split->out(s);
const auto eit_e = eit.end();
// 0 Check if it is already sorted
if (std::is_sorted(eit.begin(), eit_e, comp_edge))
return false; // No change
// 1 Get all edges numbers and sort them
std::transform(eit.begin(), eit_e, std::back_inserter(edge_nums),
[&](const auto& e)
{ return strat_split->edge_number(e); });
std::sort(edge_nums.begin(), edge_nums.end(),
[&](unsigned ne1, unsigned ne2)
{ return comp_edge(strat_split->edge_storage(ne1),
strat_split->edge_storage(ne2)); });
// 2 Correct the order
auto& sd = split_graph.state_storage(s);
sd.succ = edge_nums.front();
sd.succ_tail = edge_nums.back();
const unsigned n_edges_p = edge_nums.size()-1;
for (unsigned i = 0; i < n_edges_p; ++i)
split_graph.edge_storage(edge_nums[i]).next_succ = edge_nums[i+1];
split_graph.edge_storage(edge_nums.back()).next_succ = 0; //terminal
// All nicely chained
return true;
};
auto merge_edges_of = [&](unsigned s)
{
// Call this after sort edges of
// Mergeable edges are nicely chained
bool changed = false;
auto eit = strat_split->out_iteraser(s);
unsigned idx_last = strat_split->edge_number(*eit);
++eit;
while (eit)
{
auto& e_last = strat_split->edge_storage(idx_last);
if (std::tie(e_last.dst, e_last.acc)
== std::tie(eit->dst, eit->acc))
{
//Same dest and acc -> or condition
e_last.cond |= eit->cond;
eit.erase();
changed = true;
}
else
{
idx_last = strat_split->edge_number(*eit);
++eit;
}
}
return changed;
};
auto merge_able = [&](unsigned s1, unsigned s2)
{
auto eit1 = strat_split->out(s1);
auto eit2 = strat_split->out(s2);
// Note: No self-loops here
return std::equal(eit1.begin(), eit1.end(),
eit2.begin(), eit2.end(),
[](const auto& e1, const auto& e2)
{
return std::tuple(e1.dst, e1.acc, e1.cond.id())
== std::tuple(e2.dst, e2.acc, e2.cond.id());
});
};
const unsigned n_sstrat = strat_split->num_states();
std::vector<unsigned> remap(n_sstrat, -1u);
bool changed_any;
std::vector<unsigned> to_check;
to_check.reserve(n_sstrat);
// First iteration -> all env states are candidates
for (unsigned i = 0; i < n_sstrat; ++i)
if (!spnew[i])
to_check.push_back(i);
while (true)
{
changed_any = false;
std::for_each(to_check.begin(), to_check.end(),
[&](unsigned s){ sort_edges_of(s); merge_edges_of(s); });
// Check if we can merge env states
for (unsigned s1 : to_check)
for (unsigned s2 = 0; s2 < n_sstrat; ++s2)
{
if (spnew[s2] || (s1 == s2))
continue; // Player state or s1 == s2
if ((remap[s2] < s2))
continue; //s2 is already remapped
if (merge_able(s1, s2))
{
changed_any = true;
if (s1 < s2)
remap[s2] = s1;
else
remap[s1] = s2;
break;
}
}
if (!changed_any)
break;
// Redirect changed targets and set possibly mergeable states
to_check.clear();
for (auto& e : strat_split->edges())
if (remap[e.dst] != -1u)
{
e.dst = remap[e.dst];
to_check.push_back(e.src);
assert(spnew[e.src]);
}
// Now check the player states
// We can skip sorting -> only one edge
// todo change when multistrat
changed_any = false;
for (unsigned s1 : to_check)
for (unsigned s2 = 0; s2 < n_sstrat; ++s2)
{
if (!spnew[s2] || (s1 == s2))
continue; // Env state or s1 == s2
if ((remap[s2] < s2))
continue; //s2 is already remapped
if (merge_able(s1, s2))
{
changed_any = true;
if (s1 < s2)
remap[s2] = s1;
else
remap[s1] = s2;
break;
}
}
if (!changed_any)
break;
// Redirect changed targets and set possibly mergeable states
to_check.clear();
for (auto& e : strat_split->edges())
if (remap[e.dst] != -1u)
{
e.dst = remap[e.dst];
to_check.push_back(e.src);
assert(!spnew[e.src]);
}
}
// Defrag and alternate
if (remap[strat_split->get_init_state_number()] != -1u)
strat_split->set_init_state(remap[strat_split->get_init_state_number()]);
unsigned st = 0;
for (auto& s: remap)
if (s == -1U)
s = st++;
else
s = -1U;
strat_split->defrag_states(remap, st);
alternate_players(strat_split, false, false);
// What we do now depends on whether we unsplit or not
if (unsplit)
{
auto final = unsplit_2step(strat_split);
set_synthesis_outputs(final, outs);
return final;
}
// Keep the splitted version
set_state_winners(strat_split, region_t(strat_split->num_states(), true));
std::vector<unsigned> new_strat(strat_split->num_states(), -1u);
for (unsigned i = 0; i < strat_split->num_states(); ++i)
{
if (!sp[i])
continue;
new_strat[i] = strat_split->edge_number(*strat_split->out(i).begin());
}
set_strategy(strat_split, std::move(new_strat));
set_synthesis_outputs(strat_split, outs);
return strat_split;
}
std::ostream& operator<<(std::ostream& os, synthesis_info::algo s)
{
using algo = synthesis_info::algo;
@ -1059,7 +976,7 @@ namespace spot
} //end switch solver
// Set the named properties
assert(dpa->get_named_prop<std::vector<bool>>("state-player")
&& "DPA has no state-players");
&& "DPA has no \"state-player\"");
set_synthesis_outputs(dpa, outs);
return dpa;
}
@ -1087,78 +1004,15 @@ namespace spot
return ltl_to_game(parse_formula(f), all_outs, gi);
}
void
minimize_strategy_here(twa_graph_ptr& strat, int min_lvl)
{
if (!strat->acc().is_t())
throw std::runtime_error("minimize_strategy_here(): strategy is expected "
"to accept all runs! Otherwise it does not "
"correspond to a mealy machine and can not be "
"optimized this way.");
// 0 -> No minimization
// 1 -> Regular monitor/DFA minimization
// 2 -> Mealy minimization based on language inclusion
// with output assignement
// 3 -> Exact Mealy minimization using SAT
// 4 -> Monitor min then exact minimization
// 5 -> Mealy minimization based on language inclusion then exact
// minimization
bdd outs = get_synthesis_outputs(strat);
switch (min_lvl)
{
case 0:
return;
case 1:
{
minimize_mealy_fast_here(strat, false);
break;
}
case 2:
{
minimize_mealy_fast_here(strat, true);
break;
}
case 3:
{
strat = minimize_mealy(strat, -1);
break;
}
case 4:
{
strat = minimize_mealy(strat, 0);
break;
}
case 5:
{
strat = minimize_mealy(strat, 1);
break;
}
default:
throw std::runtime_error("Unknown minimization option");
}
set_synthesis_outputs(strat, outs);
}
twa_graph_ptr
minimize_strategy(const_twa_graph_ptr& strat, int min_lvl)
{
auto strat_dup = spot::make_twa_graph(strat, spot::twa::prop_set::all());
set_synthesis_outputs(strat_dup,
get_synthesis_outputs(strat));
if (auto sp_ptr = strat->get_named_prop<region_t>("state-player"))
set_state_players(strat_dup, *sp_ptr);
minimize_strategy_here(strat_dup, min_lvl);
return strat_dup;
}
twa_graph_ptr
create_strategy(twa_graph_ptr arena, synthesis_info& gi)
solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi)
{
assert(arena->get_named_prop<region_t>("state-player")
&& "Need prop \"state-player\"");
if (!arena)
throw std::runtime_error("Arena can not be null");
spot::stopwatch sw;
stopwatch sw;
if (gi.bv)
sw.start();
@ -1168,32 +1022,34 @@ namespace spot
// If we use minimizations 0,1 or 2 -> unsplit
const bool do_unsplit = gi.minimize_lvl < 3;
twa_graph_ptr strat_aut = apply_strategy(arena, do_unsplit, false);
auto m = apply_strategy(arena, do_unsplit, false);
strat_aut->prop_universal(true);
m->prop_universal(true);
minimize_strategy_here(strat_aut, gi.minimize_lvl);
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);
assert(do_unsplit
|| strat_aut->get_named_prop<std::vector<bool>>("state-player"));
if (!do_unsplit)
strat_aut = unsplit_2step(strat_aut);
m = unsplit_mealy(m);
if (gi.bv)
{
gi.bv->strat2aut_time += sw.stop();
gi.bv->nb_strat_states += strat_aut->num_states();
gi.bv->nb_strat_edges += strat_aut->num_edges();
gi.bv->nb_strat_states += m->num_states();
gi.bv->nb_strat_edges += m->num_edges();
}
return strat_aut;
assert(is_separated_mealy(m));
return m;
}
twa_graph_ptr
create_strategy(twa_graph_ptr arena)
solved_game_to_separated_mealy(twa_graph_ptr arena)
{
synthesis_info dummy;
return create_strategy(arena, dummy);
return solved_game_to_separated_mealy(arena, dummy);
}
}
@ -1241,7 +1097,7 @@ namespace spot
};
}
strategy_like_t
mealy_like
try_create_direct_strategy(formula f,
const std::vector<std::string>& output_aps,
synthesis_info &gi)
@ -1256,8 +1112,8 @@ namespace spot
{
if (vs)
*vs << "direct strategy might exist but was not found.\n";
return strategy_like_t{
strategy_like_t::realizability_code::UNKNOWN,
return mealy_like{
mealy_like::realizability_code::UNKNOWN,
nullptr,
bddfalse};
};
@ -1265,8 +1121,8 @@ namespace spot
{
if (vs)
*vs << "no strategy exists.\n";
return strategy_like_t{
strategy_like_t::realizability_code::UNREALIZABLE,
return mealy_like{
mealy_like::realizability_code::UNREALIZABLE,
nullptr,
bddfalse};
};
@ -1279,8 +1135,8 @@ namespace spot
<< "direct strat has " << strat->num_states()
<< " states and " << strat->num_sets() << " colors\n";
}
return strategy_like_t{
strategy_like_t::realizability_code::REALIZABLE_REGULAR,
return mealy_like{
mealy_like::realizability_code::REALIZABLE_REGULAR,
strat,
bddfalse};
};

82
spot/twaalgos/synthesis.hh
View file

@ -58,29 +58,13 @@ namespace spot
split_2step(const const_twa_graph_ptr& aut,
const bdd& output_bdd, bool complete_env);
/// \ingroup synthesis
/// \brief make each transition a 2-step transition.
///
/// This algorithm is only applicable if all transitions of the
/// graph have the form p -- ins & outs --> q.
/// That is they are a conjunction of a condition over the input
/// propositions ins and a condition over the output propositions outs
///
/// \param aut automaton to be transformed
/// \param output_bdd conjunction of all output AP, all APs not present
/// are treated as inputs
/// @{
SPOT_API void
split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd);
SPOT_API twa_graph_ptr
split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd);
/// @}
/// \ingroup synthesis
/// \brief the reverse of split_2step
/// \brief the inverse of split_2step
///
/// \pre aut is an alternating arena
/// \post All edge conditions in the returned automaton are of the form
/// ins&outs, with ins/outs being a condition over the input/output
/// propositions
/// \note This function relies on the named property "state-player"
SPOT_API twa_graph_ptr
unsplit_2step(const const_twa_graph_ptr& aut);
@ -174,57 +158,23 @@ namespace spot
/// @}
/// \ingroup synthesis
/// \brief Takes a solved game and restricts the automaton to the
/// winning strategy of the player
///
/// \param arena twa_graph with named properties "state-player",
/// "strategy" and "state-winner"
/// \param unsplit Whether or not to unsplit the automaton
/// \param keep_acc Whether or not keep the acceptance condition
/// \return the resulting twa_graph
SPOT_API spot::twa_graph_ptr
apply_strategy(const spot::twa_graph_ptr& arena,
bool unsplit, bool keep_acc);
/// \ingroup synthesis
/// \brief Minimizes a strategy. Strategies are infact
/// Mealy machines. So we can use techniques designed for them
///
/// \param strat The machine to minimize
/// \param min_lvl How to minimize the machine:
/// 0: No minimization, 1: Minimizing it like an DFA,
/// means the language is preserved, 2: Inclusion with
/// output assignement, 3: Exact minimization using
/// SAT solving, 4: SAT solving with DFA minimization as
/// preprocessing, 5: SAT solving using inclusion based
/// minimization with output assignment as preprocessing
/// \note min_lvl 1 and 2 work more efficiently on UNSPLIT strategies,
/// whereas min_lvl 3, 4 and 5 mandate a SPLIT strategy
/// \brief creates a separated mealy machine from a solved game
/// taking into account the options given in \a gi.
/// This concerns in particular whether or not the machine is to be reduced
/// and how.
/// @{
SPOT_API void
minimize_strategy_here(twa_graph_ptr& strat, int min_lvl);
SPOT_API twa_graph_ptr
minimize_strategy(const_twa_graph_ptr& strat, int min_lvl);
solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info& gi);
SPOT_API twa_graph_ptr
solved_game_to_separated_mealy(twa_graph_ptr arena);
/// @}
/// \ingroup synthesis
/// \brief creates a strategy from a solved game taking into account the
/// options given in \a gi
/// @{
SPOT_API twa_graph_ptr
create_strategy(twa_graph_ptr arena, synthesis_info& gi);
SPOT_API twa_graph_ptr
create_strategy(twa_graph_ptr arena);
/// @}
/// \ingroup synthesis
/// \brief A struct that represents different types of strategy like
/// \brief A struct that represents different types of mealy like
/// objects
struct SPOT_API
strategy_like_t
mealy_like
{
enum class realizability_code
{
UNREALIZABLE,
@ -235,7 +185,7 @@ namespace spot
};
realizability_code success;
twa_graph_ptr strat_like;
twa_graph_ptr mealy_like;
bdd glob_cond;
};
@ -272,7 +222,7 @@ namespace spot
/// \param f The formula to synthesize a strategy for
/// \param output_aps A vector with the name of all output properties.
/// All APs not named in this vector are treated as inputs
SPOT_API strategy_like_t
SPOT_API mealy_like
try_create_direct_strategy(formula f,
const std::vector<std::string>& output_aps,
synthesis_info& gi);

109
tests/python/_mealy.ipynb
View file

@ -3,7 +3,6 @@
{
"cell_type": "code",
"execution_count": 1,
"id": "99baf49c",
"metadata": {},
"outputs": [],
"source": [
@ -13,7 +12,6 @@
},
{
"cell_type": "markdown",
"id": "066489fd",
"metadata": {},
"source": [
"Test the Mealy printer."
@ -22,7 +20,6 @@
{
"cell_type": "code",
"execution_count": 2,
"id": "08d7d512",
"metadata": {},
"outputs": [],
"source": [
@ -32,7 +29,6 @@
{
"cell_type": "code",
"execution_count": 3,
"id": "4e5b66f4",
"metadata": {},
"outputs": [
{
@ -53,7 +49,6 @@
{
"cell_type": "code",
"execution_count": 4,
"id": "ce2ff962",
"metadata": {},
"outputs": [
{
@ -140,7 +135,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d8c04f720> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f300caabba0> >"
]
},
"execution_count": 4,
@ -155,17 +150,15 @@
{
"cell_type": "code",
"execution_count": 5,
"id": "3bcbeef2",
"metadata": {},
"outputs": [],
"source": [
"x = spot.apply_strategy(g, True, False)"
"x = spot.solved_game_to_separated_mealy(g)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "47d298f0",
"metadata": {},
"outputs": [
{
@ -220,7 +213,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d8c04f630> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f300c179300> >"
]
},
"execution_count": 6,
@ -235,7 +228,6 @@
{
"cell_type": "code",
"execution_count": 7,
"id": "f0d098ac",
"metadata": {},
"outputs": [],
"source": [
@ -245,7 +237,6 @@
{
"cell_type": "code",
"execution_count": 8,
"id": "adf92ac7",
"metadata": {},
"outputs": [
{
@ -294,7 +285,7 @@
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d8c04f630> >"
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f300c179300> >"
]
},
"execution_count": 8,
@ -305,96 +296,6 @@
"source": [
"x"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "6e8cd892",
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
"<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
" \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
"<!-- Generated by graphviz version 2.43.0 (0)\n",
" -->\n",
"<!-- Pages: 1 -->\n",
"<svg width=\"247pt\" height=\"204pt\"\n",
" viewBox=\"0.00 0.00 247.00 204.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 200)\">\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-200 243,-200 243,4 -4,4\"/>\n",
"<text text-anchor=\"start\" x=\"8\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
"<text text-anchor=\"start\" x=\"29\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"<text text-anchor=\"start\" x=\"45\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">) | (Fin(</text>\n",
"<text text-anchor=\"start\" x=\"87\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
"<text text-anchor=\"start\" x=\"103\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">) &amp; (Inf(</text>\n",
"<text text-anchor=\"start\" x=\"149\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
"<text text-anchor=\"start\" x=\"165\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">) | Fin(</text>\n",
"<text text-anchor=\"start\" x=\"203\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
"<text text-anchor=\"start\" x=\"219\" y=\"-181.8\" font-family=\"Lato\" font-size=\"14.00\">)))</text>\n",
"<text text-anchor=\"start\" x=\"64\" y=\"-167.8\" font-family=\"Lato\" font-size=\"14.00\">[parity max odd 4]</text>\n",
"<!-- I -->\n",
"<!-- 0 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>0</title>\n",
"<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"123\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
"<text text-anchor=\"middle\" x=\"123\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
"</g>\n",
"<!-- I&#45;&gt;0 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>I&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M64.17,-18C66.01,-18 82.75,-18 97.75,-18\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"104.9,-18 97.9,-21.15 101.4,-18 97.9,-18 97.9,-18 97.9,-18 101.4,-18 97.9,-14.85 104.9,-18 104.9,-18\"/>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M119.4,-35.78C118.79,-45.31 119.99,-54 123,-54 125.21,-54 126.44,-49.32 126.7,-43.05\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"126.6,-35.78 129.85,-42.74 126.65,-39.28 126.7,-42.78 126.7,-42.78 126.7,-42.78 126.65,-39.28 123.55,-42.83 126.6,-35.78 126.6,-35.78\"/>\n",
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"72,-77 72,-96 115,-96 115,-77 72,-77\"/>\n",
"<text text-anchor=\"start\" x=\"74\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !c</text>\n",
"<text text-anchor=\"start\" x=\"119\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"130,-77 130,-96 174,-96 174,-77 130,-77\"/>\n",
"<text text-anchor=\"start\" x=\"132\" y=\"-82.8\" font-family=\"Lato\" font-size=\"14.00\">!b &amp; !d</text>\n",
"<text text-anchor=\"start\" x=\"115\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;0 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>0&#45;&gt;0</title>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M117.81,-35.4C113.5,-60.54 115.23,-98 123,-98 130.08,-98 132.14,-66.97 129.21,-42.44\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"128.19,-35.4 132.31,-41.88 128.69,-38.86 129.19,-42.33 129.19,-42.33 129.19,-42.33 128.69,-38.86 126.07,-42.78 128.19,-35.4 128.19,-35.4\"/>\n",
"<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"86,-121 86,-140 115,-140 115,-121 86,-121\"/>\n",
"<text text-anchor=\"start\" x=\"88\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">a | c</text>\n",
"<text text-anchor=\"start\" x=\"119\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
"<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"130,-121 130,-140 161,-140 161,-121 130,-121\"/>\n",
"<text text-anchor=\"start\" x=\"132\" y=\"-126.8\" font-family=\"Lato\" font-size=\"14.00\">b | d</text>\n",
"<text text-anchor=\"start\" x=\"115.5\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#6a3d9a\">❸</text>\n",
"</g>\n",
"</g>\n",
"</svg>\n"
],
"text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f3d76e561e0> >"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"spot.apply_strategy(g, True, True)"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "5948f923",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
@ -413,7 +314,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.9.2"
"version": "3.8.10"
}
},
"nbformat": 4,

7
tests/python/aiger.py
View file

@ -3339,9 +3339,10 @@ for strat_string, (ins_str, outs_str) in strats:
for ss in [""] + [f"+sub{ii}" for ii in range(3)]:
for ddx in ["", "+dc"]:# todo prob here
for uud in ["", "+ud"]:
aig = spot.strategy_to_aig(strat, m+ss+ddx+uud)
aig = spot.mealy_machine_to_aig(strat, m+ss+ddx+uud)
strat2_s = aig.as_automaton(True)
if not spot.is_mealy_specialization(strat_s, strat2_s):
if not spot.is_split_mealy_specialization(strat_s,
strat2_s):
print(f"Mode is {m+ss+ddx+uud}")
print(f"""Strat is \n{strat_s.to_str("hoa")}""")
print(f"""Aig as aut is \n{strat2_s.to_str("hoa")}""")
@ -3361,7 +3362,7 @@ for aout in outs_str:
outs &= buddy.bdd_ithvar(strat.register_ap(aout))
spot.set_synthesis_outputs(strat, outs)
aig = spot.strategy_to_aig(strat, "isop")
aig = spot.mealy_machine_to_aig(strat, "isop")
ins = [True, False, False, False, True, True, True, True, True, True]
exp_latches = [(False, False),

50
tests/python/mealy.py
View file

@ -43,9 +43,10 @@ spot.set_synthesis_outputs(a, o1&o2)
b = spot.minimize_mealy(a)
assert(list(spot.get_state_players(b)).count(False) == 2)
assert(spot.is_mealy_specialization(a, b))
assert(spot.is_split_mealy_specialization(a, b))
test_auts = [("""HOA: v1
test_auts = [
("""HOA: v1
States: 22
Start: 0
AP: 6 "i0" "i1" "i2" "i3" "o0" "o1"
@ -360,13 +361,6 @@ for (mealy_str, nenv_min) in test_auts:
mealy = spot.automaton(mealy_str)
mealy.merge_edges()
mealy_min_ks = spot.minimize_mealy(mealy, -1, True)
mealy_min_us = spot.minimize_mealy(mealy, -1, False)
n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)])
assert(n_e == nenv_min)
assert(mealy_min_us.num_states() == nenv_min)
assert(spot.is_mealy_specialization(mealy, mealy_min_ks, True))
outs = buddy.bddtrue
ins = buddy.bddtrue
@ -378,8 +372,20 @@ for (mealy_str, nenv_min) in test_auts:
ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name()))
else:
assert("""Aps must start with either "i" or "o".""")
mealy_min_us_s = spot.split_2step(mealy_min_us, outs, False)
assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True))
spot.set_synthesis_outputs(mealy, outs)
mealy_min_ks = spot.minimize_mealy(mealy, -1)
n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)])
assert(n_e == nenv_min)
assert(spot.is_split_mealy_specialization(mealy, mealy_min_ks))
# Test un- and resplit
tmp = spot.unsplit_2step(mealy_min_ks)
mealy_min_rs = spot.split_2step(tmp, spot.get_synthesis_outputs(tmp), False)
assert(spot.is_split_mealy_specialization(mealy, mealy_min_rs, True))
assert(spot.are_equivalent(mealy_min_ks, mealy_min_rs))
# Testing bisimulation (with output assignment)
@ -498,13 +504,23 @@ State: 16
--END--""")
# Build an equivalent deterministic monitor
min_equiv = spot.minimize_mealy_fast(aut, False)
# ;
# ;
#
spot.set_synthesis_outputs(aut,
buddy.bdd_ithvar(
aut.register_ap("u02alarm29control02alarm29control"))\
& buddy.bdd_ithvar(
aut.register_ap("u02alarm29control0f1d2alarm29turn2on1b"))\
& buddy.bdd_ithvar(
aut.register_ap("u02alarm29control0f1d2alarm29turn2off1b")))
min_equiv = spot.reduce_mealy(aut, False)
assert min_equiv.num_states() == 6
assert spot.are_equivalent(min_equiv, aut)
# Build an automaton that recognizes a subset of the language of the original
# automaton
min_sub = spot.minimize_mealy_fast(aut, True)
min_sub = spot.reduce_mealy(aut, True)
assert min_sub.num_states() == 5
prod = spot.product(spot.complement(aut), min_sub)
assert spot.generic_emptiness_check(prod)
@ -531,6 +547,8 @@ State: 3
--END--
""")
spot.set_synthesis_outputs(aut, buddy.bdd_ithvar(aut.register_ap("b")))
exp = """HOA: v1
States: 1
Start: 0
@ -544,7 +562,7 @@ State: 0
--END--"""
# An example that shows that we should not build a tree when we use inclusion.
res = spot.minimize_mealy_fast(aut, True)
res = spot.reduce_mealy(aut, True)
assert res.to_str() == exp
aut = spot.automaton("""
@ -569,6 +587,8 @@ State: 3
--END--
""")
spot.set_synthesis_outputs(aut, buddy.bdd_ithvar(aut.register_ap("b")))
exp = """HOA: v1
States: 2
Start: 0
@ -585,7 +605,7 @@ State: 1
[0&1] 1
--END--"""
res = spot.minimize_mealy_fast(aut, True)
res = spot.reduce_mealy(aut, True)
assert res.to_str() == exp

4366
tests/python/synthesis.ipynb
View file

File diff suppressed because it is too large Load diff