state-space-control

The state-space-control worked example.

Run it from sema/:

sema check examples/state-space-control
SEMA_STRICT=1 sema run examples/state-space-control
sema assure examples/state-space-control --grade silver

Source

src/main.sema

"""Deterministic state-space model, controllability gate, and closed-loop rollout."""

assure silver


struct StateSpace:
    a: any
    b: any
    c: any
    d: any
    sample_period_s: f64


equation controllability_determinant(a: any, b: any) -> any:
    ab := matmul(a, b)
    return b[0][0] * ab[1][0] - b[1][0] * ab[0][0]


def state_step(system: StateSpace, state: any, control: any):
    return matmul(system.a, state) + matmul(system.b, control)


def observe(system: StateSpace, state: any, control: any):
    return matmul(system.c, state) + matmul(system.d, control)


def main() !{}:
    system = StateSpace(
        a=tensor([[1.0, 0.1], [0.0, 1.0]]),
        b=tensor([[0.005], [0.1]]),
        c=tensor([[1.0, 0.0]]),
        d=tensor([[0.0]]),
        sample_period_s=0.1,
    )
    StateSpace(sample_period_s=sample_period_s) = system
    check sample_period_s == 0.1
    sample_indices = [
        sample_index
        for re"^sample-(?P<sample_index:int>[0-9]+)$"
        in ["sample-1", "invalid", "sample-2"]
    ]
    check sample_indices == [1, 2]
    check abs(controllability_determinant(system.a, system.b)) > 0.000001

    state = tensor([1.0, 0.0])
    control = tensor([-2.0])
    next_state = state_step(system, state, control)
    output = observe(system, state, control)
    check abs(next_state[0] - 0.99) < 0.000000001
    check abs(next_state[1] + 0.2) < 0.000000001
    check abs(output[0] - 1.0) < 0.000000001

    mut trajectory = []
    for _ in range(40):
        control = tensor([0.0 - 2.0 * state[0] - 1.5 * state[1]])
        state = state_step(system, state, control)
        trajectory = trajectory + [[state[0], state[1]]]
    check len(trajectory) == 40
    (final_position, final_velocity) = (state[0], state[1])
    check abs(final_position) < 0.1
    check abs(final_velocity) < 0.1
    print(f"state_space controllable=true samples={sample_indices} steps={len(trajectory)} final=({final_position:.6f}, {final_velocity:.6f})")

Reflected API

main

Deterministic state-space model, controllability gate, and closed-loop rollout.

struct StateSpace

Fields

field	type	descriptor
a	any
b	any
c	any
d	any
sample_period_s	f64

def state_step

def state_step(system: StateSpace, state: any, control: any)

Parameters

name	type
system	StateSpace
state	any
control	any

def observe

def observe(system: StateSpace, state: any, control: any)

Parameters

name	type
system	StateSpace
state	any
control	any

def main

def main() !{}

Effects !{}