Procedure check-response-property if y = q then if ( z |= q a nd z |=   p ) then output "Verification succeeds."
else output "Avoid this instance of ogen" ; endif else if ( z |=   p ) then output "Verification succeeds."
else output "Avoid this instance of ogen" ; endif endif end procedure

## Figure Gen - R Reverification Algorithm

' satisfies    In other words  '
Therefore     gen-i is sound  We also know that it is complete because if ∃
then it must be the case that In conclusion     gen-i  which consists of the test            " is sound and complete  For maximal efficiency  our implementation of    gen-i halts after the first error  although it is simple to modify it to find all errors and this does not significantly affect the empirical time complexity results of Subsection      nor does it affect the worst case time complexity gn-; is incremental because it is localized to just checking whether the property holds of the newly added atoms in    rather than all atoms in     '    Finally  this algorithm only nneeds to be executed for gen but not for spec+gen OI delete+gen because gen is the only version that can add      atoms via generalization  Recall that  spec+gen and  delete+gen are SMLs for Invariance properties As an example of    gen-i suppose a b c d and e are atoms and the transition condition  between STATE  and STATE  equals a  Let  a  b  b  d  d  d where the ellipsis indicates infinite repetition of d  be a string in       that includes STATE  and The STATE as the first two vertices in its accepting run  The property is
□ e Assume the fact that this string satisfies - e was proved in the original verification Suppose sen generalizes k STATE STATE from a to a c i e it adds a new allowable action c from STATE which adds the string c b b d d d     to      ' Then rather than test whether all of the elements of a b c d are     e  we really only need to test whether e  because c is the only newly added atom C
The next algorithm      gen-R  is for generalization and full Response properties  and is nothing more than some simple tests    Like      gen-I       gen-R localizes reverification to a restricted portion of the FSA Assume the Response property is l i .

where is the trigger and   is the response for c state formulae   and    Assume property    holds for   prior to learning We need to verify that  '
where gen   K   1   3 gen - R for gen and full Response properties is in Figure gen - R is also appli cable for  delete+gen and  spec+gen   The algorithm first checks whether a response could be required of the transition condition x 1 3 A response is required if  for at least one whose run includes   1  3   the prefix of this string before visiting vertex string in 1 includes the trigger not followed by response and the string suffix after 3 does not include either Such a string satisfies the property if and only if Thus if