diff --git a/Physics/MovingParticles_simulation.json b/Physics/MovingParticles_simulation.json
new file mode 100644
index 0000000000000000000000000000000000000000..0fe55e760b857a4de4420df3d89931e584c23e31
--- /dev/null
+++ b/Physics/MovingParticles_simulation.json
@@ -0,0 +1,20 @@
+{
+ "activations": [
+ {
+ "id": "$setup_constants",
+ "execute": "$setup_constants"
+ },
+ {
+ "id": "$initialise_machine",
+ "execute": "$initialise_machine",
+ "activating": "Move"
+ },
+ {
+ "id": "Move",
+ "execute": "Move",
+ "after": 100,
+ "probabilisticVariables": "uniform",
+ "activating": "Move"
+ }
+ ]
+}
diff --git a/Physics/SolarSystem.mch b/Physics/SolarSystem.mch
new file mode 100644
index 0000000000000000000000000000000000000000..6723e649285b20f1a29064d2d980bc9e4904be88
--- /dev/null
+++ b/Physics/SolarSystem.mch
@@ -0,0 +1,49 @@
+MACHINE SolarSystem
+// Encoding of an n-body problem in B using the REAL datatype
+INCLUDES MovingParticles PROMOTES Move
+DEFINITIONS
+ VISB_JSON_FILE == "three_bodies.json";
+ NOBJS == 9;
+ SCALE == 5.0e11; // 100 % in visualisation
+ SCALE100 == (SCALE/100.0);
+ SPEED_MULTIPLIER == 1000000.0;
+ GRAV_MULTIPLIER == 1000000000000.0;
+ MAXMASS == 1.989e30;
+ "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 = NOBJS &
+ /*@label "mass_values" */ mass = [1.989e30, 3.30e23, 4.87e24, 5.97e24, 0.64e24, 1898.19e24, 568.34e24, 86.81e24, 102.41e24]
+ /*@desc "The mass of the 9 objects" */
+ &
+ initial_pos = [ make_vec([0.0,0.0]) , make_vec([0.0,57.91e9]), make_vec([0.0,108.21e9]),
+ make_vec([0.0,149.6e9]), make_vec([0.0,227.92e9]), make_vec([0.0,778.57e9]),
+ make_vec([0.0,1433.53e9]), make_vec([0.0,2872.46e9]), make_vec([0.0,4495.06e9])] &
+ initial_speed = [ make_vec([0.0,0.0]), make_vec([4.736e04,0.0]), make_vec([3.5e04,0.0]),
+ make_vec([2.98e04,0.0]), make_vec([2.41e04,0.0]), make_vec([1.3e04,0.0]),
+ make_vec([0.97e04,0.0]), make_vec([0.68e04,0.0]), make_vec([0.54e04,0.0]) ]
+
+//orbital_entities[0] = { 0.0,0.0,0.0, 0.0,0.0,0.0, 1.989e30 }; // a star similar to the sun
+//orbital_entities[1] = { 57.909e9,0.0,0.0, 0.0,47.36e3,0.0, 0.33011e24 }; // a planet similar to mercury
+//orbital_entities[2] = { 108.209e9,0.0,0.0, 0.0,35.02e3,0.0, 4.8675e24 }; // a planet similar to venus
+//orbital_entities[3] = { 149.596e9,0.0,0.0, 0.0,29.78e3,0.0, 5.9724e24 }; // a planet similar to earth
+//orbital_entities[4] = { 227.923e9,0.0,0.0, 0.0,24.07e3,0.0, 0.64171e24 }; // a planet similar to mars
+//orbital_entities[5] = { 778.570e9,0.0,0.0, 0.0,13e3,0.0, 1898.19e24 }; // a planet similar to jupiter
+//orbital_entities[6] = { 1433.529e9,0.0,0.0, 0.0,9.68e3,0.0, 568.34e24 }; // a planet similar to saturn
+//orbital_entities[7] = { 2872.463e9,0.0,0.0, 0.0,6.80e3,0.0, 86.813e24 }; // a planet similar to uranus
+//orbital_entities[8] = { 4495.060e9,0.0,0.0, 0.0,5.43e3,0.0, 102.413e24 }; // a planet similar to neptune
+
+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/n_bodies.svg b/Physics/n_bodies.svg
index 1f4f045b8e99df2f0fb5e01424c308f188120f8d..462cd666f0f1c55f8c093d307b556f8b675c1593 100644
--- a/Physics/n_bodies.svg
+++ b/Physics/n_bodies.svg
@@ -1,29 +1,29 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<svg
+<svg
xmlns="http://www.w3.org/2000/svg"
- height="400" width="400"
- viewBox="-100 -100 200 200"
+ height="1200" width="400"
+ viewBox="-100 -100 200 1100"
>
-
-
+
+
<defs>
- <marker id="arrowhead" markerWidth="10" markerHeight="7"
+ <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"
+
+ <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"
+
+ <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>
-
-
-
-</svg>
+
+
+
+</svg>
diff --git a/VisB-Examples.prob2project b/VisB-Examples.prob2project
index f10a67c0ec2a282ace46406c7964767b8381f6c3..51b36dd756febdb22ab8137df7ff5fcde289e0a6 100644
--- a/VisB-Examples.prob2project
+++ b/VisB-Examples.prob2project
@@ -7,7 +7,8 @@
"description": "",
"location": "Button/button.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [
@@ -36,7 +37,8 @@
"description": "",
"location": "N-Queens/QueensWithEvents.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [
@@ -72,7 +74,8 @@
"description": "",
"location": "Reals/Grapher.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -90,7 +93,8 @@
"description": "",
"location": "Physics/MovingParticles3.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -111,7 +115,8 @@
"description": "",
"location": "Physics/MovingParticles4.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -121,7 +126,7 @@
"traces": [],
"modelcheckingItems": [],
"simulation": null,
- "visBVisualisation": "Physics/four_bodies.json",
+ "visBVisualisation": "Physics/n_bodies_visb.json",
"historyChartItems": []
},
{
@@ -129,7 +134,8 @@
"description": "",
"location": "Waterboiler/WasserkocherEinfach_mch.eventb",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -160,7 +166,8 @@
"description": "",
"location": "Waterboiler/WasserKocherFalsch1_mch.eventb",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -178,7 +185,8 @@
"description": "",
"location": "Waterboiler/WasserkocherFalsch2_mch.eventb",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -196,7 +204,8 @@
"description": "",
"location": "Bridge/m0_island_bridge_3cars_mch.eventb",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -214,7 +223,8 @@
"description": "",
"location": "Bridge/m1_bridge_mch.eventb",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -232,7 +242,8 @@
"description": "",
"location": "Lift/Lift.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -250,7 +261,8 @@
"description": "",
"location": "Train/SimpleTrainTrack.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -270,7 +282,8 @@
"description": "",
"location": "TrafficLight/TrafficLight.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -288,7 +301,8 @@
"description": "",
"location": "Button/Z/button.tex",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -306,7 +320,8 @@
"description": "",
"location": "Button/TLA/button.tla",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -324,7 +339,8 @@
"description": "",
"location": "Einstein/einsteins_puzzle.als",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -348,7 +364,8 @@
"description": "",
"location": "Einstein/Einstein.tla",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [
@@ -372,7 +389,8 @@
"description": "",
"location": "Einstein/einsteins_enum.als",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -390,7 +408,8 @@
"description": "",
"location": "Train/TwoTrains.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -410,7 +429,8 @@
"description": "",
"location": "Train/TwoTrainsB.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -442,7 +462,8 @@
"description": "",
"location": "Train/TwoTrainsMA.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -488,7 +509,8 @@
"description": "",
"location": "Train/TwoTrainsMA_Unicode.mch",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -508,7 +530,8 @@
"description": "",
"location": "LandingGear/model/R6GearsDoorsHandleValvesControllerSwitch.bum",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -526,7 +549,8 @@
"description": "",
"location": "HD/m913.bum",
"lastUsedPreferenceName": "default",
- "requirements": [],
+ "validationTasks": [],
+ "validationObligations": [],
"ltlFormulas": [],
"ltlPatterns": [],
"symbolicCheckingFormulas": [],
@@ -541,13 +565,52 @@
"simulation": null,
"visBVisualisation": "HD/hd.json",
"historyChartItems": []
+ },
+ {
+ "name": "button2",
+ "description": "",
+ "location": "Button/button2.mch",
+ "lastUsedPreferenceName": "default",
+ "validationTasks": [],
+ "validationObligations": [],
+ "ltlFormulas": [],
+ "ltlPatterns": [],
+ "symbolicCheckingFormulas": [],
+ "symbolicAnimationFormulas": [],
+ "simulationItems": [],
+ "testCases": [],
+ "traces": [],
+ "modelcheckingItems": [],
+ "simulation": null,
+ "visBVisualisation": "Button/button2.json",
+ "historyChartItems": []
+ },
+ {
+ "name": "SolarSystem",
+ "description": "",
+ "location": "Physics/SolarSystem.mch",
+ "lastUsedPreferenceName": "default",
+ "validationTasks": [],
+ "validationObligations": [],
+ "ltlFormulas": [],
+ "ltlPatterns": [],
+ "symbolicCheckingFormulas": [],
+ "symbolicAnimationFormulas": [],
+ "simulationItems": [],
+ "testCases": [],
+ "traces": [],
+ "modelcheckingItems": [],
+ "simulation": "Physics/MovingParticles_simulation.json",
+ "visBVisualisation": null,
+ "historyChartItems": []
}
],
+ "requirements": [],
"preferences": [],
"metadata": {
"fileType": "Project",
- "formatVersion": 20,
- "savedAt": "2022-01-31T10:28:13.452413Z",
+ "formatVersion": 23,
+ "savedAt": "2022-04-14T12:01:28.278060Z",
"creator": "User",
"proB2KernelVersion": "4.0.0-SNAPSHOT",
"proBCliVersion": null,