TorchLean API

Docs HomeGuideExamplesGraphs

NN.Runtime.RL.Artifacts.GridWorld.Path

GridWorld Path-Difference Artifacts #

A PathDiff stores before/after episode trajectories for a fixed GridWorld. It uses the shared position codec and validates that every recorded (row, col) stays inside the declared grid.

Rollout paths #

source
structure Runtime.RL.Artifacts.GridWorld.PathDiff :
Type

Before/after episode path snapshots for a fixed width × height GridWorld.

Each position is stored as a pair (row, col) with row < height and col < width.

Instances For
    source
    @[implicit_reducible]
    instance Runtime.RL.Artifacts.GridWorld.instInhabitedPathDiff :
    Inhabited PathDiff
    source
    def Runtime.RL.Artifacts.GridWorld.instInhabitedPathDiff.default :
    PathDiff
    Instances For
      source
      def Runtime.RL.Artifacts.GridWorld.PathDiff.validateE (p : PathDiff) :
      Except String Unit

      Validate a PathDiff record (positions are in bounds).

      Instances For
        source
        def Runtime.RL.Artifacts.GridWorld.PathDiff.toJson (p : PathDiff) :
        Lean.Json

        JSON encoding for PathDiff.

        Instances For
          source
          def Runtime.RL.Artifacts.GridWorld.PathDiff.ofJsonE (j : Lean.Json) :
          Except String PathDiff

          JSON decoding for PathDiff.

          Instances For
            source
            def Runtime.RL.Artifacts.GridWorld.PathDiff.writeJson (path : System.FilePath) (p : PathDiff) (pretty : Bool := true) :
            IO Unit

            Write a PathDiff JSON file to disk (creating parent directories if needed).

            Instances For
              source
              def Runtime.RL.Artifacts.GridWorld.PathDiff.readJson (path : System.FilePath) :
              IO PathDiff

              Read a PathDiff from a JSON file.

              Instances For