diff --git a/Button/button.mch b/Button/button.mch
index eb871880a1e57dac9f6b907623743c5787576318..7afcf136cb62c899afa62ab3f2c635063c99841f 100644
--- a/Button/button.mch
+++ b/Button/button.mch
@@ -1,5 +1,7 @@
 MACHINE button
-DEFINITIONS "LibraryMeta.def"
+DEFINITIONS 
+     "LibraryMeta.def";
+      VISB_JSON_FILE == "button.json"
 VARIABLES
   button
 INVARIANT
diff --git a/Lift/Lift.mch b/Lift/Lift.mch
index 2dd88119b6061d41a524b420dfd448faf2420685..9cf25f1b4ea8deda0178c8823218585ac5f3f561 100644
--- a/Lift/Lift.mch
+++ b/Lift/Lift.mch
@@ -3,6 +3,7 @@ MACHINE Lift
    will be added in a refinement (by refining the lift moving operations) or
    by a CSP controller */
 DEFINITIONS
+  VISB_JSON_FILE == "lift_groups.json";
   FLOORS == (groundf .. topf);
   all_buttons_pressed == (inside_buttons \/ call_buttons);
   /* Note: one could make a slightly simpler spec by only keeping a single all_buttons_pressed variable */
diff --git a/N-Queens/QueensWithEvents.mch b/N-Queens/QueensWithEvents.mch
index 105d57ce48de5c16ef9e3c48c659c18dee0a191e..406fd4260e66e9670f45526a32dc3d891a81c4ae 100644
--- a/N-Queens/QueensWithEvents.mch
+++ b/N-Queens/QueensWithEvents.mch
@@ -4,6 +4,7 @@ PROPERTIES
  n : NATURAL &
  n < 121
 DEFINITIONS
+      VISB_JSON_FILE == "queens_20.json";
       SET_PREF_TIME_OUT == 6000;
       SET_PREF_CLPFD == TRUE;
       SET_PREF_MAX_INITIALISATIONS == 121;
diff --git a/Physics/MovingParticles3.mch b/Physics/MovingParticles3.mch
index db435213ecf10eb55de6638906aafc11c0e0ae7b..7a91c514a7e138dff9236712978704e8fbac004c 100644
--- a/Physics/MovingParticles3.mch
+++ b/Physics/MovingParticles3.mch
@@ -2,6 +2,7 @@ MACHINE MovingParticles3
 // Encoding of an n-body problem in B using the REAL datatype
 INCLUDES MovingParticles PROMOTES Move
 DEFINITIONS
+  VISB_JSON_FILE == "three_bodies.json";
   SCALE == 1.25e11; // 100 % in visualisation
   SCALE100 == (SCALE/100.0);
   SPEED_MULTIPLIER == 1000000.0;
diff --git a/Physics/MovingParticles4.mch b/Physics/MovingParticles4.mch
index 97886781fc396b38e74d1a6377bcad35a1298dbe..8b5192e0a5d5a16c7a3e8ec48f334c66418cd181 100644
--- a/Physics/MovingParticles4.mch
+++ b/Physics/MovingParticles4.mch
@@ -2,6 +2,7 @@ MACHINE MovingParticles4
 // Encoding of an n-body problem in B using the REAL datatype
 INCLUDES MovingParticles PROMOTES Move
 DEFINITIONS
+  VISB_JSON_FILE == "four_bodies.json";
   SCALE == 5.0e10; // 100 % in visualisation
   SCALE100 == (SCALE/100.0);
   SPEED_MULTIPLIER == 1000000.0;
diff --git a/TrafficLight/TrafficLight.mch b/TrafficLight/TrafficLight.mch
index 922d3d224728c50fa116f6d54bc1cc15e7d9ead6..451be3170c27a31aaa04185a11704c2692cb099a 100644
--- a/TrafficLight/TrafficLight.mch
+++ b/TrafficLight/TrafficLight.mch
@@ -4,12 +4,15 @@ VARIABLES tl_cars, tl_peds
 INVARIANT tl_cars : colors & tl_peds : {red, green} &
 	  (tl_peds = red or tl_cars = red)
               
-INITIALISATION  tl_cars := red; tl_peds := red
+INITIALISATION
+   tl_cars := red; tl_peds := red
 OPERATIONS
-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_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;
-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
+	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_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;
+	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
+DEFINITIONS
+  VISB_JSON_FILE == "Traffic_light.json"
 END