Skip to content

Commit 8af831b

Browse files
committed
Implemented pruning
1 parent 0299def commit 8af831b

File tree

2 files changed

+9
-5
lines changed

2 files changed

+9
-5
lines changed

analysis/markov/Linleios/Evolve.lean

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -74,8 +74,11 @@ def evolve (transition : State → List (State × Probability)) : Probabilities
7474
7575

7676
def simulate (transition : State → List (State × Probability)) (start : Probabilities) : Nat → Probabilities
77-
| 0 => start
78-
| n + 1 => simulate transition (evolve transition start) n
77+
| 0 => start
78+
| n + 1 => simulate transition (evolve transition start) n
79+
80+
def prune (ε : Float) : Probabilities → Probabilities :=
81+
HashMap.filter (fun _ p => p ≥ ε)
7982

8083
def totalProbability (states : Probabilities) : Probability :=
8184
states.values.sum

analysis/markov/Main.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,11 @@ import Linleios
55
def env : Environment := makeEnvironment 0.05 1 4 7
66

77
def s0 : Probabilities := default
8-
def sn := simulate (@forge env) s0 5
8+
def sn := simulate (@forge env) s0 50
99
def pn := totalProbability sn
1010

1111
def main : IO Unit :=
1212
do
13-
IO.println $ (reprPrec sn 0).pretty
14-
IO.println $ (reprPrec pn 0).pretty
13+
let print {α : Type} [Repr α] (x : α) : IO Unit := IO.println $ (reprPrec x 0).pretty
14+
print sn
15+
print pn

0 commit comments

Comments
 (0)