-- allium: 1
-- bDS Background Task Manager
-- Scope: core (Wave 1)
-- Distilled from: src/main/engine/TaskManager.ts

entity Task {
    name: String
    status: pending | running | completed | failed | cancelled
    source: local | remote
    cancellable: Boolean
    cancellation_requested: Boolean
    progress: Decimal?              -- 0.0..1.0
    message: String?
    group_id: String?               -- Optional task grouping
    group_name: String?
    created_at: Timestamp

    transitions status {
        pending -> running
        running -> completed
        running -> failed
        running -> cancelled
        pending -> cancelled
    }
}

surface TaskControlSurface {
    facing _: TaskOperator

    provides:
        SubmitTaskRequested(name, work)
        CancelTaskRequested(task)
        RegisterExternalTaskRequested(name)
        TaskStateRequested()
}

surface TaskRuntimeSurface {
    facing _: TaskRuntime

    provides:
        TaskWorkCompleted(task)
        TaskWorkFailed(task, error_message)
        ProgressReported(task, value, message)
        FinishedTaskEvictionDue()
        WorkerCapacityAvailable()
        TaskWorkStopped(task)
}

surface TaskSurface {
    context task: Task

    exposes:
        task.name
        task.status
        task.source
        task.progress when task.progress != null
        task.message when task.message != null
        task.group_id when task.group_id != null
        task.group_name when task.group_name != null
        task.created_at
}

config {
    -- Runtime default: all online CPU workers, matching bDS2.
    max_concurrent: Integer
    progress_throttle: Duration = 250.milliseconds
    finished_task_ttl: Duration = 1.hour
    recent_finished_limit: Integer = 10
}

invariant MaxConcurrency {
    -- At most max_concurrent tasks run simultaneously
    let running_tasks = Tasks where status = running
    running_tasks.count <= config.max_concurrent
}

invariant FifoQueue {
    -- When max concurrent reached, new tasks queue in FIFO order
    -- Queued tasks transition to running as slots open
}

rule SubmitTask {
    when: SubmitTaskRequested(name, work)
    ensures:
        let task = Task.created(
            name: name,
            status: pending,
            source: local,
            cancellable: true,
            cancellation_requested: false
        )
        task.status = pending
}

rule StartNextTask {
    when: WorkerCapacityAvailable()
    let pending_tasks = Tasks where status = pending
    requires: pending_tasks.count > 0
    ensures: pending_tasks.first.status = running
    ensures: TaskStarted(pending_tasks.first)
}

rule CompleteTask {
    when: TaskWorkCompleted(task)
    ensures: task.status = completed
    ensures: task.progress = 1.0
    ensures: NextQueuedTaskStarted()
}

rule FailTask {
    when: TaskWorkFailed(task, error_message)
    ensures: task.status = failed
    ensures: task.message = error_message
    ensures: NextQueuedTaskStarted()
}

rule CancelTask {
    when: CancelTaskRequested(task)
    requires: task.status = pending
    ensures: task.status = cancelled
    ensures: NextQueuedTaskStarted()
}

rule RequestRunningTaskCancellation {
    when: CancelTaskRequested(task)
    requires: task.status = running
    requires: task.cancellable
    ensures: task.cancellation_requested = true
    ensures: StopTaskWorkRequested(task)
    @guidance
        -- Long operations observe the request at phase or item boundaries.
        -- Owned child processes are terminated when the platform permits it.
        -- The task remains running and occupies its worker slot until work
        -- actually stops; status surfaces expose cancellation_requested.
}

rule FinishRunningTaskCancellation {
    when: TaskWorkStopped(task)
    requires: task.status = running
    requires: task.cancellation_requested
    ensures: task.status = cancelled
    ensures: NextQueuedTaskStarted()
}

rule ReportProgress {
    when: ProgressReported(task, value, message)
    -- Progress events throttled to 250ms
    ensures: task.progress = value
    ensures: task.message = message
    @guidance
        -- A report whose value is 1.0 is always accepted so the terminal
        -- localized phase text cannot be dropped by throttling.
}

invariant ProgressThrottled {
    -- Progress update events are throttled to prevent UI flooding
    -- At most one progress event per 250ms per task
}

invariant GroupProgressAggregatesChildren {
    -- Matches bDS2: group progress averages every child task contribution.
    -- Pending tasks contribute 0 and completed tasks contribute 1.
}

invariant FinishedTaskRetention {
    -- The status snapshot surfaces only the most recent finished tasks:
    -- completed/failed/cancelled tasks beyond config.recent_finished_limit
    -- (newest first) are not shown.
    let finished = Tasks where status in {completed, failed, cancelled}
    -- At most config.recent_finished_limit finished tasks are reported.
}

rule EvictFinishedTasks {
    when: FinishedTaskEvictionDue()
    -- Periodic sweep (every config.finished_task_ttl). A finished task whose
    -- finished_at is older than config.finished_task_ttl is dropped from state.
    for task in Tasks where status in {completed, failed, cancelled}:
        if now - task.finished_at >= config.finished_task_ttl:
            ensures: not exists task
}

rule PruneFinishedTasksOnAccess {
    when: TaskStateRequested()
    for task in Tasks where status in {completed, failed, cancelled}:
        if now - task.finished_at >= config.finished_task_ttl:
            ensures: not exists task
}

-- External tasks: lifecycle controlled by caller (e.g., renderer-side scripts)
rule RegisterExternalTask {
    when: RegisterExternalTaskRequested(name)
    ensures:
        let task = Task.created(
            name: name,
            status: running,
            source: remote,
            cancellable: true,
            cancellation_requested: false
        )
        task.status = running
    @guidance
        -- External tasks are not managed by the queue
        -- The caller is responsible for updating status
}