From 7a7b32e3973ca0ceca73eb09cf5d3dd61cd969d7 Mon Sep 17 00:00:00 2001 From: schillic Date: Sun, 24 Feb 2019 14:28:34 +0100 Subject: [PATCH] better description of properties --- src/Properties/IntersectionProperty.jl | 12 +++++++++++- src/Properties/SubsetProperty.jl | 9 +++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/src/Properties/IntersectionProperty.jl b/src/Properties/IntersectionProperty.jl index 9a203e70..bdc9044d 100644 --- a/src/Properties/IntersectionProperty.jl +++ b/src/Properties/IntersectionProperty.jl @@ -9,6 +9,15 @@ set of bad states is empty. - `bad` -- convex set representing the bad states - `witness` -- witness point (empty vector if not set) + +### Notes + +The following formula characterizes whether a set ``X`` satisfies a safety +property characterized by a set of bad states 𝑃: + +```math + X \\models 𝑃 \\iff X ∩ 𝑃.\\texttt{bad} = ∅ +``` """ mutable struct IntersectionProperty{N<:Real} <: Property bad::LazySet @@ -33,7 +42,8 @@ Checks whether a convex set is disjoint from the set of bad states. ### Output -`true` iff the given set of states does not intersect with the bad states. +`true` iff the given set of states does not intersect with the set of bad +states. """ @inline function check(𝑃::IntersectionProperty, X::LazySet)::Bool empty_intersection, witness = is_intersection_empty(X, 𝑃.bad, true) diff --git a/src/Properties/SubsetProperty.jl b/src/Properties/SubsetProperty.jl index e4dddaff..e57baabe 100644 --- a/src/Properties/SubsetProperty.jl +++ b/src/Properties/SubsetProperty.jl @@ -9,6 +9,15 @@ contained in the set of safe states. - `safe` -- convex set representing the safe states - `witness` -- witness point (empty vector if not set) + +### Notes + +The following formula characterizes whether a set ``X`` satisfies a safety +property characterized by a set of safe states 𝑃: + +```math + X \\models 𝑃 \\iff X ⊆ 𝑃.\\texttt{safe} +``` """ mutable struct SubsetProperty{N<:Real} <: Property safe::LazySet