First thought: we could do that, but that puts the cart before the horse! The goal of writing the spec is to make sure that a higher-level property is guaranteed by a lower-level specification.
Second thought: I wonder if any safety property can be turned into a deadlock property by doing exactly what you said, and incorporating the property as part of the spec.
First thought: we could do that, but that puts the cart before the horse! The goal of writing the spec is to make sure that a higher-level property is guaranteed by a lower-level specification.
Second thought: I wonder if any safety property can be turned into a deadlock property by doing exactly what you said, and incorporating the property as part of the spec.