124
specs/task.allium
Normal file
124
specs/task.allium
Normal file
@@ -0,0 +1,124 @@
|
||||
-- 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
|
||||
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
|
||||
}
|
||||
}
|
||||
|
||||
surface TaskControlSurface {
|
||||
facing _: TaskOperator
|
||||
|
||||
provides:
|
||||
SubmitTaskRequested(name, work)
|
||||
CancelTaskRequested(task)
|
||||
RegisterExternalTaskRequested(name)
|
||||
}
|
||||
|
||||
surface TaskRuntimeSurface {
|
||||
facing _: TaskRuntime
|
||||
|
||||
provides:
|
||||
TaskWorkCompleted(task)
|
||||
TaskWorkFailed(task, error_message)
|
||||
ProgressReported(task, value, message)
|
||||
}
|
||||
|
||||
surface TaskSurface {
|
||||
context task: Task
|
||||
|
||||
exposes:
|
||||
task.name
|
||||
task.status
|
||||
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 {
|
||||
max_concurrent: Integer = 3
|
||||
progress_throttle: Duration = 250.milliseconds
|
||||
}
|
||||
|
||||
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)
|
||||
let running_tasks = Tasks where status = running
|
||||
ensures:
|
||||
let task = Task.created(name: name, status: pending)
|
||||
task.status = pending
|
||||
if running_tasks.count < config.max_concurrent:
|
||||
task.status = running
|
||||
TaskStarted(task, work)
|
||||
}
|
||||
|
||||
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 = running or task.status = pending
|
||||
-- Cancellation uses a runtime-specific cancellation mechanism
|
||||
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
|
||||
}
|
||||
|
||||
invariant ProgressThrottled {
|
||||
-- Progress update events are throttled to prevent UI flooding
|
||||
-- At most one progress event per 250ms per 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)
|
||||
task.status = running
|
||||
@guidance
|
||||
-- External tasks are not managed by the queue
|
||||
-- The caller is responsible for updating status
|
||||
}
|
||||
Reference in New Issue
Block a user