From 94b6de8c53f82b6197cd34d2e70165521a834a16 Mon Sep 17 00:00:00 2001 From: PJ Date: Sat, 6 Jun 2026 12:46:41 +0530 Subject: [PATCH] test(ltl): marshal bounded Always steps/duration/deadline --- internal/ltl/formula_test.go | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/internal/ltl/formula_test.go b/internal/ltl/formula_test.go index aae560a..ffb700e 100644 --- a/internal/ltl/formula_test.go +++ b/internal/ltl/formula_test.go @@ -220,6 +220,30 @@ func TestMarshalJSON_EventuallyMillisecondsAndDeadline(t *testing.T) { } } +// TestMarshalJSON_AlwaysStepsMillisecondsDeadline mirrors the Eventually +// marshal test for bounded Always: the within node must carry the right unit +// and amount for each bound flavor. Bug class: a bounded Always serializing the +// wrong bound (unit/amount) into the trace AST the replay UI consumes. +func TestMarshalJSON_AlwaysStepsMillisecondsDeadline(t *testing.T) { + steps := AlwaysFormula{Inner: Pure(true), StepBound: 4, HasStepBound: true} + body, _ := json.Marshal(steps) + if !strings.Contains(string(body), `"unit":"steps"`) || !strings.Contains(string(body), `"amount":4`) { + t.Errorf("always steps within wrong: %s", body) + } + + duration := AlwaysFormula{Inner: Pure(true), Duration: 250 * time.Millisecond} + body, _ = json.Marshal(duration) + if !strings.Contains(string(body), `"unit":"milliseconds"`) || !strings.Contains(string(body), `"amount":250`) { + t.Errorf("always milliseconds within wrong: %s", body) + } + + deadline := AlwaysFormula{Inner: Pure(true), Deadline: time.UnixMilli(1700000000000), HasDeadline: true} + body, _ = json.Marshal(deadline) + if !strings.Contains(string(body), `"unit":"deadline"`) || !strings.Contains(string(body), `"amount":1700000000000`) { + t.Errorf("always deadline within wrong: %s", body) + } +} + func TestMarshalJSON_NextAndThunkAndError(t *testing.T) { body, _ := json.Marshal(Next(Pure(true))) if string(body) != `{"op":"next","arg":{"op":"true"}}` {