Methods

readsxmodel(file; [raw_dict]=false, [ST]=nothing, [kwargs]...)

Read a SpaceEx model file.

Input

• file – the filename of the SpaceEx file (in XML format)
• raw_dict – (optional, default: false) if true, return the raw dictionary with the objects that define the model (see Output below), without actually returning a HybridSystem; otherwise, instantiate a HybridSystem with the given assumptions
• ST – (optional, default: nothing) assumption for the type of system for each mode

Output

Hybrid system that corresponds to the given SpaceEx model and the given assumptions on the system type if raw_dict=true; otherwise, a dictionary with the Julia expression objects that define the model. The keys of this dictionary are:

• automaton
• variables
• transitionlabels
• invariants
• flows
• assignments
• guards
• switchings
• nlocations
• ntransitions

Notes

Currently, this function makes the following assumptions:

1. The model contains only 1 component. If the model contains more than 1 component, an error is raised. In this case, recall that network components can be flattened using sspaceex.
2. The default and a custom ST parameter assume that all modes are of the same type. In general, you may pass a vector of system's types in kwargs (not implemented).

Moreover, let us note that:

1. The tags `<notes> ... <

otes>` are ignored.

1. Variable names are stored in the dictionary variables, together with other information such as if the variable is controlled or not. This dictionary is then stored in the extension field (ext) of the hybrid system.
2. The transition labels are stored in the extension field (ext) of the hybrid system.
3. We use the location "id" field (an integer), such that each of the vectors modes, resetmaps and switchings corresponds to the location with the given "id". For example, modes[1] corresponds to the mode for the location with id="1".
4. The name field of a location is ignored.
5. The nature of the switchings is autonomous. If there are guards, these define state-dependent switchings only. Switching control functions are not yet implemented.
6. The resetmaps field consists of the vector of tuples (assignment, guard), for each location.

These comments apply whenever raw_dict=false:

1. The field variables is an ordered dictionary, where the order is given by the insertion order. This allows deterministic iteration over the dictionary, (notice that in a usual dictionary, the order in which the elements are returned does not correspond, in general, to the order in which the symbols were saved). The variables are stored in the coefficients matrix using this insertion order.
2. If ST is nothing, the modes are given as the vector of tuples (flows, invariants), each component being a list of expressions, and similarly the reset maps are the vector of tuples (assignments, guards).

linearHS(HDict; ST=ConstrainedLinearControlContinuousSystem,
         STD=ConstrainedLinearControlDiscreteSystem,
         kwargs...)

Convert the given hybrid-system object into a concrete system type for each mode, and convert Julia expressions into SymEngine symbolic expressions.

Input

• HDict – raw dictionary of hybrid system objects
• ST – (optional, default: ConstrainedLinearControlContinuousSystem) assumption for the type of mathematical system for each mode
• STD – (optional, default: ConstrainedLinearControlDiscreteSystem) assumption for the type of mathematical system for the assignments and guards

Output

The tuple (modes, resetmaps).

Notes

1. "Controlled" variables are interpreted as state variables (there is an ODE flow for them), otherwise these are interpreted as input variables (there is not an ODE for them).
2. If the system has nonlinearities, then some first order derivatives cannot be evaluated to numbers, and this function does not apply. In that case, you will see the error message: ArgumentError: symbolic value cannot be evaluated to a numeric value.
3. We assume that inequalities in invariants are of the form ax <= b or ax >= b, where b is a scalar value. Other combinations are NOT yet supported.
4. In inequalities, x is a vector of variables of two different types only: either all of them are state variables, or all of them are input variables. Other combinations are not yet allowed.
5. Strict and non-strict inequalities are treated as being the same: both are mapped to half-spaces.

count_locations_and_transitions(root_sxmodel)

Returns the number of locations and transitions for each component.

Input

• root_sxmodel – the root element of a SpaceEx file

Output

Two vectors of integers (lcount, tcount), where the i-th entry of lcount and tcount are the number of locations and transitions, respectively, of the i-th component.

parse_sxmath(s; assignment=false)

Returns the list of expressions corresponding to a given SpaceExParser string.

Input

• s – string
• assignment – (optional, default: false)

Output

Vector of expressions, equations or inequalities.

Examples

julia> using SpaceExParser: parse_sxmath

julia> parse_sxmath("x >= 0")
1-element Vector{Expr}:
 :(x >= 0)

julia> parse_sxmath("x' == x & v' == -0.75*v")
2-element Vector{Expr}:
 :(x' = x)
 :(v' = -0.75v)

julia> parse_sxmath("x == 0 & v <= 0")
2-element Vector{Expr}:
 :(x = 0)
 :(v <= 0)

Parentheses are ignored:

julia> parse_sxmath("(x == 0) & (v <= 0)")
2-element Vector{Expr}:
 :(x = 0)
 :(v <= 0)

Splitting is also performend over double ampersand symbols:

julia> parse_sxmath("x == 0 && v <= 0")
2-element Vector{Expr}:
 :(x = 0)
 :(v <= 0)

If you want to parse an assignment, use the assignment flag:

julia> parse_sxmath("x := -x*0.1", assignment=true)
1-element Vector{Expr}:
 :(x = -x * 0.1)

Check that we can parse expressions involving parentheses:

julia> parse_sxmath("(t <= 125 & y>= -100)")
2-element Vector{Expr}:
 :(t <= 125)
 :(y >= -100)
julia> parse_sxmath("t <= 125 & (y>= -100)")
2-element Vector{Expr}:
 :(t <= 125)
 :(y >= -100)

Algorithm

First a sanity check (assertion) is made that the expression makes a coherent use of parentheses.

Then, the following steps are done (in the given order):

• split the string with the & key, or &&
• remove trailing whitespace of each substring
• replace double == with single =
• detect unbalanced parentheses (beginning and final subexpressions) and in that case delete them
• cast to a Julia expression with parse

Notes

For assignments, the nomenclature := is also valid and here it is replaced to =, but you need to set assignment=true for this replacement to take effect.

The characters '(' and ')' are deleted (replaced by the empty character), whenever it is found that there are unbalanced parentheses after the expression is split into subexpressions.

parse_sxmodel!(root_sxmodel, HDict)

Input

• root_sxmodel – root element of an XML document
• HDict – dictionary that wraps the hybrid model and contains the keys (automaton, variables, transitionlabels, invariants, flows, assignments, guards, switchings, nlocations, ntransitions)

Output

The HDict dictionary.

Notes

1. Edge labels are not used and their symbol is (arbitrarily) set to the integer 1.
2. Location identifications ("id" field) are assumed to be integers.
3. The switchings types are assumed to be autonomous. See Switching in Systems and Control, D. Liberzon, for further details on the classification of switchings.
4. We add fresh variables for each component (id_variable += 1). In general variables can be shared among components if the bindings are defined. Currently, we make the simplifying assumption that the model has only one component and we don't take bindings into account.

add_variable!(variables, field, id=1)

Input

• variables – vector of symbolic variables
• field – an EzXML.Node node with containing information about a param field
• id – (optional, default: 1) integer that identifies the variable

Output

The updated vector of symbolic variables.

Notes

Parameters can be either variable names (type "real") or labels (type "label").

add_transition_label!(labels, field)

Input

• labels – vector of transition labels
• field – node with a param label field

Output

The updated vector of transition labels.

parse_location(field)

Input

• field – location node

Output

The tuple (id, invariant, flow) where:

• id is the integer that identifies the location,
• invariant is the list of subexpressions that determine that invariant for this location,
• flow is the list of ODEs that define the flow for this location.

Both the invariant and the flow are vectors of symbolic expressions Expr.

parse_transition(field)

Input

• field – transition node

Output

The tuple (q, r, G, A) where q and r are the source mode and target mode respectively for this transition, G is the list of guards for this transition, and A is the list of assignments. G and A are vectors of symbolic expressions Expr.

Notes

It is assumed that the "source" and "target" fields can be cast to integers.

It can happen that the given transition does not contain the "guard" field (or the "assignment", or both); in that case this function returns an empty of expressions for those cases.

convert(::Type{HalfSpace{N}}, expr::Expr; vars=nothing) where {N}

Return a LazySet.HalfSpace given a symbolic expression that represents a half-space.

Input

• expr – a symbolic expression
• vars – (optional, default: nothing): set of variables with respect to which the gradient is taken; if nothing, it takes the free symbols in the given expression

Output

A HalfSpace, in the form ax <= b.

Examples

julia> using LazySets: HalfSpace

julia> convert(HalfSpace, :(x1 <= -0.03))
HalfSpace{Float64, Vector{Float64}}([1.0], -0.03)

julia> convert(HalfSpace, :(x1 < -0.03))
HalfSpace{Float64, Vector{Float64}}([1.0], -0.03)

julia> convert(HalfSpace, :(x1 > -0.03))
HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03)

julia> convert(HalfSpace, :(x1 >= -0.03))
HalfSpace{Float64, Vector{Float64}}([-1.0], 0.03)

julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6))
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, -2.0], 6.0)

You can also specify the set of "ambient" variables, even if not all of them appear:

julia> using SymEngine: Basic

julia> convert(HalfSpace, :(x1 + x2 <= 2*x4 + 6), vars=Basic[:x1, :x2, :x3, :x4])
HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0)

convert(::Type{Hyperplane{N}}, expr::Expr; vars=nothing) where {N}

Return a LazySet.Hyperplane given a symbolic expression that represents a hyperplane.

Input

• expr – a symbolic expression
• vars – (optional, default: nothing): set of variables with respect to which the gradient is taken; if nothing, it takes the free symbols in the given expression

Output

A Hyperplane, in the form ax = b.

Examples

julia> using LazySets: Hyperplane

julia> convert(Hyperplane, :(x1 = -0.03))
Hyperplane{Float64, Vector{Float64}}([1.0], -0.03)

julia> convert(Hyperplane, :(x1 + 0.03 = 0))
Hyperplane{Float64, Vector{Float64}}([1.0], -0.03)

julia> convert(Hyperplane, :(x1 + x2 = 2*x4 + 6))
Hyperplane{Float64, Vector{Float64}}([1.0, 1.0, -2.0], 6.0)

You can also specify the set of "ambient" variables in the hyperplane, even if not all of them appear:

julia> using SymEngine: Basic

julia> convert(Hyperplane, :(x1 + x2 = 2*x4 + 6), vars=Basic[:x1, :x2, :x3, :x4])
Hyperplane{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0)

free_symbols(expr::Expr, set_type::Type{LazySet})

Return the free symbols in an expression that represents a given set type.

Input

• expr – symbolic expression

Output

A list of symbols, in the form of SymEngine Basic objects.

Examples

julia> using SpaceExParser: free_symbols

julia> using LazySets: HalfSpace

julia> free_symbols(:(x1 <= -0.03), HalfSpace)
1-element Vector{SymEngine.Basic}:
 x1

julia> free_symbols(:(x1 + x2 <= 2*x4 + 6), HalfSpace)
3-element Vector{SymEngine.Basic}:
 x2
 x1
 x4

is_halfspace(expr::Expr)

Determine whether the given expression corresponds to a half-space.

Input

• expr – a symbolic expression

Output

true if expr corresponds to a half-space or false otherwise.

Examples

julia> using SpaceExParser: is_halfspace

julia> all(is_halfspace.([:(x1 <= 0), :(x1 < 0), :(x1 > 0), :(x1 >= 0)]))
true

julia> is_halfspace(:(2*x1 <= 4))
true

julia> is_halfspace(:(6.1 <= 5.3*f - 0.1*g))
true

julia> is_halfspace(:(2*x1^2 <= 4))
false

julia> is_halfspace(:(x1^2 > 4*x2 - x3))
false

julia> is_halfspace(:(x1 > 4*x2 - x3))
true

is_hyperplane(expr::Expr)

Determine whether the given expression corresponds to a hyperplane.

Input

• expr – a symbolic expression

Output

true if expr corresponds to a half-space or false otherwise.

Examples

julia> using SpaceExParser: is_hyperplane

julia> is_hyperplane(:(x1 = 0))
true

julia> is_hyperplane(:(2*x1 = 4))
true

julia> is_hyperplane(:(6.1 = 5.3*f - 0.1*g))
true

julia> is_hyperplane(:(2*x1^2 = 4))
false

julia> is_hyperplane(:(x1^2 = 4*x2 - x3))
false

julia> is_hyperplane(:(x1 = 4*x2 - x3))
true

is_linearcombination(L::Basic)

Determine whether the expression L is a linear combination of its symbols.

Input

• L – expression

Output

true if L is a linear combination or false otherwise.

Examples

julia> using SpaceExParser: is_linearcombination

julia> is_linearcombination(:(2*x1 - 4))
true

julia> is_linearcombination(:(6.1 - 5.3*f - 0.1*g))
true

julia> is_linearcombination(:(2*x1^2))
false

julia> is_linearcombination(:(x1^2 - 4*x2 + x3 + 2))
false