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

New game api

Browse source 
Introduce a new, uniform way to create and solve
games.
Games can now be created directly from specification
using creat_game, uniformly solved using
solve_game and transformed into a strategy
using create_strategy.
Strategy are mealy machines, which can be minimized.

* bin/ltlsynt.cc: Minor adaption
* spot/twaalgos/game.cc: solve_game, setters and getters
for named properties
* spot/twaalgos/game.hh: Here too
* spot/twaalgos/mealy_machine.cc: Minor adaption
* spot/twaalgos/synthesis.cc: create_game, create_strategy and
minimize_strategy
* spot/twaalgos/synthesis.hh: Here too
* tests/core/ltlsynt.test: Adapting
* tests/python/aiger.py
, tests/python/games.ipynb
, tests/python/mealy.py
, tests/python/parity.py
, tests/python/split.py: Adapting
This commit is contained in:
philipp 2021-08-13 14:50:16 +02:00 • committed by Florian Renkin
parent 786599ed20
commit 4260b17fba
12 changed files with 3163 additions and 305 deletions
Download patch file Download diff file Expand all files Collapse all files

13
bin/ltlsynt.cc
View file

@ -353,7 +353,7 @@ namespace
<< paritize_time << " seconds\n";
if (want_time)
sw.start();
dpa = split_2step(tmp, all_inputs, all_outputs, true, true);
dpa = split_2step(tmp, all_outputs, true, false);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
@ -376,7 +376,7 @@ namespace
<< " states\n";
if (want_time)
sw.start();
dpa = split_2step(aut, all_inputs, all_outputs, true, true);
dpa = split_2step(aut, all_outputs, true, false);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
@ -390,7 +390,7 @@ namespace
{
if (want_time)
sw.start();
auto split = split_2step(aut, all_inputs, all_outputs,
auto split = split_2step(aut, all_outputs,
true, false);
if (want_time)
split_time = sw.stop();
@ -447,7 +447,7 @@ namespace
if (want_time)
sw.start();
dpa = split_2step(dpa, all_inputs, all_outputs, true, true);
dpa = split_2step(dpa, all_outputs, true, false);
spot::colorize_parity_here(dpa, true);
if (want_time)
split_time = sw.stop();
@ -472,7 +472,7 @@ namespace
spot::print_hoa(std::cout, dpa, opt_print_hoa_args) << '\n';
return 0;
}
set_synthesis_outputs(dpa, all_outputs);
if (want_time)
sw.start();
bool player1winning = solve_parity_game(dpa);
@ -489,8 +489,7 @@ namespace
{
if (want_time)
sw.start();
auto strat_aut = apply_strategy(dpa, all_outputs,
true, false);
auto strat_aut = apply_strategy(dpa, true, false);
if (want_time)
strat2aut_time = sw.stop();

219
spot/twaalgos/game.cc
View file

@ -19,6 +19,9 @@
#include "config.h"
#include <utility>
#include <spot/misc/timer.hh>
#include <spot/twaalgos/game.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/sccinfo.hh>
@ -764,12 +767,81 @@ namespace spot
} // anonymous
std::ostream& operator<<(std::ostream& os, game_info::solver s)
{
using solver = game_info::solver;
switch (s)
{
case (solver::DET_SPLIT):
os << "ds";
break;
case (solver::SPLIT_DET):
os << "sd";
break;
case (solver::DPA_SPLIT):
os << "ps";
break;
case (solver::LAR):
os << "lar";
break;
case (solver::LAR_OLD):
os << "lar.old";
break;
}
return os;
}
std::ostream&
operator<<(std::ostream& os, const game_info& gi)
{
os << "force sbacc: " << gi.force_sbacc << '\n'
<< "solver: " << gi.s << '\n'
<< "minimization-lvl: " << gi.minimize_lvl << '\n'
<< (gi.verbose_stream ? "Is verbose\n" : "Is not verbose\n")
<< "the bdd_dict used is " << gi.dict.get();
return os;
}
bool solve_parity_game(const twa_graph_ptr& arena)
{
parity_game pg;
return pg.solve(arena);
}
bool solve_game(twa_graph_ptr arena, game_info& gi)
{
stopwatch sw;
if (gi.bv)
sw.start();
bool dummy1, dummy2;
bool ret;
if (arena->acc().is_parity(dummy1, dummy2, true))
{
if (gi.verbose_stream)
*(gi.verbose_stream) << "Identified as parity game.\n";
ret = solve_parity_game(arena);
}
else
throw std::runtime_error("No solver available for this arena due to its"
"acceptance condition.");
if (gi.bv)
gi.bv->solve_time += sw.stop();
if (gi.verbose_stream)
*(gi.verbose_stream) << "game solved in "
<< gi.bv->solve_time << " seconds\n";
return ret;
}
bool
solve_game(twa_graph_ptr arena)
{
game_info dummy1;
return solve_game(arena, dummy1);
}
void pg_print(std::ostream& os, const const_twa_graph_ptr& arena)
{
auto owner = ensure_parity_game(arena, "pg_print");
@ -901,60 +973,86 @@ namespace spot
return aut;
}
void set_state_players(twa_graph_ptr arena, std::vector<bool> owners)
void set_state_players(twa_graph_ptr arena, const region_t& owners)
{
std::vector<bool>* owners_ptr = new std::vector<bool>(owners);
set_state_players(arena, owners_ptr);
set_state_players(arena, region_t(owners));
}
void set_state_players(twa_graph_ptr arena, std::vector<bool>* owners)
void set_state_players(twa_graph_ptr arena, region_t&& owners)
{
if (owners->size() != arena->num_states())
if (owners.size() != arena->num_states())
throw std::runtime_error
("set_state_players(): There must be as many owners as states");
arena->set_named_prop<std::vector<bool>>("state-player", owners);
arena->set_named_prop<region_t>("state-player",
new region_t(std::forward<region_t>(owners)));
}
void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner)
void set_state_player(twa_graph_ptr arena, unsigned state, bool owner)
{
if (state >= arena->num_states())
throw std::runtime_error("set_state_player(): invalid state number");
std::vector<bool> *owners = arena->get_named_prop<std::vector<bool>>
("state-player");
region_t *owners = arena->get_named_prop<region_t>("state-player");
if (!owners)
{
owners = new std::vector<bool>(arena->num_states(), false);
arena->set_named_prop<std::vector<bool>>("state-player", owners);
}
throw std::runtime_error("set_state_player(): Can only set the state of "
"an individual "
"state if \"state-player\" already exists.");
if (owners->size() != arena->num_states())
throw std::runtime_error("set_state_player(): The \"state-player\" "
"vector has a different "
"size comparerd to the automaton! "
"Called new_state in between?");
(*owners)[state] = owner;
}
const std::vector<bool>& get_state_players(const_twa_graph_ptr arena)
const region_t& get_state_players(const_twa_graph_ptr arena)
{
std::vector<bool> *owners = arena->get_named_prop<std::vector<bool>>
region_t *owners = arena->get_named_prop<region_t>
("state-player");
if (!owners)
throw std::runtime_error
("get_state_players(): state-player property not defined, not a game");
("get_state_players(): state-player property not defined, not a game?");
return *owners;
}
unsigned get_state_player(const_twa_graph_ptr arena, unsigned state)
bool get_state_player(const_twa_graph_ptr arena, unsigned state)
{
if (state >= arena->num_states())
throw std::runtime_error("get_state_player(): invalid state number");
std::vector<bool>* owners = arena->get_named_prop<std::vector<bool>>
("state-player");
region_t* owners = arena->get_named_prop<region_t>("state-player");
if (!owners)
throw std::runtime_error
("get_state_player(): state-player property not defined, not a game");
("get_state_player(): state-player property not defined, not a game?");
return (*owners)[state] ? 1 : 0;
return (*owners)[state];
}
const strategy_t& get_strategy(const_twa_graph_ptr arena)
{
auto strat_ptr = arena->get_named_prop<strategy_t>("strategy");
if (!strat_ptr)
throw std::runtime_error("get_strategy(): Named prop "
"\"strategy\" not set."
"Arena not solved?");
return *strat_ptr;
}
void set_strategy(twa_graph_ptr arena, const strategy_t& strat)
{
set_strategy(arena, strategy_t(strat));
}
void set_strategy(twa_graph_ptr arena, strategy_t&& strat)
{
if (arena->num_states() != strat.size())
throw std::runtime_error("set_strategy(): strategies need to have "
"the same size as the automaton.");
arena->set_named_prop<strategy_t>("strategy",
new strategy_t(std::forward<strategy_t>(strat)));
}
void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs)
@ -971,6 +1069,85 @@ namespace spot
("get_synthesis_outputs(): synthesis-outputs not defined");
}
std::vector<std::string>
get_synthesis_output_aps(const const_twa_graph_ptr& arena)
{
std::vector<std::string> out_names;
bdd outs = get_synthesis_outputs(arena);
auto dict = arena->get_dict();
auto to_bdd = [&](const auto& x)
{
return bdd_ithvar(dict->has_registered_proposition(x, arena.get()));
};
for (const auto& ap : arena->ap())
if (bdd_implies(outs, to_bdd(ap)))
out_names.push_back(ap.ap_name());
return out_names;
}
void set_state_winners(twa_graph_ptr arena, const region_t& winners)
{
set_state_winners(arena, region_t(winners));
}
void set_state_winners(twa_graph_ptr arena, region_t&& winners)
{
if (winners.size() != arena->num_states())
throw std::runtime_error
("set_state_winners(): There must be as many winners as states");
arena->set_named_prop<region_t>("state-winner",
new region_t(std::forward<region_t>(winners)));
}
void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner)
{
if (state >= arena->num_states())
throw std::runtime_error("set_state_winner(): invalid state number");
region_t *winners = arena->get_named_prop<region_t>("state-winner");
if (!winners)
throw std::runtime_error("set_state_winner(): Can only set the state of "
"an individual "
"state if \"state-winner\" already exists.");
if (winners->size() != arena->num_states())
throw std::runtime_error("set_state_winner(): The \"state-winnerr\" "
"vector has a different "
"size compared to the automaton! "
"Called new_state in between?");
(*winners)[state] = winner;
}
const region_t& get_state_winners(const_twa_graph_ptr arena)
{
region_t *winners = arena->get_named_prop<region_t>("state-winner");
if (!winners)
throw std::runtime_error
("get_state_winners(): state-winner property not defined, not a game?");
return *winners;
}
bool get_state_winner(const_twa_graph_ptr arena, unsigned state)
{
if (state >= arena->num_states())
throw std::runtime_error("get_state_winner(): invalid state number");
region_t* winners = arena->get_named_prop<region_t>("state-winner");
if (!winners)
throw std::runtime_error
("get_state_winner(): state-winner property not defined, not a game?");
return (*winners)[state];
}
bool solve_safety_game(twa_graph_ptr game)
{

131
spot/twaalgos/game.hh
View file

@ -26,6 +26,7 @@
#include <vector>
#include <bddx.h>
#include <spot/misc/optionmap.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/parity.hh>
@ -88,6 +89,90 @@ namespace spot
SPOT_API
bool solve_safety_game(twa_graph_ptr game);
/// \brief Benchmarking and options structure for games and synthesis
///
/// \note This structure is designed to interface with the algorithms
/// found in spot/twaalgos/synthesis.hh
struct SPOT_API game_info
{
enum class solver
{
DET_SPLIT=0,
SPLIT_DET,
DPA_SPLIT,
LAR,
LAR_OLD,
};
struct bench_var
{
double total_time = 0.0;
double trans_time = 0.0;
double split_time = 0.0;
double paritize_time = 0.0;
double solve_time = 0.0;
double strat2aut_time = 0.0;
double aig_time = 0.0;
unsigned nb_states_arena = 0;
unsigned nb_states_arena_env = 0;
unsigned nb_states_parity_game = 0;
unsigned nb_strat_states = 0;
unsigned nb_strat_edges = 0;
unsigned nb_latches = 0;
unsigned nb_gates = 0;
bool realizable = false;
};
game_info()
: force_sbacc{false},
s{solver::LAR},
minimize_lvl{0},
out_choice{0},
bv{},
verbose_stream{nullptr},
dict(make_bdd_dict())
{
}
bool force_sbacc;
solver s;
int minimize_lvl;
int out_choice;
std::optional<bench_var> bv;
std::ostream* verbose_stream;
option_map opt;
bdd_dict_ptr dict;
};
/// \brief Stream solvers
SPOT_API std::ostream&
operator<<(std::ostream& os, game_info::solver s);
/// \brief Stream benchmarks and options
SPOT_API std::ostream &
operator<<(std::ostream &os, const game_info &gi);
/// \brief Generic interface for game solving
///
/// Calls the most suitable solver, depending on the type of game/
/// acceptance condition
///
/// \param arena The game arena
/// \param gi struct ofr options and benchmarking
/// \return Whether the initial state is won by player or not
/// \pre Relies on the named properties "state-player"
/// \post The named properties "strategy" and "state-winner" are set
SPOT_API bool
solve_game(twa_graph_ptr arena, game_info& gi);
/// \brief Generic interface for game solving
///
/// See solve_game(arena, gi)
SPOT_API bool
solve_game(twa_graph_ptr arena);
/// \brief Print a max odd parity game using PG-solver syntax
SPOT_API
void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
@ -103,26 +188,54 @@ namespace spot
/// \brief Set the owner for all the states.
SPOT_API
void set_state_players(twa_graph_ptr arena, std::vector<bool> owners);
void set_state_players(twa_graph_ptr arena, const region_t& owners);
SPOT_API
void set_state_players(twa_graph_ptr arena, std::vector<bool>* owners);
void set_state_players(twa_graph_ptr arena, region_t&& owners);
/// \brief Set the owner of a state.
SPOT_API
void set_state_player(twa_graph_ptr arena, unsigned state, unsigned owner);
/// \brief Get the owner of all the state.
SPOT_API
const std::vector<bool>& get_state_players(const_twa_graph_ptr arena);
void set_state_player(twa_graph_ptr arena, unsigned state, bool owner);
/// \brief Get the owner of a state.
SPOT_API
unsigned get_state_player(const_twa_graph_ptr arena, unsigned state);
bool get_state_player(const_twa_graph_ptr arena, unsigned state);
/// \brief Get the owner of all states
SPOT_API
const region_t& get_state_players(const_twa_graph_ptr arena);
/// \brief Get or set the strategy
SPOT_API
const strategy_t& get_strategy(const_twa_graph_ptr arena);
SPOT_API
void set_strategy(twa_graph_ptr arena, const strategy_t& strat);
SPOT_API
void set_strategy(twa_graph_ptr arena, strategy_t&& strat);
/// \brief Set all synthesis outputs as a conjunction
SPOT_API
void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
SPOT_API
bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
/// \brief Get the vector with the names of the output propositions
SPOT_API
std::vector<std::string>
get_synthesis_output_aps(const const_twa_graph_ptr& arena);
/// \brief Set the winner for all the states.
SPOT_API
void set_state_winners(twa_graph_ptr arena, const region_t& winners);
SPOT_API
void set_state_winners(twa_graph_ptr arena, region_t&& winners);
/// \brief Set the winner of a state.
SPOT_API
void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner);
/// \brief Get the winner of a state.
SPOT_API
bool get_state_winner(const_twa_graph_ptr arena, unsigned state);
/// \brief Get the winner of all states
SPOT_API
const region_t& get_state_winners(const_twa_graph_ptr arena);
}

14
spot/twaalgos/mealy_machine.cc
View file

@ -507,12 +507,7 @@ namespace spot
// Split if the initial aut was split
if (orig_is_split)
{
bdd ins = bddtrue;
for (const auto& ap : mmc->ap())
if (!bdd_implies(outs,
bdd_ithvar(mmc->register_ap(ap))))
ins &= bdd_ithvar(mmc->register_ap(ap));
mmc = split_2step(mmc, ins, outs, false, false);
mmc = split_2step(mmc, outs, false, false);
bool orig_init_player =
mm->get_named_prop<std::vector<bool>>("state-player")
->at(mm->get_init_state_number());
@ -587,12 +582,7 @@ namespace spot
mm->purge_unreachable_states();
if (orig_is_split)
{
bdd ins = bddtrue;
for (const auto& ap : mm->ap())
if (!bdd_implies(outs,
bdd_ithvar(mm->register_ap(ap))))
ins &= bdd_ithvar(mm->register_ap(ap));
mm = split_2step(mm, ins, outs, false, false);
mm = split_2step(mm, outs, false, false);
alternate_players(mm, init_player, false);
mm->set_named_prop("synthesis-outputs", new bdd(outs));
}

846
spot/twaalgos/synthesis.cc
View file

@ -18,10 +18,22 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/misc/bddlt.hh>
#include <spot/misc/hash.hh>
#include <spot/misc/timer.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/mealy_machine.hh>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/synthesis.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/misc/minato.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twaalgos/toparity.hh>
#include <spot/tl/parse.hh>
#include <algorithm>
@ -122,7 +134,7 @@ namespace{
namespace spot
{
twa_graph_ptr
split_2step(const const_twa_graph_ptr& aut, const bdd& input_bdd,
split_2step(const const_twa_graph_ptr& aut,
const bdd& output_bdd, bool complete_env,
bool do_simplify)
{
@ -132,6 +144,21 @@ namespace spot
split->new_states(aut->num_states());
split->set_init_state(aut->get_init_state_number());
bdd input_bdd = bddtrue;
{
bdd allbdd = aut->ap_vars();
while (allbdd != bddtrue)
{
bdd l = bdd_ithvar(bdd_var(allbdd));
if (not bdd_implies(output_bdd, l))
// Input
input_bdd &= l;
allbdd = bdd_high(allbdd);
assert(allbdd != bddfalse);
}
}
// The environment has all states
// with num <= aut->num_states();
// So we can first loop over the aut
@ -292,11 +319,10 @@ namespace spot
// The named property
// compute the owners
// env is equal to false
std::vector<bool>* owner =
new std::vector<bool>(split->num_states(), false);
std::vector<bool> owner(split->num_states(), false);
// All "new" states belong to the player
std::fill(owner->begin()+aut->num_states(), owner->end(), true);
split->set_named_prop("state-player", owner);
std::fill(owner.begin()+aut->num_states(), owner.end(), true);
set_state_players(split, std::move(owner));
// Done
return split;
}
@ -312,10 +338,7 @@ namespace spot
// split_2step is not guaranteed to produce
// states that alternate between env and player do to do_simplify
auto owner_ptr = aut->get_named_prop<std::vector<bool>>("state-player");
if (!owner_ptr)
throw std::runtime_error("unsplit requires the named prop "
"state-player as set by split_2step");
auto owner = get_state_players(aut);
std::vector<unsigned> state_map(aut->num_states(), unseen_mark);
auto seen = [&](unsigned s){return state_map[s] != unseen_mark; };
@ -338,7 +361,7 @@ namespace spot
for (const auto& i : aut->out(cur))
{
// if the dst is also owned env
if (!(*owner_ptr)[i.dst])
if (!owner[i.dst])
{
// This can only happen if there is only
// one outgoing edges for cur
@ -364,129 +387,730 @@ namespace spot
out->set_init_state(map_s(aut->get_init_state_number()));
// Try to set outputs
if (bdd* outptr = aut->get_named_prop<bdd>("synthesis-outputs"))
out->set_named_prop("synthesis-outputs", new bdd(*outptr));
set_synthesis_outputs(out, *outptr);
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,
bdd all_outputs,
bool unsplit, bool keep_acc)
{
std::vector<bool>* w_ptr =
arena->get_named_prop<std::vector<bool>>("state-winner");
std::vector<unsigned>* s_ptr =
arena->get_named_prop<std::vector<unsigned>>("strategy");
std::vector<bool>* sp_ptr =
arena->get_named_prop<std::vector<bool>>("state-player");
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 (!w_ptr || !s_ptr || !sp_ptr)
throw std::runtime_error("Arena missing state-winner, strategy "
"or state-player");
if (!(w_ptr->at(arena->get_init_state_number())))
if (!win[arena->get_init_state_number()])
throw std::runtime_error("Player does not win initial state, strategy "
"is not applicable");
std::vector<bool>& w = *w_ptr;
std::vector<unsigned>& s = *s_ptr;
assert((sp[arena->get_init_state_number()] == false)
&& "Env needs to have first turn!");
auto aut = spot::make_twa_graph(arena->get_dict());
aut->copy_ap_of(arena);
assert(std::all_of(arena->edges().begin(), arena->edges().end(),
[&sp](const auto& e)
{ return sp.at(e.src) != sp.at(e.dst); }));
auto strat_split = spot::make_twa_graph(arena->get_dict());
strat_split->copy_ap_of(arena);
if (keep_acc)
aut->copy_acceptance_of(arena);
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))
^ 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> todo{arena->get_init_state_number()};
std::vector<unsigned> pg2aut(arena->num_states(), unseen_mark);
aut->set_init_state(aut->new_state());
pg2aut[arena->get_init_state_number()] = aut->get_init_state_number();
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 v = todo.back();
todo.pop_back();
// Check if a simplification occurred
// in the aut and we have env -> env
// Env edge -> keep all
for (auto &e1: arena->out(v))
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))
{
assert(w.at(e1.dst));
// Check if a simplification occurred
// in the aut and we have env -> env
if (!(*sp_ptr)[e1.dst])
{
assert(([&arena, v]()
{
auto out_cont = arena->out(v);
return (++(out_cont.begin()) == out_cont.end());
})());
// If so we do not need to unsplit
if (pg2aut[e1.dst] == unseen_mark)
{
pg2aut[e1.dst] = aut->new_state();
todo.push_back(e1.dst);
}
// Create the edge
aut->new_edge(pg2aut[v],
pg2aut[e1.dst],
e1.cond,
keep_acc ? e1.acc : spot::acc_cond::mark_t({}));
// Done
continue;
}
if (!unsplit)
{
if (pg2aut[e1.dst] == unseen_mark)
pg2aut[e1.dst] = aut->new_state();
aut->new_edge(pg2aut[v], pg2aut[e1.dst], e1.cond,
keep_acc ? e1.acc : spot::acc_cond::mark_t({}));
}
// Player strat
auto &e2 = arena->edge_storage(s[e1.dst]);
if (pg2aut[e2.dst] == unseen_mark)
{
pg2aut[e2.dst] = aut->new_state();
todo.push_back(e2.dst);
}
aut->new_edge(unsplit ? pg2aut[v] : pg2aut[e1.dst],
pg2aut[e2.dst],
unsplit ? (e1.cond & e2.cond) : e2.cond,
keep_acc ? e2.acc : spot::acc_cond::mark_t({}));
// 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;
aut->set_named_prop("synthesis-outputs", new bdd(all_outputs));
// If no unsplitting is demanded, it remains a two-player arena
// We do not need to track winner as this is a
// strategy automaton
if (!unsplit)
// 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)
{
const std::vector<bool>& sp_pg = * sp_ptr;
std::vector<bool> sp_aut(aut->num_states());
std::vector<unsigned> str_aut(aut->num_states());
for (unsigned i = 0; i < arena->num_states(); ++i)
{
if (pg2aut[i] == unseen_mark)
// Does not appear in strategy
continue;
sp_aut[pg2aut[i]] = sp_pg[i];
str_aut[pg2aut[i]] = s[i];
}
aut->set_named_prop(
"state-player", new std::vector<bool>(std::move(sp_aut)));
aut->set_named_prop(
"state-winner", new std::vector<bool>(aut->num_states(), true));
aut->set_named_prop(
"strategy", new std::vector<unsigned>(std::move(str_aut)));
}
return aut;
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());
});
};
// print_hoa(std::cout, strat_split) << '\n';
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;
}
}
// std::for_each(remap.begin(), remap.end(),
// [](auto e){std::cout << e << ' ';});
// std::cout << std::endl;
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;
}
}
// std::for_each(remap.begin(), remap.end(), [](auto e)
// {std::cout << e << ' '; });
// std::cout << std::endl;
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]);
}
}
// print_hoa(std::cout, strat_split) << std::endl;
// 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);
// unsigned n_old;
// do
// {
// n_old = strat_split->num_edges();
// strat_split->merge_edges();
// strat_split->merge_states();
// } while (n_old != strat_split->num_edges());
alternate_players(strat_split, false, false);
// print_hoa(std::cout, strat_split) << std::endl;
// 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;
}
} // spot
namespace // Anonymous create_game
{
static translator
create_translator(game_info& gi)
{
using solver = game_info::solver;
option_map& extra_options = gi.opt;
auto sol = gi.s;
const bdd_dict_ptr& dict = gi.dict;
for (auto&& p : std::vector<std::pair<const char*, int>>
{{"simul", 0},
{"ba-simul", 0},
{"det-simul", 0},
{"tls-impl", 1},
{"wdba-minimize", 2}})
extra_options.set(p.first, extra_options.get(p.first, p.second));
translator trans(dict, &extra_options);
switch (sol)
{
case solver::LAR:
SPOT_FALLTHROUGH;
case solver::LAR_OLD:
trans.set_type(postprocessor::Generic);
trans.set_pref(postprocessor::Deterministic);
break;
case solver::DPA_SPLIT:
trans.set_type(postprocessor::ParityMaxOdd);
trans.set_pref(postprocessor::Deterministic | postprocessor::Colored);
break;
case solver::DET_SPLIT:
SPOT_FALLTHROUGH;
case solver::SPLIT_DET:
break;
}
return trans;
}
twa_graph_ptr
ntgba2dpa(const twa_graph_ptr& aut, bool force_sbacc)
{
// if the input automaton is deterministic, degeneralize it to be sure to
// end up with a parity automaton
auto dpa = tgba_determinize(degeneralize_tba(aut),
false, true, true, false);
dpa->merge_edges();
if (force_sbacc)
dpa = sbacc(dpa);
reduce_parity_here(dpa, true);
change_parity_here(dpa, parity_kind_max,
parity_style_odd);
assert((
[&dpa]() -> bool {
bool max, odd;
dpa->acc().is_parity(max, odd);
return max && odd;
}()));
assert(is_deterministic(dpa));
return dpa;
}
} // anonymous
twa_graph_ptr
create_game(const formula& f,
const std::vector<std::string>& all_outs,
game_info& gi)
{
using solver = game_info::solver;
[](std::vector<std::string> sv, std::string msg)
{
std::sort(sv.begin(), sv.end());
const unsigned svs = sv.size() - 1;
for (unsigned i = 0; i < svs; ++i)
if (sv[i] == sv[i+1])
throw std::runtime_error(msg + sv[i]);
}(all_outs, "Output propositions are expected to appear once "
"in all_outs. Violating: ");
auto trans = create_translator(gi);
// Shortcuts
auto& bv = gi.bv;
auto& vs = gi.verbose_stream;
stopwatch sw;
if (bv)
sw.start();
auto aut = trans.run(f);
if (bv)
bv->trans_time += sw.stop();
if (vs)
{
assert(bv);
*vs << "translating formula done in "
<< bv->trans_time << " seconds\n";
*vs << "automaton has " << aut->num_states()
<< " states and " << aut->num_sets() << " colors\n";
}
auto tobdd = [&aut](const std::string& ap_name)
{
return bdd_ithvar(aut->register_ap(ap_name));
};
auto is_out = [&all_outs](const std::string& ao)->bool
{
return std::find(all_outs.begin(), all_outs.end(),
ao) != all_outs.end();
};
// Check for each ap that actually appears in the graph
// whether its an in or out
bdd ins = bddtrue;
bdd outs = bddtrue;
for (auto&& aap : aut->ap())
{
if (is_out(aap.ap_name()))
outs &= tobdd(aap.ap_name());
else
ins &= tobdd(aap.ap_name());
}
twa_graph_ptr dpa = nullptr;
switch (gi.s)
{
case solver::DET_SPLIT:
{
if (bv)
sw.start();
auto tmp = ntgba2dpa(aut, gi.force_sbacc);
if (vs)
*vs << "determinization done\nDPA has "
<< tmp->num_states() << " states, "
<< tmp->num_sets() << " colors\n";
tmp->merge_states();
if (bv)
bv->paritize_time += sw.stop();
if (vs)
*vs << "simplification done\nDPA has "
<< tmp->num_states() << " states\n"
<< "determinization and simplification took "
<< bv->paritize_time << " seconds\n";
if (bv)
sw.start();
dpa = split_2step(tmp, outs, true, false);
colorize_parity_here(dpa, true);
if (bv)
bv->split_time += sw.stop();
if (vs)
*vs << "split inputs and outputs done in " << bv->split_time
<< " seconds\nautomaton has "
<< tmp->num_states() << " states\n";
break;
}
case solver::DPA_SPLIT:
{
if (bv)
sw.start();
aut->merge_states();
if (bv)
bv->paritize_time += sw.stop();
if (vs)
*vs << "simplification done in " << bv->paritize_time
<< " seconds\nDPA has " << aut->num_states()
<< " states\n";
if (bv)
sw.start();
dpa = split_2step(aut, outs, true, false);
colorize_parity_here(dpa, true);
if (bv)
bv->split_time += sw.stop();
if (vs)
*vs << "split inputs and outputs done in " << bv->split_time
<< " seconds\nautomaton has "
<< dpa->num_states() << " states\n";
break;
}
case solver::SPLIT_DET:
{
sw.start();
auto split = split_2step(aut, outs,
true, false);
if (bv)
bv->split_time += sw.stop();
if (vs)
*vs << "split inputs and outputs done in " << bv->split_time
<< " seconds\nautomaton has "
<< split->num_states() << " states\n";
if (bv)
sw.start();
dpa = ntgba2dpa(split, gi.force_sbacc);
if (vs)
*vs << "determinization done\nDPA has "
<< dpa->num_states() << " states, "
<< dpa->num_sets() << " colors\n";
dpa->merge_states();
if (bv)
bv->paritize_time += sw.stop();
if (vs)
*vs << "simplification done\nDPA has "
<< dpa->num_states() << " states\n"
<< "determinization and simplification took "
<< bv->paritize_time << " seconds\n";
// The named property "state-player" is set in split_2step
// but not propagated by ntgba2dpa
alternate_players(dpa);
break;
}
case solver::LAR:
SPOT_FALLTHROUGH;
case solver::LAR_OLD:
{
if (bv)
sw.start();
if (gi.s == solver::LAR)
{
dpa = to_parity(aut);
// reduce_parity is called by to_parity(),
// but with colorization turned off.
colorize_parity_here(dpa, true);
}
else
{
dpa = to_parity_old(aut);
dpa = reduce_parity_here(dpa, true);
}
change_parity_here(dpa, parity_kind_max, parity_style_odd);
if (bv)
bv->paritize_time += sw.stop();
if (vs)
*vs << "LAR construction done in " << bv->paritize_time
<< " seconds\nDPA has "
<< dpa->num_states() << " states, "
<< dpa->num_sets() << " colors\n";
if (bv)
sw.start();
dpa = split_2step(dpa, outs, true, false);
colorize_parity_here(dpa, true);
if (bv)
bv->split_time += sw.stop();
if (vs)
*vs << "split inputs and outputs done in " << bv->split_time
<< " seconds\nautomaton has "
<< dpa->num_states() << " states\n";
break;
}
} //end switch solver
// Set the named properties
assert(dpa->get_named_prop<std::vector<bool>>("state-player")
&& "DPA has no state-players");
set_synthesis_outputs(dpa, outs);
return dpa;
}
twa_graph_ptr
create_game(const formula& f,
const std::vector<std::string>& all_outs)
{
game_info dummy;
return create_game(f, all_outs, dummy);
}
twa_graph_ptr
create_game(const std::string& f,
const std::vector<std::string>& all_outs)
{
return create_game(parse_formula(f), all_outs);
}
twa_graph_ptr
create_game(const std::string& f,
const std::vector<std::string>& all_outs,
game_info& gi)
{
return create_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, game_info& gi)
{
if (!arena)
throw std::runtime_error("Arena can not be null");
spot::stopwatch sw;
if (gi.bv)
sw.start();
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;
twa_graph_ptr strat_aut = apply_strategy(arena, do_unsplit, false);
strat_aut->prop_universal(true);
minimize_strategy_here(strat_aut, gi.minimize_lvl);
assert(do_unsplit
|| strat_aut->get_named_prop<std::vector<bool>>("state-player"));
if (!do_unsplit)
strat_aut = unsplit_2step(strat_aut);
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();
}
return strat_aut;
}
twa_graph_ptr
create_strategy(twa_graph_ptr arena)
{
game_info dummy;
return create_strategy(arena, dummy);
}
} // spot

73
spot/twaalgos/synthesis.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2020 Laboratoire de Recherche et
// Copyright (C) 2020-2021 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -20,6 +20,7 @@
#pragma once
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/game.hh>
#include <bddx.h>
namespace spot
@ -40,8 +41,8 @@ namespace spot
/// This function is used to transform an automaton into a turn-based game in
/// the context of LTL reactive synthesis.
/// \param aut automaton to be transformed
/// \param input_bdd conjunction of all input AP
/// \param output_bdd conjunction of all output AP
/// \param output_bdd conjunction of all output AP, all APs not present
/// are treated as inputs
/// \param complete_env Whether the automaton should be complete for the
/// environment, i.e. the player of I
/// \param do_simplify If a state has a single outgoing transition
@ -52,7 +53,7 @@ namespace spot
/// then egdes between the sinks will be added
/// (assuming that the environnement/player of I) plays first
SPOT_API twa_graph_ptr
split_2step(const const_twa_graph_ptr& aut, const bdd& input_bdd,
split_2step(const const_twa_graph_ptr& aut,
const bdd& output_bdd, bool complete_env, bool do_simplify);
/// \brief the reverse of split_2step
@ -62,16 +63,74 @@ namespace spot
unsplit_2step(const const_twa_graph_ptr& aut);
/// \brief Takes a solved game and restricts the automat to the
/// \brief Creates a game from a specification and a set of
/// output propositions
///
/// \param f The specification given as LTL/PSL formula
/// \param all_outs The names of all output propositions
/// \param gi game_info structure
/// \note All propositions in the formula that do not appear in all_outs
/// arer treated as input variables.
SPOT_API twa_graph_ptr
create_game(const formula& f,
const std::vector<std::string>& all_outs,
game_info& gi);
/// \brief create_game called with default options
SPOT_API twa_graph_ptr
create_game(const formula& f,
const std::vector<std::string>& all_outs);
/// \brief Like create_game but formula given as string
SPOT_API twa_graph_ptr
create_game(const std::string& f,
const std::vector<std::string>& all_outs,
game_info& gi);
/// \brief create_game called with default options
SPOT_API twa_graph_ptr
create_game(const std::string& f,
const std::vector<std::string>& all_outs);
/// \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 all_outputs bdd of all output signals
/// \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,
bdd all_outputs, bool unsplit, bool keep_acc);
bool unsplit, bool keep_acc);
/// \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
SPOT_API void
minimize_strategy_here(twa_graph_ptr& strat, int min_lvl);
///\brief Like minimize_strategy_here
SPOT_API twa_graph_ptr
minimize_strategy(const_twa_graph_ptr& strat, int min_lvl);
/// \brief creates a strategy from a solved game taking into account the
/// options given in gi
SPOT_API twa_graph_ptr
create_strategy(twa_graph_ptr arena, game_info& gi);
SPOT_API twa_graph_ptr
create_strategy(twa_graph_ptr arena);
}

152
tests/core/ltlsynt.test
View file

@ -74,17 +74,11 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 9 1 2 1 6
aag 3 1 1 1 1
2
4 16
6 18
14
8 5 7
10 4 6
12 2 9
14 11 12
16 3 11
18 2 11
4 1
6
6 2 4
i0 a
o0 b
EOF
@ -93,14 +87,10 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 6 1 2 1 3
aag 2 1 1 1 0
2
4 1
2
4 12
6 10
10
8 4 6
10 2 9
12 3 9
i0 a
o0 b
EOF
@ -109,21 +99,11 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 13 1 2 1 10
aag 3 1 1 1 1
2
4 23
6 27
17
8 2 5
10 6 8
12 2 4
14 7 12
16 11 15
18 3 5
20 3 7
22 19 21
24 2 7
26 9 25
4 1
6
6 2 4
i0 a
o0 b
EOF
@ -132,17 +112,11 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 9 1 2 1 6
aag 3 1 1 1 1
2
4 16
6 18
14
8 5 7
10 4 6
12 2 9
14 11 12
16 3 11
18 2 11
4 1
6
6 2 4
i0 a
o0 b
EOF
@ -151,18 +125,11 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 10 1 2 1 7
aag 3 1 1 1 1
2
4 18
6 20
14
8 5 6
10 4 7
12 9 11
14 2 13
16 4 6
18 3 17
20 2 17
4 1
6
6 2 4
i0 a
o0 b
EOF
@ -171,14 +138,10 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 6 1 2 1 3
aag 2 1 1 1 0
2
4 1
2
4 12
6 10
10
8 4 6
10 2 9
12 3 9
i0 a
o0 b
EOF
@ -187,18 +150,11 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 10 1 2 1 7
aag 3 1 1 1 1
2
4 18
6 20
14
8 4 7
10 5 6
12 11 9
14 2 13
16 4 9
18 3 17
20 2 17
4 1
6
6 2 4
i0 a
o0 b
EOF
@ -207,15 +163,10 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 7 1 2 1 4
aag 2 1 1 1 0
2
4 1
2
4 14
6 12
12
8 4 7
10 4 9
12 2 11
14 3 11
i0 a
o0 b
EOF
@ -224,18 +175,12 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 9 1 2 2 6
aag 3 1 1 2 1
2
4 16
6 18
14
14
8 5 7
10 4 6
12 2 9
14 11 12
16 3 11
18 2 11
4 1
6
6
6 2 4
i0 a
o0 b
o1 c
@ -245,15 +190,11 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 6 1 2 2 3
aag 2 1 1 2 0
2
4 1
2
2
4 12
6 10
10
10
8 4 6
10 2 9
12 3 9
i0 a
o0 b
o1 c
@ -263,19 +204,12 @@ diff out exp
cat >exp <<EOF
REALIZABLE
aag 10 1 2 2 7
aag 3 1 1 2 1
2
4 18
6 20
14
14
8 4 7
10 5 6
12 11 9
14 2 13
16 4 9
18 3 17
20 2 17
4 1
6
6
6 4 2
i0 a
o0 b
o1 c

2
tests/python/aiger.py
View file

@ -3333,7 +3333,7 @@ for strat_string, (ins_str, outs_str) in strats:
outs &= buddy.bdd_ithvar(strat.register_ap(aout))
spot.set_synthesis_outputs(strat, outs)
strat_s = spot.split_2step(strat, ins, outs, False, False)
strat_s = spot.split_2step(strat, outs, False, False)
for m in ["isop", "ite", "both"]:
for ss in [""] + [f"+sub{ii}" for ii in range(3)]:

1995
tests/python/games.ipynb
View file

File diff suppressed because it is too large Load diff

2
tests/python/mealy.py
View file

@ -378,7 +378,7 @@ 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, ins, outs, False, False)
mealy_min_us_s = spot.split_2step(mealy_min_us, outs, False, False)
assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True))

16
tests/python/parity.py
View file

@ -124,10 +124,16 @@ except RuntimeError as e:
else:
report_missing_exception()
spot.set_state_player(a, 1, 1)
assert spot.get_state_players(a) == (False, True, False)
assert spot.get_state_player(a, 0) == 0
assert spot.get_state_player(a, 1) == 1
try:
spot.set_state_player(a, 1, True)
except RuntimeError as e:
assert "Can only" in str(e)
else:
report_missing__exception()
spot.set_state_players(a, (False, True, False))
assert spot.get_state_player(a, 0) == False
assert spot.get_state_player(a, 1) == True
assert spot.get_state_player(a, 2) == False
try:
spot.set_state_players(a, [True, False, False, False])
@ -144,7 +150,7 @@ else:
report_missing_exception()
try:
spot.set_state_player(a, 4, 1)
spot.set_state_player(a, 4, True)
except RuntimeError as e:
assert "invalid state number" in str(e)
else:

5
tests/python/split.py
View file

@ -43,13 +43,10 @@ def equiv(a, b):
def do_split(f, in_list, out_list):
aut = spot.translate(f)
inputs = spot.buddy.bddtrue
for a in in_list:
inputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a)))
outputs = spot.buddy.bddtrue
for a in out_list:
outputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a)))
s = spot.split_2step(aut, inputs, outputs, False, False)
s = spot.split_2step(aut, outputs, False, False)
return aut, s
def str_diff(expect, obtained):