Skip to content
Snippets Groups Projects
Commit 20136c1c authored by Michael Leuschel's avatar Michael Leuschel
Browse files

improve physics example

parent 13de262b
No related branches found
No related tags found
No related merge requests found
MACHINE MovingParticles MACHINE MovingParticles
INCLUDES Vectors
DEFINITIONS DEFINITIONS
"LibraryReals.def";
MASS == FLOAT; MASS == FLOAT;
POS == FLOAT; POS == FLOAT;
SPEED == FLOAT; SPEED == FLOAT;
OBJ == 1..n OBJ == 1..nobjs;
ABSTRACT_CONSTANTS sum_vec G == 6.67e-11;
CONSTANTS mass, n SCALE == 1.25e11; // 100 % in visualisation
SCALE100 == (SCALE/100.0);
SPEED_MULTIPLIER == 1000000.0;
MAXMASS == 1.989e30
CONSTANTS mass, nobjs
PROPERTIES PROPERTIES
n : 1..10 & nobjs : 1..10 &
mass : OBJ --> MASS & mass : OBJ --> MASS &
sum_vec = %(v1,v2).(v1:OBJ-->REAL & v2:OBJ-->REAL | %i.(i:OBJ| v1(i)+v2(i))) n = 2 & // two dimensional space
nobjs = 3 & mass = [5.97e24, 1.989e30, 1.989e30]
& n = 3 & mass = [1.0, 100.0, 2.0] VARIABLES pos, speed
VARIABLES xpos, ypos, xspeed, yspeed
INVARIANT INVARIANT
xpos : OBJ --> POS & pos : OBJ --> VEC &
ypos : OBJ --> POS & speed : OBJ --> VEC
xspeed : OBJ --> SPEED & INITIALISATION pos := [ [0.0,0.0] , [0.0,4.5e10] , [0.0,-4.5e10 ] ] ||
yspeed : OBJ --> SPEED speed := [ [0.05e04,0.0], [3.0e04,0.0], [-3.0e04,0.0] ]
INITIALISATION xpos := [ -1.0, 0.0 , 1.0 ] ||
ypos := [ 0.0, 0.0, 0.0 ] ||
xspeed := [ 0.0, 0.0, 0.0 ] ||
yspeed := [ 1.0, 0.0, -1.0 ]
OPERATIONS OPERATIONS
Move = BEGIN r <-- ForceBetween(a,b) = PRE a:OBJ & b:OBJ & a/= b THEN
xpos := sum_vec(xpos,xspeed) || r := (G * mass(a) * mass(b)) / (distance(pos(a),pos(b))**2)
ypos := sum_vec(ypos,yspeed) END;
Move(delta) = PRE delta:REAL & delta = 100000.0 THEN
pos := %i.(i:OBJ | add_vec(pos(i),times_vec(delta,speed(i))) )
END END
END END
MACHINE Vectors
DEFINITIONS
"LibraryReals.def"
ABSTRACT_CONSTANTS
n,
VEC, DIM,
add_vec,
delta_vec,
dot_product,
magnitude,
unit_vec,
times_vec,
distance,
add_first,
sigma_reals
PROPERTIES
n:NATURAL1 &
DIM = (1..n) &
VEC = DIM --> REAL &
add_first = %v.(v:seq1(REAL) | (v(1)+v(2)) -> tail(tail(v))) &
sigma_reals = %v.(v:VEC | (iterate(add_first,n-1)(v))(1)) &
add_vec = %(v1,v2).(v1:VEC & v2:VEC | %i.(i:DIM| v1(i)+v2(i))) &
delta_vec = %(v1,v2).(v1:VEC & v2:VEC | %i.(i:DIM| v1(i)-v2(i))) &
// dot_product = %(v1,v2).(v1:VEC & v2:VEC | SIGMA(i).(i:DIM| v1(i)*v2(i))) &
dot_product = %(v1,v2).(v1:VEC & v2:VEC | sigma_reals(%i.(i:DIM| v1(i)*v2(i)))) &
magnitude = %v1.(v1:VEC | RSQRT(dot_product(v1,v1))) &
unit_vec = %v1.(v1:VEC | LET m BE m=magnitude(v1) IN
%i.(i:DIM| v1(i)/m) END ) &
times_vec = %(k,v1).(k:REAL & v1:VEC | %i.(i:DIM| k*v1(i))) &
distance = %(v1,v2).(v1:VEC & v2:VEC | magnitude(delta_vec(v1,v2)))
END
\ No newline at end of file
...@@ -5,19 +5,45 @@ ...@@ -5,19 +5,45 @@
"for": {"from":1, "to":3}, "for": {"from":1, "to":3},
"id": "body%0", "id": "body%0",
"attr": "cx", "attr": "cx",
"value" : "10.0*xpos(%0)" "value" : "pos(%0)(1) / SCALE100"
}, },
{ {
"for": {"from":1, "to":3}, "for": {"from":1, "to":3},
"id": "body%0", "id": "body%0",
"attr": "cy", "attr": "cy",
"value" : "10.0*ypos(%0)" "value" : "pos(%0)(2) / SCALE100"
}, },
{ {
"for": {"from":1, "to":3}, "for": {"from":1, "to":3},
"id": "body%0", "id": "body%0",
"attr": "r", "attr": "r",
"value" : "2.0+mass(%0)/10.0" "value" : "2.0+5.0*mass(%0)/MAXMASS"
},
{
"for": {"from":1, "to":3},
"id": "speed%0",
"attr": "x1",
"value" : "pos(%0)(1) / SCALE100"
},
{
"for": {"from":1, "to":3},
"id": "speed%0",
"attr": "y1",
"value" : "pos(%0)(2) / SCALE100"
},
{
"for": {"from":1, "to":3},
"id": "speed%0",
"attr": "x2",
"value" : "(pos(%0)(1)+ SPEED_MULTIPLIER*speed(%0)(1)) / SCALE100"
},
{
"for": {"from":1, "to":3},
"id": "speed%0",
"attr": "y2",
"value" : "(pos(%0)(2)+ SPEED_MULTIPLIER*speed(%0)(2)) / SCALE100"
} }
], ],
"events": [ "events": [
......
...@@ -5,13 +5,46 @@ ...@@ -5,13 +5,46 @@
viewBox="-100 -100 200 200" viewBox="-100 -100 200 200"
> >
<circle id="body1" cx="45" cy="15" r="25"
stroke="black" stroke-width="1" fill="green" /> <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="blue" />
</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="blue" />
</marker>
</defs>
<circle id="body1" cx="45" cy="15" r="10"
stroke="black" stroke-width="0.5" fill="green" />
<circle id="body2" cx="5" cy="15" r="5" <circle id="body2" cx="5" cy="15" r="5"
stroke="black" stroke-width="1" fill="red" /> stroke="black" stroke-width="0.5" fill="red" />
<circle id="body3" cx="35" cy="45" r="5"
stroke="black" stroke-width="0.5" fill="blue" />
<circle id="body3" cx="35" cy="45" r="20" <line x1="45" y1="15" x2="55" y2="15" stroke="#000"
stroke="black" stroke-width="1" fill="blue" /> stroke-width="0.3" marker-end="url(#arrowhead)"
id = "speed1"
/>
<line x1="5" y1="15" x2="0" y2="0" stroke="#000"
stroke-width="0.3" marker-end="url(#arrowhead)"
id = "speed2"
/>
<line x1="35" y1="45" x2="35" y2="55" stroke="#000"
stroke-width="0.3" marker-end="url(#arrowhead)"
id = "speed3"
/>
</svg> </svg>
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment