Your goal is to design a control-system for a lunar base, this one:
In particular, we're going to focus on the airlock system, consisting of three doors A, B and C. Each internal segment AB and BC may be variably pressurized.
Each door exists in either OPEN or CLOSED states. Each segment is either PRESSURIZED or DEPRESSURIZED.
We would like your implementation to satisfy the following constraints:
- At no time may all doors be open. (This depressurizes the main base and kills the astronauts.)
- At no time may a pressurized segment be vented.
- At no time may an astronaut be permanently trapped in a segment.
- It is admissible for a single door only to be in the CLOSED state.
Your implementation will receive the following four signals, appropriate to your application and with any transliteration to your language's native types:
{open, Door}{close, Door}{pressurize, Segment}{depressurize, Segment}
Callers may be assumed to never send Segment or Door values that do not exist. If a request violates one of the above restraints your implementation must return an unsatisfiable signal. For convenience please allow that your implementation will interface wiht some low-level system which will naively handle the details of opening and closing the airlocks. That is, you may assume a system which will open any or all airlocks but not in a manner subject to the above constraints. Further assume that this application will respond to query signals of the form:
{door, Door}{segment, Segment}
and will return either 'OPEN', 'CLOSED', 'PRESSURIZED' or 'DEPRESSURIZED' as discussed above.
Please discuss any tools you might use to ensure correctness of the system.