Provide "reachable" feature in AGREE
Closed this issue · 2 comments
A keyword "reachable" has been proposed to provide a means for a user to investigate whether properties are true only vacuously. For example, a user may write a property in the form of an implication. The user could then write a "reachable" check to confirm that the antecedent clause of the property is not universally false, resulting inthe property being vacuously true. While such a method is not strictly necessary, it can aid in user understanding of the model and confirming that the model has been written as intended.
The proposed grammatical form of the "reachable" analysis is similar to that for other properties. For analysis AGREE would negate the property and present the results as a JKind inverted property result.