Merge pull request #1 from will62794/animation

Add a new SVG.tla module for producing animations of TLC error traces

modules/SVG.java

@@ -0,0 +1,111 @@
+/*******************************************************************************
+ * Copyright (c) 2019 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   William Schultz - initial API and implementation
+ ******************************************************************************/
+import util.UniqueString;
+import tlc2.value.impl.TupleValue;
+import tlc2.value.impl.StringValue;
+import tlc2.value.impl.RecordValue;
+import tlc2.value.impl.Value;
+
+public final class SVG {
+
+	private SVG() {
+		// no-instantiation!
+	}
+
+	/**
+	 * Converts an SVG element to its string representation.
+	 * 
+	 * In TLA+, an SVG object must be represented as a record with the following format:
+	 * 
+	 * [ name 		|-> <string>
+	 *	 attrs 		|-> <record>
+	 *	 children 	|-> <tuple>
+	 *	 innerText 	|-> <string> ]
+	 */
+	public static Value SVGElemToString(Value elem) throws Exception {
+		if (!(elem instanceof RecordValue)) {
+			throw new Exception(
+					"An SVG element must be a record. Value given is of type: " + elem.getClass().toString());
+		}
+
+		RecordValue frv = (RecordValue) elem;
+
+		// Get 'name'.
+		StringValue nameVal = (StringValue) frv.apply(new StringValue("name"), 0);
+		String name = nameVal.getVal().toString();
+
+		// Get 'attrs'. We convert it to 'RecordValue' type, which we expect should always be possible.
+		Value attrsVal = frv.apply(new StringValue("attrs"), 0);
+		RecordValue attrs = (RecordValue)(attrsVal.toRcd());
+		if(attrs == null){
+			throw new Exception("Was unable to convert element to a record: " + attrsVal.toString());
+		}
+		String attrStr = "";
+		for (UniqueString us : attrs.names) {
+			attrStr += " ";
+			attrStr += us.toString();
+			attrStr += "=";
+			String v = ((StringValue) attrs.apply(new StringValue(us), 0)).getVal().toString();
+			// Quote all SVG attribute values. Technically, attribute values in HTML
+			// don't always need to be quoted, but we use quotes so we can handle all
+			// possible values. We single quote them to play nice with TLC string formatting.
+			attrStr += "'" + v + "'";
+		}
+
+		// Get 'children'. We convert it to a TupleValue, which we expect should
+		// always be possible.
+		Value childrenVal = frv.apply(new StringValue("children"), 0);
+		TupleValue children = (TupleValue)(childrenVal.toTuple());
+		if(children == null){
+			throw new Exception("Was unable to convert element to a tuple: " + childrenVal.toString());
+		}
+		String childStr = "";
+		for (Value child : children.elems) {
+			StringValue cv = (StringValue)SVGElemToString(child);
+			childStr += cv.getVal().toString();
+		}
+
+		// Get 'innerText'.
+		// This is raw text placed inside the current SVG element. For example, if
+		// 'innerText' was "hello", then we would output an SVG element like:
+		//
+		// <elem>hello</elem>
+		//
+		// For SVG elements that are not of type <text>, text inside an element is not
+		// rendered, so this property is only meaningful for <text> elements. It is expected
+		// to be empty for all other element types, but since it's not rendered, we don't 
+		// explicitly disallow it.
+		StringValue innerTextVal = (StringValue) frv.apply(new StringValue("innerText"), 0);
+		String innerText = innerTextVal.getVal().toString();
+
+		// Produce the SVG element string.
+		String svg = String.format("<%s%s>", name, attrStr);
+		svg += innerText;
+		svg += childStr;
+		svg += String.format("</%s>", name);
+		return new StringValue(svg);
+	}
+}

modules/SVG.tla

@@ -0,0 +1,130 @@
+----------------------------- MODULE SVG -----------------------------
+EXTENDS Naturals, Sequences, Integers, TLC, FiniteSets
+
+(******************************************************************************)
+(* Helper Operators                                                           *)
+(******************************************************************************)
+
+LOCAL Merge(r1, r2) == 
+    (**************************************************************************)
+    (* Merge two records.                                                     *)
+    (*                                                                        *)
+    (* If a field appears in both records, then the value from 'r1' is kept.  *)
+    (**************************************************************************)
+    LET D1 == DOMAIN r1 
+        D2 == DOMAIN r2 IN
+    [k \in (D1 \cup D2) |-> IF k \in D1 THEN r1[k] ELSE r2[k]]
+
+LOCAL SVGElem(_name, _attrs, _children, _innerText) == 
+    (**************************************************************************)
+    (* SVG element constructor.                                               *)
+    (*                                                                        *)
+    (* An SVG element like:                                                   *)
+    (*                                                                        *)
+    (* [name |-> "elem", attrs |-> [k1 |-> "0", k2 |-> "1"], children |->     *)
+    (* <<>>, innerText |-> ""]                                                *)
+    (*                                                                        *)
+    (* would represent the SVG element '<elem k1="0" k2="1"></elem>'          *)
+    (**************************************************************************)
+    [name       |-> _name, 
+     attrs      |-> _attrs, 
+     children   |-> _children,
+     innerText  |-> _innerText ]
+
+SVGElemToString(elem) == 
+    (**************************************************************************)
+    (* Convert an SVG element record into its string representation.          *)
+    (*                                                                        *)
+    (* This operator is expected to be replaced by a Java module override.    *)
+    (* We do not implement it in pure TLA+ because doing non-trivial string   *)
+    (* manipulation in TLA+ is tedious.  Also, the performance of             *)
+    (* implementing this in TLA+ has been demonstrated to be prohibitively    *)
+    (* slow.                                                                  *)
+    (**************************************************************************)
+    TRUE
+
+(******************************************************************************)
+(*                                                                            *)
+(* Core Graphic Elements.                                                     *)
+(*                                                                            *)
+(* These primitives are TLA+ wrappers around SVG elements.  We base them on   *)
+(* SVG since it is a widely used format and provides good features for        *)
+(* representing and laying out vector graphics.  Each primitive below should  *)
+(* roughly correspond to a standard SVG element type.  We represent a graphic *)
+(* element as a record with the fields 'name', 'attrs', 'children', and       *)
+(* 'innerText'.  'name' is the name of the SVG element, 'attrs' is a record   *)
+(* mapping SVG attribute names to values, 'children' is a tuple containing    *)
+(* any children elements, and 'innerText' is a string that represents any raw *)
+(* text that is contained directly inside the SVG element.  The 'innerText'   *)
+(* field is only meaningful for text elements.                                *)
+(*                                                                            *)
+(* All elements accept an 'attrs' argument, which must be a function mapping  *)
+(* string keys to string values.  These key-value pairs describe any          *)
+(* additional SVG attributes of the element.  To pass no attributes, just     *)
+(* pass attrs=<<>>.                                                           *)
+(*                                                                            *)
+(******************************************************************************)
+
+Line(x1, y1, x2, y2, attrs) == 
+    (**************************************************************************)
+    (* Line element.  'x1', 'y1', 'x2', and 'y2' should be given as integers. *)
+    (**************************************************************************)
+    LET svgAttrs == [x1 |-> ToString(x1), 
+                     y1 |-> ToString(y1), 
+                     x2 |-> ToString(x2),
+                     y2 |-> ToString(y2)] IN
+    SVGElem("line", Merge(svgAttrs, attrs), <<>>, "")
+
+Circle(cx, cy, r, attrs) == 
+    (**************************************************************************)
+    (* Circle element. 'cx', 'cy', and 'r' should be given as integers.       *)
+    (**************************************************************************)
+    LET svgAttrs == [cx |-> ToString(cx), 
+                     cy |-> ToString(cy), 
+                     r  |-> ToString(r)] IN
+    SVGElem("circle", Merge(svgAttrs, attrs), <<>>, "")
+
+Rect(x, y, w, h, attrs) == 
+    (**************************************************************************)
+    (* Rectangle element.  'x', 'y', 'w', and 'h' should be given as          *)
+    (* integers.                                                              *)
+    (**************************************************************************)
+    LET svgAttrs == [x      |-> ToString(x), 
+                     y      |-> ToString(y), 
+                     width  |-> ToString(w), 
+                     height |-> ToString(h)] IN
+    SVGElem("rect", Merge(svgAttrs, attrs), <<>>, "")
+
+Text(x, y, text, attrs) == 
+    (**************************************************************************)
+    (* Text element.'x' and 'y' should be given as integers, and 'text' given *)
+    (* as a string.                                                           *)
+    (**************************************************************************)
+    LET svgAttrs == [x |-> ToString(x), 
+                     y |-> ToString(y)] IN
+    SVGElem("text", Merge(svgAttrs, attrs), <<>>, text) 
+
+Group(children, attrs) == 
+    (**************************************************************************)
+    (* Group element.  'children' is a sequence of elements that will be      *)
+    (* contained in this group.                                               *)
+    (**************************************************************************)
+    SVGElem("g", attrs, children, "")
+
+SetToSeq(S) == 
+    (**************************************************************************)
+    (* Convert a set to some sequence that contains all the elements of the   *)
+    (* set exactly once, and contains no other elements.                      *)
+    (**************************************************************************)
+    LET Injective(f) == \A x, y \in DOMAIN f : (f[x] = f[y]) => (x = y) IN
+    CHOOSE f \in [1..Cardinality(S) -> S] : Injective(f)
+
+MakeFrame(elem) == 
+    (******************************************************************************)
+    (* Builds a single frame for part of a sequence of animation frames.  This is *)
+    (* an SVG group element that contains identifying information about the       *)
+    (* frame.                                                                     *)
+    (******************************************************************************)
+    SVGElemToString(Group(<<elem>>, [class |-> "tlaframe"]))
+
+=============================================================================

tests/SVGTests.tla

@@ -0,0 +1,123 @@
+------------------------- MODULE SVGTests -------------------------
+EXTENDS SVG, Sequences, Naturals, TLC
+
+\* AssertEq(a, b) is logically equivalent to the expression 'a = b'. If a and b are not equal, 
+\* however, AssertEq(a, b) will print out the values of 'a' and 'b'. If the two values are equal,
+\* nothing will be printed.
+AssertEq(a, b) == 
+    IF a # b THEN
+        /\ PrintT("Assertion failed")
+        /\ PrintT(a)
+        /\ PrintT(b)
+        /\ a = b
+    ELSE a = b
+
+(******************************************************************************)
+(* Test conversion of SVG element records to strings.                         *)
+(*                                                                            *)
+(* We aren't worried about using real SVG element names and attributes here,  *)
+(* since the logic only deals with converting the TLA+ record representing    *)
+(* the element into a string.  The particular names of elements and           *)
+(* attributes aren't important.                                               *)
+(******************************************************************************)
+
+ASSUME(LET 
+        elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<>>, innerText |-> ""] 
+        expected == "<test a='10'></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Test empty 'attrs'.
+ASSUME(LET 
+        elem == [name |-> "test", attrs |-> <<>>, children |-> <<>>, innerText |-> ""] 
+        expected == "<test></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Specifying the 'attrs' value as a function instead of a record should also be allowed.
+ASSUME(LET 
+        elem == [name |-> "test", attrs |-> ("a" :> "10" @@ "b" :> "20"), children |-> <<>>, innerText |-> ""] 
+        expected == "<test a='10' b='20'></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Test an element with 1 child.
+ASSUME(LET 
+        child == [name |-> "child", attrs |-> [c |-> "10"], children |-> <<>>, innerText |-> ""]
+        elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<child>>, innerText |-> ""]
+        expected == "<test a='10'><child c='10'></child></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Specifying the children as a function instead a tuple should also be allowed.
+ASSUME(LET 
+        child == [name |-> "child", attrs |-> [c |-> "10"], children |-> <<>>, innerText |-> ""]
+        elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> (1 :> child), innerText |-> ""]
+        expected == "<test a='10'><child c='10'></child></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Test an element with multiple children.
+ASSUME(LET 
+        child1 == [name |-> "child1", attrs |-> [c1 |-> "10"], children |-> <<>>, innerText |-> ""]
+        child2 == [name |-> "child2", attrs |-> [c2 |-> "10"], children |-> <<>>, innerText |-> ""]
+        elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<child1, child2>>, innerText |-> ""]
+        expected == "<test a='10'><child1 c1='10'></child1><child2 c2='10'></child2></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Test an element with 'innerText'.
+ASSUME(LET 
+        elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<>>, innerText |-> "hello"]
+        expected == "<test a='10'>hello</test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+\* Test an element with both children and 'innerText'.
+\* It is not really meaningful/useful to have both 'children' and 'innerText', but
+\* but we test it anyway since it is allowed.
+ASSUME(LET 
+        child == [name |-> "child", attrs |-> [c |-> "10"], children |-> <<>>, innerText |-> ""]
+        elem == [name |-> "test", attrs |-> [a |-> "10"], children |-> <<child>>, innerText |-> "hello"]
+        expected == "<test a='10'>hello<child c='10'></child></test>" IN
+        AssertEq(SVGElemToString(elem), expected))
+
+(******************************************************************************)
+(* Test production of SVG element objects.                                    *)
+(******************************************************************************)
+
+ASSUME(LET 
+        elem == Line(0, 1, 2, 3, [fill |-> "red"]) 
+        expected == [ name |-> "line", 
+                       attrs |-> [x1 |-> "0", y1 |-> "1", x2 |-> "2", y2 |-> "3", fill |-> "red"], 
+                      children |-> <<>>, 
+                      innerText |-> ""] IN
+        AssertEq(elem, expected))
+
+ASSUME(LET 
+        elem == Circle(5, 5, 10, [fill |-> "red"])
+        expected == [ name |-> "circle", 
+                      attrs |-> [cx |-> "5", cy |-> "5", r |-> "10", fill |-> "red"], 
+                      children |-> <<>>, 
+                      innerText |-> ""] IN
+        AssertEq(elem, expected))
+
+ASSUME(LET 
+        elem == Rect(0, 1, 2, 3, [fill |-> "red"]) 
+        expected == [ name |-> "rect", 
+                       attrs |-> [x |-> "0", y |-> "1", width |-> "2", height |-> "3", fill |-> "red"], 
+                      children |-> <<>>, 
+                      innerText |-> ""] IN
+        AssertEq(elem, expected))
+
+ASSUME(LET 
+        elem == Text(0, 1, "hello", [fill |-> "red"]) 
+        expected == [ name |-> "text", 
+                       attrs |-> [x |-> "0", y |-> "1", fill |-> "red"], 
+                      children |-> <<>>, 
+                      innerText |-> "hello"] IN
+        AssertEq(elem, expected))
+
+ASSUME(LET 
+        child == Rect(0, 1, 2, 3, [fill |-> "red"])
+        elem == Group(<<child>>, [fill |-> "blue"])
+        expected == [ name |-> "g", 
+                       attrs |-> [fill |-> "blue"], 
+                      children |-> <<child>>, 
+                      innerText |-> ""] IN
+        AssertEq(elem, expected))
+
+=============================================================================