Collecting Additional Hypothesis Sample Clauses

Collecting Additional Hypothesis. There is a way to discharge proof obligations like in the example above without strengthening event guards. Indeed, by looking at the flow expression one should notice that close1 is always preceded by pr_low and thus may only be enabled when pr = LOW . Likewise, since close1 always follows open1 and the second door is always closed in the after-states of open1 (due to the safety invariant of the model requiring that at most one door is open a time) it is known that the condition d2 = CL is always true for states when close1 is enabled. Hence all the information that was introduced into proofs by strengthening event guards is already present in a model. To benefit from this information it must be collected and added in the form of hypothesis to flow proof obligations. Let vi−1 be a model state preceding state vi and state vn be the most recent previous state preceding the current state v. Also, let Hi(v1,..., vn, v) be the current collection of hypothesis for some event a. Then for an instance of sequential composition a; b the collection of hypothesis available in the after-state of b is computed as Hi+1 = Hi(v1,..., vn, vn+1) G(vn+1) S(vn+1, v) where G and S are the guard and actions of b. It is straightforward to generalise this ba- sic procedure to the complete flow language. However, there an issue of filtering out irrelevant hypothesis as a large number of hypothesis slows down some provers.