proper successors/predecessors

[chudicek]

currently, if a "transition" loops over a state (ie does not actually transition), it is still considered to be a successor (predecessor) of self.

this can be fixed by creating bdd representing set of states capable doing transition under symbolic variable v_i (similar to what T_i = x_i <!=> f_i is in the boolean alternative). This set can be done by oring x_i <!=> f_i over all the relevant i bdd bits of the symbolic variable.

also mention this in the documentation (allow user to choose between the two options, in case of predecessors likely by wrapping one alternative with another function, that just intersects the result with appropriate capable of transition under v set; successors: intersect the input with that set)