diff --git a/Physics/SpringPhysics_prob01_mch.eventb b/Physics/SpringPhysics_prob01_mch.eventb
new file mode 100644
index 0000000000000000000000000000000000000000..b850a8d70f55f89999ec1b7a1e90e2593ee9bf95
--- /dev/null
+++ b/Physics/SpringPhysics_prob01_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,'SpringPhysics_prob01',[sees(none,['SpringConstants']),refines(none,'SpringPhysics'),variables(none,[identifier(none,dist),identifier(none,speed)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos('SpringPhysics_prob01','INITIALISATION',','),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('SpringPhysics_prob01',act1,'\''),[identifier(none,dist)],[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics_prob01',act2,'('),[identifier(none,speed)],[typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))])],[]),event(rodinpos('SpringPhysics_prob01',move_spring,'-'),move_spring,ordinary(none),[move_spring],[identifier(rodinpos('SpringPhysics_prob01',[],'-'),acc),identifier(rodinpos('SpringPhysics_prob01',[],'\''),delta)],[truth(rodinpos('SpringPhysics_prob01','smr(delta,one)','(')),truth(rodinpos('SpringPhysics_prob01','smr(zero,delta)',')')),member(rodinpos('SpringPhysics_prob01',grd1,'+'),identifier(none,delta),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),member(rodinpos('SpringPhysics_prob01',grd2,'.'),identifier(none,acc),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringPhysics_prob01',grd3,'/'),identifier(none,acc),typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,minus,[identifier(none,dist)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,inv,[identifier(none,mass)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))),equal(rodinpos('SpringPhysics_prob01',grd4,'('),identifier(none,delta),typeof(none,extended_expr(none,inv,[typeof(none,extended_expr(none,mult,[identifier(none,four),identifier(none,four)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])))],[],[assign(rodinpos('SpringPhysics_prob01',act1,'*'),[identifier(none,dist)],[typeof(none,extended_expr(none,plus,[identifier(none,dist),typeof(none,extended_expr(none,mult,[identifier(none,speed),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics_prob01',act2,','),[identifier(none,speed)],[typeof(none,extended_expr(none,plus,[identifier(none,speed),typeof(none,extended_expr(none,mult,[identifier(none,acc),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))])],[])])]),event_b_model(none,'SpringPhysics',[sees(none,['SpringConstants']),variables(none,[identifier(none,dist),identifier(none,speed)]),invariant(none,[member(rodinpos('SpringPhysics',inv1,')'),identifier(none,dist),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),member(rodinpos('SpringPhysics',inv2,','),identifier(none,speed),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))]),theorems(none,[]),events(none,[event(rodinpos('SpringPhysics','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('SpringPhysics',act1,'\''),[identifier(none,dist)],[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics',act2,'('),[identifier(none,speed)],[typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))])],[]),event(rodinpos('SpringPhysics',move_spring,'*'),move_spring,ordinary(none),[],[identifier(rodinpos('SpringPhysics',[],'-'),acc),identifier(rodinpos('SpringPhysics',[],'\''),delta)],[truth(rodinpos('SpringPhysics','smr(delta,one)','(')),truth(rodinpos('SpringPhysics','smr(zero,delta)',')')),member(rodinpos('SpringPhysics',grd1,'+'),identifier(none,delta),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),member(rodinpos('SpringPhysics',grd2,'.'),identifier(none,acc),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringPhysics',grd3,'/'),identifier(none,acc),typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,minus,[identifier(none,dist)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,inv,[identifier(none,mass)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])))],[],[assign(rodinpos('SpringPhysics',act1,'*'),[identifier(none,dist)],[typeof(none,extended_expr(none,plus,[identifier(none,dist),typeof(none,extended_expr(none,mult,[identifier(none,speed),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics',act2,','),[identifier(none,speed)],[typeof(none,extended_expr(none,plus,[identifier(none,speed),typeof(none,extended_expr(none,mult,[identifier(none,acc),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))])],[])])])],[event_b_context(none,'SpringConstants',[extends(none,[]),constants(none,[identifier(none,sixteen),identifier(none,four),identifier(none,mass)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('SpringConstants',axm1,'('),identifier(none,mass),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringConstants',axm2,')'),identifier(none,four),typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))),member(rodinpos('SpringConstants',axm3,'+'),identifier(none,four),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringConstants',axm4,','),identifier(none,sixteen),typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,mult,[identifier(none,four),identifier(none,four)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,four),identifier(none,four)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))),member(rodinpos('SpringConstants',axm5,'.'),identifier(none,sixteen),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringConstants',axm6,'/'),identifier(none,mass),typeof(none,extended_expr(none,mult,[identifier(none,sixteen),identifier(none,sixteen)],[]),extended_expr(none,'\20435\',[],[])))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('SpringPhysics_prob01','Well-definedness of Guard',[guard(grd4),event(move_spring)],false),po('SpringPhysics','Well-definedness of Guard',[guard(grd3),event(move_spring)],false),po('SpringPhysics','Well-definedness of action',[action(act1)],false),po('SpringPhysics','Well-definedness of action',[action(act2)],false),theory(theory_name('RealTheory2','Real2'),[],[],[],[],[axiomatic_def_block(real_def,['\20435\'],[opdef(plus,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(zero,[],[]),opdef(minus,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(mult,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(one,[],[]),opdef(inv,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(leq,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(sup,[argument('A',pow_subset(none,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))))],[]),opdef(inf,[argument('A',pow_subset(none,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))))],[]),opdef(smr,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(sub,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(cnt,[argument(f,pow_subset(none,cartesian_product(none,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))))),argument(x,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(gtr,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[])],[forall(none,[identifier(none,x),identifier(none,y)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,y),extended_expr(none,'\20435\',[],[]))]),equal(none,typeof(none,extended_expr(none,plus,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[identifier(none,y),identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),conjunct(none,[member(none,identifier(none,y),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,z),extended_expr(none,'\20435\',[],[]))])]),equal(none,typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,plus,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[identifier(none,x),typeof(none,extended_expr(none,plus,[identifier(none,y),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),equal(none,typeof(none,extended_expr(none,plus,[identifier(none,x),typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),identifier(none,x)))),forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),equal(none,typeof(none,extended_expr(none,plus,[identifier(none,x),typeof(none,extended_expr(none,minus,[identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x),identifier(none,y)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,y),extended_expr(none,'\20435\',[],[]))]),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,y),identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),conjunct(none,[member(none,identifier(none,y),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,z),extended_expr(none,'\20435\',[],[]))])]),equal(none,typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,mult,[identifier(none,y),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),identifier(none,x)))),forall(none,[identifier(none,x)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),not_equal(none,identifier(none,x),typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[])))]),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,inv,[identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))))),not_equal(none,typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))),forall(none,[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),conjunct(none,[member(none,identifier(none,y),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,z),extended_expr(none,'\20435\',[],[]))])]),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,plus,[identifier(none,y),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])))))])],[])],_Error)).
+
diff --git a/Physics/spring_physics.json b/Physics/spring_physics.json
new file mode 100644
index 0000000000000000000000000000000000000000..18a049c76635de21bcddbda24fc7ce08b7890a7e
--- /dev/null
+++ b/Physics/spring_physics.json
@@ -0,0 +1,31 @@
+{
+  "svg": "spring_physics.svg",
+  "comment": "version which uses new svg object creation",
+  "items": [
+	{
+      "id": "body0",
+      "attr": "cx",
+      "value" : "dist * 100.0"
+    },
+    
+    
+	{
+      "id": "speed0",
+      "attr": "x1",
+      "value" : "dist * 100.0"
+    },
+	{
+      "id": "speed0",
+      "attr": "x2",
+      "value" : "(dist+speed*100.0) * 100.0"
+    }
+  ],
+  "events": [
+    {
+      "id": "body0",
+      "event": "move_spring",
+      "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+                 { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+    }
+  ]
+}
diff --git a/Physics/spring_physics.svg b/Physics/spring_physics.svg
new file mode 100644
index 0000000000000000000000000000000000000000..64e764ea21dbd7d00d5e371d70158e6693a1bf68
--- /dev/null
+++ b/Physics/spring_physics.svg
@@ -0,0 +1,44 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+   xmlns="http://www.w3.org/2000/svg"
+   height="100" width="400"
+   viewBox="-140 -15 280 30"
+   >
+   <defs>
+    <marker id="arrowhead" markerWidth="10" markerHeight="7"
+    refX="0" refY="3.5" orient="auto">
+      <polygon points="0 0, 10 3.5, 0 7" />
+    </marker>
+
+    <marker id="startarrow" markerWidth="10" markerHeight="7"
+    refX="10" refY="3.5" orient="auto">
+      <polygon points="10 0, 10 7, 0 3.5" fill="green" />
+    </marker>
+
+    <marker id="endarrow" markerWidth="10" markerHeight="7"
+    refX="0" refY="3.5" orient="auto">
+      <polygon points="0 0, 10 3.5, 0 7"  fill="green" />
+    </marker>
+  </defs>
+
+
+ <circle id="body0" cx="45" cy="0" r="9.5"
+    stroke="black" stroke-width="0.5" fill="wheat" />
+    
+    
+  <line x1="45" y1="0" x2="55" y2="0" stroke="#000" 
+  stroke-width="0.5" marker-end="url(#arrowhead)"
+   id = "speed0"
+   />
+
+  <line x1="0" y1="-10" x2="0" y2="10" stroke="gray" 
+  stroke-width="0.5"
+   />
+
+  <line x1="100" y1="-5" x2="100" y2="5" stroke="gray" 
+  stroke-width="0.5"
+   />
+  <line x1="-100" y1="-5" x2="-100" y2="5" stroke="gray" 
+  stroke-width="0.5"
+   />
+</svg>