Skip to content
Snippets Groups Projects
Commit 7fbc77d6 authored by Fabian Vu's avatar Fabian Vu
Browse files

Update N Bodies

parent 946157cf
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Physics/MovingParticles_simulation.json 0 → 100644
+ 20
− 0
View file @ 7fbc77d6
{
"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"
}
]
}
Physics/SolarSystem.mch 0 → 100644
+ 49
− 0
View file @ 7fbc77d6
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
Physics/n_bodies.svg
+ 14
− 14
View file @ 7fbc77d6
<?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"
height="1200" width="400"
viewBox="-100 -100 200 1100"
>
......
VisB-Examples.prob2project
+ 90
− 27
View file @ 7fbc77d6
......@@ -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,
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment