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

add definitions for VisB files

parent b35f2d4a
No related branches found
No related tags found
No related merge requests found
MACHINE button MACHINE button
DEFINITIONS "LibraryMeta.def" DEFINITIONS
"LibraryMeta.def";
VISB_JSON_FILE == "button.json"
VARIABLES VARIABLES
button button
INVARIANT INVARIANT
......
...@@ -3,6 +3,7 @@ MACHINE Lift ...@@ -3,6 +3,7 @@ MACHINE Lift
will be added in a refinement (by refining the lift moving operations) or will be added in a refinement (by refining the lift moving operations) or
by a CSP controller */ by a CSP controller */
DEFINITIONS DEFINITIONS
VISB_JSON_FILE == "lift_groups.json";
FLOORS == (groundf .. topf); FLOORS == (groundf .. topf);
all_buttons_pressed == (inside_buttons \/ call_buttons); all_buttons_pressed == (inside_buttons \/ call_buttons);
/* Note: one could make a slightly simpler spec by only keeping a single all_buttons_pressed variable */ /* Note: one could make a slightly simpler spec by only keeping a single all_buttons_pressed variable */
......
...@@ -4,6 +4,7 @@ PROPERTIES ...@@ -4,6 +4,7 @@ PROPERTIES
n : NATURAL & n : NATURAL &
n < 121 n < 121
DEFINITIONS DEFINITIONS
VISB_JSON_FILE == "queens_20.json";
SET_PREF_TIME_OUT == 6000; SET_PREF_TIME_OUT == 6000;
SET_PREF_CLPFD == TRUE; SET_PREF_CLPFD == TRUE;
SET_PREF_MAX_INITIALISATIONS == 121; SET_PREF_MAX_INITIALISATIONS == 121;
......
...@@ -2,6 +2,7 @@ MACHINE MovingParticles3 ...@@ -2,6 +2,7 @@ MACHINE MovingParticles3
// Encoding of an n-body problem in B using the REAL datatype // Encoding of an n-body problem in B using the REAL datatype
INCLUDES MovingParticles PROMOTES Move INCLUDES MovingParticles PROMOTES Move
DEFINITIONS DEFINITIONS
VISB_JSON_FILE == "three_bodies.json";
SCALE == 1.25e11; // 100 % in visualisation SCALE == 1.25e11; // 100 % in visualisation
SCALE100 == (SCALE/100.0); SCALE100 == (SCALE/100.0);
SPEED_MULTIPLIER == 1000000.0; SPEED_MULTIPLIER == 1000000.0;
......
...@@ -2,6 +2,7 @@ MACHINE MovingParticles4 ...@@ -2,6 +2,7 @@ MACHINE MovingParticles4
// Encoding of an n-body problem in B using the REAL datatype // Encoding of an n-body problem in B using the REAL datatype
INCLUDES MovingParticles PROMOTES Move INCLUDES MovingParticles PROMOTES Move
DEFINITIONS DEFINITIONS
VISB_JSON_FILE == "four_bodies.json";
SCALE == 5.0e10; // 100 % in visualisation SCALE == 5.0e10; // 100 % in visualisation
SCALE100 == (SCALE/100.0); SCALE100 == (SCALE/100.0);
SPEED_MULTIPLIER == 1000000.0; SPEED_MULTIPLIER == 1000000.0;
......
...@@ -4,7 +4,8 @@ VARIABLES tl_cars, tl_peds ...@@ -4,7 +4,8 @@ VARIABLES tl_cars, tl_peds
INVARIANT tl_cars : colors & tl_peds : {red, green} & INVARIANT tl_cars : colors & tl_peds : {red, green} &
(tl_peds = red or tl_cars = red) (tl_peds = red or tl_cars = red)
INITIALISATION tl_cars := red; tl_peds := red INITIALISATION
tl_cars := red; tl_peds := red
OPERATIONS OPERATIONS
cars_ry = SELECT tl_cars = red & tl_peds = red THEN tl_cars := redyellow END; cars_ry = SELECT tl_cars = red & tl_peds = red THEN tl_cars := redyellow END;
cars_y = SELECT tl_cars = green & tl_peds = red THEN tl_cars := yellow END; cars_y = SELECT tl_cars = green & tl_peds = red THEN tl_cars := yellow END;
...@@ -12,4 +13,6 @@ cars_g = SELECT tl_cars = redyellow & tl_peds = red THEN tl_cars := green END; ...@@ -12,4 +13,6 @@ cars_g = SELECT tl_cars = redyellow & tl_peds = red THEN tl_cars := green END;
cars_r = SELECT tl_cars = yellow & tl_peds = red THEN tl_cars := red END; cars_r = SELECT tl_cars = yellow & tl_peds = red THEN tl_cars := red END;
peds_r = SELECT tl_peds = green & tl_cars = red THEN tl_peds := red END; peds_r = SELECT tl_peds = green & tl_cars = red THEN tl_peds := red END;
peds_g = SELECT tl_peds = red & tl_cars = red THEN tl_peds := green END peds_g = SELECT tl_peds = red & tl_cars = red THEN tl_peds := green END
DEFINITIONS
VISB_JSON_FILE == "Traffic_light.json"
END END
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment