diff --git a/env/env_base.py b/env/env_base.py
index 038d59a6815566325a0c7716923d9425090897af..b006b9b118a6c2898a21e4ef9c3b394c95796aa0 100644
--- a/env/env_base.py
+++ b/env/env_base.py
@@ -1,4 +1,4 @@
-from model_checker import Parser
+from verifier import Parser
 
 
 class GymCompliantEnvBase:
diff --git a/env/simple_intersection/simple_intersection_env.py b/env/simple_intersection/simple_intersection_env.py
index 58ef9a3a5b9d7a36e9ca75f12d81f9ce7b238fa2..f310fc0490801afc256097ea6b168b0ec5f0788a 100644
--- a/env/simple_intersection/simple_intersection_env.py
+++ b/env/simple_intersection/simple_intersection_env.py
@@ -10,7 +10,7 @@ from .utilities import BoundingBox as bb_utils
 from .features import Features
 from .constants import *
 
-from model_checker.simple_intersection import LTLProperty
+from verifier.simple_intersection import LTLProperty
 
 # import the classes for graphical output.
 from .shapes import Text, Image
diff --git a/env/simple_intersection/vehicles.py b/env/simple_intersection/vehicles.py
index e1aae4f1ebd6023a959fb1728058a6c12a2ff161..a614b0a5d0f2202b3d318b593418b55f10e5d38d 100644
--- a/env/simple_intersection/vehicles.py
+++ b/env/simple_intersection/vehicles.py
@@ -1,6 +1,6 @@
 from . import road_geokinemetry as rd
 import numpy as np
-from model_checker.simple_intersection import AtomicPropositions
+from verifier.simple_intersection import AtomicPropositions
 from .utilities import BoundingBox as bb_utils
 from .constants import *
 
diff --git a/options/simple_intersection/maneuvers.py b/options/simple_intersection/maneuvers.py
index 2cf2e7f1c85a07fbe204e2f929555dec75a3e1a2..2902949f12657e222144fde055db290ce800f88c 100644
--- a/options/simple_intersection/maneuvers.py
+++ b/options/simple_intersection/maneuvers.py
@@ -2,12 +2,19 @@ from .maneuver_base import ManeuverBase
 from env.simple_intersection.constants import *
 import env.simple_intersection.road_geokinemetry as rd
 from env.simple_intersection.features import extract_ego_features, extract_other_veh_features
-from model_checker.simple_intersection import LTLProperty
+from verifier.simple_intersection import LTLProperty
 
 import numpy as np
 
 # TODO: separate out into different files?? is it really needed?
 
+"""
+enable_additional_properties=
+    True means the maneuver uses the additional properties,
+    False means not.
+"""
+enable_additional_properties = False
+
 
 class KeepLane(ManeuverBase):
     def _init_param(self):
@@ -35,7 +42,8 @@ class KeepLane(ManeuverBase):
         # the goal reward and termination is led by the SimpleIntersectionEnv
         self.env._terminate_in_goal = False
         self.env._reward_in_goal = None
-        self._enable_low_level_training_properties = True
+        global enable_additional_properties
+        self._enable_low_level_training_properties = enable_additional_properties
         self._extra_action_weights_flag = True
 
     def generate_validation_scenario(self):
@@ -45,8 +53,9 @@ class KeepLane(ManeuverBase):
             ego_perturb_lim=(rd.hlanes.width / 4, np.pi / 6),
             ego_heading_towards_lane_centre=True)
         # the goal reward and termination is led by the SimpleIntersectionEnv
-        self.env._terminate_in_goal = False
-        self.env._reward_in_goal = None
+        self.env._terminate_in_goal = True
+        self.env._reward_in_goal = 200
+        self._enable_low_level_training_properties = False
 
     @staticmethod
     def _features_dim_reduction(features_tuple):
@@ -91,7 +100,8 @@ class Halt(ManeuverBase):
         self._target_lane = self.env.ego.APs['lane']
 
     def _init_LTL_preconditions(self):
-
+        # TODO: give another variable in ManeuverBase that enables high-level-only properties
+        # (currently, this functionality is implemented by "not self._enable_low_level_training_properties")
         self._LTL_preconditions.append(
             LTLProperty(
                 "G ( (veh_ahead and before_but_close_to_stop_region) U highest_priority )",
@@ -114,11 +124,14 @@ class Halt(ManeuverBase):
         self.env._terminate_in_goal = False
         self.env._reward_in_goal = None
         self._reward_in_goal = 200
-        self._enable_low_level_training_properties = True
+        global enable_additional_properties
+        self._enable_low_level_training_properties = enable_additional_properties
         self._extra_action_weights_flag = True
 
     def generate_validation_scenario(self):
         self._ego_pos_range = (rd.hlanes.start_pos, rd.hlanes.end_pos)
+        # TODO: Separate out the high-level-only properties and add a code
+        # "self._enable_low_level_training_properties = False" (just like the other maneuvers).
         self.generate_learning_scenario()
 
     def _low_level_manual_policy(self):
@@ -201,7 +214,8 @@ class Stop(ManeuverBase):
             ego_heading_towards_lane_centre=True)
         self._reward_in_goal = 200
         self._penalty_in_violation = 150
-        self._enable_low_level_training_properties = True
+        global enable_additional_properties
+        self._enable_low_level_training_properties = enable_additional_properties
         self._extra_action_weights_flag = True
 
     def _low_level_manual_policy(self):
@@ -302,7 +316,8 @@ class Wait(ManeuverBase):
         self.env.init_APs(False)
         self.env._terminate_in_goal = False
         self._reward_in_goal = 200
-        self._enable_low_level_training_properties = True
+        global enable_additional_properties
+        self._enable_low_level_training_properties = enable_additional_properties
         self._extra_action_weights_flag = False
 
     @property
@@ -452,20 +467,21 @@ class ChangeLane(ManeuverBase):
         # print('our range was %s, %s, ego at %s' % (before_intersection, after_intersection, self.env.ego.x))
         self._reward_in_goal = 200
         self._violation_penalty_in_low_level_training = 150
-        self._enable_low_level_training_properties = True
+        global enable_additional_properties
+        self._enable_low_level_training_properties = enable_additional_properties
         self._extra_action_weights_flag = True
         self.env._terminate_in_goal = False
 
     def generate_validation_scenario(self):
         self.generate_scenario(
             enable_LTL_preconditions=False,
-            ego_pos_range=(rd.hlanes.start_pos, rd.hlanes.end_pos),
+            ego_pos_range=(rd.intersection_width_w_offset, rd.hlanes.end_pos),
             ego_perturb_lim=(rd.hlanes.width / 4, np.pi / 6))
 
         # print('our range was %s, %s, ego at %s' % (before_intersection, after_intersection, self.env.ego.x))
         self._reward_in_goal = 200
         self._violation_penalty_in_low_level_training = 150
-        self._enable_low_level_training_properties = True
+        self._enable_low_level_training_properties = False
         self.env._terminate_in_goal = False
 
 
@@ -516,7 +532,8 @@ class Follow(ManeuverBase):
         self.env._terminate_in_goal = False
         self._penalty_for_out_of_range = 200
         self._penalty_for_change_lane = 200
-        self._enable_low_level_training_properties = True
+        global enable_additional_properties
+        self._enable_low_level_training_properties = enable_additional_properties
         self._extra_action_weights_flag = True
 
     def _init_param(self):
diff --git a/options/simple_intersection/mcts_maneuvers.py b/options/simple_intersection/mcts_maneuvers.py
index 60c7876d8faf53d81e6e2e83b4d65fd820171bee..60dc20b2382bbb830a203d809cc5a7479b8ff087 100644
--- a/options/simple_intersection/mcts_maneuvers.py
+++ b/options/simple_intersection/mcts_maneuvers.py
@@ -2,7 +2,7 @@ from .maneuver_base import ManeuverBase
 from env.simple_intersection.constants import *
 import env.simple_intersection.road_geokinemetry as rd
 from env.simple_intersection.features import extract_ego_features, extract_other_veh_features
-from model_checker.simple_intersection import LTLProperty
+from verifier.simple_intersection import LTLProperty
 
 import numpy as np
 
diff --git a/model_checker/LTL_property_base.py b/verifier/LTL_property_base.py
similarity index 96%
rename from model_checker/LTL_property_base.py
rename to verifier/LTL_property_base.py
index 4d5a9d8536e5e94934d61a2c2dc925c0b8d76c78..8eae284ef6c80d09d6d7f3e35fda2f48bb0b524b 100644
--- a/model_checker/LTL_property_base.py
+++ b/verifier/LTL_property_base.py
@@ -1,5 +1,5 @@
-from model_checker.scanner import Scanner
-from model_checker.parser import Parser, Errors
+from verifier.scanner import Scanner
+from verifier.parser import Parser, Errors
 
 
 class LTLPropertyBase(object):
diff --git a/model_checker/__init__.py b/verifier/__init__.py
similarity index 100%
rename from model_checker/__init__.py
rename to verifier/__init__.py
diff --git a/model_checker/atomic_propositions_base.py b/verifier/atomic_propositions_base.py
similarity index 100%
rename from model_checker/atomic_propositions_base.py
rename to verifier/atomic_propositions_base.py
diff --git a/model_checker/parser.py b/verifier/parser.py
similarity index 99%
rename from model_checker/parser.py
rename to verifier/parser.py
index 8a6dc99811f4bff954db833002446e2be4822919..06702cecd2c302ae70c1f43fa105c215f4055ebb 100644
--- a/model_checker/parser.py
+++ b/verifier/parser.py
@@ -29,10 +29,10 @@
 
 import sys
 
-# Sean changed Scanner to model_checker.scanner
-from model_checker.scanner import Token
-from model_checker.scanner import Scanner
-from model_checker.scanner import Position
+# Sean changed Scanner to verifier.scanner
+from verifier.scanner import Token
+from verifier.scanner import Scanner
+from verifier.scanner import Position
 
 
 class ErrorRec(object):
diff --git a/model_checker/scanner.py b/verifier/scanner.py
similarity index 100%
rename from model_checker/scanner.py
rename to verifier/scanner.py
diff --git a/model_checker/simple_intersection/AP_dict.py b/verifier/simple_intersection/AP_dict.py
similarity index 100%
rename from model_checker/simple_intersection/AP_dict.py
rename to verifier/simple_intersection/AP_dict.py
diff --git a/model_checker/simple_intersection/LTL_test.py b/verifier/simple_intersection/LTL_test.py
similarity index 87%
rename from model_checker/simple_intersection/LTL_test.py
rename to verifier/simple_intersection/LTL_test.py
index a84922eab3ce1d2dde967803edcd64c7a425efa8..b914d331faf1cd0967d26ba3e8e65e355414f963 100644
--- a/model_checker/simple_intersection/LTL_test.py
+++ b/verifier/simple_intersection/LTL_test.py
@@ -1,8 +1,8 @@
-from model_checker.simple_intersection import LTLProperty
-from model_checker.simple_intersection.AP_dict import AP_dict_simple_intersection
-from model_checker import Parser
+from verifier.simple_intersection import LTLProperty
+from verifier.simple_intersection.AP_dict import AP_dict_simple_intersection
+from verifier import Parser
 
-# TODO: Refactor LTL_test to model_checker part.
+# TODO: Refactor LTL_test to verifier part.
 
 
 def test_model_check(LTL, trace):
diff --git a/model_checker/simple_intersection/__init__.py b/verifier/simple_intersection/__init__.py
similarity index 100%
rename from model_checker/simple_intersection/__init__.py
rename to verifier/simple_intersection/__init__.py
diff --git a/model_checker/simple_intersection/classes.py b/verifier/simple_intersection/classes.py
similarity index 93%
rename from model_checker/simple_intersection/classes.py
rename to verifier/simple_intersection/classes.py
index 4a88c83b9710df3f054e422722e485df3b1ec22b..7fe92aa7ac70644c02365d838c1ed3da1d1b94f2 100644
--- a/model_checker/simple_intersection/classes.py
+++ b/verifier/simple_intersection/classes.py
@@ -1,4 +1,4 @@
-from model_checker import LTLPropertyBase, AtomicPropositionsBase
+from verifier import LTLPropertyBase, AtomicPropositionsBase
 from .AP_dict import AP_dict_simple_intersection