<jupyter_start><jupyter_text>IntroductionThis Notebook can be used for plotting Table 1 and Figure 2 of the paper. Each box with code is called a *Cell*. To execute the contents of a *Cell*, place the cursor inside it and press `Ctrl+Enter`; or else click on the Cell menu at the top of the page and select `Run cells`. You may also choose to execute all cells at once by selecting `Run all`.*Note: each cell depends on the previous, and hence trying to run one of the later cells without running all previous cells will end in an error.*<jupyter_code>import glob
import json
import numpy as np
import pandas as pd
import mpmath as mp

# Set the location of logs 
# selct_and_run.sh writes to logs/evaluation by default

log_folder = "logs/evaluation"

# Uncomment the next line to plot the logs used in the paper
# log_folder = "logs/paper"

models = {
     "consensus.2.prism": { "type":"MDP", "states":272, "pretty_name":"consensus" },
     "csma.2-2.prism": { "type":"MDP", "states":1038, "pretty_name":"csma-2-2" },
     "firewire.true.prism": { "type":"MDP", "states":83153, "pretty_name":"firewire" },
     "ij.3.v1.prism": { "type":"MDP", "states":7, "pretty_name":"ij-3" },
     "ij.10.v1.prism": { "type":"MDP", "states":1023, "pretty_name":"ij-10" },
     "pacman.nm": { "type":"MDP", "states":498, "pretty_name":"pacman" },
     "philosophers-mdp.3.v1.prism": { "type":"MDP", "states":956, "pretty_name":"philosophers-mdp-3" },
     "pnueli-zuck.3.v1.prism": { "type":"MDP", "states":2701, "pretty_name":"pnueli-zuck-3" },
     "rabin.3.prism": { "type":"MDP", "states":27766, "pretty_name":"rabin-3" },
     "wlan.0.prism": { "type":"MDP", "states":2954, "pretty_name":"wlan-0" },
     "zeroconf.prism": { "type":"MDP", "states":670, "pretty_name":"zeroconf" },
     "cdmsn.prism": { "type":"SMG", "states":1240, "pretty_name":"cdmsn" },
     "cloud_5.prism": { "type":"SMG", "states":8842, "pretty_name":"cloud-5" },
     "mdsm.prism-player_1": { "type":"SMG", "states":62245, "pretty_name":"mdsm-1" },
     "mdsm.prism-player_2": { "type":"SMG", "states":62245, "pretty_name":"mdsm-2" },
     "team-form-3.prism": { "type":"SMG", "states":12476, "pretty_name":"team-form-3" }
}

param_strings = {
    "consensus.2.prism": "S:272;Av:2;e:1e-8;d:0.01;p:0.5;post:2",
    "csma.2-2.prism": "S:1038;Av:2;e:1e-8;d:0.01;p:0.25;post:4",
    "firewire.true.prism": "S:83153;Av:3;e:1e-8;d:0.01;p:0.5;post:2",
    "ij.3.v1.prism": "S:7;Av:3;e:1e-8;d:0.01;p:0.5;post:2",
    "ij.10.v1.prism": "S:1023;Av:10;e:1e-8;d:0.01;p:0.5;post:2",
    "pacman.nm": "S:498;Av:5;e:1e-8;d:0.01;p:0.08;post:3",
    "philosophers-mdp.3.v1.prism": "S:956;Av:6;e:1e-8;d:0.01;p:0.5;post:2",
    "pnueli-zuck.3.v1.prism": "S:2701;Av:6;e:1e-8;d:0.01;p:0.5;post:2",
    "rabin.3.prism": "S:27766;Av:3;e:1e-8;d:0.01;p:0.03125;post:6",
    "wlan.0.prism": "S:2954;Av:3;e:1e-8;d:0.01;p:0.0625;post:16",
    "zeroconf.prism": "S:670;Av:3;e:1e-8;d:0.01;p:1.025262467191601E-4;post:6",
    "cdmsn.prism": "S:1240;Av:2;e:1e-8;d:0.01;p:0.059071881973375796;post:5",
    "cloud_5.prism": "S:8842;Av:11;e:1e-8;d:0.01;p:0.001;post:2",
    "mdsm.prism-player_1": "S:62245;Av:2;e:1e-8;d:0.01;p:0.0684;post:5",
    "mdsm.prism-player_2": "S:62245;Av:2;e:1e-8;d:0.01;p:0.0684;post:5",
    "team-form-3.prism": "S:12476;Av:3;e:1e-8;d:0.01;p:0.02040816326530612;post:49"
}

# Function to compute m (log of which is given in Table 1)
def compute_m(param_string):
    param_split = param_string.split(";")
    params = {}
    for p in param_split:
        key, value = p.split(":")
        params[key] = value

    eps = 0.1
    pmin = mp.mpf(params["p"])
    Em = int(params["Av"])
    S = int(params["S"])
    d = mp.mpf(params["d"])
    A = Em*S
    
    ebar = (eps*(pmin/Em)**S)/(12*S)
    
    m = mp.log(6*S*A*(1 + (S*A)/ebar)/d)/(2*ebar*ebar)
    
    return int(mp.log10(m))

# Identify the log files and label them
logs = {}

for model in models:
    l_g = glob.glob(log_folder+"/"+model+"*grey*.log")
    s_g = glob.glob(log_folder+"/"+model+"*grey*.stat")
    l_b = glob.glob(log_folder+"/"+model+"*black*.log")
    s_b = glob.glob(log_folder+"/"+model+"*black*.stat")
    model_type = ""

    if l_g and s_g and l_b and s_b:
        model_type = [models[model]["type"]]*len(l_g)
        logs[model] = list(zip(model_type, l_g, l_b, s_g, s_b))
        
print("Processed logs for " + str(len(logs)) + " models")

if len(logs) == 0:
    print("\nPlease recheck that log_folder is set correctly/contains logs. You need to run select-and-run.sh as described in the README before you run this script. If you already ran select-and-run.sh, check pueue status to see if the jobs have finished.")<jupyter_output><empty_output><jupyter_text>Plot graphs The following code goes through the log files and1. Plots the evolution of the lower and upper bounds as well as the precision.2. Populates the `raw_results` array which will be used to plot Table 1 (see [below](Table-1)). Comments about the output1. The figures with the title `cloud-5`, `pacman`, `csma` and `mdsm-1` should be similar to those in Fig. 1.2. In the text of Section 4 of the paper, we have made some claims such as "We obtained epsilon < 0.1 on 6 benchmarks" or "On 14/16 benchmarks, it took ...". The claims can be verified manually with the help of the plotted figures. Again, note that due to statistical noise, one might require more than 1 repetition in order to verify these claims.<jupyter_code>import matplotlib.pyplot as plt
from matplotlib import ticker
%matplotlib inline

raw_results = []

for model in logs:
    i = 0
    for e in logs[model]:
        i = i+1
        model_type, log_file_g, log_file_b, stat_file_g, stat_file_b = e
        with open(log_file_g) as f_g, open(log_file_b) as f_b:
            # Grey
            global_times_g = []
            precisions_g = []
            trials_g = []
            lower_bounds_g = []
            upper_bounds_g = []
            states_g = -1
            unset_g = 0
            result_g = -1
            completed_g = -1
            
            # Black
            global_times_b = []
            precisions_b = []
            trials_b = []
            lower_bounds_b = []
            upper_bounds_b = []
            states_b = -1
            result_b = -1
            completed_b = -1
            
            prop, consts, _, _ = log_file_g.split("/")[2][len(model)+1:].split("-")
            prop1, consts1, _, _ = log_file_b.split("/")[2][len(model)+1:].split("-")
            
            # Parse the logs
            for line in f_g:
                if line.startswith("JSON: "):
                    cur = json.loads(line[len("JSON: "):])
                    global_times_g.append(float(cur['GlobalTimerSecs']))
                    precisions_g.append(float(cur['Precision']))
                    trials_g.append(float(cur['Trials']))
                    lower_bounds_g.append(float(cur['Value']['Lower']))
                    upper_bounds_g.append(float(cur['Value']['Upper']))
                    states_g = int(cur['StateInfos']['numStates'])
                    unset_g = int(cur['StateInfos']['numUnset'])
                if line.startswith("Model checking completed in"):
                    completed_g = float(line.split(" ")[4])
                if line.startswith("Result"):
                    result_g = float(line.split(": ")[1])
                    
            for line in f_b:
                if line.startswith("JSON: "):
                    cur = json.loads(line[len("JSON: "):])
                    global_times_b.append(float(cur['GlobalTimerSecs']))
                    precisions_b.append(float(cur['Precision']))
                    trials_b.append(float(cur['Trials']))
                    lower_bounds_b.append(float(cur['Value']['Lower']))
                    upper_bounds_b.append(float(cur['Value']['Upper']))
                    states_b = int(cur['StateInfos']['numStates'])
                if line.startswith("Model checking completed in"):
                    completed_b = float(line.split(" ")[4])
                if line.startswith("Result"):
                    result_b = float(line.split(": ")[1])
            
            if (len(global_times_g) == 0 and result_g < 0):
                raw_results.append([model, models[model]['type'],
                                  1 if len(precisions_g) == 0 else precisions_g[-1], 
                                  1 if len(precisions_b) == 0 else precisions_b[-1], 
                                  (states_g-unset_g),
                                  states_b-1, models[model]['states']])
            else:
                plt.figure(figsize=(3.5,3.5))
                plt.style.use('seaborn')
                if len(global_times_g) == 1 and result_g >= 0:
                    plt.plot(global_times_g, lower_bounds_g, label='Lower Bound (G)', marker='o', markersize=3)
                    plt.plot(global_times_g, upper_bounds_g, label='Upper Bound (G)', marker='o', markersize=3)
                else:
                    if result_g < 0:
                        global_times_g.append(1800)
                        lower_bounds_g.append(lower_bounds_g[-1])
                        upper_bounds_g.append(upper_bounds_g[-1])
                    plt.plot(global_times_g, lower_bounds_g, label='Lower Bound (G)')
                    plt.plot(global_times_g, upper_bounds_g, label='Upper Bound (G)')
                if (len(global_times_b) == 0 and result_b < 0):
                    global_times_b.append(0)
                    global_times_b.append(1800)
                    lower_bounds_b.append(0)
                    lower_bounds_b.append(0)
                    upper_bounds_b.append(1)
                    upper_bounds_b.append(1)
                    precisions_b.append(1)
                    precisions_b.append(1)
                    states_b = 0
                    plt.plot(global_times_b, lower_bounds_b, label='Lower Bound (B)', marker='o', linestyle='dashed', markersize=3)
                    plt.plot(global_times_b, upper_bounds_b, label='Upper Bound (B)', marker='o', linestyle='dashed', markersize=3)
                elif len(global_times_b) == 1 and result_b >= 0:
                    plt.plot(global_times_b, lower_bounds_b, label='Lower Bound (B)', marker='o', linestyle='dashed', markersize=3)
                    plt.plot(global_times_b, upper_bounds_b, label='Upper Bound (B)', marker='o', linestyle='dashed', markersize=3)
                else:
                    if result_b < 0:
                        #global_times_b.append(3600)
                        global_times_b.append(1800)
                        lower_bounds_b.append(lower_bounds_b[-1])
                        upper_bounds_b.append(upper_bounds_b[-1])
                    plt.plot(global_times_b, lower_bounds_b, label='Lower Bound (B)', linestyle='dashed')
                    plt.plot(global_times_b, upper_bounds_b, label='Upper Bound (B)', linestyle='dashed')
                if completed_g >= 0:
                    plt.plot(completed_g, result_g, marker='*', markersize=10, label="Result (G)")
                if completed_b >= 0:
                    plt.plot(completed_b, result_b, marker='*', markersize=10, label="Result (B)")
                ax = plt.gca()
                ax.set_yticks(np.arange(0,1.1,0.1))
                ax.set_xlim(-100, 1900)
                plt.xticks([0, 300, 600, 900, 1200, 1500, 1800], ("0", "5", "10", "15", "20", "25", "30"), rotation=0)
                plt.ylabel('Value')
                plt.xlabel('Time (min)')
                plt.title("Model: " + models[model]['pretty_name'])
                plt.legend()            
                plt.grid(True)
                plt.ylim(-0.1,1.1)
                plt.show()
                # filename = model.replace(".", "-")+"-"+prop+"-"+consts+"-"+str(i)+"-full"
                # plt.savefig(folder_output+"/"+filename+".pdf", bbox_inches='tight')
                raw_results.append([model, models[model]['type'],
                                    precisions_g[-1], precisions_b[-1], 
                                    (states_g-unset_g), states_b-1, models[model]['states']
                                   ])
                plt.close()<jupyter_output><empty_output><jupyter_text>Table 1Run the following `Cell` to plot Table 1. Make sure you have run the [previous](Plot-graphs) cell so that `raw_results` is populated.*Please ignore the warning which would be shown when you run the following cell* Comments about the outputAs long as the number of repetitions is high, the output will resemble the table in the paper. If you used a small value for repetitions such as 1 or 2, you might find differences because of statistical noise.<jupyter_code>if raw_results != []:    
    df = pd.DataFrame(raw_results, columns=['Model', 'Type', 'Precision Grey', 'Precision Black', 'states_g', 'states_b', 'States'])
    df1 = df.groupby('Type').apply(lambda x: x.groupby('Model').mean())
    df1['Explored% Grey'] = np.round(100*df1['states_g']/df1['States']).astype('int32')
    df1['Explored% Black'] = np.round(100*df1['states_b']/df1['States']).astype('int32')
    df1['States'] = df1['States'].astype('int32')
    df1.sort_values(['Type', 'Model'])
    df1['Explored % (Grey/Black)'] = df1['Explored% Grey'].map(str) + '/' + df1['Explored% Black'].map(str)

    # Restrict table to columns present in Table 1
    df2 = df1[['States', 'Explored % (Grey/Black)', 'Precision Grey', 'Precision Black']]

    # Compute log10(m)
    param_strings_subset = [param_strings[model] for model in [df1.index.levels[1][x] for x in df1.index.labels[1]]]
    df2['log10(m)'] = np.vectorize(compute_m)(param_strings_subset)
else:
    df2 = []
    print("Please run the previous cell. raw_results is empty.")

# Display the table
df2<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.16006660392383987, 'fraction_numerical': 0.04300296821834504, 'mean_word_length': 2.445747069094537, 'pattern_counts': {'":': 83, '<': 18, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 7, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '3', 'dir': 'jupyter-structured-clean-dedup', 'id': '374088', 'license': 'MIT', 'n_tokens_mistral': 5107, 'n_tokens_neox': 4721, 'n_words': 962, 'path': 'src/prism-fruit/Games-DQL/data/ArtifactEvaluation.ipynb', 'repo_name': 'kushgrover/apt-vs-dift', 'size': '13813'}