From d2892d5f20c9adbcbb8ff156e34478ed4a6bf42f Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Wed, 10 Feb 2021 16:01:12 +0100 Subject: [PATCH] add definitions for VisB files --- Button/button.mch | 4 +++- Lift/Lift.mch | 1 + N-Queens/QueensWithEvents.mch | 1 + Physics/MovingParticles3.mch | 1 + Physics/MovingParticles4.mch | 1 + TrafficLight/TrafficLight.mch | 17 ++++++++++------- 6 files changed, 17 insertions(+), 8 deletions(-) diff --git a/Button/button.mch b/Button/button.mch index eb87188..7afcf13 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 2dd8811..9cf25f1 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 105d57c..406fd42 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 db43521..7a91c51 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 9788678..8b5192e 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 922d3d2..451be31 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 -- GitLab