Add SVGDoc and SVGSerialize functions for SVG document creation and

serialization.

[Feature]

Signed-off-by: Markus Alexander Kuppe <[email protected]>

Author: lemmy

modules/SVG.tla

@@ -122,6 +122,28 @@ Group(children, attrs) ==
 Svg(children, attrs) == 
     SVGElem("svg", attrs, children, "")
 
+(**************************************************************************)
+(* Creates a complete SVG document with viewBox and additional attributes.*)
+(*                                                                        *)
+(* Parameters:                                                            *)
+(*   children: A sequence of SVG elements to include in the document      *)
+(*   vbX, vbY: The x,y coordinates of the top-left corner of the viewBox  *)
+(*   vbW, vbH: The width and height of the viewBox                        *)
+(*   attrs:    Additional attributes to merge with the SVG root element   *)
+(*                                                                        *)
+(* The viewBox defines the coordinate system and viewport dimensions for  *)
+(* the SVG content. This is essential for proper scaling and positioning  *)
+(* of elements within the document.                                       *)
+(**************************************************************************)
+SVGDoc(children, vbX, vbY, vbW, vbH, attrs) ==
+    LET svgAttrs == ("xmlns:xlink" :> "http://www.w3.org/1999/xlink" @@
+                     "xmlns"       :> "http://www.w3.org/2000/svg" @@
+                     "viewBox" :> ToString(vbX) \o " " \o
+                                  ToString(vbY) \o " " \o
+                                  ToString(vbW) \o " " \o
+                                  ToString(vbH)) IN
+    Svg(<<children>>, Merge(svgAttrs, attrs))
+
 (**************************************************************************)
 (* Convert an SVG element record into its string representation.          *)
 (*                                                                        *)
@@ -132,7 +154,7 @@ Svg(children, attrs) ==
 (* slow.                                                                  *)
 (**************************************************************************)
 SVGElemToString(elem) == 
-    TRUE
+    TRUE    
 
 -------------------------------------------------------------------------------
 
@@ -190,4 +212,33 @@ PointOnLine(from, to, segment) ==
     [x |-> from.x + ((to.x - from.x) \div segment), 
      y |-> from.y + ((to.y - from.y) \div segment)]
 
+-------------------------------------------------------------------------------
+
+(**************************************************************************)
+(* Serializes an SVG element to a file on disk.                           *)
+(*                                                                        *)
+(* Parameters:                                                            *)
+(*   svg:             The SVG element/document to serialize               *)
+(*   frameNamePrefix: String prefix for the output filename               *)
+(*   frameNumber:     Numeric identifier appended to create unique files  *)
+(*                                                                        *)
+(* Creates a file named "<frameNamePrefix><frameNumber>.svg" containing   *)
+(* the serialized SVG content. This is useful for generating animation    *)
+(* frames or saving visualization snapshots.                              *)
+(*                                                                        *)
+(* Example usage:                                                         *)
+(*   SVGSerialize(SVGDoc(myElements, 0, 0, 800, 600, <<>>),               *)
+(*                "svg_frame_", TLCGet("level"))                          *)
+(*                                                                        *)
+(* This creates files like: svg_frame_1.svg,                              *)
+(*                          svg_frame_2.svg, etc.                         *)
+(**************************************************************************)
+SVGSerialize(svg, frameNamePrefix, frameNumber) ==
+    LET IO == INSTANCE IOUtils IN
+    IO!Serialize(
+        SVGElemToString(svg),
+        frameNamePrefix \o ToString(frameNumber) \o ".svg",
+        [format |-> "TXT", charset |-> "UTF-8", 
+         openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>])
+
 =============================================================================

tests/SVGTests.tla

@@ -138,5 +138,62 @@ ASSUME(LET
       IN
         AssertEq(SVGElemToString(elem), "<text x='0' y='0'>&lt;&lt;1, 2, 3&gt;&gt;</text>"))
 
+(******************************************************************************)
+(* Test SVGDoc operator                                                       *)
+(******************************************************************************)
+
+\* Test SVGDoc with basic elements and viewBox
+ASSUME(LET 
+        circle == Circle(50, 50, 20, [fill |-> "blue"])
+        rect == Rect(10, 10, 30, 40, [fill |-> "red"])
+        doc == SVGDoc(<<circle, rect>>, 0, 0, 100, 100, [width |-> "200", height |-> "200"])
+        expected == [ name |-> "svg", 
+                      attrs |-> ("xmlns:xlink" :> "http://www.w3.org/1999/xlink" @@
+                                 "xmlns" :> "http://www.w3.org/2000/svg" @@
+                                 "viewBox" :> "0 0 100 100" @@
+                                 "width" :> "200" @@
+                                 "height" :> "200"), 
+                      children |-> <<<<circle, rect>>>>, 
+                      innerText |-> ""] IN
+        AssertEq(doc, expected))
+
+\* Test SVGDoc with empty children and no additional attributes
+ASSUME(LET 
+        doc == SVGDoc(<<>>, 10, 20, 800, 600, <<>>)
+        expected == [ name |-> "svg", 
+                      attrs |-> ("xmlns:xlink" :> "http://www.w3.org/1999/xlink" @@
+                                 "xmlns" :> "http://www.w3.org/2000/svg" @@
+                                 "viewBox" :> "10 20 800 600"), 
+                      children |-> <<<<>>>>, 
+                      innerText |-> ""] IN
+        AssertEq(doc, expected))
+
+\* Test SVGDoc string conversion
+ASSUME(LET 
+        text == Text(25, 25, "Hello SVG", [fill |-> "green"])
+        doc == SVGDoc(text, 0, 0, 50, 50, [id |-> "test-svg"])
+        expectedString == "<svg id='test-svg' xmlns:xlink='http://www.w3.org/1999/xlink' xmlns='http://www.w3.org/2000/svg' viewBox='0 0 50 50'><text x='25' y='25' fill='green'>Hello SVG</text></svg>" IN
+        AssertEq(SVGElemToString(doc), expectedString))
+
+(******************************************************************************)
+(* Test SVGSerialize operator                                                 *)
+(******************************************************************************)
+
+\* Test SVGSerialize creates a file (we can't directly test file creation in TLA+,
+\* but we can test that the operator doesn't crash and returns the expected result)
+ASSUME(LET 
+        circle == Circle(25, 25, 15, [fill |-> "purple"])
+        doc == SVGDoc(circle, 0, 0, 50, 50, [width |-> "100", height |-> "100"])
+        result == SVGSerialize(doc, "test_frame_", 1) IN
+        \* SVGSerialize should return TRUE if successful (based on IOUtils pattern)
+        result.exitValue = 0)
+
+\* Test SVGSerialize with different frame numbers
+ASSUME(LET 
+        line == Line(0, 0, 50, 50, "stroke" :> "black" @@ "stroke-width" :> "2")
+        doc == SVGDoc(line, 0, 0, 50, 50, <<>>)
+        result == SVGSerialize(doc, "animation_", 42) IN
+        result.exitValue = 0)
+
 
 =============================================================================