diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index c229e6f..c66d336 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.10.0","generation_timestamp":"2024-02-09T22:37:14","documenter_version":"1.2.1"}} \ No newline at end of file +{"documenter":{"julia_version":"1.10.1","generation_timestamp":"2024-02-27T21:43:56","documenter_version":"1.2.1"}} \ No newline at end of file diff --git a/dev/about/index.html b/dev/about/index.html index c09b821..12b6a53 100644 --- a/dev/about/index.html +++ b/dev/about/index.html @@ -1,4 +1,4 @@ About · SpaceExParser.jl
GitHub

About

This page contains some general information about this project, and recommendations about contributing.

Contributing

If you like this package, consider contributing!

Creating an issue in the GitHub issue tracker to report a bug, open a discussion about existing functionality, or suggesting new functionality is appreciated.

If you have written code and would like it to be peer reviewed and added to the library, you can fork the repository and send a pull request (see below). Typical contributions include fixing a bug, adding a new feature or improving the documentation (either in source code or the online manual).

Below we detail some general comments about contributing to this package. The JuliaReach Developer's Documentation describes coding guidelines; take a look when in doubt about the coding style that is expected for the code that is finally merged into the library.

Branches

Each pull request (PR) should be pushed in a new branch with the name of the author followed by a descriptive name, e.g. mforets/my_feature. If the branch is associated to a previous discussion in one issue, we use the name of the issue for easier lookup, e.g. mforets/7.

Unit testing and continuous integration (CI)

This project is synchronized with GitHub Actions such that each PR gets tested before merging (and the build is automatically triggered after each new commit). For the maintainability of this project, it is important to make all unit tests pass.

To run the unit tests locally, you can do:

julia> using Pkg
 
-julia> Pkg.test("ReachabilityBase")

We also advise adding new unit tests when adding new features to ensure long-term support of your contributions.

Contributing to the documentation

This documentation is written in Markdown, and it relies on Documenter.jl to produce the HTML layout. To build the docs, run make.jl:

$ julia --color=yes docs/make.jl

Credits

These persons have contributed to SpaceExParser.jl (in alphabetic order):

+julia> Pkg.test("ReachabilityBase")

We also advise adding new unit tests when adding new features to ensure long-term support of your contributions.

Contributing to the documentation

This documentation is written in Markdown, and it relies on Documenter.jl to produce the HTML layout. To build the docs, run make.jl:

$ julia --color=yes docs/make.jl

Credits

These persons have contributed to SpaceExParser.jl (in alphabetic order):

diff --git a/dev/examples/bball/index.html b/dev/examples/bball/index.html index 0257f49..21aa570 100644 --- a/dev/examples/bball/index.html +++ b/dev/examples/bball/index.html @@ -1,2 +1,2 @@ -Bouncing ball · SpaceExParser.jl
GitHub
+Bouncing ball · SpaceExParser.jl
GitHub
diff --git a/dev/examples/examples/index.html b/dev/examples/examples/index.html index 78f15cb..a5888dc 100644 --- a/dev/examples/examples/index.html +++ b/dev/examples/examples/index.html @@ -20,4 +20,4 @@ 6. Constructed Flow: x' == v & v' == -0.999999 with offset support_function(x >= 0 & SLACK2 <= 0.0999999 & SLACK2 >= 0 & -SLACK4 <= 0.199999 & SLACK4 >= 0, mapped by x' == 0 & v' == -SLACK2+0.0499999 ) +SLACK4 <= 0.199999 & SLACK4 >= 0, mapped by x' == 0 & v' == -SLACK2+0.0499999 ) diff --git a/dev/index.html b/dev/index.html index 8097fe4..925c3fa 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,2 +1,2 @@ -Home · SpaceExParser.jl
GitHub

SpaceExParser.jl

SpaceExParser is a Julia package to read SpaceEx modeling files.

The SpaceEx modeling language (SpaceExParser) is a format for the mathematical description of hybrid dynamical systems. It has been described in The SpaceEx Modeling Language, Scott Cotton, Goran Frehse, Olivier Lebeltel. See also An Introduction to SpaceEx, Goran Frehse, 2010.

A visual model editor is available for download on the SpaceEx website. See the examples in this documentation for screenshots and further details.

The aim of this library is to read SpaceExParser modeling files and transform them into Julia objects, for their inspection and analysis, such as reachability computations.

Features

  • Parse SpaceExParser files into types defined in Julia packages HybridSystems.jl and MathematicalSystems.jl.
  • Can read arbitrary ODEs, eg. non-linear dynamics in the ODE flow for each mode.

Library Outline

+Home · SpaceExParser.jl
GitHub

SpaceExParser.jl

SpaceExParser is a Julia package to read SpaceEx modeling files.

The SpaceEx modeling language (SpaceExParser) is a format for the mathematical description of hybrid dynamical systems. It has been described in The SpaceEx Modeling Language, Scott Cotton, Goran Frehse, Olivier Lebeltel. See also An Introduction to SpaceEx, Goran Frehse, 2010.

A visual model editor is available for download on the SpaceEx website. See the examples in this documentation for screenshots and further details.

The aim of this library is to read SpaceExParser modeling files and transform them into Julia objects, for their inspection and analysis, such as reachability computations.

Features

  • Parse SpaceExParser files into types defined in Julia packages HybridSystems.jl and MathematicalSystems.jl.
  • Can read arbitrary ODEs, eg. non-linear dynamics in the ODE flow for each mode.

Library Outline

diff --git a/dev/lib/methods/index.html b/dev/lib/methods/index.html index 99391ec..c10ec32 100644 --- a/dev/lib/methods/index.html +++ b/dev/lib/methods/index.html @@ -1,7 +1,7 @@ -Methods · SpaceExParser.jl
GitHub

Methods

This section describes systems methods implemented in SpaceExParser.jl.

Input/Output

SpaceExParser.readsxmodel — Function
readsxmodel(file; raw_dict=false, ST=ConstrainedLinearControlContinuousSystem, kwargs...)

Read a SpaceExParser model file.

Input

  • file – the filename of the SpaceExParser 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 mathematical system for each mode

Output

Hybrid system that corresponds to the given SpaceExParser 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).
source
SpaceExParser.linearHS — Function
linearHS(HDict; ST=ConstrainedLinearControlContinuousSystem,
+Methods · SpaceExParser.jl
GitHub
Methods
This section describes systems methods implemented in SpaceExParser.jl.
Input/Output
SpaceExParser.readsxmodel — Function
readsxmodel(file; raw_dict=false, ST=ConstrainedLinearControlContinuousSystem, kwargs...)
Read a SpaceExParser model file.
Input
  • file      – the filename of the SpaceExParser 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 mathematical                system for each mode
Output
Hybrid system that corresponds to the given SpaceExParser 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).
source
SpaceExParser.linearHS — Function
linearHS(HDict; ST=ConstrainedLinearControlContinuousSystem,
          STD=ConstrainedLinearControlDiscreteSystem,
-         kwargs...)
Convert the given hybrid system objects into a concrete system type for each node, and 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.
source
Parsing the SpaceExParser language
SpaceExParser.count_locations_and_transitions — Function
count_locations_and_transitions(root_sxmodel)
Returns the number of locations and transitions for each component.
Input
  • root_sxmodel – the root element of a SpaceExParser 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.
source
SpaceExParser.parse_sxmath — Function
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
+         kwargs...)
Convert the given hybrid system objects into a concrete system type for each node, and 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.
source
Parsing the SpaceExParser language
SpaceExParser.count_locations_and_transitions — Function
count_locations_and_transitions(root_sxmodel)
Returns the number of locations and transitions for each component.
Input
  • root_sxmodel – the root element of a SpaceExParser 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.
source
SpaceExParser.parse_sxmath — Function
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}:
@@ -30,7 +30,7 @@
 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.
source
SpaceExParser.parse_sxmodel! — Function
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.
source
SpaceExParser.add_variable! — Function
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").
source
SpaceExParser.add_transition_label! — Function
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.
source
SpaceExParser.parse_location — Function
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.
source
SpaceExParser.parse_transition — Function
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.
source
Conversion of symbolic expressions into sets
Base.convert — Function
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
+ :(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.
source
SpaceExParser.parse_sxmodel! — Function
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.
source
SpaceExParser.add_variable! — Function
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").
source
SpaceExParser.add_transition_label! — Function
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.
source
SpaceExParser.parse_location — Function
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.
source
SpaceExParser.parse_transition — Function
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.
source
Conversion of symbolic expressions into sets
Base.convert — Function
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)
@@ -48,7 +48,7 @@
 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)
source
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
+HalfSpace{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0)
source
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)
@@ -60,7 +60,7 @@
 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)
source
SymEngine.free_symbols — Function
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
+Hyperplane{Float64, Vector{Float64}}([1.0, 1.0, 0.0, -2.0], 6.0)
source
SymEngine.free_symbols — Function
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
 
@@ -72,7 +72,7 @@
 3-element Vector{SymEngine.Basic}:
  x2
  x1
- x4
source
SpaceExParser.is_halfspace — Function
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
+ x4
source
SpaceExParser.is_halfspace — Function
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
@@ -90,7 +90,7 @@
 false
 
 julia> is_halfspace(:(x1 > 4*x2 - x3))
-true
source
SpaceExParser.is_hyperplane — Function
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
+true
source
SpaceExParser.is_hyperplane — Function
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
@@ -108,7 +108,7 @@
 false
 
 julia> is_hyperplane(:(x1 = 4*x2 - x3))
-true
source
SpaceExParser.is_linearcombination — Function
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
+true
source
SpaceExParser.is_linearcombination — Function
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
@@ -120,4 +120,4 @@
 false
 
 julia> is_linearcombination(:(x1^2 - 4*x2 + x3 + 2))
-false
source

+false
source
diff --git a/dev/lib/types/index.html b/dev/lib/types/index.html index f4adb34..9002288 100644 --- a/dev/lib/types/index.html +++ b/dev/lib/types/index.html @@ -1,2 +1,2 @@ -Types · SpaceExParser.jl
GitHub

Types

This section describes systems types implemented in SpaceExParser.jl.

+Types · SpaceExParser.jl
GitHub

Types

This section describes systems types implemented in SpaceExParser.jl.