Merge pull request #102 from JuliaReach/schillic/90_MS

Fix piracies with MathematicalSystems
JuliaReach · Jun 28, 2024 · 4a3635d · 4a3635d
2 parents 18ab15a + df5de70
commit 4a3635d
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 48 deletions.
diff --git a/src/write.jl b/src/write.jl
@@ -1,31 +1,3 @@
-# ==============
-# API extensions
-# ==============
-
-function MathematicalSystems.statedim(H::HybridSystem)
-    ns = [statedim(H, i) for i in 1:nmodes(H)]
-    if !all(==(ns[1]), ns)
-        @warn("the number of state dimensions differs across locations")
-    end
-    return maximum(ns)
-end
-
-function MathematicalSystems.inputdim(H::HybridSystem)
-    ms = [inputdim(H, i) for i in 1:nmodes(H)]
-    if !all(==(ms[1]), ms)
-        @warn("the number of input dimensions differs across locations")
-    end
-    return maximum(ms)
-end
-
-function MathematicalSystems.isconstrained(X::LazySet)
-    return !isuniversal(X)
-end
-
-function MathematicalSystems.isconstrained(v::AbstractVector{<:LazySet})
-    return !all(isuniversal, v)
-end
-
 # ===========
 # Indentation
 # ===========
@@ -153,19 +125,37 @@ function _write_invariant(io, system, dictionary, indentation)
         return  # nothing to write
     end
 
-    _write_indented(io, "<invariant>", indentation)
-    indent!(indentation)
+    wrote_prefix = false
 
     X = stateset(system)
-    if !isnothing(X)
+    if !isnothing(X) && !isuniversal(X)
+        if !wrote_prefix
+            _write_invariant_prefix(io, indentation)
+            wrote_prefix = true
+        end
         _write_state_constraints_specific(io, system, X, dictionary, indentation)
     end
 
     U = inputset(system)
-    if !isnothing(U)
+    if !isnothing(U) && !isuniversal(U)
+        if !wrote_prefix
+            _write_invariant_prefix(io, indentation)
+            wrote_prefix = true
+        end
         _write_input_constraints_specific(io, system, U, dictionary, indentation)
     end
 
+    if wrote_prefix
+        _write_invariant_suffix(io, indentation)
+    end
+end
+
+function _write_invariant_prefix(io, indentation)
+    _write_indented(io, "<invariant>", indentation)
+    return indent!(indentation)
+end
+
+function _write_invariant_suffix(io, indentation)
     dedent!(indentation)
     return write(io, "</invariant>\n")
 end
@@ -176,11 +166,6 @@ function _write_state_constraints_specific(::IO, ::AbstractSystem, X, ::Dict,
                    "not supported and will be ignored")
 end
 
-function _write_state_constraints_specific(::IO, ::AbstractSystem, ::Universe, ::Dict,
-                                           ::Indentation)
-    # nothing to write
-end
-
 function _write_state_constraints_specific(io::IO, ::AbstractSystem, X::AbstractHyperrectangle,
                                            dictionary::Dict, ::Indentation)
     for i in 1:dim(X)
@@ -237,7 +222,7 @@ function _write_state_constraints_specific(io::IO, ::AbstractSystem,
     return write(io, " $operator $b")
 end
 
-function _write_state_constraints_specific(io::IO, system::Dict, X::AbstractVector{<:LazySet},
+function _write_state_constraints_specific(io::IO, system::Dict, X::Intersection,
                                            dictionary::Dict, indentation::Indentation)
     first = true
     for Xi in X
@@ -255,11 +240,6 @@ function _write_input_constraints_specific(::IO, system, U, dictionary, indentat
                    "not supported and will be ignored")
 end
 
-function _write_input_constraints_specific(::IO, system, U::Universe, dictionary,
-                                           indentation)
-    # nothing to write
-end
-
 function _write_input_constraints_specific(io::IO, ::AbstractSystem, U::AbstractHyperrectangle,
                                            dictionary, ::Indentation)
     for i in 1:dim(U)
@@ -404,7 +384,7 @@ end
 
 function _write_guard(io, H, transition, dictionary, indentation)
     G = guard(H, transition)
-    if !isconstrained(G)
+    if isuniversal(G)
         return  # nothing to write
     end
     _write_indented(io, "<guard>", indentation)
@@ -418,7 +398,7 @@ function _write_assignment(io, H, transition, dictionary, indentation)
         return  # nothing to write
     end
 
-    n = statedim(H)
+    n = _statedim(H)
     if asgn isa AbstractMap
         if (asgn isa IdentityMap) || (asgn isa ConstrainedIdentityMap)
             return  # nothing to write
@@ -502,3 +482,11 @@ function _write_assignment(io, H, transition, dictionary, indentation)
     end
     return write(io, "</assignment>\n")
 end
+
+function _statedim(H::HybridSystem)
+    ns = [statedim(H, i) for i in 1:nmodes(H)]
+    if !all(==(ns[1]), ns)
+        @warn("the number of state dimensions differs across locations")
+    end
+    return maximum(ns)
+end
diff --git a/test/Aqua.jl b/test/Aqua.jl
@@ -2,9 +2,7 @@ using SpaceExParser, Test
 import Aqua
 
 @testset "Aqua tests" begin
-    Aqua.test_all(SpaceExParser; ambiguities=false,
-                  # the piracies should be resolved in the future
-                  piracies=(broken=true,))
+    Aqua.test_all(SpaceExParser; ambiguities=false)
 
     # do not warn about ambiguities in dependencies
     Aqua.test_ambiguities(SpaceExParser)