class HouseSettings {
    public attribute Settings: [int; 10];

    operation get(id: int) -> int { return 0; }
    operation set(id: int, value: int) {}
}

enumeration DoorState {
    Closed,
    Open,
}

derivable class GenericDoorControl {
    attribute Runtime: int;
    attribute SensorState: DoorState;

    operation Close() {}
    operation Open() {}

    operation SetRuntime(time: int) {}
    operation State() -> DoorState { return DoorState::Closed; }
}

class DoorControl derives GenericDoorControl {
    associate itsHouseSettings: HouseSettings;

    attribute State: DoorState;
    attribute locked: bool;

    operation SetState(state: DoorState) {}
    operation GetState() -> DoorState { return DoorState::Closed; }

    operation Lock() { this.locked = true; }
    operation Unlock() { this.locked = false; }

    state_machine {
        entry {
            transition DoorControl;
        }
        DoorControl {
            state_machine "Door operation" {
                initial {
                    transition Closing {
                        SetState(DoorState::Closed);
                    }
                }
                Closing {
                    entry {
                        Lock();
                    }
                    exit {
                        Unlock();
                    }
                    transition Opening {
                        SetState(DoorState::Open);
                    };
                }
                Opening {
                    state_machine {
                        initial {
                            transition Unlocked;
                        }
                        Unlocked {
                            ThreadSleepSeconds(1);
                            if this.locked
                                transition Unlocked
                            else
                                transition final {
                                    SetState(DoorState::Open);
                                };
                        }
                    }
                }
            }
            state_machine "Check sensor" {
                initial {
                    transition Check;
                }
                Check {
                    ThreadSleepSeconds(1);
                    transition Check;
                }
            }
        }
    }
}

class WinterGardenControl {
    associate itsHouseSettings: HouseSettings;
    associate itsDoorControl: &[HouseSettings];

    public attribute NofDoors: int;

    operation SetState(amount: int) {}
    operation SetDoors(amount: int) {}

    operation GetState() -> DoorState;
    operation GetState(door: int) -> DoorState;
}