synthesis: minor typos
* spot/twaalgos/game.cc, spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Here.
This commit is contained in:
parent
6555af1f44
commit
1443d45ac7
4 changed files with 18 additions and 19 deletions
|
|
@ -827,7 +827,7 @@ namespace spot
|
|||
auto um = arena->acc().unsat_mark();
|
||||
if (!um.first && complete0)
|
||||
throw std::runtime_error
|
||||
("alternate_players(): Can not complete monitor!");
|
||||
("alternate_players(): Cannot complete monitor.");
|
||||
|
||||
unsigned sink_env = 0;
|
||||
unsigned sink_con = 0;
|
||||
|
|
@ -857,8 +857,8 @@ namespace spot
|
|||
else if ((*owner)[e.dst] == osrc)
|
||||
{
|
||||
delete owner;
|
||||
throw
|
||||
std::runtime_error("alternate_players(): odd cycle detected");
|
||||
throw std::runtime_error
|
||||
("alternate_players(): Odd cycle detected.");
|
||||
}
|
||||
}
|
||||
if (complete0 && !(*owner)[src] && missing != bddfalse)
|
||||
|
|
|
|||
|
|
@ -938,9 +938,9 @@ namespace
|
|||
{
|
||||
#ifndef NDEBUG
|
||||
if (i >= dim_)
|
||||
throw std::runtime_error("i exceeds dim!");
|
||||
throw std::runtime_error("i exceeds dim");
|
||||
if (j >= dim_)
|
||||
throw std::runtime_error("j exceeds dim!");
|
||||
throw std::runtime_error("j exceeds dim");
|
||||
#endif
|
||||
return idx_(i, j);
|
||||
}
|
||||
|
|
@ -1068,7 +1068,7 @@ namespace
|
|||
return false;
|
||||
}
|
||||
return true;
|
||||
}() && "Player states have multiple edges!");
|
||||
}() && "Player states have multiple edges.");
|
||||
|
||||
#ifdef TRACE
|
||||
trace << "State reorganize mapping\n";
|
||||
|
|
@ -2029,13 +2029,13 @@ namespace
|
|||
auto [it, inserted] = sxi_map_.try_emplace(xi, next_var_);
|
||||
if (inserted)
|
||||
inc_var();
|
||||
assert((!frozen_xi_ || !inserted) && "Created lit when frozen!");
|
||||
assert((!frozen_xi_ || !inserted) && "Created lit when frozen.");
|
||||
return it->second;
|
||||
}
|
||||
|
||||
int sxi2lit(xi_t xi) const
|
||||
{
|
||||
assert(sxi_map_.count(xi) && "Can not create lit when const!");
|
||||
assert(sxi_map_.count(xi) && "Cannot create lit when const.");
|
||||
return sxi_map_.at(xi);
|
||||
}
|
||||
|
||||
|
|
@ -2059,11 +2059,11 @@ namespace
|
|||
|
||||
int ziaj2lit(iaj_t iaj)
|
||||
{
|
||||
assert(iaj.i < n_classes_ && "Exceeds source class!");
|
||||
assert(iaj.a < n_sigma_red_ && "Exceeds max letter idx!");
|
||||
assert(iaj.j < n_classes_&& "Exceeds dest class!");
|
||||
assert(iaj.i < n_classes_ && "Exceeds source class.");
|
||||
assert(iaj.a < n_sigma_red_ && "Exceeds max letter idx.");
|
||||
assert(iaj.j < n_classes_&& "Exceeds dest class.");
|
||||
auto [it, inserted] = ziaj_map_.try_emplace(iaj, next_var_);
|
||||
assert((!frozen_iaj_ || !inserted) && "Created lit when frozen!");
|
||||
assert((!frozen_iaj_ || !inserted) && "Created lit when frozen.");
|
||||
if (inserted)
|
||||
inc_var();
|
||||
return it->second;
|
||||
|
|
@ -2071,7 +2071,7 @@ namespace
|
|||
|
||||
int ziaj2lit(iaj_t iaj) const
|
||||
{
|
||||
assert(ziaj_map_.count(iaj) && "Can not create lit when const!");
|
||||
assert(ziaj_map_.count(iaj) && "Cannot create lit when const.");
|
||||
return ziaj_map_.at(iaj);
|
||||
}
|
||||
int get_iaj(iaj_t iai) const // Gets the literal or zero of not defined
|
||||
|
|
@ -3403,7 +3403,7 @@ namespace
|
|||
// partial solution
|
||||
x_in_class[i].second[psolv[i]] = true;
|
||||
unsigned first_x = find_first_index_of(x_in_class[i].second);
|
||||
assert(first_x != n_env && "No state in class!");
|
||||
assert(first_x != n_env && "No state in class.");
|
||||
x_in_class[i].first = red.which_group[first_x];
|
||||
}
|
||||
#ifdef TRACE
|
||||
|
|
|
|||
|
|
@ -454,7 +454,7 @@ namespace spot
|
|||
|
||||
auto [is_unsat, unsat_mark] = aut->acc().unsat_mark();
|
||||
if (!is_unsat && complete_env)
|
||||
throw std::runtime_error("split_2step(): Can not complete arena for "
|
||||
throw std::runtime_error("split_2step(): Cannot complete arena for "
|
||||
"env as there is no unsat mark.");
|
||||
|
||||
bdd input_bdd = bddtrue;
|
||||
|
|
|
|||
|
|
@ -44,16 +44,16 @@ namespace spot
|
|||
/// (p,a) may be non-deterministic.
|
||||
/// This function is used to transform an automaton into a turn-based game in
|
||||
/// the context of LTL reactive synthesis.
|
||||
/// The player of inputs (aka environment) plays first.
|
||||
///
|
||||
/// \param aut automaton to be transformed
|
||||
/// \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
|
||||
/// environment, i.e. the player of inputs
|
||||
/// \note This function also computes the state players
|
||||
/// \note If the automaton is to be completed for both env and player
|
||||
/// 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& output_bdd, bool complete_env);
|
||||
|
|
@ -172,8 +172,7 @@ namespace spot
|
|||
/// \ingroup synthesis
|
||||
/// \brief A struct that represents different types of mealy like
|
||||
/// objects
|
||||
struct SPOT_API
|
||||
mealy_like
|
||||
struct SPOT_API mealy_like
|
||||
{
|
||||
enum class realizability_code
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue