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

aiger: fix some typos and inconsistencies

Browse source 
* spot/twaalgos/aiger.hh: Fix errors in documentation.
* spot/twaalgos/aiger.cc: Adjust text of exception.
This commit is contained in:
Alexandre Duret-Lutz 2021-10-03 18:33:57 +02:00
parent 590929fbcf
commit 17070b6cee
2 changed files with 23 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/aiger.cc
View file

@ -1706,7 +1706,7 @@ namespace
else else
throw std::runtime_error(buffer + " does not describe a " throw std::runtime_error(buffer + " does not describe a "
"mode supported for AIGER creation. Expected\n" "mode supported for AIGER creation. Expected\n"
"ite|isop|both[+sub][+dc][+ud]\n" "ite|isop|both[+sub0|sub1|sub2][+dc][+ud]\n"
"or a coma separated list of such expressions."); "or a coma separated list of such expressions.");
} }
res.push_back(std::move(this_opt)); res.push_back(std::move(this_opt));

44
spot/twaalgos/aiger.hh
View file

@ -50,7 +50,7 @@ namespace spot
/// AIG circuits can be used to represent controllers, which is currently /// AIG circuits can be used to represent controllers, which is currently
/// their sole purpose within spot. /// their sole purpose within spot.
/// AIGs produce a output sequence based on the following rules: /// AIGs produce a output sequence based on the following rules:
/// 1) All latches are initialised to 0 /// 1) All latches are initialized to 0
/// 2) The next input is read. /// 2) The next input is read.
/// 3) The output and the state of the latches for the next turn /// 3) The output and the state of the latches for the next turn
/// are given by the gates as a function of the current latches and inputs /// are given by the gates as a function of the current latches and inputs
@ -145,17 +145,17 @@ namespace spot
/// \brief roll_back to the saved point. /// \brief roll_back to the saved point.
/// ///
/// \param sp : The safe_point to revert back to /// \param sp The safe_point to revert back to
/// \param do_stash : Whether or not to save the changes to be possibly /// \param do_stash Whether or not to save the changes to be possibly
/// reapplied later on /// reapplied later on
/// \note: This function is semi-public. Make sure you know what you are /// \note This function is semi-public. Make sure you know what you are
/// doing when using it. /// doing when using it.
safe_stash roll_back_(safe_point sp, safe_stash roll_back_(safe_point sp,
bool do_stash = false); bool do_stash = false);
/// \brief Reapply to stored changes on top of a safe_point /// \brief Reapply to stored changes on top of a safe_point
/// \note: ss has to be obtained from roll_back_(sp, true) /// \note \a ss has to be obtained from `roll_back_(sp, true)`
/// This function is semi-public. Make sure you know what you are /// This function is semi-public. Make sure you know what you are
/// doing when using it. /// doing when using it.
void reapply_(safe_point sp, const safe_stash& ss); void reapply_(safe_point sp, const safe_stash& ss);
/// \brief Get the number of outputs /// \brief Get the number of outputs
@ -163,8 +163,8 @@ namespace spot
{ {
return num_outputs_; return num_outputs_;
} }
/// \brief Get the variables associated to the ouputs /// \brief Get the variables associated to the outputs
/// \note Only available after call to aig::set_output /// \note Only available after a call to aig::set_output
const std::vector<unsigned>& outputs() const const std::vector<unsigned>& outputs() const
{ {
SPOT_ASSERT(std::none_of(outputs_.begin(), outputs_.end(), SPOT_ASSERT(std::none_of(outputs_.begin(), outputs_.end(),
@ -414,20 +414,20 @@ namespace spot
}; };
/// \brief Convert a strategy into an aig relying on the transformation /// \brief Convert a strategy into an aig relying on the transformation
/// described by mode. /// described by \a mode.
/// \param mode This param has to be of the form /// \param mode This param has to be of the form
/// ite|isop|both [+dc][+dual][+so0|+so1|+so2|+so3] /// `ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2]`
/// Where ite means encoded via if-then-else normalform /// Where `ite` means encoded via if-then-else normal form,
/// isop means encoded via irreducible sum of products /// `isop` means encoded via irredundant sum-of-products,
/// both means trying both encodings and keep the smaller circuit. /// `both` means trying both encodings to keep the smaller one.
/// +dc is optional and tries to take advantage of "do not care" /// `+dc` is optional and tries to take advantage of "do not care"
/// outputs to minimize the circuit. /// outputs to minimize the encoding.
/// +dual is optional and indicates that the algorithm /// `+dual` is optional and indicates that the algorithm
/// should also try to encode the negation to generate smaller /// should also try to encode the negation of each condition in
/// circuits. /// case its encoding is smaller.
/// +sox indicates that the conditions can be seperated into /// `+subN` indicates that the conditions can be separated into
/// blocks with so0 being no separation, so1 separation into /// blocks with `sub0` being no separation, `sub1` separation into
/// input/latches/gates (isop only) and so2 tries to seek /// input/latches/gates (`isop` only) and `sub2` tries to seek
/// common subformulas. /// common subformulas.
SPOT_API aig_ptr SPOT_API aig_ptr
strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode); strategy_to_aig(const const_twa_graph_ptr& aut, const char* mode);