From 1443d45ac72685a70dba7277e6138f97962c3e83 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Nov 2021 22:44:08 +0100 Subject: [PATCH] synthesis: minor typos * spot/twaalgos/game.cc, spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Here. --- spot/twaalgos/game.cc | 6 +++--- spot/twaalgos/mealy_machine.cc | 22 +++++++++++----------- spot/twaalgos/synthesis.cc | 2 +- spot/twaalgos/synthesis.hh | 7 +++---- 4 files changed, 18 insertions(+), 19 deletions(-) diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 3a9a00088..9b8fdcee9 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -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) diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index f4b15b9d4..ac8107247 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -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 diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index ca176dfcd..08cfcad30 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -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; diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index f9e0d6cf5..9ecd90e73 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -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 {