Closed johnyf closed 7 years ago
Addressed by ac9f32927c69e1f474fc2df018ed042479e9bf2d, d496963136c345d15b55c35c4e3d869cf3b3bc35. The method BDD.add_var
has been kept. Instead of deprecating and removing it, declare
iteratively calls add_var
. The usefulness of add_var
is that it allows for more detailed information to be passed (for now a desired level for the variable being declared). The method add_var
could remain as is, or be hidden in the future.
Methods and functions that change state should preferably have a verb as name. "add_var" isn't a verb. It's not even an English word. To what are we "adding"?
Strictly speaking, we are extending a formal system by a definition of a nullary operator name. We call a nullary operator a "variable". In any given interpretation, the operator is applied to no arguments, yielding a value (for variables in
BDD.vars
, it so happens that we always reason about models that assign to the variables values in the setBOOLEAN
in TLA+). For example, the operator"x"
is applied to yield"x()"
. For brevity, we never write the empty parentheses.In Python, "add" is used mostly for unordered containers, with
set
as a prototype. I named the methodadd_var
afternetworkx
conventions. Innetworkx
though, adding nodes and edges makes more sense for a graph as a collection of containers. It is awkward to conceptualize aBDD
as a container of variables.Practicality:
add_var
involves pressingSHIFT + -
declare
is shorter thanadd_vars
(the plural)Readability:
declare
reads more naturally:declare('x', 'y', 'z')
reads "declare [the variables] x, y, z"declare
is a little ambiguous as to what we are declaring. But a little familiarity with programming should suffice. Besides, after one reads the docstring once, they don't have to repeat "vars" throughout their code. Forgetting that variables are "declared" is a little difficult.