Discrete Event Simulation

Model concurrent agents as time-ordered events
Thread all state through a purely functional event loop, avoiding mutation
Use the inverse-CDF method to sample exponential inter-arrival times from a LCG
Parse parameters from command-line arguments or a JSON configuration file

A discrete event simulation advances time by jumping from one event to the next
- No fixed time step: time skips forward to whatever happens next
- Like an agenda that only records appointments, not empty minutes
We model P producers depositing items into a shared queue and C consumers taking them out
- Queue capacity N bounds how many items can wait at once
- Producers block when the queue is full; consumers block when it is empty
Every component is a pure function: easy to test with #guard

Random Numbers

-- Linear congruential generator constants from Numerical Recipes
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296  -- 2^32

def nextSeed (seed : Nat) : Nat :=
  (lcgA * seed + lcgC) % lcgM

-- Sample from Exp(lambda): X = -ln(U) / lambda via the inverse-CDF method
def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  -- shift numerator so u is in (0, 1), never exactly 0
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

A linear congruential generator (LCG) advances a seed
- seed' = (A × seed + C) mod M
- The constants A, C, M are from [Press2007]; they pass standard randomness tests
- The same seed always produces the same sequence — reproducible simulations
expVariate converts a uniform sample U into an exponential variate X = -ln(U) / λ
- This is the inverse-CDF method: if U ~ Uniform(0,1) then X ~ Exp(λ)
- Shifting the numerator by 1 keeps U strictly inside (0, 1) so logarithm is always defined
High λ = high rate = short inter-arrival times (like a busy coffee shop)
Like Python's random.expovariate(λ)

Events and State

-- Each event records when it fires and which agent fires it
inductive Event where
  | Produce : Float → Nat → Event  -- (time, producer-id)
  | Consume : Float → Nat → Event  -- (time, consumer-id)

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

-- Simulation parameters
structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float  -- producer inter-arrival rate
  lambdaC      : Float  -- consumer inter-arrival rate
  seed         : Nat

-- All simulation state threaded through the event loop
structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat   -- producer ids blocked on a full queue
  waitingConsumers : List Nat   -- consumer ids blocked on an empty queue
  events           : List Event -- pending events, sorted earliest-first
  totalProduced    : Nat
  totalConsumed    : Nat

Each Event carries its firing time and the ID of the agent that fires it
- Two constructors: Produce and Consume
- eventTime extracts the time from either constructor
Params bundles all five simulation parameters together with the RNG seed
SimState records everything that changes as the simulation runs
- waitingProducers and waitingConsumers are the blocked agent queues
- events is the pending event list, kept sorted earliest-first

Scheduling Events

-- Insert one event into a time-sorted list (earliest event first)
def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | []     => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

schedule inserts one event into a sorted list by walking the list until the right position
- O(n) per insertion; fine for teaching, but real system would use a heap
Ties are resolved by keeping the new event first (<=), which is arbitrary but consistent
Like Python's bisect.insort but on an immutable list instead of a mutable array

Handling a Produce Event

-- A producer tries to add an item to the bounded queue
def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize < p.capacity then
    -- Space available: deposit the item and reschedule this producer
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    -- Queue was empty: wake every consumer that was blocked waiting for an item
    let (evs', remCons) :=
      if s.queueSize == 0
      then (s.waitingConsumers.foldl (fun e cid => schedule e (Event.Consume t cid)) evs, [])
      else (evs, s.waitingConsumers)
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    -- Queue full: block this producer until the queue drains to empty
    ({ s with time := t,
              waitingProducers := s.waitingProducers ++ [pid] }, seed)

When a producer fires:
- If there is space (queueSize < capacity): deposit the item, schedule the next arrival
- If the queue was empty before depositing: wake every blocked consumer immediately
- If the queue is full: add this producer to waitingProducers without rescheduling it
"Blocking" in a DES means not scheduling the agent's next event until conditions change
Waking is done by inserting a Consume event at the current time t for each waiter

Handling a Consume Event

-- A consumer tries to take an item from the bounded queue
def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    -- Item available: take it and reschedule this consumer
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    -- Queue just drained: wake every producer that was blocked waiting for space
    let (evs', remProds) :=
      if s.queueSize == 1
      then (s.waitingProducers.foldl (fun e pid => schedule e (Event.Produce t pid)) evs, [])
      else (evs, s.waitingProducers)
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    -- Queue empty: block this consumer until an item arrives
    ({ s with time := t,
              waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

When a consumer fires:
- If there is an item (queueSize > 0): take it, schedule the next arrival
- If the queue just drained (queueSize went from 1 to 0): wake every blocked producer
- If the queue is empty: add this consumer to waitingConsumers without rescheduling it
The symmetric pair with handleProduce: full/empty are the two blocking conditions

The Event Loop

-- Pop and dispatch the earliest event from the queue
def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

-- Schedule the first arrival for every producer and consumer
def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

-- Run for exactly n events; structural recursion on n guarantees termination
def runLoop : Params → SimState → Nat → Nat → SimState
  | _, s, 0,     _ => s
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (numEvents : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 numEvents s1

stepSim pops the earliest event and dispatches it; returns none when no events remain
initSim seeds the simulation by scheduling one arrival for each producer and consumer
runLoop uses structural recursion on n: when n reaches zero the loop terminates
- Lean accepts this without a proof: the pattern n + 1 guarantees n decreases
- DEBT: explain this more clearly
runSim packages initSim + runLoop into a single call

Tests

-- schedule keeps events in ascending time order
#guard
  let evs := schedule (schedule [] (Event.Produce 3.0 0)) (Event.Produce 1.0 1)
  evs.map eventTime == [1.0, 3.0]

-- expVariate always returns a positive inter-arrival time
#guard (expVariate 0    1.0).1 > 0.0
#guard (expVariate 42   2.5).1 > 0.0
#guard (expVariate 9999 0.5).1 > 0.0

-- a balanced simulation produces and consumes items
#guard
  let p : Params := { numProducers := 2, numConsumers := 2,
                      capacity := 4, lambdaP := 1.0, lambdaC := 1.0, seed := 42 }
  let s := runSim p 200
  s.totalProduced > 0 && s.totalConsumed > 0

-- items are conserved: produced = consumed + items still in queue
#guard
  let p : Params := { numProducers := 3, numConsumers := 2,
                      capacity := 5, lambdaP := 1.0, lambdaC := 1.5, seed := 99 }
  let s := runSim p 500
  s.totalProduced == s.totalConsumed + s.queueSize

-- queue size never exceeds capacity
#guard
  let p : Params := { numProducers := 5, numConsumers := 1,
                      capacity := 3, lambdaP := 5.0, lambdaC := 0.5, seed := 7 }
  let s := runSim p 300
  s.queueSize ≤ p.capacity

schedule test: insert a later event then an earlier event; expect earliest-first order
expVariate tests: any seed and rate must produce a positive inter-arrival time
Conservation invariant: every item produced is either in the queue or has been consumed
Capacity invariant: queue size never exceeds the declared capacity

Parsing Input

-- Parse all six parameters from a JSON object string using Lean.Data.Json
def parseJson (json : String) : Option Params := do
  let j    ← (Json.parse json).toOption
  let numP ← (j.getObjValAs? Nat   "P").toOption
  let numC ← (j.getObjValAs? Nat   "C").toOption
  let cap  ← (j.getObjValAs? Nat   "N").toOption
  let lp   ← (j.getObjValAs? Float "lambda_p").toOption
  let lc   ← (j.getObjValAs? Float "lambda_c").toOption
  let sd   ← (j.getObjValAs? Nat   "seed").toOption
  some { numProducers := numP, numConsumers := numC, capacity := cap,
         lambdaP := lp, lambdaC := lc, seed := sd }

parseJson uses Json.parse from Lean.Data.Json to parse the file contents
- getObjValAs? Nat "P" extracts field "P" and converts it to Nat
- getObjValAs? Float "lambda_p" extracts "lambda_p" and converts it to Float
- Both return Except String α; .toOption converts errors to none
Chaining six ← binds inside a do block for Option: any missing field short-circuits to none
Like Python's json.loads(text)["P"] but with explicit None-propagation at every step

Running the Program

def printResults (p : Params) (s : SimState) (numEvents : Nat) : IO Unit := do
  IO.println s!"producers={p.numProducers}  consumers={p.numConsumers}  capacity={p.capacity}"
  IO.println s!"lambda_p={p.lambdaP}  lambda_c={p.lambdaC}  seed={p.seed}"
  IO.println s!"events processed : {numEvents}"
  IO.println s!"total produced   : {s.totalProduced}"
  IO.println s!"total consumed   : {s.totalConsumed}"
  IO.println s!"final queue size : {s.queueSize}"
  IO.println s!"blocked producers: {s.waitingProducers.length}"
  IO.println s!"blocked consumers: {s.waitingConsumers.length}"
  IO.println s!"simulation time  : {s.time}"

def main (args : List String) : IO Unit := do
  let numEvents := 10000
  match args with
  | [path] =>
    -- single argument: read parameters from a JSON file
    let json ← IO.FS.readFile path
    match parseJson json with
    | none   => IO.eprintln s!"error: could not parse parameters from {path}"
    | some p => printResults p (runSim p numEvents) numEvents
  | [sP, sC, sN, sLp, sLc, sSeed] =>
    -- six arguments: P C N lambda_p lambda_c seed
    let p : Params := {
      numProducers := sP.toNat?.getD 1,
      numConsumers := sC.toNat?.getD 1,
      capacity     := sN.toNat?.getD 1,
      lambdaP      := (parseFloat? sLp).getD 1.0,
      lambdaC      := (parseFloat? sLc).getD 1.0,
      seed         := sSeed.toNat?.getD 0
    }
    printResults p (runSim p numEvents) numEvents
  | _ =>
    IO.eprintln "usage: des P C N lambda_p lambda_c seed"
    IO.eprintln "       des params.json"

producers=2  consumers=3  capacity=5
lambda_p=1.000000  lambda_c=1.500000  seed=20240101
events processed : 10000
total produced   : 2730
total consumed   : 2730
final queue size : 0
blocked producers: 0
blocked consumers: 2
simulation time  : 1382.369325
---
producers=2  consumers=3  capacity=5
lambda_p=1.000000  lambda_c=1.500000  seed=42
events processed : 10000
total produced   : 2736
total consumed   : 2736
final queue size : 0
blocked producers: 0
blocked consumers: 1
simulation time  : 1342.125916

main accepts two call styles:
- Six arguments: P C N lambda_p lambda_c seed — one value per parameter
- One argument: a path to a JSON file containing the same six fields
The separator line --- in the output separates the two modes shown by the script
Run with:
- lake env lean --run des/code.lean 2 3 5 1.0 1.5 20240101
- lake env lean --run des/code.lean des/params.json

Exercises

Fix: Events Inserted in Wrong Order

-- schedule inserts events in reverse time order; fix the comparison
inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | []     => [e]
  | h :: t =>
    if eventTime e >= eventTime h  -- BUG: should be <=
    then e :: h :: t
    else h :: schedule t e

#guard
  let evs := schedule (schedule [] (Event.Produce 3.0 0)) (Event.Produce 1.0 1)
  evs.map eventTime == [1.0, 3.0]

#guard
  let evs := schedule (schedule (schedule [] (Event.Consume 5.0 0))
                                            (Event.Consume 2.0 1))
                                            (Event.Consume 4.0 2)
  evs.map eventTime == [2.0, 4.0, 5.0]

hint

schedule inserts a new event before h when the comparison is true
With >=, a later event is placed before an earlier one — reversing the sort order
Change >= to <= so earlier events come first

Fix: Queue Exceeds Capacity

-- handleProduce allows the queue to exceed capacity; fix the guard
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296

def nextSeed (seed : Nat) : Nat := (lcgA * seed + lcgC) % lcgM

def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | [] => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float
  lambdaC      : Float
  seed         : Nat

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List Event
  totalProduced    : Nat
  totalConsumed    : Nat

def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize <= p.capacity then  -- BUG: should be <
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    let (evs', remCons) :=
      if s.queueSize == 0
      then (s.waitingConsumers.foldl (fun e cid => schedule e (Event.Consume t cid)) evs, [])
      else (evs, s.waitingConsumers)
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    ({ s with time := t, waitingProducers := s.waitingProducers ++ [pid] }, seed)

def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    let (evs', remProds) :=
      if s.queueSize == 1
      then (s.waitingProducers.foldl (fun e pid => schedule e (Event.Produce t pid)) evs, [])
      else (evs, s.waitingProducers)
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    ({ s with time := t, waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

def runLoop : Params → SimState → Nat → Nat → SimState
  | _, s, 0,     _ => s
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (n : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 n s1

-- queue size should never exceed capacity
#guard
  let p : Params := { numProducers := 4, numConsumers := 1,
                      capacity := 2, lambdaP := 5.0, lambdaC := 0.5, seed := 7 }
  let s := runSim p 300
  s.queueSize ≤ p.capacity

hint

handleProduce should add to the queue only when there is space (queueSize < capacity)
With <=, a producer adds even when the queue is already at capacity, making it one over
Change <= to <

Fix: Blocked Consumers Never Wake

-- handleProduce never wakes blocked consumers; fix the wakeup condition
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296

def nextSeed (seed : Nat) : Nat := (lcgA * seed + lcgC) % lcgM

def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | [] => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float
  lambdaC      : Float
  seed         : Nat

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List Event
  totalProduced    : Nat
  totalConsumed    : Nat

def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize < p.capacity then
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    -- BUG: consumers are never woken; remCons should be [] when queue was empty
    let evs'    := evs
    let remCons := s.waitingConsumers
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    ({ s with time := t, waitingProducers := s.waitingProducers ++ [pid] }, seed)

def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    let (evs', remProds) :=
      if s.queueSize == 1
      then (s.waitingProducers.foldl (fun e pid => schedule e (Event.Produce t pid)) evs, [])
      else (evs, s.waitingProducers)
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    ({ s with time := t, waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

def runLoop : Params → SimState → Nat → Nat → SimState
  | _, s, 0,     _ => s
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (n : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 n s1

-- consumers arrive quickly and block on an empty queue; the slow producer
-- fills the queue later, but with the bug consumers are never woken
#guard
  let p : Params := { numProducers := 1, numConsumers := 3,
                      capacity := 5, lambdaP := 0.1, lambdaC := 100.0, seed := 42 }
  let s := runSim p 500
  s.totalConsumed > 20

hint

When a producer deposits the first item into an empty queue, every blocked consumer should be rescheduled at the current time
The bug discards the wakeup logic and leaves waitingConsumers unchanged
Add: if s.queueSize == 0 then (wake all in s.waitingConsumers, []) else (evs, s.waitingConsumers)

Fix: Blocked Producers Never Wake

-- handleConsume never wakes blocked producers; fix the wakeup condition
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296

def nextSeed (seed : Nat) : Nat := (lcgA * seed + lcgC) % lcgM

def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | [] => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float
  lambdaC      : Float
  seed         : Nat

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List Event
  totalProduced    : Nat
  totalConsumed    : Nat

def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize < p.capacity then
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    let (evs', remCons) :=
      if s.queueSize == 0
      then (s.waitingConsumers.foldl (fun e cid => schedule e (Event.Consume t cid)) evs, [])
      else (evs, s.waitingConsumers)
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    ({ s with time := t, waitingProducers := s.waitingProducers ++ [pid] }, seed)

def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    -- BUG: producers are never woken; remProds should be [] when queue just drained
    let evs'     := evs
    let remProds := s.waitingProducers
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    ({ s with time := t, waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

def runLoop : Params → SimState → Nat → Nat → SimState
  | _, s, 0,     _ => s
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (n : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 n s1

-- with many fast producers and a small queue, producers keep filling and being
-- unblocked; with the bug they fill once and stay blocked forever
#guard
  let p : Params := { numProducers := 5, numConsumers := 1,
                      capacity := 1, lambdaP := 5.0, lambdaC := 1.0, seed := 42 }
  let s := runSim p 1000
  s.totalProduced > 10

hint

When a consumer takes the last item from the queue, every blocked producer should be rescheduled at the current time
The bug leaves waitingProducers unchanged after the queue drains
Add: if s.queueSize == 1 then (wake all in s.waitingProducers, []) else (evs, s.waitingProducers)

Write: Throughput

-- Write a function that computes throughput: items consumed per unit of simulation time
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296

def nextSeed (seed : Nat) : Nat := (lcgA * seed + lcgC) % lcgM

def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | [] => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float
  lambdaC      : Float
  seed         : Nat

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List Event
  totalProduced    : Nat
  totalConsumed    : Nat

def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize < p.capacity then
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    let (evs', remCons) :=
      if s.queueSize == 0
      then (s.waitingConsumers.foldl (fun e cid => schedule e (Event.Consume t cid)) evs, [])
      else (evs, s.waitingConsumers)
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    ({ s with time := t, waitingProducers := s.waitingProducers ++ [pid] }, seed)

def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    let (evs', remProds) :=
      if s.queueSize == 1
      then (s.waitingProducers.foldl (fun e pid => schedule e (Event.Produce t pid)) evs, [])
      else (evs, s.waitingProducers)
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    ({ s with time := t, waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

def runLoop : Params → SimState → Nat → Nat → SimState
  | _, s, 0,     _ => s
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (n : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 n s1

-- Write throughput: items consumed per unit simulation time
-- Return 0.0 if simulation time is 0
def throughput (s : SimState) : Float :=
  0.0

#guard
  let p : Params := { numProducers := 2, numConsumers := 2,
                      capacity := 4, lambdaP := 1.0, lambdaC := 1.0, seed := 42 }
  let s := runSim p 500
  throughput s > 0.0

#guard
  let empty : SimState := { time := 0, queueSize := 0, waitingProducers := [],
                             waitingConsumers := [], events := [],
                             totalProduced := 0, totalConsumed := 0 }
  throughput empty == 0.0

hint

Throughput is items consumed divided by total simulation time
Guard against division by zero when time == 0
Use Float.ofNat s.totalConsumed / s.time

Write: Conservation Check

-- Write a function that checks the conservation invariant:
-- every item produced is either in the queue or has been consumed
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296

def nextSeed (seed : Nat) : Nat := (lcgA * seed + lcgC) % lcgM

def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | [] => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float
  lambdaC      : Float
  seed         : Nat

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List Event
  totalProduced    : Nat
  totalConsumed    : Nat

def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize < p.capacity then
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    let (evs', remCons) :=
      if s.queueSize == 0
      then (s.waitingConsumers.foldl (fun e cid => schedule e (Event.Consume t cid)) evs, [])
      else (evs, s.waitingConsumers)
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    ({ s with time := t, waitingProducers := s.waitingProducers ++ [pid] }, seed)

def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    let (evs', remProds) :=
      if s.queueSize == 1
      then (s.waitingProducers.foldl (fun e pid => schedule e (Event.Produce t pid)) evs, [])
      else (evs, s.waitingProducers)
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    ({ s with time := t, waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

def runLoop : Params → SimState → Nat → Nat → SimState
  | _, s, 0,     _ => s
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (n : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 n s1

-- Write conserved: returns true when totalProduced == totalConsumed + queueSize
def conserved (s : SimState) : Bool :=
  false

#guard
  let p : Params := { numProducers := 2, numConsumers := 3,
                      capacity := 5, lambdaP := 1.0, lambdaC := 1.5, seed := 99 }
  conserved (runSim p 500)

#guard
  let p : Params := { numProducers := 5, numConsumers := 1,
                      capacity := 2, lambdaP := 3.0, lambdaC := 0.5, seed := 7 }
  conserved (runSim p 300)

hint

Every item produced is either waiting in the queue or has already been consumed
The invariant is totalProduced == totalConsumed + queueSize
Return s.totalProduced == s.totalConsumed + s.queueSize

Fix: Step Counter Runs Extra Loop

-- The simulation loop is supposed to run exactly n steps, but it runs
-- one extra. Fix the loop so it stops at the right time.
def lcgA : Nat := 1664525
def lcgC : Nat := 1013904223
def lcgM : Nat := 4294967296

def nextSeed (seed : Nat) : Nat := (lcgA * seed + lcgC) % lcgM

def expVariate (seed : Nat) (lambda : Float) : Float × Nat :=
  let s := nextSeed seed
  let u := (s.toFloat + 1.0) / (lcgM.toFloat + 1.0)
  (-Float.log u / lambda, s)

inductive Event where
  | Produce : Float → Nat → Event
  | Consume : Float → Nat → Event

def eventTime : Event → Float
  | .Produce t _ => t
  | .Consume t _ => t

def schedule (evs : List Event) (e : Event) : List Event :=
  match evs with
  | [] => [e]
  | h :: t =>
    if eventTime e <= eventTime h then e :: h :: t
    else h :: schedule t e

structure Params where
  numProducers : Nat
  numConsumers : Nat
  capacity     : Nat
  lambdaP      : Float
  lambdaC      : Float
  seed         : Nat

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List Event
  totalProduced    : Nat
  totalConsumed    : Nat

def handleProduce (p : Params) (s : SimState) (t : Float) (pid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize < p.capacity then
    let (dt, seed') := expVariate seed p.lambdaP
    let evs := schedule s.events (Event.Produce (t + dt) pid)
    let (evs', remCons) :=
      if s.queueSize == 0
      then (s.waitingConsumers.foldl (fun e cid => schedule e (Event.Consume t cid)) evs, [])
      else (evs, s.waitingConsumers)
    ({ s with time := t, queueSize := s.queueSize + 1,
              waitingConsumers := remCons, events := evs',
              totalProduced := s.totalProduced + 1 }, seed')
  else
    ({ s with time := t, waitingProducers := s.waitingProducers ++ [pid] }, seed)

def handleConsume (p : Params) (s : SimState) (t : Float) (cid : Nat) (seed : Nat)
    : SimState × Nat :=
  if s.queueSize > 0 then
    let (dt, seed') := expVariate seed p.lambdaC
    let evs := schedule s.events (Event.Consume (t + dt) cid)
    let (evs', remProds) :=
      if s.queueSize == 1
      then (s.waitingProducers.foldl (fun e pid => schedule e (Event.Produce t pid)) evs, [])
      else (evs, s.waitingProducers)
    ({ s with time := t, queueSize := s.queueSize - 1,
              waitingProducers := remProds, events := evs',
              totalConsumed := s.totalConsumed + 1 }, seed')
  else
    ({ s with time := t, waitingConsumers := s.waitingConsumers ++ [cid] }, seed)

def stepSim (p : Params) (s : SimState) (seed : Nat) : Option (SimState × Nat) :=
  match s.events with
  | []     => none
  | e :: rest =>
    let s' := { s with events := rest }
    match e with
    | .Produce t pid => some (handleProduce p s' t pid seed)
    | .Consume t cid => some (handleConsume p s' t cid seed)

def initSim (p : Params) (seed : Nat) : SimState × Nat :=
  let (evs1, s1) := List.range p.numProducers |>.foldl
    (fun (acc : List Event × Nat) pid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaP
      (schedule evs (Event.Produce dt pid), s'))
    ([], seed)
  let (evs2, s2) := List.range p.numConsumers |>.foldl
    (fun (acc : List Event × Nat) cid =>
      let (evs, s) := acc
      let (dt, s') := expVariate s p.lambdaC
      (schedule evs (Event.Consume dt cid), s'))
    (evs1, s1)
  ({ time := 0, queueSize := 0, waitingProducers := [], waitingConsumers := [],
     events := evs2, totalProduced := 0, totalConsumed := 0 }, s2)

-- BUG: the loop runs n+1 steps instead of n because the base case is wrong
def runLoop : Params → SimState → Nat → Nat → SimState
  | p, s, 0,     seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' 0 sd'
  | p, s, n + 1, seed =>
    match stepSim p s seed with
    | none           => s
    | some (s', sd') => runLoop p s' n sd'

def runSim (p : Params) (n : Nat) : SimState :=
  let (s0, s1) := initSim p p.seed
  runLoop p s0 n s1

-- Running exactly 1 step should process at most 1 event
#guard
  let p : Params := { numProducers := 1, numConsumers := 1,
                      capacity := 10, lambdaP := 100.0, lambdaC := 0.1, seed := 42 }
  let s := runSim p 1
  s.totalProduced + s.totalConsumed ≤ 1

-- Running 0 steps should produce no change
#guard
  let p : Params := { numProducers := 1, numConsumers := 1,
                      capacity := 10, lambdaP := 100.0, lambdaC := 0.1, seed := 42 }
  let s := runSim p 0
  s.totalProduced == 0 && s.totalConsumed == 0

hint

The runLoop base case 0 still calls stepSim instead of returning s
When n is 0, the loop should stop immediately — not run one more step
Change the 0 case to just | p, s, 0, _ => s

Write: Average Queue Size

-- Write a function that computes the average queue size over the
-- simulation's lifetime. Return 0.0 if the simulation ran for 0 time.

structure SimState where
  time             : Float
  queueSize        : Nat
  waitingProducers : List Nat
  waitingConsumers : List Nat
  events           : List (Nat × Float × Nat)
  totalProduced    : Nat
  totalConsumed    : Nat

-- Compute average queue size: total items that passed through / time
-- For this simplified version, use totalConsumed as a proxy for total items
-- and the final time as the simulation duration.
def avgQueueSize (s : SimState) : Float :=
  0.0

#guard
  let s : SimState := { time := 10.0, queueSize := 3, waitingProducers := [],
                         waitingConsumers := [], events := [],
                         totalProduced := 20, totalConsumed := 17 }
  avgQueueSize s >= 0.0

#guard
  let s : SimState := { time := 0.0, queueSize := 0, waitingProducers := [],
                         waitingConsumers := [], events := [],
                         totalProduced := 0, totalConsumed := 0 }
  avgQueueSize s == 0.0

#guard
  let s : SimState := { time := 5.0, queueSize := 0, waitingProducers := [],
                         waitingConsumers := [], events := [],
                         totalProduced := 10, totalConsumed := 10 }
  avgQueueSize s == 0.0

hint

Average queue size is totalConsumed / simulation time for a naive approximation
Guard against division by zero: if s.time == 0, return 0.0
Use Float.ofNat s.totalConsumed / s.time

Write: Maximum Queue Size

-- Write a function that computes the maximum queue size during a simulation.
-- You'll need to track the peak. For this simplified version, return the
-- final queue size as a starting point and improve from there.

structure SimState where
  time         : Float
  queueSize    : Nat
  totalProduced : Nat
  totalConsumed : Nat

-- Return the highest queue size ever observed.
-- Since this simplified SimState only tracks the current queue, use
-- max of what's currently in the queue vs. what was produced but not consumed.
def maxQueueSize (s : SimState) : Nat :=
  0

#guard
  let s : SimState := { time := 10.0, queueSize := 5,
                         totalProduced := 20, totalConsumed := 15 }
  maxQueueSize s >= s.queueSize

#guard
  let s : SimState := { time := 0.0, queueSize := 0,
                         totalProduced := 0, totalConsumed := 0 }
  maxQueueSize s == 0

#guard
  let s : SimState := { time := 5.0, queueSize := 0,
                         totalProduced := 5, totalConsumed := 5 }
  maxQueueSize s == 0

hint

The maximum queue size is at least the final queue size
Since we don't track the peak in this simplified struct, return max s.queueSize (s.totalProduced - s.totalConsumed)
Use Nat.max to compare two Nat values

Write: Queue Utilization

-- Write a function that computes the utilization of the queue:
-- the fraction of capacity that's in use. Return 0.0 for zero capacity.

structure SimState where
  queueSize    : Nat
  totalProduced : Nat
  totalConsumed : Nat

-- Utilization is the ratio of current queue size to capacity.
-- Return 0.0 when capacity is 0 to avoid division by zero.
def utilization (s : SimState) (capacity : Nat) : Float :=
  0.0

#guard
  let s : SimState := { queueSize := 3, totalProduced := 10, totalConsumed := 7 }
  utilization s 5 == 0.6

#guard
  let s : SimState := { queueSize := 0, totalProduced := 0, totalConsumed := 0 }
  utilization s 5 == 0.0

#guard
  let s : SimState := { queueSize := 4, totalProduced := 4, totalConsumed := 0 }
  utilization s 0 == 0.0

hint

Utilization is the fraction of capacity in use: queueSize / capacity
Guard against zero capacity: if capacity == 0 then 0.0 else Float.ofNat s.queueSize / Float.ofNat capacity
The #guard expects exact floating-point values, so use Float.ofNat for the conversion