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

Add setter and getter for synthesis-outputs

Browse source 
* spot/twaalgos/game.cc, spot/twaalgos/game.hh: Here
This commit is contained in:
philipp 2021-07-12 08:09:11 +02:00
parent 08113e0e04
commit e8f5865fb8
2 changed files with 24 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

19
spot/twaalgos/game.cc
View file

@ -809,9 +809,9 @@ namespace spot
bool first_player, bool complete0)
{
auto um = arena->acc().unsat_mark();
if (!um.first)
if (!um.first && complete0)
throw std::runtime_error
("alternate_players(): game winning condition is a tautology");
("alternate_players(): Can not complete monitor!");
unsigned sink_env = 0;
unsigned sink_con = 0;
@ -957,6 +957,21 @@ namespace spot
return (*owners)[state] ? 1 : 0;
}
void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs)
{
arena->set_named_prop<bdd>("synthesis-outputs", new bdd(outs));
}
bdd get_synthesis_outputs(const const_twa_graph_ptr& arena)
{
if (auto outptr = arena->get_named_prop<bdd>("synthesis-outputs"))
return *outptr;
else
throw std::runtime_error
("get_synthesis_outputs(): synthesis-outputs not defined");
}
bool solve_safety_game(twa_graph_ptr game)
{
if (!game->acc().is_t())

7
spot/twaalgos/game.hh
View file

@ -118,4 +118,11 @@ namespace spot
/// \brief Get the owner of a state.
SPOT_API
unsigned get_state_player(const_twa_graph_ptr arena, unsigned state);
/// \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);
}