Wander Lairson Costa <[email protected]> writes: > Add return type annotations to RVGenerator base class methods and > LTL operator classes to resolve pyright reportIncompatibleMethodOverride > errors. > > In generator.py, add string return type annotations to all template > filling methods and annotate the template_dir class attribute to enable > proper type checking during initialization. > > In ltl2ba.py, introduce a LTLNode type alias as a Union of all AST node > types (BinaryOp, UnaryOp, Variable, Literal) to properly type operator > transformations. The operator base classes BinaryOp and UnaryOp receive > return type annotations using this type alias for their normalize and > negate methods, since these transformations can return different node > types depending on the expression. The Variable and Literal classes gain > return type annotations for their manipulation methods, and all temporal > checking methods are annotated to return bool. > > The LTLNode type alias is necessary because operator transformations are > polymorphic: NotOp.negate() can return BinaryOp, UnaryOp, Variable, or > Literal depending on what expression is being negated. > > In ltl2k.py, fix the _fill_states return type from str to list[str] to > match the actual implementation. > > Signed-off-by: Wander Lairson Costa <[email protected]>
Reviewed-by: Nam Cao <[email protected]>
