An Example Specification for

Implementing a Car Lock Component

State diagram