diff --git a/specs/AsyncGameOfLife_anim.tla b/specs/AsyncGameOfLife_anim.tla
index 5210280..674db18 100644
--- a/specs/AsyncGameOfLife_anim.tla
+++ b/specs/AsyncGameOfLife_anim.tla
@@ -59,10 +59,8 @@ AnimAlias ==
     [
         grid |-> grid
     ] @@
-    [ _anim |-> Serialize("<svg viewBox='-100 0 " \o ToString(N * CellSize + 300) \o " " \o ToString(N * CellSize + 120) \o "' xmlns='http://www.w3.org/2000/svg'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "AsyncGameOfLife_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(
+                    SVGDoc(AnimView, -100, 0, N * CellSize + 300, N * CellSize + 120, <<>>),
+                    "AsyncGameOfLife_anim_", TLCGet("level")) ]
 
 =============================================================================
diff --git a/specs/BatteryRelay_anim.tla b/specs/BatteryRelay_anim.tla
index 49ec2b4..7c88980 100644
--- a/specs/BatteryRelay_anim.tla
+++ b/specs/BatteryRelay_anim.tla
@@ -55,11 +55,6 @@ AnimAlias ==
         batteryLeft |-> batteryLeft,
         batteryLevel |-> batteryLevel        
     ] @@ 
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 230 200' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "BatteryRelay_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 230, 200, <<>>), "BatteryRelay_anim_", TLCGet("level")) ]
 
 ====
\ No newline at end of file
diff --git a/specs/BlockingQueue_anim.tla b/specs/BlockingQueue_anim.tla
index 796f677..36af64a 100644
--- a/specs/BlockingQueue_anim.tla
+++ b/specs/BlockingQueue_anim.tla
@@ -125,11 +125,6 @@ AnimAlias ==
     [
         buffer |-> buffer, waitSet |-> waitSet
     ] @@
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 560 350' xmlns='http://www.w3.org/2000/svg'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "BlockingQueue_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 560, 350, <<>>), "BlockingQueue_anim_", TLCGet("level")) ]
 
 ====
\ No newline at end of file
diff --git a/specs/CabbageGoatWolf_anim.tla b/specs/CabbageGoatWolf_anim.tla
index bf128b2..711710e 100644
--- a/specs/CabbageGoatWolf_anim.tla
+++ b/specs/CabbageGoatWolf_anim.tla
@@ -51,11 +51,6 @@ AnimAlias ==
     [
         banks |-> banks, boat |-> boat
     ] @@
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 530 420' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "CabbageGoatWolf_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 530, 420, <<>>), "CabbageGoatWolf_anim_", TLCGet("level"))]
 
 ====
diff --git a/specs/DiningPhilosophers_anim.tla b/specs/DiningPhilosophers_anim.tla
index 696d41c..ccca941 100644
--- a/specs/DiningPhilosophers_anim.tla
+++ b/specs/DiningPhilosophers_anim.tla
@@ -40,11 +40,6 @@ AnimAlias ==
     [
         philosophers |-> philosophers, forks |-> forks
     ] @@
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 270 270' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "DiningPhilosophers_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 270, 270, <<>>), "DiningPhilosophers_anim_", TLCGet("level")) ]
 
 ====
\ No newline at end of file
diff --git a/specs/EWD998_anim.tla b/specs/EWD998_anim.tla
index fe98e38..9769310 100644
--- a/specs/EWD998_anim.tla
+++ b/specs/EWD998_anim.tla
@@ -232,11 +232,6 @@ AnimAlias ==
     [
         active |-> active, pending |-> pending, color |-> color, counter |-> counter, token |-> token
     ] @@
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 760 480' xmlns='http://www.w3.org/2000/svg'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "EWD998_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 760, 480, <<>>), "EWD998_anim_", TLCGet("level")) ]
 
 ====
diff --git a/specs/MongoRaftReconfig_anim.tla b/specs/MongoRaftReconfig_anim.tla
index 296d88e..bb8c012 100644
--- a/specs/MongoRaftReconfig_anim.tla
+++ b/specs/MongoRaftReconfig_anim.tla
@@ -107,11 +107,6 @@ AnimAlias ==
     [
         currentTerm |-> currentTerm, state |-> state, log |-> log, immediatelyCommitted |-> immediatelyCommitted, config |-> config, configVersion |-> configVersion, configTerm |-> configTerm
     ] @@
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 720 350' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "MongoRaftReconfig_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 720, 350, <<>>), "MongoRaftReconfig_anim_", TLCGet("level")) ]
 
 =============================================================================
diff --git a/specs/TwoPhase_anim.tla b/specs/TwoPhase_anim.tla
index a6a9ec7..828f84a 100644
--- a/specs/TwoPhase_anim.tla
+++ b/specs/TwoPhase_anim.tla
@@ -45,11 +45,6 @@ AnimAlias ==
     [
         rmState |-> rmState, tmState |-> tmState, tmPrepared |-> tmPrepared, msgs |-> msgs
     ] @@
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 180 200' xmlns='http://www.w3.org/2000/svg'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "TwoPhase_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 180, 200, <<>>), "TwoPhase_anim_", TLCGet("level"))]
 
 =============================================================================
diff --git a/specs/bfs_anim.tla b/specs/bfs_anim.tla
index dcb7493..590c58f 100644
--- a/specs/bfs_anim.tla
+++ b/specs/bfs_anim.tla
@@ -34,12 +34,7 @@ AnimAlias ==
         frontier |-> frontier,
         visited |-> visited,
         startNode |-> startNode
-    ] @@ 
-    LET IO == INSTANCE IOUtils IN
-    [ _anim |-> IO!Serialize("<svg viewBox='0 0 1000 1000' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>" \o 
-                         SVGElemToString(AnimView) \o 
-                         "</svg>", 
-                         "bfs_anim_" \o ToString(TLCGet("level")) \o ".svg",
-                         [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>]) ]
+    ] @@
+    [ _anim |-> SVGSerialize(SVGDoc(AnimView, 0, 0, 1000, 1000, <<>>), "bfs_anim_", TLCGet("level")) ]
 
 ====