diff --git a/sandbox/GNAT.jl b/sandbox/GNAT.jl index 4f95a034532b625c409db63c08979c7d97db983d..167f19c22dafac86a6acdfd148c7e335ccfe2891 100644 --- a/sandbox/GNAT.jl +++ b/sandbox/GNAT.jl @@ -1,5 +1,5 @@ ### A Pluto.jl notebook ### -# v0.19.22 +# v0.19.20 using Markdown using InteractiveUtils @@ -73,17 +73,11 @@ C ∩ D # ╔═╡ b37d3f48-0b23-4700-bb45-050b08209669 @time L ∩ C -# ╔═╡ 26a8c2c5-27da-4389-bfd8-ca3793dd994e -I = FSA( - kron(L.α, C.α), - kron(L.T, C.T), - kron(L.ω, C.ω), - L.ρ * C.ρ, - kron(L.λ, C.λ) -) - # ╔═╡ 183f8031-b384-408b-8cd6-c84f23693dfc +# ╠═╡ disabled = true +#=╠═╡ M = sparse([1,1,2,3,4,4,5,6,7,7,8,9],[1,3,2,4,1,3,2,4,1,3,2,4], one(K), nstates(L), nstates(C)) + ╠═╡ =# # ╔═╡ b605383a-4080-4916-857c-2528f6ad172c M' * L.ω @@ -122,20 +116,11 @@ G = DenseFSA(H, sort(collect(Σ)), zero(K)) # ╔═╡ 54888ef8-6ee9-446d-9b78-364fe35e52b6 G, L -# ╔═╡ b2290feb-24a1-4f7d-8216-7c69ea363a67 -L - -# ╔═╡ 5c3893f7-b64f-410f-9be2-5c2023fd9093 -# C = A ∩ B - -# ╔═╡ 5ecadd35-feea-459f-9776-3a2762b0de9f -# FSA(C) - -# ╔═╡ 2ea1644a-8836-443b-a1ee-8d13dbd4a534 -H[:, 2] +# ╔═╡ 40ba3c52-84e0-4d70-8d8e-840ec2225baf +G ∩ C -# ╔═╡ 68d8f4b3-48e1-49ca-b910-c65c2ec19768 -ones(K, 3) * H[:,2]' +# ╔═╡ 91b52b46-b8d8-4d14-9f9c-732de9d906ff +G ∩ C |> connect # ╔═╡ Cell order: # ╠═510f7d8a-ce11-11ed-2832-cdc20fa6f700 @@ -153,15 +138,11 @@ ones(K, 3) * H[:,2]' # ╠═b37d3f48-0b23-4700-bb45-050b08209669 # ╠═049d12b4-0107-4ecc-89e4-45d3955bdd0b # ╠═54888ef8-6ee9-446d-9b78-364fe35e52b6 -# ╠═26a8c2c5-27da-4389-bfd8-ca3793dd994e # ╠═183f8031-b384-408b-8cd6-c84f23693dfc # ╠═b605383a-4080-4916-857c-2528f6ad172c # ╠═e91b7104-7149-4770-8abe-fb0a968bd197 # ╠═49fb8a23-bae8-4c66-8490-01d7e28f25f9 # ╠═29a16022-6ebc-4e74-8245-e7293fcb160a # ╠═ada373ae-0e4e-42ca-80a5-98be29aca610 -# ╠═b2290feb-24a1-4f7d-8216-7c69ea363a67 -# ╠═5c3893f7-b64f-410f-9be2-5c2023fd9093 -# ╠═5ecadd35-feea-459f-9776-3a2762b0de9f -# ╠═2ea1644a-8836-443b-a1ee-8d13dbd4a534 -# ╠═68d8f4b3-48e1-49ca-b910-c65c2ec19768 +# ╠═40ba3c52-84e0-4d70-8d8e-840ec2225baf +# ╠═91b52b46-b8d8-4d14-9f9c-732de9d906ff diff --git a/src/FiniteStateAutomata.jl b/src/FiniteStateAutomata.jl index 0d9da0816ee973e9df151f888c7f28b9ffdc54db..3e2beca6e1773ae41625908619d785047dabe543 100644 --- a/src/FiniteStateAutomata.jl +++ b/src/FiniteStateAutomata.jl @@ -34,6 +34,7 @@ export # FSA operations addskipedges, closure, + connect, determinize, globalrenorm, minimize, diff --git a/src/dense_fsa.jl b/src/dense_fsa.jl index dbef9e29045e56d9ee28bfbc8f517bb73bd4d0c4..a044b3eb7ebad65c2d85c9f6a88519c7bda1c85a 100644 --- a/src/dense_fsa.jl +++ b/src/dense_fsa.jl @@ -39,6 +39,8 @@ end ρ(G::DenseFSA) = G.ρ λ(G::DenseFSA) = repeat(G.Σ, size(G.H, 2) - 1) +Base.reverse(A::DenseFSA) = DenseFSA(A.H[:, end:-1:1], A.Σ, A.ρ) + # Intersection with DenseFSA struct IntersectedDenseFSA{K, L, T<:AbstractFSA{K, L}} <: IntersectedAbstractFSA{K, L, DenseFSA{K, L}, T} A::DenseFSA{K, L} @@ -72,6 +74,8 @@ end Base.intersect(A::DenseFSA, B::AbstractFSA) = IntersectedDenseFSA(A, B) Base.intersect(A::AbstractFSA, B::DenseFSA) = IntersectedDenseFSA(B, A) # we assume ∩ to be commutative w.r.t any K +Base.reverse(A::IntersectedDenseFSA) = IntersectedDenseFSA(A.A |> reverse, A.B |> reverse, A.C) + α(I::IntersectedDenseFSA) = begin h1 = I.A.H[:, 1] Q = nstates(I.B) * (size(I.A.H, 2) - 1) @@ -113,3 +117,4 @@ end λ(I::IntersectedDenseFSA) = repeat(λ(I.B), size(I.A.H, 2) - 1) ρ(I::IntersectedDenseFSA) = ρ(I.B) * ρ(I.A) + diff --git a/src/ops.jl b/src/ops.jl index f44d17e08155a85453897751fb43f9b3c60f2eac..400b06b036f8ce36a0a32186a21cf7e65ecb1127 100644 --- a/src/ops.jl +++ b/src/ops.jl @@ -224,7 +224,38 @@ end Returns a vector `x` of dimension `nstates(A)` where `x[i]` is `one(K)` if the state `i` is not accessible, `zero(K)` otherwise. """ -coaccessible(A::AbstractFSA) = accessible(A |> reverse) +function coaccessible(A::AbstractFSA) + vₙ = ω(A) + + m = ones(Bool, nstates(A)) + m[findnz(vₙ)[1]] .= false + + while nnz(vₙ) > 0 + uₙ = T(A) * vₙ + vₙ = uₙ .* m + m[findnz(uₙ)[1]] .= false + end + .! m +end + +""" + connect(A::AbstractFSA) + +Return a FSA ``B`` equivalent of ``A`` such that all states in ``B`` +are accessible and coaccessible. +""" +function connect(A::AbstractFSA{K}) where K + m = accessible(A) .* coaccessible(A) + I = findall(m) + M = sparse(I, 1:length(I), one(K), nstates(A), length(I)) + FSA( + M' * α(A), + M' * T(A) * M, + M' * ω(A), + ρ(A), + λ(A)[I] + ) +end """ renorm(A::FSA)