Can now chain formulas, added AtomicFunctions

sisl · Jul 31, 2024 · 1a53117 · 1a53117
1 parent 1db5642
commit 1a53117
Show file tree

Hide file tree

Showing 3 changed files with 79 additions and 31 deletions.
diff --git a/src/SignalTemporalLogic.jl b/src/SignalTemporalLogic.jl
@@ -8,11 +8,13 @@ export
     ∧,
     ∨,
     ⟹,
+    ⟺,
     Formula,
     Interval,
     eventually,
     always,
     Atomic,
+    AtomicFunction,
     ⊤,
     ⊥,
     Predicate,

diff --git a/src/stl.jl b/src/stl.jl
@@ -1,5 +1,5 @@
 ### A Pluto.jl notebook ###
-# v0.19.29
+# v0.19.40
 
 using Markdown
 using InteractiveUtils
@@ -86,6 +86,14 @@ begin
 	∨(ϕ1::Formula, ϕ2::Formula) = xᵢ->ϕ1(xᵢ) ∨ ϕ2(xᵢ)
 end
 
+# ╔═╡ 474a0852-ebd0-4483-9627-f9669f17fab6
+md"""
+## Mapping over time
+"""
+
+# ╔═╡ 4b6a17a2-a914-4408-ac5a-a51ed9f126ce
+Base.map(ϕ::Formula, x::AbstractArray) = map(t->ϕ(x[t:end]), eachindex(x))
+
 # ╔═╡ 50e69922-f07e-48dd-981d-d68c8cd07f7f
 md"""
 # Robustness
@@ -129,6 +137,23 @@ begin
 	ρ̃(xₜ, ϕ::Atomic; kwargs...) = ρ(xₜ, ϕ)
 end
 
+# ╔═╡ 75b654ee-e8a8-4d70-bf9b-f8ddf20847a4
+md"""
+## Atomic Function
+"""
+
+# ╔═╡ f3813cc2-af90-4710-9afb-e56a3b568338
+begin
+	Base.@kwdef mutable struct AtomicFunction <: Formula
+		f::Function # ℝⁿ → 𝔹
+		ρ_max = Inf
+	end
+
+	(ϕ::AtomicFunction)(x) = map(xₜ->all(xₜ), ϕ.f(x))
+	ρ(xₜ, ϕ::AtomicFunction) = xₜ ? ϕ.ρ_max : -ϕ.ρ_max
+	ρ̃(xₜ, ϕ::AtomicFunction; kwargs...) = ρ(xₜ, ϕ)
+end
+
 # ╔═╡ 296c7321-db0d-4878-a4d9-6e2b6ee76e4e
 md"""
 ## Predicate
@@ -561,10 +586,7 @@ function parse_formula(ex)
 	if ex isa Formula
 		return ex
 	elseif ex isa Symbol
-		local sym = string(ex)
-		return quote
-			error("Symbol `$($sym)` needs to be a Formula type.")
-		end
+		return esc(ex) # assume the Symbol is a @formula that is already parsed
 	elseif is_junction(ex.head)
 		return parse_junction(ex)
 	else
@@ -627,6 +649,8 @@ function parse_formula(ex)
 						return :(Disjunction(FlippedPredicate($(esc(μ)), $c), Predicate($(esc(μ)), $c)))
 					elseif is_junction(formula_type)
 						return parse_junction(ex)
+					elseif ex.head == :(->)
+						return :(AtomicFunction(f=$(esc(ex))))
 					else
 						error("""
 						No formula parser for:
@@ -636,7 +660,9 @@ function parse_formula(ex)
 							core.head = $(core.head)
 							core.args = $(core.args)
 							body = $body
-							ex = $ex""")
+							ex = $ex
+							ex.head = $(ex.head)
+							ex.args = $(ex.args)""")
 					end
 				end
             end
@@ -1287,6 +1313,8 @@ version = "17.4.0+0"
 # ╠═5c454ece-de05-4cce-9996-037df54024e5
 # ╟─8c2a500b-8d62-48a3-ac22-b6466858eef9
 # ╠═dc6bec3c-4ca0-457e-886d-0b2a3f8845e8
+# ╟─474a0852-ebd0-4483-9627-f9669f17fab6
+# ╠═4b6a17a2-a914-4408-ac5a-a51ed9f126ce
 # ╟─50e69922-f07e-48dd-981d-d68c8cd07f7f
 # ╠═d57941cf-655b-45f8-b5e2-b39d3cfeb9fb
 # ╠═5c1e16b3-1b3c-4c7a-a484-44b935eaa2a9
@@ -1295,6 +1323,8 @@ version = "17.4.0+0"
 # ╠═851997de-b0f5-4273-a15b-0e1440c2e6cd
 # ╠═916d7fae-6599-41c6-b909-4e1dd66e48f1
 # ╠═c1e17481-91c3-430f-99f3-1b328ec31417
+# ╟─75b654ee-e8a8-4d70-bf9b-f8ddf20847a4
+# ╠═f3813cc2-af90-4710-9afb-e56a3b568338
 # ╟─296c7321-db0d-4878-a4d9-6e2b6ee76e4e
 # ╟─0158daf7-bc8d-4764-81b1-b5e73e02dc8a
 # ╠═1ec0bddb-28d8-420b-856d-2c1ed70a77a4

diff --git a/test/runtests.jl b/test/runtests.jl
@@ -1,5 +1,5 @@
 ### A Pluto.jl notebook ###
-# v0.19.29
+# v0.19.40
 
 using Markdown
 using InteractiveUtils
@@ -85,8 +85,11 @@ $$\exists i: \psi(x_i) \wedge \bigl(\forall j < i: \phi(x_j)\bigr)$$
 # ╔═╡ 1d0e135e-6cc3-422e-ba44-fee53cc1965f
 μ(x) = x
 
-# ╔═╡ 2305b206-0c6d-440d-81b7-0f485cc8a6a8
-# U = @formula 𝒰(_ϕ, _ψ); NOTE: does not work like this.
+# ╔═╡ 4efe597d-a2b3-4a2e-916a-323e4c86a823
+x1 = [0.001, 1, 2, 3, 4, 5, 6, 7, -8, -9, -10];
+
+# ╔═╡ b9643ca4-58aa-4902-a103-2c8140eb6e74
+x1
 
 # ╔═╡ 2d65db96-f8cf-4ccc-b4f5-1c642249ed7b
 md"""
@@ -439,35 +442,25 @@ _ϕ(x[1])
 # ╔═╡ 14f52f51-ec7b-4a30-af2d-4dfeed8618c0
 _ψ = @formula xₜ -> -μ(xₜ) > 0;
 
-# ╔═╡ 2c8c423e-ed23-4be9-90f6-d96e9ca8c3cb
-U = @formula 𝒰(xₜ -> μ(xₜ) > 0, xₜ -> -μ(xₜ) > 0);
+# ╔═╡ 2305b206-0c6d-440d-81b7-0f485cc8a6a8
+U = @formula 𝒰(_ϕ, _ψ);
 
 # ╔═╡ ba9e4d5a-e791-4f04-9be1-bbdd5de09d6c
-U([0.1, 1, 2, 3, -10, -9, -8])
+@test U([0.1, 1, 2, 3, -10, -9, -8])
 
 # ╔═╡ d79856be-3c2f-4ff7-a9c6-94a3a4bf8ffe
-U(x)
-
-# ╔═╡ 4efe597d-a2b3-4a2e-916a-323e4c86a823
-begin
-	x1 = [0.001, 1, 2, 3, 4, 5, 6, 7, -8, -9, -10]
-	ϕ1 = @formula xᵢ -> xᵢ > 0
-	ψ1 = @formula xᵢ -> -xᵢ > 0 # xᵢ < 0
-end;
-
-# ╔═╡ b9643ca4-58aa-4902-a103-2c8140eb6e74
-x1
+@test U(x)
 
 # ╔═╡ 562d3796-bf48-4260-9683-0999f628b43c
-U(x1)
+@test U(x1)
 
 # ╔═╡ 482600d2-e1a7-446c-934d-3234885ba14c
 begin
 	time = 1:length(x1)
 	steptype = :steppost
-	plot(time, miss(ϕ1.(x1)) .+ 1, lw=5, c=:blue, lab=false, lt=steptype)
-	plot!(time, miss(ψ1.(x1)), lw=5, c=:red, lab=false, lt=steptype)
-	plot!(time, .∨(ϕ1.(x1), ψ1.(x1)) .- 1, lw=5, c=:purple, lab=false, lt=steptype)
+	plot(time, miss(_ϕ.(x1)) .+ 1, lw=5, c=:blue, lab=false, lt=steptype)
+	plot!(time, miss(_ψ.(x1)), lw=5, c=:red, lab=false, lt=steptype)
+	plot!(time, map(U, x1) .- 1, lw=5, c=:purple, lab=false, lt=steptype)
 	plot!(ytickfont=12, xtickfont=12)
 
 	yticks!(0:2, [L"\phi \mathcal{U} \psi", L"\psi", L"\phi"])
@@ -511,6 +504,27 @@ begin
 	plot!(1:length(x2), vec(∇ρ̃(x2, ϕ_until; w=2)), label="soft ∇ρ̃(x,ϕ; w=2)")
 end
 
+# ╔═╡ d4bc34f1-bbee-4f4f-9599-6294c013f495
+function until_local_test()
+	__ψ = @formula xₜ->xₜ[1]
+	__ϕ = @formula xₜ->xₜ[2]
+	__until = @formula 𝒰(__ψ, __ϕ)
+	x = [
+	    [false, false],
+	    [false, false],
+	    [true, false],
+	    [true, false],
+	    [true, true],
+	    [false, true],
+	    [false, true],
+	    [false, true],
+	]
+	return map(__until, x)
+end
+
+# ╔═╡ 5ecad5e6-48f3-43d5-921e-6dfbdb516bf4
+@test until_local_test() == [false, false, true, true, true, true, true, true]
+
 # ╔═╡ ab72fec1-8266-4064-8a58-6de08b318ada
 begin
     x_comb = [4, 3, 2, 1, 0, -1, -2, -3, -4]
@@ -701,14 +715,15 @@ end
 # ╔═╡ 5ccc7a0f-c3b2-4429-9bd5-d7fd9bcb97b5
 @test begin
 	local upright = @formula s -> abs(s[1]) < π / 4
-	local ψ = @eval @formula □($upright) # input anonymous function MUST be a Formula
+	local ψ = @formula □(upright)
 	ψ([π/10]) && !(ψ([π/3]))
 end
 
 # ╔═╡ e2313bcd-dd8f-4ffd-ac1e-7e08304c37b5
-@test_throws "Symbol " begin
-	local variable
+@test begin
+	local variable = @formula x->x > 0
 	local ψ = @formula □(variable)
+	true
 end
 
 # ╔═╡ aea96bbd-d006-4933-a8cb-5165a0158499
@@ -816,7 +831,6 @@ IS_NOTEBOOK && TableOfContents()
 # ╠═0f661852-d1b4-4e48-946f-33c111230047
 # ╠═14f52f51-ec7b-4a30-af2d-4dfeed8618c0
 # ╠═2305b206-0c6d-440d-81b7-0f485cc8a6a8
-# ╠═2c8c423e-ed23-4be9-90f6-d96e9ca8c3cb
 # ╠═b74bd2ee-eb33-4c41-b3b0-e2544166a8ae
 # ╠═ba9e4d5a-e791-4f04-9be1-bbdd5de09d6c
 # ╠═d79856be-3c2f-4ff7-a9c6-94a3a4bf8ffe
@@ -837,6 +851,8 @@ IS_NOTEBOOK && TableOfContents()
 # ╠═d32bf800-51d5-455f-ab50-91bb31f67e83
 # ╠═c738c26d-10a7-488a-976e-cc5f69fc4526
 # ╠═26a3441c-9128-46c6-8b5a-6858d642509c
+# ╠═d4bc34f1-bbee-4f4f-9599-6294c013f495
+# ╠═5ecad5e6-48f3-43d5-921e-6dfbdb516bf4
 # ╟─b30d0b1e-493b-48c0-b492-5f7dd2ad872b
 # ╟─ce82cf55-0e32-412e-b6c6-f95563796e7e
 # ╠═ab72fec1-8266-4064-8a58-6de08b318ada