main.py

import logging
numba_logger = logging.getLogger('numba')
numba_logger.setLevel(logging.WARNING)
import warnings
warnings.filterwarnings("ignore", category=DeprecationWarning)
import yaml
import numpy as np
import pandas as pd
import shap
import math
import pickle
import os
import torch
from copy import deepcopy
from torch.utils.data import DataLoader
from src import Executer
from src.tester import TesterDeviated, TesterAttack, TesterUniform, TesterSamples
from src.converter import Converter
from src.dataset import DrivingDataset
from src.attacker import Attacker
from src.FNN import Network
from src.verifier import Verifier
from src.loss_func_maxima import Loss_Func_Maxima
from src.loss_func_minima import Loss_Func_Minima
from src.trainer import Trainer
import time
import argparse

def dataset_2_pdframe(dataset, col):
    X = []
    Y = []
    for i in range(len(dataset)):
        x, y = dataset[i]
        X.append(x)
        Y.append(y)
    X = np.asarray(X).astype(float)
    X = pd.DataFrame(X, columns=col)
    Y = np.asarray(Y).astype(float)
    return X, Y

class regression_model_wrapper(object):

    def __init__(self, model) -> None:
        self.model = model
        self.model.to('cuda')
    
    def predict(self, X):
        with torch.no_grad():
            X = torch.tensor(X.to_numpy()).float().cuda()
            if len(X.shape) == 1:
                X = X.unsqueeze(0)
            return self.model(X).detach().clone().cpu().reshape(-1).numpy()
        
def shapley_based_explanation(dataset, parameter_order, model):
    ## Parameter-wise Explanation based on Shapley Value
    logging.info('Shapley Explanation Start')
    start_time = time.time()
    warpped_model = regression_model_wrapper(model)
    X, y = dataset_2_pdframe(dataset, parameter_order)
    X100 = shap.utils.sample(X, 100)
    explainer = shap.Explainer(warpped_model.predict, X100)
    shap_values = explainer(X)
    shap_argsort = shap_values.abs.mean(axis=0).values.argsort()[::-1]    
    parameter_priority = [parameter_order[i] for i in shap_argsort]
    logging.debug('Shapley Values (Mean):' + str(shap_values.abs.mean(axis=0)))
    logging.debug('Parameters by order: '+ str(parameter_priority))
    logging.info('Shapley Explanation Ends.. Time:%.2f', time.time() - start_time)
    return shap_values, parameter_priority[0], shap_argsort[0]

def case_split(filename, trainset, testset, dim_div, dim_div_i, bounds, settings_all, early_stop=False):    
    ## Dimension Division    
    settings_left = deepcopy(settings_all)
    settings_left['metainfo']['divided_dimension'].append(dim_div)
    settings_left['metainfo']['parent'] = settings_all['metainfo']['splits']
    settings_left['metainfo']['splits'] = settings_all['metainfo']['splits'] * 2
    settings_left['metainfo']['current_stage'] = -1
    settings_left['metainfo']['current_status'] = 'EarlyStop' if early_stop else 'Nan'

    settings_right = deepcopy(settings_all)
    settings_right['metainfo']['divided_dimension'].append(dim_div)
    settings_right['metainfo']['parent'] = settings_all['metainfo']['splits']
    settings_right['metainfo']['splits'] = settings_all['metainfo']['splits'] * 2 + 1
    settings_right['metainfo']['current_stage'] = -1
    settings_right['metainfo']['current_status'] = 'EarlyStop' if early_stop else 'Nan'

    ## Divide the samples into two categories
    trainset_ind_left = trainset.data[:, dim_div_i] <= (bounds[0, dim_div_i] + bounds[1, dim_div_i]) / 2.
    trainset_left_data = trainset.data[trainset_ind_left].tolist()
    trainset_left_value = trainset.value[trainset_ind_left].tolist()
    trainset_left = dict()
    trainset_left['data'] = trainset_left_data
    trainset_left['value'] = trainset_left_value
    testset_ind_left = testset.data[:, dim_div_i] <= (bounds[0, dim_div_i] + bounds[1, dim_div_i]) / 2.
    testset_left_data = testset.data[testset_ind_left].tolist()
    testset_left_value = testset.value[testset_ind_left].tolist()
    testset_left = dict()
    testset_left['data'] = testset_left_data
    testset_left['value'] = testset_left_value

    trainset_ind_right = trainset.data[:, dim_div_i] >= (bounds[0, dim_div_i] + bounds[1, dim_div_i]) / 2.
    trainset_right_data = trainset.data[trainset_ind_right].tolist()
    trainset_right_value = trainset.value[trainset_ind_right].tolist()
    trainset_right = dict()
    trainset_right['data'] = trainset_right_data
    trainset_right['value'] = trainset_right_value
    testset_ind_right = testset.data[:, dim_div_i] >= (bounds[0, dim_div_i] + bounds[1, dim_div_i]) / 2.
    testset_right_data = testset.data[testset_ind_right].tolist()
    testset_right_value = testset.value[testset_ind_right].tolist()
    testset_right = dict()
    testset_right['data'] = testset_right_data
    testset_right['value'] = testset_right_value

    ## Write Samples and Settings File
    file_name_left = filename.rsplit('_', maxsplit=1)[0]+'_'+str(settings_left['metainfo']['splits'])+'.yaml'
    file_name_right = filename.rsplit('_', maxsplit=1)[0]+'_'+str(settings_right['metainfo']['splits'])+'.yaml'
    with open(file_name_left, 'w') as f:
        yaml.safe_dump(settings_left, f)
    
    with open(file_name_right, 'w') as f:
        yaml.safe_dump(settings_right, f)

    root_cwd = os.getcwd()
    left_analyse_dir = settings_left['data']['analyse_result_rootdir']
    left_analyse_dir = os.path.join(root_cwd, left_analyse_dir)
    left_analyse_dir = os.path.join(left_analyse_dir, settings_left['metainfo']['scenario_name']+'_'+str(settings_left['metainfo']['scenario_id']))
    left_analyse_dir = os.path.join(left_analyse_dir, str(settings_left['metainfo']['splits']))
    os.makedirs(left_analyse_dir, exist_ok=True)
    if len(trainset_left_data) > 0:
        with open(os.path.join(left_analyse_dir, 'init_pre.pickle'), 'wb') as f:
            pickle.dump(trainset_left, f)
    if len(testset_left_data) > 0:
        with open(os.path.join(left_analyse_dir, 'scenario_pre.pickle'), 'wb') as f:
            pickle.dump(testset_left, f)

    right_analyse_dir = settings_right['data']['analyse_result_rootdir']
    right_analyse_dir = os.path.join(root_cwd, right_analyse_dir)
    right_analyse_dir = os.path.join(right_analyse_dir, settings_right['metainfo']['scenario_name']+'_'+str(settings_right['metainfo']['scenario_id']))
    right_analyse_dir = os.path.join(right_analyse_dir, str(settings_right['metainfo']['splits']))
    os.makedirs(right_analyse_dir, exist_ok=True)
    if len(trainset_right_data) > 0:
        with open(os.path.join(right_analyse_dir, 'init_pre.pickle'), 'wb') as f:
            pickle.dump(trainset_right, f)
    if len(testset_right_data) > 0:
        with open(os.path.join(right_analyse_dir, 'scenario_pre.pickle'), 'wb') as f:
            pickle.dump(testset_right, f)

def verify(config_file, early_stop=True):
    ## Logging Module Initialize
    logfile = os.path.basename(config_file).replace('.yaml', '.log')
    logfile = os.path.join('logs', logfile)
    # Remove all handlers associated with the root logger object.
    for handler in logging.root.handlers[:]:
        logging.root.removeHandler(handler)
    logging.basicConfig(filename=logfile, format='%(asctime)s %(levelname)s:%(message)s', datefmt='%m/%d/%Y %I:%M:%S %p', level=logging.DEBUG)
    logging.info('Task Start.... Loading Configs...')
    

    root_cwd = os.getcwd()
    with open(config_file, 'r') as f:
        settings_all = yaml.safe_load(f)

    ## Load Sub Configs
    settings_config = settings_all['config']

    ## Load Metainfo
    settings_meta = settings_all['metainfo']
    meta_splits = settings_meta['splits']
    scenario_name = settings_meta['scenario_name']
    scenario_id = settings_meta['scenario_id']
    divided_dimension = settings_meta['divided_dimension']
    # -1 just created, 0 initial sampling, 1 ~ total_iterations refine sampling
    current_stage = settings_meta['current_stage']    
    current_status = settings_meta['current_status']
    parent = settings_meta['parent']
    if current_status in {'Verified', 'Unsafe', 'Unknown'}:
        logging.info('Analysed Case..Skipping...')
        return
    elif current_status == 'EarlyStop':
        if early_stop:
            logging.info('EarlyStop Case..Skipping...')
            return

    with open(settings_config['scenario_config'], 'r') as f:
        scenario_config = yaml.safe_load(f)

    with open(settings_config['weather_config'], 'r') as f:
        weather_config = yaml.safe_load(f)
    example_json = os.path.join(root_cwd, settings_config['example_json'])

    ## Load Simulation Details
    simulation_config = settings_all['simulation']    
    srunner_xml = os.path.join(root_cwd, simulation_config['srunner_xml'])
    carla_port = simulation_config['port']
    carla_traffic_port = simulation_config['traffic_port']

    ## Get the parameter order and the converter
    parameter_order = []
    for item in scenario_config:
        if isinstance(scenario_config[item], list):
            parameter_order.append(item)
    for item in weather_config:
        if isinstance(weather_config[item], list):
            parameter_order.append(item)
    parameter_order = sorted(parameter_order)
    converter = Converter(scenario_config, weather_config, parameter_order)    

    ## Calculate Current Parameter Bounds 
    split_branches = bin(meta_splits)[3:]
    bounds = np.array([np.zeros(len(parameter_order)), np.ones(len(parameter_order))])
    for parameter_name, split_branch in zip(divided_dimension, split_branches):
        parameter_pos = parameter_order.index(parameter_name)
        if split_branch == '0':
            ## Left Branch
            bounds[1][parameter_pos] = (bounds[0][parameter_pos] + bounds[1][parameter_pos]) / 2            
        else:
            ## Right Branch
            bounds[0][parameter_pos] = (bounds[0][parameter_pos] + bounds[1][parameter_pos]) / 2                

    ## Get Root Dirs
    running_result_rootdir = settings_all['data']['running_result_rootdir']
    analyse_result_rootdir = settings_all['data']['analyse_result_rootdir']
    save_rootdir = settings_all['data']['save_rootdir']

    running_result_rootdir = os.path.join(root_cwd, running_result_rootdir)
    analyse_result_rootdir = os.path.join(root_cwd, analyse_result_rootdir)
    save_rootdir = os.path.join(root_cwd, save_rootdir)

    ## Get Verification Details
    verification_settings = settings_all['verification_info']
    scenario_opt_samples = math.ceil(2./verification_settings['error'] * math.log(1./verification_settings['significance'] + 1))
    property_threshold = verification_settings['property_threshold']

    ## Get Learning Details
    learning_settings = settings_all['learning_info']
    #### Future Improvements: Currently only working on single target properties ####
    model_structure = [len(parameter_order)] + learning_settings['model_structure'] + [1]
    max_iterations = learning_settings['max_iterations']
    initial_samples = learning_settings['initial_samples']
    learning_rate = learning_settings['lr']
    epoches = learning_settings['epoches']
    batch_size = learning_settings['batch_size']
    sample_uniform = learning_settings['sample_number']['uniform']
    sample_deviated = learning_settings['sample_number']['deviated']
    sample_attacking = learning_settings['sample_number']['attacking']    

    ## Main Procedure
    current_analyse_dir = os.path.join(analyse_result_rootdir, scenario_name+'_'+str(scenario_id))
    current_analyse_dir = os.path.join(current_analyse_dir, str(meta_splits))
    current_sim_dir = os.path.join(running_result_rootdir, scenario_name+'_'+str(scenario_id))
    current_sim_dir = os.path.join(current_sim_dir, str(meta_splits))
    save_rootdir = os.path.join(save_rootdir, scenario_name+'_'+str(scenario_id))
    save_rootdir = os.path.join(save_rootdir, str(meta_splits))

    os.makedirs(current_analyse_dir, exist_ok=True)
    os.makedirs(current_sim_dir, exist_ok=True)
    os.makedirs(save_rootdir, exist_ok=True)

    logging.info('Config Loaded...')

    # print(save_rootdir)
    # print(current_analyse_dir)
    # print(current_sim_dir)

    if current_stage < 0:        
        ## Initial Sampling (Uniform for Scenario Optimization and Model Learning)
        logging.info('Pre-refine Sampling Start...')

        # 1. Check the legacy from previous verification
        init_pre_filepath = os.path.join(current_analyse_dir, 'init_pre.pickle')
        data_init_pre_number = 0        
        if os.path.exists(init_pre_filepath):
            with open(init_pre_filepath, 'rb') as f:
                data_init_pre = pickle.load(f)        
                data_init_pre_number = len(data_init_pre['data'])
        
        scenario_pre_filepath = os.path.join(current_analyse_dir, 'scenario_pre.pickle')
        data_scenario_pre_number = 0
        if os.path.exists(scenario_pre_filepath):
            with open(scenario_pre_filepath, 'rb') as f:
                data_scenario_pre = pickle.load(f)
                data_scenario_pre_number = len(data_scenario_pre['data'])
        
        logging.debug('Inital Sample Legacy Found: %d' % data_init_pre_number)
        logging.debug('Scenario Sample Legacy Found: %d' % data_scenario_pre_number)
        
        init_samples_needed = max(initial_samples - data_init_pre_number, 0)
        scenario_samples_needed = max(scenario_opt_samples - data_scenario_pre_number, 0)                

        ## Samples for the rest.... (Uniform)
        ### Sample the initial batch
        if init_samples_needed > 0:
            logging.info('Initial Sampling Start.. Total number: %d' % init_samples_needed)
            start_time = time.time()
            initial_samples_dir = os.path.join(current_sim_dir, 'init')
            initial_json_dir = os.path.join(initial_samples_dir, 'json')
            initlal_log_dir = os.path.join(initial_samples_dir, 'log')
            initial_json_savepath = os.path.join(initial_json_dir, 'init_%d.json')                
            executer = Executer(srunner_xml, example_json, initial_json_savepath, initlal_log_dir, carla_port, carla_traffic_port)
            tester_init = TesterUniform(bounds, init_samples_needed, converter, executer)
            init_samples = tester_init.sampling()        
            with open(os.path.join(current_analyse_dir, 'init.pickle'), 'wb') as f:
                pickle.dump(init_samples, f)
            end_time = time.time()
            logging.info('Inital Sampling End.. Total Time: %.2f Adversarial Sampling:%d' % (time.time()-start_time, (np.array(init_samples['value']) <= property_threshold).sum()))
        else:
            logging.info('Inital Sample Legacy Fulfills the Requirements. Skipping the Initial Sampling')
        
        ### Sample the scenario batch
        if scenario_samples_needed > 0:
            logging.info('Scenario Sampling Start.. Total number: %d' % scenario_samples_needed)
            start_time = time.time()
            scenario_samples_dir = os.path.join(current_sim_dir, 'scenario')
            scenario_json_dir = os.path.join(scenario_samples_dir, 'json')
            scenario_log_dir = os.path.join(scenario_samples_dir, 'log')
            scenario_json_savepath = os.path.join(scenario_json_dir, 'scenario_%d.json')                
            executer = Executer(srunner_xml, example_json, scenario_json_savepath, scenario_log_dir, carla_port, carla_traffic_port)
            tester_scenario = TesterUniform(bounds, scenario_samples_needed, converter, executer)
            scenario_samples = tester_scenario.sampling()        
            with open(os.path.join(current_analyse_dir, 'scenario.pickle'), 'wb') as f:
                pickle.dump(scenario_samples, f)
            logging.info('Scenario Sampling End.. Total Time: %.2f Adversarial Sampling:%d' % (time.time()-start_time, (np.array(scenario_samples['value']) <= property_threshold).sum()))
        else:
            logging.info('Scenario Sample Legacy Fulfills the Requirements. Skipping the Scenario Sampling')
        
        ## Update Yaml File
        settings_all['metainfo']['current_stage'] = 0
        with open(config_file, 'w') as f:
            yaml.safe_dump(settings_all, f)    
    ## Iterative Refinement
    ## Refresh the current stage
    current_stage = settings_all['metainfo']['current_stage']    
    model = Network(model_structure)
    trainer = Trainer(epoches, learning_rate)
    trainset = DrivingDataset(current_analyse_dir, training=True)
    testset = DrivingDataset(current_analyse_dir, training=False)
    no_adv = True
    for i in range(current_stage, max_iterations):
        logging.info('Refinement %d Start' % i)
        ## Iteratively Refinement
        ## Train the model according to current dataset   
        logging.info('Training Model %d Start..' % i)     
        start_time = time.time()
        trainset.update()
        testset.update()
        no_adv = (trainset.value <= property_threshold).sum() + (testset.value <= property_threshold).sum() == 0
        trainloader = DataLoader(trainset, batch_size)        
        testloader = DataLoader(testset, batch_size)
        ## Evaluate the absolute difference
        model = trainer.train(model, trainloader)
        logging.info('Training Model %d Ends.. Time:%.2f' % (i, time.time() - start_time))
        ### Save Model Weights
        torch.save(model.state_dict(), os.path.join(save_rootdir, 'weights_%d.pth' % i))
        abs_diff_eval = trainer.evaluate_absolute_difference(model, testloader)

        ## Verify the surrogate model and perform early stop        
        potential_adversarial = []
        verification_result = False
        if no_adv:
            logging.info('Verification %d Start..' % i)
            start_time = time.time()
            verifier = Verifier(model, torch.tensor(bounds[0]), torch.tensor(bounds[1]), -torch.ones((1,1)), torch.tensor([abs_diff_eval + property_threshold]).reshape(1,1), 'cuda')
            verification_result, potential_adversarial = verifier.verify()
            logging.info('Verification %d Ends.. Time:%.2f' % (i, time.time() - start_time))
            ### Perform Early Stop if verified, save the potential_adv otherwise
            if verification_result:                
                settings_all['metainfo']['current_status'] = 'Verified'
                shapley_values, most_important_param, most_important_param_i = shapley_based_explanation(trainset, parameter_order, model)
                with open(os.path.join(save_rootdir, 'shapley_values_%d.pickle' % i), 'wb') as f:
                    pickle.dump(shapley_values, f)
                logging.info('Case Splitting...')
                case_split(config_file, trainset, testset, most_important_param, most_important_param_i, bounds, settings_all,early_stop=True)
                logging.info('Case Finished.. Status:Verified (Early Stop)')
                ## Update Yaml File        
                with open(config_file, 'w') as f:
                    yaml.safe_dump(settings_all, f)                
                return                            
        else:
            logging.info('Found Adv, Skip the verification..')        
        ## Incremental Sampling
        samples_dir_iter = os.path.join(current_sim_dir, 'iter'+str(i))
        samples_json_dir = os.path.join(samples_dir_iter, 'json')
        samples_log_dir = os.path.join(samples_dir_iter, 'log')
        ### Potential Adversarial Example Sampling        
        if len(potential_adversarial) > 0:
            logging.info('Evaluating the potential adversarial example from the verification..')
            start_time = time.time()
            adv_json_savepath = os.path.join(samples_json_dir, 'potential_adv_%d.json')
            executer = Executer(srunner_xml, example_json, adv_json_savepath, samples_log_dir, carla_port, carla_traffic_port)            
            potential_adversarial = np.array(potential_adversarial)            
            tester_samples = TesterSamples(potential_adversarial, converter, executer)
            adv_samples = tester_samples.sampling()
            with open(os.path.join(current_analyse_dir, 'potential_adv_%d.pickle' % i), 'wb') as f:
                pickle.dump(adv_samples, f)
            logging.info('Evaluation Ends.. Time:%.2f Found Adv:%d' % (time.time()-start_time, (np.array(adv_samples['value']) <= property_threshold).sum()))
        ### Attack Sampling
        attacker = Attacker(model, torch.tensor(bounds[0]), torch.tensor(bounds[1]))        
        ## Minimal Attack
        logging.info('Incremental Sampling (Adversarial Attack, Minimal) Number:%d' % sample_attacking)
        start_time = time.time()
        attack_json_savepath = os.path.join(samples_json_dir, 'attack_minimal_%d.json')
        executer = Executer(srunner_xml, example_json, attack_json_savepath, samples_log_dir, carla_port, carla_traffic_port)        
        loss_func_minimal = Loss_Func_Minima()
        tester_attack_minimal = TesterAttack(sample_attacking, attacker, loss_func_minimal, converter, executer)
        minimal_samples = tester_attack_minimal.sampling()
        with open(os.path.join(current_analyse_dir, 'attack_minimal_%d.pickle' % i), 'wb') as f:
            pickle.dump(minimal_samples, f)
        logging.info('Incremental Sampling (Adversarial Attack, Minimal) Ends.. Time:%.2f Found Adv:%d' % (time.time() - start_time, (np.array(minimal_samples['value']) <= property_threshold).sum()))

        ## Maximal Attack
        logging.info('Incremental Sampling (Adversarial Attack, Maximal) Number:%d' % sample_attacking)
        start_time = time.time()
        attack_json_savepath = os.path.join(samples_json_dir, 'attack_maximal_%d.json')
        executer = Executer(srunner_xml, example_json, attack_json_savepath, samples_log_dir, carla_port, carla_traffic_port)        
        loss_func_maximal = Loss_Func_Maxima()
        tester_attack_maximal = TesterAttack(sample_attacking, attacker, loss_func_maximal, converter, executer)
        maximal_samples = tester_attack_maximal.sampling()
        with open(os.path.join(current_analyse_dir, 'attack_maximal_%d.pickle' % i), 'wb') as f:
            pickle.dump(maximal_samples, f)
        logging.info('Incremental Sampling (Adversarial Attack, Maximal) Ends.. Time:%.2f Found Adv:%d' % (time.time() - start_time, (np.array(maximal_samples['value']) <= property_threshold).sum()))

        ## Deviated Sampling
        logging.info('Incremental Sampling (Deviated) Number:%d' % sample_deviated)
        start_time = time.time()
        deviated_json_savepath = os.path.join(samples_json_dir, 'deviated_%d.json')
        executer = Executer(srunner_xml, example_json, deviated_json_savepath, samples_log_dir, carla_port, carla_traffic_port)                
        tester_deviated = TesterDeviated(bounds, trainset, sample_deviated, converter, executer)        
        deviated_samples = tester_deviated.sampling(model)
        with open(os.path.join(current_analyse_dir, 'deviated_%d.pickle' % i), 'wb') as f:
            pickle.dump(deviated_samples, f)
        logging.info('Incremental Sampling (Deviated) Ends.. Time:%.2f Found Adv:%d' % (time.time() - start_time, (np.array(deviated_samples['value']) <= property_threshold).sum()))

        ## Uniform Sampling
        logging.info('Incremental Sampling (Uniform) Number:%d' % sample_uniform)
        start_time = time.time()
        uniform_json_savepath = os.path.join(samples_json_dir, 'uniform_%d.json')
        executer = Executer(srunner_xml, example_json, uniform_json_savepath, samples_log_dir, carla_port, carla_traffic_port)                
        tester_uniform = TesterUniform(bounds, sample_uniform, converter, executer)        
        uniform_samples = tester_uniform.sampling()
        with open(os.path.join(current_analyse_dir, 'uniform_%d.pickle' % i), 'wb') as f:
            pickle.dump(uniform_samples, f)
        logging.info('Incremental Sampling (Uniform) Ends.. Time:%.2f Found Adv:%d' % (time.time() - start_time, (np.array(uniform_samples['value']) <= property_threshold).sum()))

        ## Update Yaml File
        settings_all['metainfo']['current_stage'] = i + 1
        with open(config_file, 'w') as f:
            yaml.safe_dump(settings_all, f)        
    
    ## Last Learning, Verification and Case Split
    trainset.update()
    testset.update()
    trainloader = DataLoader(trainset, batch_size)        
    testloader = DataLoader(testset, batch_size)
    ## Evaluate the absolute difference
    logging.info('Last Learning Start..')
    start_time = time.time()
    model = trainer.train(model, trainloader)
    logging.info('Last Learning Ends.. Time:%.2f' % (time.time() - start_time))
    torch.save(model.state_dict(), os.path.join(save_rootdir, 'weights_last.pth'))
    abs_diff_eval = trainer.evaluate_absolute_difference(model, testloader)
    verifier = Verifier(model, torch.tensor(bounds[0]), torch.tensor(bounds[1]), -torch.ones((1,1)), torch.tensor([abs_diff_eval + property_threshold]).reshape(1,1), 'cuda')
    logging.info('Last Verification Start..')
    start_time = time.time()
    verification_result, potential_adversarial = verifier.verify()
    logging.info('Last Verification Ends.. Time:%.2f' % (time.time() - start_time))
    samples_dir_iter = os.path.join(current_sim_dir, 'last_verification')
    samples_json_dir = os.path.join(samples_dir_iter, 'json')
    samples_log_dir = os.path.join(samples_dir_iter, 'log')
    if len(potential_adversarial) > 0:  
            logging.info('Evaluating the potential adversarial example from the verification..')
            start_time = time.time()        
            adv_json_savepath = os.path.join(samples_json_dir, 'potential_adv_%d.json')
            executer = Executer(srunner_xml, example_json, adv_json_savepath, samples_log_dir, carla_port, carla_traffic_port)            
            potential_adversarial = np.array(potential_adversarial)            
            tester_samples = TesterSamples(potential_adversarial, converter, executer)
            adv_samples = tester_samples.sampling()
            with open(os.path.join(current_analyse_dir, 'potential_adv_last.pickle'), 'wb') as f:
                pickle.dump(adv_samples, f)
            logging.info('Evaluation Ends.. Time:%.2f Found Adv:%d' % (time.time()-start_time, (np.array(adv_samples['value']) <= property_threshold).sum()))
    shapley_values, most_important_param, most_important_param_i = shapley_based_explanation(trainset, parameter_order, model)
    with open(os.path.join(save_rootdir, 'shapley_values_last.pickle'), 'wb') as f:
                    pickle.dump(shapley_values, f)
    if verification_result:
        settings_all['metainfo']['current_status'] = 'Verified'        
        case_split(config_file, trainset, testset, most_important_param, most_important_param_i, bounds, settings_all, early_stop=True)        
    else:
        trainset.update()
        testset.update()
        no_adv = (trainset.value <= property_threshold).sum() + (testset.value <= property_threshold).sum() == 0
        if no_adv:
            settings_all['metainfo']['current_status'] = 'Unknown'
        else:
            settings_all['metainfo']['current_status'] = 'Unsafe'        
        case_split(config_file, trainset, testset, most_important_param, most_important_param_i, bounds, settings_all, early_stop=False)                
    ## Update Yaml File        
    with open(config_file, 'w') as f:
        yaml.safe_dump(settings_all, f)
    logging.info('Case Finished.. Status:%s' % settings_all['metainfo']['current_status'])

def main(args):
    filename_base = args.scenario + '_%d.yaml'
    node_lower = args.l
    node_upper = args.u    
    for taskcase_i in range(node_lower, node_upper + 1):
        filename_i = os.path.join('configs', filename_base % taskcase_i)
        if os.path.exists(filename_i):            
            print('Taskfile %s Running...' % filename_i)
            verify(filename_i)

if __name__ == '__main__':
    parser = argparse.ArgumentParser(description='Explanation Based PAC Verification Framework for Autonoumous Driving Systems')
    parser.add_argument('--scenario', type=str, default='PedestrianCrossing_1')
    parser.add_argument('--l', type=int, default=1)
    parser.add_argument('--u', type=int, default=7)
    args = parser.parse_args()
    main(args)
    # verify('configs/PedestrianCrossing_1_demo_1.yaml')