Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Trace

Conjectura.Defs.ComputerScience.Semantics.Trace

/-
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi
-/
import Conjectura.Defs.ComputerScience.Semantics.LabelledTransitionSystem

/-! # Trace

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Semantics

/-- A **trace** of a state is a finite list of labels it can perform in order. Traces record
what a system can do, but not when it committed to doing it. -/
def LTS.HasTrace {State Label : Type*}
    (lts : LTS State Label) : State → List Label → Prop
  | _, [] => True
  | s, μ :: μs => ∃ t, lts.Tr s μ t ∧ lts.HasTrace t μs

end Conjectura.Semantics