Skip to content

Commit

Permalink
Merge pull request #97 from JuliaReach/schillic/revise
Browse files Browse the repository at this point in the history
Revise code and fix bug in error code
  • Loading branch information
schillic authored Mar 10, 2024
2 parents 2574931 + 33550f4 commit 3ff2c14
Show file tree
Hide file tree
Showing 6 changed files with 40 additions and 33 deletions.
6 changes: 3 additions & 3 deletions docs/src/index.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# SpaceExParser.jl

`SpaceExParser` is a [Julia](http://julialang.org) package to read SpaceEx modeling files.
`SpaceExParser` is a [Julia](http://julialang.org) package to read SpaceEx model files.

The SpaceEx modeling language (SpaceExParser) is a format for the mathematical description
of hybrid dynamical systems. It has been described in
Expand All @@ -11,12 +11,12 @@ Goran Frehse, 2010.
A visual model editor is available for download on the [SpaceEx website](http://spaceex.imag.fr/download-6).
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
The aim of this library is to read SpaceEx model 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`.
- Parse SpaceEx 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
Expand Down
6 changes: 3 additions & 3 deletions src/SpaceExParser.jl
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,9 @@ Input/Output functions
export readsxmodel
include("io.jl")

#=========================
Parsing SpaceExParser files
==========================#
#====================
Parsing SpaceEx files
=====================#
include("parse.jl")

#================================================
Expand Down
2 changes: 1 addition & 1 deletion src/convert.jl
Original file line number Diff line number Diff line change
Expand Up @@ -341,7 +341,7 @@ function free_symbols(expr::Expr, ::Type{<:HalfSpace})
end

function free_symbols(expr::Expr, ::Type{<:Hyperplane})
# get sides of the inequality
# get sides of the equality
lhs = convert(Basic, expr.args[1])

# treats the 4 in :(2*x1 = 4)
Expand Down
23 changes: 10 additions & 13 deletions src/io.jl
Original file line number Diff line number Diff line change
@@ -1,21 +1,21 @@
"""
readsxmodel(file; raw_dict=false, ST=ConstrainedLinearControlContinuousSystem, kwargs...)
readsxmodel(file; [raw_dict]=false, [ST]=nothing, [kwargs]...)
Read a SpaceExParser model file.
Read a SpaceEx model file.
### Input
- `file` -- the filename of the SpaceExParser file (in XML format)
- `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 mathematical
- `ST` -- (optional, default: `nothing`) assumption for the type of
system for each mode
### Output
Hybrid system that corresponds to the given SpaceExParser model and the given assumptions
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:
Expand Down Expand Up @@ -68,12 +68,10 @@ These comments apply whenever `raw_dict=false`:
each component being a list of expressions, and similarly the reset maps are
the vector of tuples `(assignments, guards)`.
"""
function readsxmodel(file; raw_dict=false,
ST=nothing,
kwargs...)

function readsxmodel(file; raw_dict=false, ST=nothing, kwargs...)
# 1) Open XML and read number of components and locations
# =======================================================

sxmodel = readxml(file)
root_sxmodel = root(sxmodel)

Expand All @@ -87,8 +85,8 @@ function readsxmodel(file; raw_dict=false,
# keep the 1st component
nlocations, ntransitions = nlocations_vector[1], ntransitions_vector[1]

# 2) Parse SpaceExParser model and make the dictionary of Julia expressions
# ==============================================================
# 2) Parse SpaceEx model and create a dictionary of Julia expressions
# ===================================================================

# hybrid automaton with the given number of locations
automaton = GraphAutomaton(nlocations)
Expand Down Expand Up @@ -141,9 +139,8 @@ function readsxmodel(file; raw_dict=false,
for i in eachindex(assignments)
push!(resetmaps, (assignments[i], guards[i]))
end

elseif ST == ConstrainedLinearControlContinuousSystem
# 2) Use a custom system type and symbolic representations
# Use a custom system type and symbolic representations
(modes, resetmaps) = linearHS(HDict; kwargs...)
else
error("the system type $(ST) is not supported")
Expand Down
2 changes: 1 addition & 1 deletion src/parse.jl
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Returns the number of locations and transitions for each component.
### Input
- `root_sxmodel` -- the root element of a SpaceExParser file
- `root_sxmodel` -- the root element of a SpaceEx file
### Output
Expand Down
34 changes: 22 additions & 12 deletions src/symbolic.jl
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ const NUM = Float64 # hard-coded numeric type for the expressions' coefficients
STD=ConstrainedLinearControlDiscreteSystem,
kwargs...)
Convert the given hybrid system objects into a concrete system type for each node,
and Julia expressions into SymEngine symbolic expressions.
Convert the given hybrid-system object into a concrete system type for each mode,
and convert Julia expressions into SymEngine symbolic expressions.
### Input
Expand Down Expand Up @@ -186,25 +186,35 @@ function _get_coeffs(flow, n, m, state_variables, input_variables)
return A, B, c
end

const STR_SET = "is neither a hyperplane nor a half-space, and conversion from this set is not implemented"
const STR_SET = "is neither a hyperplane nor a half-space; conversion from this set is not implemented"
const STR_VAR = "contains a combination of state variables and input variables"

error_msg_set(::Val{:location}, i, l) = error("invariant $i in location $l " * STR_SET)
error_msg_var(::Val{:location}, i, l) = error("invariant $i in location $l " * STR_VAR)
function error_msg_set(::Val{:location}, i, l)
throw(ArgumentError("invariant $i of location $l " * STR_SET))
end

function error_msg_var(::Val{:location}, i, l)
throw(ArgumentError("invariant $i of location $l " * STR_VAR))
end

error_msg_set(::Val{:transition}, g, t) = error("guard $g in transition $t " * STR_SET)
error_msg_var(::Val{:transition}, g, t) = error("guard $g in transition $t " * STR_VAR)
function error_msg_set(::Val{:transition}, g, t)
throw(ArgumentError("guard $g of transition $t " * STR_SET))
end

function error_msg_var(::Val{:transition}, g, t)
throw(ArgumentError("guard $g of transition $t " * STR_VAR))
end

# ref_tuple is used for the error message
function _add_invariants!(X, U, invariants, state_variables, input_variables, ref_tuple)
for (i, invi) in enumerate(invariants)
for invi in invariants
if is_hyperplane(invi)
set_type = Hyperplane{NUM}
elseif is_halfspace(invi)
set_type = HalfSpace{NUM}
else
inv_or_grd, loc_or_trans = ref_tuple
error_msg_set(inv_or_grd, invi, loc_or_trans)
loc_or_trans, id = ref_tuple
error_msg_set(loc_or_trans, invi, id)
end

vars = free_symbols(invi, set_type)
Expand All @@ -218,8 +228,8 @@ function _add_invariants!(X, U, invariants, state_variables, input_variables, re
push!(U, h)
else
# combination of state variables and input variables
loc_or_trans, inv_or_grd = ref_tuple
error_msg_var(loc_or_trans, invi, inv_or_grd)
loc_or_trans, id = ref_tuple
error_msg_var(loc_or_trans, invi, id)
end
end
end

0 comments on commit 3ff2c14

Please sign in to comment.