// Aerospace flight controller — quadcopter altitude/attitude monitoring.
// Compile: cargo run --bin mirr-compile -- --emit verilog examples/aerospace_flight_ctrl.mirr

module aerospace_flight_ctrl {
    signal altitude:        in u32;
    signal roll_angle:      in u16;
    signal pitch_angle:     in u16;
    signal yaw_rate:        in u16;
    signal battery_level:   in u16;
    signal motor_1:         out u8;
    signal motor_2:         out u8;
    signal motor_3:         out u8;
    signal motor_4:         out u8;
    signal emergency_land:  out bool;
    signal attitude_warn:   out bool;
    signal battery_warn:    out bool;

    guard altitude_low {
        when altitude < 100
        for 50 cycles;
    }

    guard altitude_high {
        when altitude > 5000
        for 20 cycles;
    }

    guard roll_excessive {
        when roll_angle > 45
        for 10 cycles;
    }

    guard pitch_excessive {
        when pitch_angle > 45
        for 10 cycles;
    }

    guard battery_critical {
        when battery_level < 10
        for 100 cycles;
    }

    reflex low_altitude_land {
        on altitude_low {
            emergency_land = true;
        }
    }

    reflex high_altitude_limit {
        on altitude_high {
            emergency_land = true;
        }
    }

    reflex roll_warning {
        on roll_excessive {
            attitude_warn = true;
        }
    }

    reflex pitch_warning {
        on pitch_excessive {
            attitude_warn = true;
        }
    }

    reflex battery_emergency {
        on battery_critical {
            battery_warn = true;
            emergency_land = true;
        }
    }

    property altitude_bounded {
        always (altitude < 10000);
    }

    property attitude_safe {
        always (roll_angle < 90 && pitch_angle < 90);
    }

    property low_battery_warns {
        always (battery_level < 20 -> battery_warn);
    }

    property emergency_land_on_critical {
        always (battery_level < 10 -> emergency_land);
    }
}