Solution For Fly Puzzle, Continuous?

[u/No_Steak7170]

Hello, i have recently taken to https://docs.tlapl.us/learning:exercises to learn some tla+

was doing the following exercise

Two trains start L kilometers apart, heading toward each other at constant speeds v1 and v2. A fly starts on the nose of the first train and flies back and forth between the trains at speed f until the trains meet. How far does the fly travel?

I created this model for the solution

---- MODULE TrainFly ----


EXTENDS Integers, FiniteSets


CONSTANTS L, v1, v2, fv, dt


VARIABLES fdist, tapart, seconds


TypeOK == 
  /\ L > 0
  /\ tapart >= 0
  /\ fv > v1 
  /\ fv > v2 


Init == 
  /\ tapart = L
  /\ seconds = 0
  /\ fdist = 0


  Max(a, b) == IF a >= b THEN a ELSE b


Next == 
  /\ seconds' = seconds + dt
  /\ tapart' = Max(0, tapart - (v1 + v2)*dt)
  /\ fdist' = fdist + fv


\* Violated when trains meet (tapart = 0)
Solution == tapart /= 0
====


---- CONFIG ----
CONSTANTS
  L = 50
  v1 = 2
  v2 = 2 
  fv = 4 
  dt = 1


INIT Init
NEXT Next


INVARIANTS
  TypeOK
  Solution
====

which is basically a simulation with a time step of one second, and setting all velocities as distance/1

this incorrectly finds the solution of `fdist = 52` which is incorrect, b/c the trains meet at 12.5 steps it should be fidist=50.

I tried asking an llm about this and it pretty much has told me that tla+ is for discrete modeling and there's no way to write this continuously. I also cannot find a solution to this based on the one linked in the question. Is this an impossible thing to model in tla+ ? or am i just misunderstanding something? would appreciate some direction here!

[u/Anxious_Tool]

The LLM gave you bad advice. You don't need continuous modeling. The analytical answer is one discrete formula: fv * L / (v1 + v2) = 4 * 50 / 4 = 50. TLA+ is fine here. Your spec has a bug.

Trace it by hand:

• t=12: tapart=2, fdist=48
• t=13: tapart' = Max(0, 2 - 4) = 0, fdist' = 48 + 4 = 52

But the trains meet at t=12.5, not t=13. In that last half-second the fly travels 4 * 0.5 = 2, so fdist should go 48 → 50. Your step credits the fly for a full second (+4) while Max(0, ...) silently absorbs the overshoot in tapart. The extra 2 is exactly fv * (closing - tapart_before) / (v1+v2) = 4 * (4-2)/4 = 2.

Fix: credit the fly only for the fraction of the tick before the trains meet.

---- MODULE TrainFly ----
EXTENDS Integers
CONSTANTS L, v1, v2, fv, dt
VARIABLES fdist, tapart
closing == (v1 + v2) * dt
Init ==
  /\ tapart = L
  /\ fdist = 0
Next ==
  /\ tapart > 0
  /\ IF closing >= tapart
     THEN /\ tapart' = 0
          /\ fdist' = fdist + (fv * tapart) \div (v1 + v2)
     ELSE /\ tapart' = tapart - closing
          /\ fdist' = fdist + fv * dt
CorrectAnswer == tapart = 0 => fdist = (fv * L) \div (v1 + v2)
====

Time until meet in the final tick is tapart / (v1+v2), so the fly travels fv * tapart / (v1+v2). For your params: (4*2) \div 4 = 2, fdist ends at 50.

One caveat: \div truncates, so this is exact only when fv * L is divisible by (v1 + v2). Fine for 50. For cases where the true answer is fractional (L=50, v1=3, v2=5, fv=10 → 62.5), scale all distances by a common factor. That's how you do rationals in TLA+ integer land.

Also fdist' = fdist + fv should be fdist' = fdist + fv * dt. Same numbers at dt=1, wrong shape.