Implemented simulation function

Author: bwbush

.github/workflows/lean_action_ci.yml

@@ -13,7 +13,6 @@ on:
 jobs:
   build:
     runs-on: ubuntu-latest
-
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1

analysis/markov/Linleios/Evolve.lean

@@ -49,7 +49,7 @@ def forge {env : Environment} (state : State) : List (State × Probability) :=
         state with
         rbCount := state.rbCount + 1
       }
-    , env.pSpacingOkay
+    , 1 - env.pSpacingOkay
     ⟩
   , ⟨
       {
@@ -72,3 +72,10 @@ def evolve (transition : State → List (State × Probability)) : Probabilities
           $ transition state
     )
     ∅
+
+def simulate (transition : State → List (State × Probability)) (start : Probabilities) : Nat → Probabilities
+| 0     => start
+| n + 1 => simulate transition (evolve transition start) n
+
+def totalProbability (states : Probabilities) : Probability :=
+  states.values.sum

analysis/markov/Main.lean

@@ -5,7 +5,10 @@ import Linleios
 def env : Environment := makeEnvironment 0.05 1 4 7
 
 def s0 : Probabilities := default
-def s1 := evolve (@forge env) s0
+def sn := simulate (@forge env) s0 5
+def pn := totalProbability sn
 
 def main : IO Unit :=
-  IO.println $ (reprPrec s1 0).pretty
+  do
+    IO.println $ (reprPrec sn 0).pretty
+    IO.println $ (reprPrec pn 0).pretty