diff --git a/Physics/MovingParticles.mch b/Physics/MovingParticles.mch
index f1ccb7cc1041a3fbce737127178d38ed650e15f7..bcb23e6fff1b7612c894a53023d272f4a2b92b4d 100644
--- a/Physics/MovingParticles.mch
+++ b/Physics/MovingParticles.mch
@@ -5,43 +5,41 @@ DEFINITIONS
"LibraryReals.def"; "SORT.def";
MASS == FLOAT;
- OBJ == 1..nobjs;
-
G == 6.67e-11;
- SCALE == 1.25e11; // 100 % in visualisation
- SCALE100 == (SCALE/100.0);
- SPEED_MULTIPLIER == 1000000.0;
- GRAV_MULTIPLIER == 1000000000000.0;
- MAXMASS == 1.989e30;
gravitation == %i.(i:OBJ | sigma_vecs(
SQUASH(
%j.(j:OBJ & j/=i |
times_vec( force_between(i,j,pos(i),pos(j)) / mass(i) ,
unit_vec(delta_vec(pos(j),pos(i)))))
- ) ) ) // acceleration
+ ) ) ) // acceleration due to gravitation
ABSTRACT_CONSTANTS
- force_between /*@desc "gravitational force between two objects" */
+ force_between /*@desc "gravitational force between two objects" */
CONSTANTS
- mass /*@desc "mass of each object OBJ --> MASS" */,
- nobjs
+ mass /*@desc "mass of each object OBJ --> MASS" */,
+ nobjs /*@desc "number of objects/planets" */,
+ OBJ /*@desc "set of objects/planets" */,
+ initial_pos /*@desc "initial position of objects OBJ --> VEC" */,
+ initial_speed /*@desc "initial speed of objects OBJ --> VEC" */
PROPERTIES
+ n = 2 & // two dimensional space
+
nobjs : 1..10 &
+ OBJ = 1..nobjs &
mass : OBJ --> MASS &
force_between = %(a,b,pa,pb).(a:OBJ & b:OBJ & a/=b | (G * mass(a) * mass(b)) / (distance(pa,pb)**2))
-
- & // specific configuration:
- n = 2 & // two dimensional space
- nobjs = 3 &
- mass = [5.97e24, 1.989e30, 1.989e30]
+ &
+
+ initial_pos : OBJ --> VEC &
+ initial_speed : OBJ --> VEC
VARIABLES pos, speed
INVARIANT
pos : OBJ --> VEC &
speed : OBJ --> VEC
INITIALISATION
- pos := [ [0.0,0.0] , [0.0,4.5e10], [0.0,-4.5e10] ] ||
- speed := [ [0.05e04,0.0], [3.0e04,0.0], [-3.0e04,0.0] ]
+ pos := initial_pos ||
+ speed := initial_speed
OPERATIONS
r <-- ForceBetween(a,b) =
PRE a:OBJ & b:OBJ & a/= b & bfalse THEN
diff --git a/Physics/MovingParticles3.mch b/Physics/MovingParticles3.mch
new file mode 100644
index 0000000000000000000000000000000000000000..780722bbac990228ed1f4876c6cc7f9d97c7c11f
--- /dev/null
+++ b/Physics/MovingParticles3.mch
@@ -0,0 +1,32 @@
+MACHINE MovingParticles3
+// Encoding of an n-body problem in B using the REAL datatype
+INCLUDES MovingParticles PROMOTES Move
+DEFINITIONS
+ SCALE == 1.25e11; // 100 % in visualisation
+ SCALE100 == (SCALE/100.0);
+ SPEED_MULTIPLIER == 1000000.0;
+ GRAV_MULTIPLIER == 1000000000000.0;
+ MAXMASS == 1.989e30;
+
+ gravitation == %i.(i:OBJ | sigma_vecs(
+ SQUASH(
+ %j.(j:OBJ & j/=i |
+ times_vec( force_between(i,j,pos(i),pos(j)) / mass(i) ,
+ unit_vec(delta_vec(pos(j),pos(i)))))
+ ) ) ) // acceleration due to gravitation
+PROPERTIES
+ nobjs = 3 &
+ mass = [5.97e24, 1.989e30, 1.989e30]
+ &
+ 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] ]
+
+END
+
+/*
+ 3
+ 1.25e11
+ 0.0e00 0.0e00 0.05e04 0.0e00 5.97e24
+ 0.0e00 4.5e10 3.0e04 0.0e00 1.989e30
+ 0.0e00 -4.5e10 -3.0e04 0.0e00 1.989e30
+*/
\ No newline at end of file
diff --git a/Physics/MovingParticles4.mch b/Physics/MovingParticles4.mch
new file mode 100644
index 0000000000000000000000000000000000000000..188892ecb4fb643ca99399ed9361dd11872c0f41
--- /dev/null
+++ b/Physics/MovingParticles4.mch
@@ -0,0 +1,32 @@
+MACHINE MovingParticles4
+// Encoding of an n-body problem in B using the REAL datatype
+INCLUDES MovingParticles PROMOTES Move
+DEFINITIONS
+ SCALE == 5.0e10; // 100 % in visualisation
+ SCALE100 == (SCALE/100.0);
+ SPEED_MULTIPLIER == 1000000.0;
+ GRAV_MULTIPLIER == 1000000000000.0;
+ MAXMASS == 3.0e28;
+ "SORT.def";
+ gravitation == %i.(i:OBJ | sigma_vecs(
+ SQUASH(
+ %j.(j:OBJ & j/=i |
+ times_vec( force_between(i,j,pos(i),pos(j)) / mass(i) ,
+ unit_vec(delta_vec(pos(j),pos(i)))))
+ ) ) ) // acceleration due to gravitation
+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] ]
+
+END
+
+/*
+4
+ 5.0e10
+-3.5e10 0.0e00 0.0e00 1.4e03 3.0e28
+-1.0e10 0.0e00 0.0e00 1.4e04 3.0e28
+ 1.0e10 0.0e00 0.0e00 -1.4e04 3.0e28
+*/
\ No newline at end of file
diff --git a/Physics/Vectors.mch b/Physics/Vectors.mch
index 843ad50dd783ee3bb93e4c202415dfdf3fa5b71f..25b6f7ec8e832c5bffc55e9de3b9779db61513c3 100644
--- a/Physics/Vectors.mch
+++ b/Physics/Vectors.mch
@@ -12,7 +12,6 @@ ABSTRACT_CONSTANTS
times_vec /*@desc "multiply scalar by a vector" */,
distance /*@desc "Eucledian distance between two vectors" */,
- add_first,
sigma_reals /*@desc "sum of a numbers of a vector" */,
add_firstv,
sigma_vecs /*@desc "sum of a sequence of vectors" */
@@ -21,8 +20,7 @@ PROPERTIES
DIM = (1..n) &
VEC = DIM --> REAL &
- add_first = %v.(v:seq1(REAL) | (v(1)+v(2)) -> tail(tail(v))) & // auxiliary function
- sigma_reals = %v.(v:VEC | (iterate(add_first,n-1)(v))(1)) & // sum the values in a vector
+ sigma_reals = %v.(v:VEC | SIGMA(i).(i:dom(v)|v(i))) & // sum the values in a vector
add_firstv = %v.(v:seq1(VEC) | add_vec(v(1),v(2)) -> tail(tail(v))) & // auxiliary function
sigma_vecs = %v.(v:seq1(VEC) | (iterate(add_firstv,size(v)-1)(v))(1)) & // sum a sequence of vectors
diff --git a/Physics/four_bodies.json b/Physics/four_bodies.json
new file mode 100644
index 0000000000000000000000000000000000000000..561e7ed5a58c0c62cb7c609fd8741a6c6bf9175d
--- /dev/null
+++ b/Physics/four_bodies.json
@@ -0,0 +1,83 @@
+{
+ "svg": "four_bodies.svg",
+ "items": [
+ {
+ "for": {"from":1, "to":4},
+ "id": "body%0",
+ "attr": "cx",
+ "value" : "pos(%0)(1) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "body%0",
+ "attr": "cy",
+ "value" : "pos(%0)(2) / SCALE100"
+ },
+
+ {
+ "for": {"from":1, "to":4},
+ "id": "body%0",
+ "attr": "r",
+ "value" : "2.0+5.0*mass(%0)/MAXMASS"
+ },
+
+ {
+ "for": {"from":1, "to":4},
+ "id": "speed%0",
+ "attr": "x1",
+ "value" : "pos(%0)(1) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "speed%0",
+ "attr": "y1",
+ "value" : "pos(%0)(2) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "speed%0",
+ "attr": "x2",
+ "value" : "(pos(%0)(1)+ SPEED_MULTIPLIER*speed(%0)(1)) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "speed%0",
+ "attr": "y2",
+ "value" : "(pos(%0)(2)+ SPEED_MULTIPLIER*speed(%0)(2)) / SCALE100"
+ },
+
+ {
+ "for": {"from":1, "to":4},
+ "id": "gravitation%0",
+ "attr": "x1",
+ "value" : "pos(%0)(1) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "gravitation%0",
+ "attr": "y1",
+ "value" : "pos(%0)(2) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "gravitation%0",
+ "attr": "x2",
+ "value" : "(pos(%0)(1)+ GRAV_MULTIPLIER*gravitation(%0)(1)) / SCALE100"
+ },
+ {
+ "for": {"from":1, "to":4},
+ "id": "gravitation%0",
+ "attr": "y2",
+ "value" : "(pos(%0)(2)+ GRAV_MULTIPLIER*gravitation(%0)(2)) / SCALE100"
+ }
+ ],
+ "events": [
+ {
+ "for": {"from":1, "to":4},
+ "id": "body%0",
+ "event": "Move",
+ "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
+ { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
+ }
+ ]
+}
diff --git a/Physics/four_bodies.svg b/Physics/four_bodies.svg
new file mode 100644
index 0000000000000000000000000000000000000000..e9d1b1b2da6cd56ec605a0d2feb32c0d22faadb8
--- /dev/null
+++ b/Physics/four_bodies.svg
@@ -0,0 +1,74 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns="http://www.w3.org/2000/svg"
+ height="400" width="400"
+ viewBox="-100 -100 200 200"
+ >
+
+
+ <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="body1" cx="45" cy="15" r="10"
+ stroke="black" stroke-width="0.5" fill="green" />
+
+ <circle id="body2" cx="5" cy="15" r="5"
+ 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="body4" cx="35" cy="25" r="5"
+ stroke="black" stroke-width="0.5" fill="yellow" />
+
+
+ <line x1="45" y1="15" x2="55" y2="15" stroke="#000"
+ 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"
+ />
+ <line x1="35" y1="45" x2="35" y2="55" stroke="#000"
+ stroke-width="0.3" marker-end="url(#arrowhead)"
+ id = "speed4"
+ />
+
+ <line x1="45" y1="15" x2="55" y2="15" stroke="green"
+ stroke-width="0.3" marker-end="url(#endarrow)"
+ id = "gravitation1"
+ />
+ <line x1="5" y1="15" x2="0" y2="0" stroke="green"
+ stroke-width="0.3" marker-end="url(#endarrow)"
+ id = "gravitation2"
+ />
+ <line x1="35" y1="45" x2="35" y2="55" stroke="green"
+ stroke-width="0.3" marker-end="url(#endarrow)"
+ id = "gravitation3"
+ />
+ <line x1="35" y1="45" x2="35" y2="55" stroke="green"
+ stroke-width="0.3" marker-end="url(#endarrow)"
+ id = "gravitation4"
+ />
+
+</svg>
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
new file mode 100644
index 0000000000000000000000000000000000000000..f3b60eab3ca881127d79008571f43b71e857309a
--- /dev/null
+++ b/VisB-Examples.prob2project
@@ -0,0 +1,113 @@
+{
+ "name": "VisB-Examples",
+ "description": "",
+ "machines": [
+ {
+ "name": "button",
+ "description": "",
+ "location": "Button/button.mch",
+ "lastUsedPreferenceName": "default",
+ "ltlFormulas": [],
+ "ltlPatterns": [],
+ "symbolicCheckingFormulas": [
+ {
+ "type": "INVARIANT",
+ "name": "",
+ "description": "Invariant",
+ "code": "",
+ "selected": true
+ },
+ {
+ "type": "SYMBOLIC_MODEL_CHECK",
+ "name": "BMC",
+ "description": "Symbolic model checking",
+ "code": "BMC",
+ "selected": true
+ }
+ ],
+ "symbolicAnimationFormulas": [],
+ "testCases": [],
+ "traces": [],
+ "modelcheckingItems": [],
+ "visBVisualisation": "Button/button.json"
+ },
+ {
+ "name": "QueensWithEvents",
+ "description": "",
+ "location": "N-Queens/QueensWithEvents.mch",
+ "lastUsedPreferenceName": "default",
+ "ltlFormulas": [],
+ "ltlPatterns": [],
+ "symbolicCheckingFormulas": [
+ {
+ "type": "SYMBOLIC_MODEL_CHECK",
+ "name": "BMC",
+ "description": "Symbolic model checking",
+ "code": "BMC",
+ "selected": true
+ },
+ {
+ "type": "INVARIANT",
+ "name": "",
+ "description": "Invariant",
+ "code": "",
+ "selected": true
+ },
+ {
+ "type": "INVARIANT",
+ "name": "SetQueen",
+ "description": "Invariant",
+ "code": "SetQueen",
+ "selected": true
+ }
+ ],
+ "symbolicAnimationFormulas": [],
+ "testCases": [],
+ "traces": [
+ "traces/QueensWithEvents.prob2trace"
+ ],
+ "modelcheckingItems": [],
+ "visBVisualisation": "N-Queens/queens_8.json"
+ },
+ {
+ "name": "Grapher",
+ "description": "",
+ "location": "Reals/Grapher.mch",
+ "lastUsedPreferenceName": "default",
+ "ltlFormulas": [],
+ "ltlPatterns": [],
+ "symbolicCheckingFormulas": [],
+ "symbolicAnimationFormulas": [],
+ "testCases": [],
+ "traces": [],
+ "modelcheckingItems": [],
+ "visBVisualisation": "Reals/Grapher.json"
+ },
+ {
+ "name": "MovingParticles3",
+ "description": "",
+ "location": "Physics/MovingParticles3.mch",
+ "lastUsedPreferenceName": "default",
+ "ltlFormulas": [],
+ "ltlPatterns": [],
+ "symbolicCheckingFormulas": [],
+ "symbolicAnimationFormulas": [],
+ "testCases": [],
+ "traces": [
+ "traces/MovingParticles.prob2trace"
+ ],
+ "modelcheckingItems": [],
+ "visBVisualisation": "Physics/three_bodies.json"
+ }
+ ],
+ "preferences": [],
+ "metadata": {
+ "fileType": "Project",
+ "formatVersion": 9,
+ "savedAt": "2020-11-11T11:29:33.443088Z",
+ "creator": "User",
+ "proB2KernelVersion": "4.0.0-SNAPSHOT",
+ "proBCliVersion": null,
+ "modelName": null
+ }
+}
\ No newline at end of file