Skip to content

Commit

Permalink
Fixed (con/dis)junction placement within a single anonymous function #5
Browse files Browse the repository at this point in the history
  • Loading branch information
@mossr
mossr committed Sep 19, 2023
1 parent 731b486 commit cac8f39
Show file tree
Hide file tree
Showing 2 changed files with 142 additions and 61 deletions.
133 changes: 87 additions & 46 deletions src/stl.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -459,6 +459,15 @@ md"""
# Robustness helpers
"""

# ╔═╡ 2dae8ed0-3bd6-44e1-a762-a75b5cc9f9f0
is_conjunction(head) = head ∈ [:(&&), :∧]

# ╔═╡ 7bc35b0b-fdbe-46d2-83c1-0c056772761e
is_disjunction(head) = head ∈ [:(||), :∨]

# ╔═╡ 512f0bdc-7e4c-4a01-ae68-adbd57d63cb0
is_junction(head) = is_conjunction(head) || is_disjunction(head)

# ╔═╡ 4bba7170-e7b7-4ccf-b6f4-a32b7ee4b809
function split_lambda(λ)
var, body = λ.args
Expand Down Expand Up @@ -495,8 +504,16 @@ end

# ╔═╡ 982ac681-79a0-4c69-a5cc-0546a5ebd3be
function split_junction(ϕ_ψ)
ϕ, ψ = ϕ_ψ.args[end-1:end]
return ϕ, ψ
if ϕ_ψ.head == :(->)
var = ϕ_ψ.args[1]
head = ϕ_ψ.args[2].args[1].head
ϕ = Expr(:(->), var, ϕ_ψ.args[2].args[1].args[1])
ψ = Expr(:(->), var, ϕ_ψ.args[2].args[1].args[2])
else
head = ϕ_ψ.head
ϕ, ψ = ϕ_ψ.args[end-1:end]
end
return ϕ, ψ, head
end

# ╔═╡ 84effb59-b744-4bd7-b724-6f3e4056a737
Expand Down Expand Up @@ -536,23 +553,17 @@ end

# ╔═╡ e44e21ed-36f6-4d2c-82bd-fa1575cc49f8
function parse_formula(ex)
ex = Base.remove_linenums!(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
elseif ex.head ∈ (:(&&), :(||))
ϕ_ex, ψ_ex = split_junction(ex)
ϕ = parse_formula(ϕ_ex)
ψ = parse_formula(ψ_ex)
if ex.head == :(&&)
return :(Conjunction($ϕ, $ψ))
elseif ex.head == :(||)
return :(Disjunction($ϕ, $ψ))
end
else
elseif is_junction(ex.head)
return parse_junction(ex)
else
var, body = ex.args
body = Base.remove_linenums!(body)
if var ∈ [:◊, :□]
Expand All @@ -569,49 +580,61 @@ function parse_formula(ex)
ψ = parse_formula(ψ_ex)
return :(Until($ϕ, $ψ, $I))
else
core = body.head == :block ? body.args[end] : body
core = body.head == :block ? body.args[end] : body
if typeof(core) == Bool
return :(Atomic(value=$(esc(core))))
else
if var ∈ (:⟺, :(==), :(!=), :⟹, :∧, :∨)
ϕ_ex, ψ_ex = split_junction(ex)
ϕ = parse_formula(ϕ_ex)
ψ = parse_formula(ψ_ex)
if is_junction(core.head)
return parse_junction(ex)
elseif var ∈ (:⟺, :(==), :(!=), :⟹) || is_junction(var)
ϕ_ex, ψ_ex, _ = split_junction(ex)
ϕ = parse_formula(ϕ_ex)
ψ = parse_formula(ψ_ex)
if var ∈ [:⟺, :(==)]
return :(Biconditional($ϕ, $ψ))
elseif var == :(==)
elseif var == :(!=)
return :(Negation(Biconditional($ϕ, $ψ)))
elseif var == :⟹
return :(Implication($ϕ, $ψ))
elseif var == :∧
return :(Conjunction($ϕ, $ψ))
elseif var == :∨
return :(Disjunction($ϕ, $ψ))
end
elseif var ∈ [:¬, :!]
ϕ_inner = parse_formula(strip_negation(ex))
return :(Negation($ϕ_inner))
else
formula_type = core.args[1]
if formula_type ∈ [:¬, :!]
ϕ_inner = parse_formula(strip_negation(ex))
return :(Negation($ϕ_inner))
elseif formula_type == :>
μ, c = split_predicate(ex)
return :(Predicate($(esc(μ)), $c))
elseif formula_type == :<
μ, c = split_predicate(ex)
return :(FlippedPredicate($(esc(μ)), $c))
return :(Implication($ϕ, $ψ))
elseif is_conjunction(var)
return :(Conjunction($ϕ, $ψ))
elseif is_disjunction(var)
return :(Disjunction($ϕ, $ψ))
end
elseif var ∈ [:¬, :!]
ϕ_inner = parse_formula(strip_negation(ex))
return :(Negation($ϕ_inner))
else
formula_type = core.args[1]
if formula_type ∈ [:¬, :!]
ϕ_inner = parse_formula(strip_negation(ex))
return :(Negation($ϕ_inner))
elseif formula_type == :>
μ, c = split_predicate(ex)
return :(Predicate($(esc(μ)), $c))
elseif formula_type == :<
μ, c = split_predicate(ex)
return :(FlippedPredicate($(esc(μ)), $c))
elseif formula_type ∈ [:⟺, :(==)]
μ, c = split_predicate(ex)
μ, c = split_predicate(ex)
return :(Conjunction(Negation(Predicate($(esc(μ)), $c)), Negation(FlippedPredicate($(esc(μ)), $c))))
elseif formula_type == :(!=)
μ, c = split_predicate(ex)
μ, c = split_predicate(ex)
return :(Disjunction(FlippedPredicate($(esc(μ)), $c), Predicate($(esc(μ)), $c)))
elseif is_junction(formula_type)
return parse_junction(ex)
else
error("No type for formula: $(formula_type) and var $(var)")
end
end
error("""
No formula parser for:
formula_type = $(formula_type)
var = $var
core = $core
core.head = $(core.head)
core.args = $(core.args)
body = $body
ex = $ex""")
end
end
end
end
end
Expand All @@ -634,6 +657,20 @@ always = @formula ¬◊(¬(xₜ -> xₜ > 0))
# ╔═╡ c1e17481-91c3-430f-99f3-1b328ec31417
⊥ = @formula xₜ -> false

# ╔═╡ 40603feb-ebd6-47c6-97c4-c27b5211ff9e
function parse_junction(ex)
ϕ_ex, ψ_ex, head = split_junction(ex)
ϕ = parse_formula(ϕ_ex)
ψ = parse_formula(ψ_ex)
if is_conjunction(head)
return :(Conjunction($ϕ, $ψ))
elseif is_disjunction(head)
return :(Disjunction($ϕ, $ψ))
else
error("No junction head for $(head).")
end
end

# ╔═╡ e16f2079-f028-46c6-b4e7-bf23fe9dcbfb
md"""
# Notebook
Expand All @@ -642,14 +679,14 @@ md"""
# ╔═╡ c66d8ffa-44d0-4550-9456-870aae5db796
IS_NOTEBOOK = @isdefined PlutoRunner

# ╔═╡ 210d23f1-2374-4511-a012-852f1f2dc3be
IS_NOTEBOOK && TableOfContents()

# ╔═╡ eeabb14a-7ca8-4446-b3d6-39a41b5b452c
if IS_NOTEBOOK
using PlutoUI
end

# ╔═╡ 210d23f1-2374-4511-a012-852f1f2dc3be
IS_NOTEBOOK && TableOfContents()

# ╔═╡ 00000000-0000-0000-0000-000000000001
PLUTO_PROJECT_TOML_CONTENTS = """
[deps]
Expand Down Expand Up @@ -1247,6 +1284,10 @@ version = "17.4.0+0"
# ╟─067dadb1-1312-4035-930c-65b1068f7013
# ╠═97adec7a-75fd-40b1-9e46-e302c1dd6b9e
# ╠═e44e21ed-36f6-4d2c-82bd-fa1575cc49f8
# ╠═2dae8ed0-3bd6-44e1-a762-a75b5cc9f9f0
# ╠═7bc35b0b-fdbe-46d2-83c1-0c056772761e
# ╠═512f0bdc-7e4c-4a01-ae68-adbd57d63cb0
# ╠═40603feb-ebd6-47c6-97c4-c27b5211ff9e
# ╠═4bba7170-e7b7-4ccf-b6f4-a32b7ee4b809
# ╠═15dc4645-b08e-4a5a-a65d-1858b948f324
# ╠═b90947cb-2cbe-4410-abbe-4869b5caa313
Expand Down
70 changes: 55 additions & 15 deletions test/runtests.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,6 @@ using Statistics
# ╔═╡ d06d3ce6-d13b-4ab6-bb66-8a07835e1ce7
using LinearAlgebra

# ╔═╡ f4ccd76d-fdf8-436a-83d3-5b062e45152e
begin
using Random
Random.seed!(4)
speeds = rand(80:125, 10)
rpms = rand(4700:4755, 10)
end

# ╔═╡ d8a7facd-1ad8-413d-9037-054472fdc50f
md"""
# STL Formula Testing
Expand Down Expand Up @@ -208,8 +200,14 @@ md"""
$$\square_{1,10} v < 120 \wedge \square_{1,5} \omega < 4750$$
"""

# ╔═╡ 8ebb7717-7563-4202-ae47-2d6c6646a874
# transmission = @formula □(1:10, x -> x[1] < 120) ∧ □(1:5, x -> x[2] < 4750)
# ╔═╡ 88403601-59c3-4e67-9e02-90fdf5800e4a
# transmission = @formula □(x -> x[1] < 120) ∧ □(x -> x[2] < 4750)

# ╔═╡ f4ccd76d-fdf8-436a-83d3-5b062e45152e
begin
speeds = Real[114, 117, 100, 96, 92, 88, 108, 101, 118, 119]
rpms = Real[4719, 4747, 4706, 4744, 4701, 4744, 4743, 4753, 4712, 4704]
end

# ╔═╡ 46036c23-797f-4f62-b9fa-64f43950747f
speeds
Expand All @@ -220,6 +218,14 @@ rpms
# ╔═╡ d0b29940-303b-41ac-9313-ee290bde89c5
signals = collect(zip(speeds, rpms))

# ╔═╡ 84496823-db6a-4070-b4e3-c8aff24c54a7
function fill2size(arr, val, n)
while length(arr) < n
push!(arr, val)
end
return arr
end

# ╔═╡ d143a411-7824-411c-be71-a7fb6b9745a5
# with_terminal() do
# T = length(signals)
Expand Down Expand Up @@ -253,6 +259,11 @@ md"""
# Variable testing
"""

# ╔═╡ fda28f2d-255f-4fd6-b08f-59d61c20eb08
md"""
# Junction testing
"""

# ╔═╡ 41dd7143-8783-45ea-9414-fa80b68b4a6c
md"""
# README Example Tests
Expand Down Expand Up @@ -582,22 +593,24 @@ map(x->ρ(x, ϕ_md), X) # ρ.(X, ϕ) doesn't work
# ╔═╡ 29b0e762-9b4e-4cde-adc3-9ead18115917
map(x->ρ̃(x, ϕ_md), X) # ρ.(X, ϕ) doesn't work

# ╔═╡ 88403601-59c3-4e67-9e02-90fdf5800e4a
transmission = @formula □(x -> x[1] < 120) ∧ □(x -> x[2] < 4750)
# ╔═╡ 8ebb7717-7563-4202-ae47-2d6c6646a874
transmission = @formula □(1:10, x -> x[1] < 120) ∧ □(1:5, x -> x[2] < 4750)

# ╔═╡ fb56bf20-317b-41bc-b0ad-33fac8d54dc2
transmission(signals)
@test transmission(signals)

# ╔═╡ 61a54891-d15d-4747-bd29-ee9d3d24fb2e
# Get the robustness at each time step.
# Only works (correctly) when the interval is fully open [1, length].
function ρ_overtime(x, ϕ)
return [ρ(x[1:t], ϕ) for t in 1:length(x)]
return [ρ(fill2size(x[1:t], (-Inf, -Inf), length(x)), ϕ) for t in 1:length(x)]
end

# ╔═╡ 01ea793a-52b4-45a8-b829-4b7acfb5b49d
ρ_overtime(signals, transmission)

# ╔═╡ 67d1440d-42f6-4255-ba27-d041b45fec78
@test ρ(signals, transmission) == 1

# ╔═╡ 324c7c0a-b627-46d3-945d-573c960d57e6
∇ρ(signals, transmission)

Expand Down Expand Up @@ -688,6 +701,27 @@ end
local ψ = @formula □(variable)
end

# ╔═╡ aea96bbd-d006-4933-a8cb-5165a0158499
@test begin
local conjunc_test = @formula s->(s[1] < 50) && (s[4] < 1)
conjunc_test([49, 0, 0, 0.9]) == true && conjunc_test([49, 0, 0, 1.1]) == false
end

# ╔═╡ 781e31e0-1688-48e0-9a22-b5aea40ffb87
@test begin
local conjunc_test2 = @formula (s->s[1] < 50) && (s->s[4] < 1)
conjunc_test2([49, 0, 0, 0.9]) == true && conjunc_test2([49, 0, 0, 1.1]) == false
end

# ╔═╡ 6c843d45-4c30-4dcd-a30b-27a12c2e1195
@test begin
local ϕ = @formula □(s->s[1] < 50 && s[4] < 1)
ϕ([[49, 0, 0, 0], [49, 0, 0, -1]]) &&
ϕ([(49, 0, 0, 0), (49, 0, 0, -1)]) &&
ϕ(([49, 0, 0, 0], [49, 0, 0, -1])) &&
ϕ(((49, 0, 0, 0), (49, 0, 0, -1)))
end

# ╔═╡ c4f343f7-8c63-4f71-8f46-668675841de7
@test begin
# Signals (i.e., trace)
Expand Down Expand Up @@ -845,8 +879,10 @@ IS_NOTEBOOK && TableOfContents()
# ╠═811f6836-e5c8-447f-aa26-dda644fecc1b
# ╠═d0b29940-303b-41ac-9313-ee290bde89c5
# ╠═fb56bf20-317b-41bc-b0ad-33fac8d54dc2
# ╠═84496823-db6a-4070-b4e3-c8aff24c54a7
# ╠═61a54891-d15d-4747-bd29-ee9d3d24fb2e
# ╠═01ea793a-52b4-45a8-b829-4b7acfb5b49d
# ╠═67d1440d-42f6-4255-ba27-d041b45fec78
# ╠═324c7c0a-b627-46d3-945d-573c960d57e6
# ╠═e0cc216e-8565-4ca5-8ee8-fe9516bc6c1a
# ╠═d143a411-7824-411c-be71-a7fb6b9745a5
Expand Down Expand Up @@ -879,6 +915,10 @@ IS_NOTEBOOK && TableOfContents()
# ╠═f725ac4b-d8b7-4955-bea0-f3d3d83265aa
# ╠═5ccc7a0f-c3b2-4429-9bd5-d7fd9bcb97b5
# ╠═e2313bcd-dd8f-4ffd-ac1e-7e08304c37b5
# ╟─fda28f2d-255f-4fd6-b08f-59d61c20eb08
# ╠═aea96bbd-d006-4933-a8cb-5165a0158499
# ╠═781e31e0-1688-48e0-9a22-b5aea40ffb87
# ╠═6c843d45-4c30-4dcd-a30b-27a12c2e1195
# ╟─41dd7143-8783-45ea-9414-fa80b68b4a6c
# ╟─cc3e80a3-b3e6-46ab-888c-2b1795d8d3d4
# ╠═c4f343f7-8c63-4f71-8f46-668675841de7
Expand Down

0 comments on commit cac8f39

Please sign in to comment.