ToJsonObject formats a PlusCal pc variable in Json syntax. The output

of ToJsonObject is valid input for [ShiViz](https://bestchai.bitbucket.io/shiviz/).

Author: lemmy

Json.tla

@@ -0,0 +1,36 @@
+-------------------------------- MODULE Json --------------------------------
+
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE TLC
+  (*************************************************************************)
+  (* Imports the definitions from the modules, but doesn't export them.    *)
+  (*************************************************************************)
+
+-----------------------------------------------------------------------------
+
+LOCAL ToJsonKeyValue(F, d) == 
+  ToString(ToString(d)) \o ":" \o ToString(F[d])
+
+RECURSIVE ToJson(_,_)
+LOCAL ToJson(F, D) == \* LOCAL just a hint for humans.
+  LET d == CHOOSE d \in D: TRUE
+  IN IF D = DOMAIN F
+     THEN "{" \o ToJsonKeyValue(F, d) \o IF D \ {d} = {}
+                                         THEN "}"
+                                         ELSE ToJson(F, D \ {d})
+     ELSE ", " \o ToJsonKeyValue(F, d) \o IF D \ {d} = {}
+                                          THEN "}" 
+                                          ELSE ToJson(F, D \ {d})
+
+ToJsonObject(F) ==
+  (*************************************************************************)
+  (* This equals a string that is the Json representation of the given     *)
+  (* function F s.t. DOMAIN F \subseteq Nat and Range(F) \subseteq STRING  *)
+  (* with Range(g) == { g[x] : x \in DOMAIN g }.                           *)
+  (*************************************************************************)
+  IF DOMAIN F = {} 
+  THEN "{}"
+  ELSE ToJson(F, DOMAIN F)
+
+
+=============================================================================

JsonTests.tla

@@ -0,0 +1,9 @@
+----------------------------- MODULE JsonTests -----------------------------
+EXTENDS Json, TLC
+
+ASSUME(ToJsonObject(<< >>) = "{}")
+ASSUME(ToJsonObject([ i \in {0,1,3} |-> "a" ]) = "{\"0\":\"a\", \"1\":\"a\", \"3\":\"a\"}")
+ASSUME(ToJsonObject([ i \in {0,1} |-> "a" ]) = "{\"0\":\"a\", \"1\":\"a\"}")
+ASSUME(ToJsonObject([ i \in {1} |-> "a" ]) = "{\"1\":\"a\"}")
+
+=============================================================================