From 265e3f1041bd751d77a898ea4bd38be3196366f5 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 24 Nov 2020 18:55:23 +0100
Subject: [PATCH] add vector as pair machine
---
Physics/MovingParticles.mch | 2 +-
Physics/MovingParticles3.mch | 4 +--
Physics/MovingParticles4.mch | 6 +++--
Physics/Vectors.mch | 8 ++++--
Physics/Vectors2.mch | 8 ++++--
Physics/VectorsAsPairs2.mch | 50 ++++++++++++++++++++++++++++++++++++
6 files changed, 69 insertions(+), 9 deletions(-)
create mode 100644 Physics/VectorsAsPairs2.mch
diff --git a/Physics/MovingParticles.mch b/Physics/MovingParticles.mch
index f26ff2c..4aa26e0 100644
--- a/Physics/MovingParticles.mch
+++ b/Physics/MovingParticles.mch
@@ -1,6 +1,6 @@
MACHINE MovingParticles
// Encoding of an n-body problem in B using the REAL datatype
-INCLUDES Vectors2
+INCLUDES Vectors2 //VectorsAsPairs2 faster; but VisB file needs to be adapted
DEFINITIONS
"LibraryReals.def"; "SORT.def";
MASS == FLOAT;
diff --git a/Physics/MovingParticles3.mch b/Physics/MovingParticles3.mch
index 451a01c..db43521 100644
--- a/Physics/MovingParticles3.mch
+++ b/Physics/MovingParticles3.mch
@@ -19,8 +19,8 @@ PROPERTIES
/*@label "mass_values" */ mass = [5.97e24, 1.989e30, 1.989e30]
/*@desc "The mass of the 3 objects" */
&
- initial_pos = [ [0.0,0.0] , [0.0,4.5e10], [0.0,-4.5e10] ] &
- initial_speed = [ [0.05e04,0.0], [3.0e04,0.0], [-3.0e04,0.0] ]
+ initial_pos = [ make_vec([0.0,0.0]) , make_vec([0.0,4.5e10]), make_vec([0.0,-4.5e10]) ] &
+ initial_speed = [ make_vec([0.05e04,0.0]), make_vec([3.0e04,0.0]), make_vec([-3.0e04,0.0]) ]
END
diff --git a/Physics/MovingParticles4.mch b/Physics/MovingParticles4.mch
index 188892e..9788678 100644
--- a/Physics/MovingParticles4.mch
+++ b/Physics/MovingParticles4.mch
@@ -18,8 +18,10 @@ PROPERTIES
nobjs = 4 &
mass = [3.0e28, 3.0e28, 3.0e28, 3.0e28]
&
- initial_pos = [ [-3.5e10,0.0e00], [-1.0e10,0.0e00], [1.0e10, 0.0e00], [3.5e10, 0.0e00] ] &
- initial_speed = [ [ 0.0e00,1.4e03], [0.0e00,1.4e03], [0.0e00,-1.4e03], [0.0e00,-1.4e03] ]
+ initial_pos = [ make_vec([-3.5e10,0.0e00]), make_vec([-1.0e10,0.0e00]),
+ make_vec([1.0e10, 0.0e00]), make_vec([3.5e10, 0.0e00]) ] &
+ initial_speed = [ make_vec([ 0.0e00,1.4e03]), make_vec([0.0e00,1.4e03]),
+ make_vec([0.0e00,-1.4e03]), make_vec([0.0e00,-1.4e03]) ]
END
diff --git a/Physics/Vectors.mch b/Physics/Vectors.mch
index 05ff9dd..51e6f08 100644
--- a/Physics/Vectors.mch
+++ b/Physics/Vectors.mch
@@ -14,7 +14,9 @@ ABSTRACT_CONSTANTS
sigma_reals /*@desc "sum of a numbers of a vector" */,
add_firstv,
- sigma_vecs /*@desc "sum of a sequence of vectors" */
+ sigma_vecs /*@desc "sum of a sequence of vectors" */,
+
+ make_vec /*@desc "construct a vector from a sequence" */
PROPERTIES
n:NATURAL1 &
DIM = (1..n) &
@@ -41,6 +43,8 @@ PROPERTIES
times_vec = %(k,v1).(k:REAL & v1:VEC | %i.(i:DIM| k*v1(i))) /*@desc "multiply scalar by a vector" */ &
distance = %(v1,v2).(v1:VEC & v2:VEC | magnitude(delta_vec(v1,v2)))
- /*@desc "Eucledian distance between two vectors" */
+ /*@desc "Eucledian distance between two vectors" */ &
+
+ make_vec = %v.(v:seq(REAL) & size(v)=n | v )
END
\ No newline at end of file
diff --git a/Physics/Vectors2.mch b/Physics/Vectors2.mch
index 825b330..d6057ad 100644
--- a/Physics/Vectors2.mch
+++ b/Physics/Vectors2.mch
@@ -12,7 +12,9 @@ ABSTRACT_CONSTANTS
times_vec /*@desc "multiply scalar by a vector" */,
distance /*@desc "Eucledian distance between two vectors" */,
- sigma_vecs /*@desc "sum of a sequence of vectors" */
+ sigma_vecs /*@desc "sum of a sequence of vectors" */,
+
+ make_vec /*@desc "construct a vector from a sequence" */
PROPERTIES
n:NATURAL1 & n = 2 &
DIM = (1..n) &
@@ -39,6 +41,8 @@ PROPERTIES
times_vec = %(k,v1).(k:REAL & v1:VEC | [k*v1(1),k*v1(2)]) /*@desc "multiply scalar by a vector" */ &
distance = %(v1,v2).(v1:VEC & v2:VEC | magnitude(delta_vec(v1,v2)))
- /*@desc "Eucledian distance between two vectors" */
+ /*@desc "Eucledian distance between two vectors" */ &
+
+ make_vec = %v.(v:seq(REAL) & size(v)=2 | v )
END
\ No newline at end of file
diff --git a/Physics/VectorsAsPairs2.mch b/Physics/VectorsAsPairs2.mch
new file mode 100644
index 0000000..35fc5a6
--- /dev/null
+++ b/Physics/VectorsAsPairs2.mch
@@ -0,0 +1,50 @@
+MACHINE VectorsAsPairs2 // an optimized instance of Vectors for n=2 with a pair representation
+DEFINITIONS
+ "LibraryReals.def";
+ p1(r) == prj1(REAL,REAL)(r);
+ p2(r) == prj2(REAL,REAL)(r)
+ABSTRACT_CONSTANTS
+ n,
+ VEC,
+ add_vec /*@desc "sum of two vectors" */,
+ delta_vec /*@desc "difference of two vectors" */,
+ dot_product /*@desc "dot product of two vectors" */,
+ magnitude /*@desc "Magnitude of a vector" */,
+ unit_vec /*@desc "unit vector of a vector" */,
+ times_vec /*@desc "multiply scalar by a vector" */,
+ distance /*@desc "Eucledian distance between two vectors" */,
+
+ sigma_vecs /*@desc "sum of a sequence of vectors" */,
+
+ make_vec /*@desc "construct a vector from a sequence" */
+PROPERTIES
+ n:NATURAL1 & n = 2 &
+ VEC = (REAL*REAL) &
+
+ sigma_vecs = %v.(v:seq1(VEC) | ( SIGMA(i).(i:dom(v)|p1(v(i))) , SIGMA(i).(i:dom(v)|p2(v(i))) ) )
+ /*@desc "sum of a sequence of vectors" */&
+
+ add_vec = %(v1,v2).(v1:VEC & v2:VEC | ( p1(v1)+p1(v2) , p2(v1)+p2(v2) ))
+ /*@desc "sum of two vectors" */ &
+
+ delta_vec = %(v1,v2).(v1:VEC & v2:VEC | ( p1(v1)-p1(v2) , p2(v1)-p2(v2) ) )
+ /*@desc "difference of two vectors" */ &
+
+ dot_product = %(v1,v2).(v1:VEC & v2:VEC | p1(v1)*p1(v2) + p2(v1)*p2(v2))
+ /*@desc "dot product of two vectors" */ &
+
+ magnitude = %v1.(v1:VEC | RSQRT(p1(v1)**2 + p2(v1)**2)) /*@desc "Magnitude of a vector" */ &
+ // alternative: RSQRT(dot_product(v1,v1)))
+
+ unit_vec = %v1.(v1:VEC | LET m BE m=magnitude(v1) IN
+ ( p1(v1)/m , p2(v1)/m ) END ) /*@desc "unit vector of a vector" */ &
+
+ times_vec = %(k,v1).(k:REAL & v1:VEC | ( k*p1(v1), k*p2(v1) ) ) /*@desc "multiply scalar by a vector" */ &
+
+ distance = %(v1,v2).(v1:VEC & v2:VEC | magnitude(delta_vec(v1,v2)))
+ /*@desc "Eucledian distance between two vectors" */ &
+
+
+ make_vec = %v.(v:seq(REAL) & size(v)=2 | ( v(1) , v(2) ) )
+
+END
\ No newline at end of file
--
GitLab