From e216cc1ca111fec80cc413cab2af96541cad2857 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 25 Oct 2025 07:56:25 -0700 Subject: [PATCH] Add SVGDoc and SVGSerialize functions for SVG document creation and serialization. [Feature] Signed-off-by: Markus Alexander Kuppe --- modules/SVG.tla | 53 +++++++++++++++++++++++++++++++++++++++++- tests/SVGTests.tla | 57 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 109 insertions(+), 1 deletion(-) diff --git a/modules/SVG.tla b/modules/SVG.tla index 29b390f..a746ec4 100644 --- a/modules/SVG.tla +++ b/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(<>, 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 ".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">>]) + ============================================================================= diff --git a/tests/SVGTests.tla b/tests/SVGTests.tla index 9859c5d..1384acb 100644 --- a/tests/SVGTests.tla +++ b/tests/SVGTests.tla @@ -138,5 +138,62 @@ ASSUME(LET IN AssertEq(SVGElemToString(elem), "<<1, 2, 3>>")) +(******************************************************************************) +(* 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(<>, 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 |-> <<<>>>, + 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 == "Hello 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) + =============================================================================