oar_formula_generator.py 4.65 KB
Newer Older
Jaime Arias's avatar
Jaime Arias committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
#!/usr/bin/env python3

import os
import stat

oar_header = """\
#!/bin/bash
#
#OAR --name {job_name}
#OAR --resource /nodes={nodes}/cpu=1/core={threads},walltime={walltime}:00:00
#OAR --stderr {error}
#OAR --stdout {output}

# Formula generator

"""


def create_folder(path):
    """Creates a folder if it does not exist

    Parameters
    ----------
    path : str
        Path of the new folder

    Examples
    --------

    >>> create_folder('./results')
    """
    if not os.path.exists(path):
        os.makedirs(path)


def create_default_paths():
    """Create the default path for the project"""
    base_folder = os.path.abspath(
        os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))

    paths = {
        # Absolute path where are stored the formulas, models, and scripts
        'project': base_folder,
        # Folder where the formulas are saved
        'formulas': os.path.join(base_folder, "formulas"),
        # Folder where the models are saved
        'models': os.path.join(base_folder, "models"),
        # Folder where the results will be saved
        'results': os.path.join(base_folder, "results"),
        # Folder where the oar batches will be saved
        'oar': os.path.join(base_folder, "oar"),
        # Folder where the scripts are saved
        'scripts': os.path.join(base_folder, "scripts"),
        # Folder where the tool are saved
        'tools': os.path.join(base_folder, "tools")
    }

    # Create paths if they don't exist
    for path in paths.values():
        create_folder(path)

    return paths


def command(model_name, model_instance, n_formulas, min_states,
            min_explored_states, timeout, paths):
    command = os.path.join(paths["scripts"], "formula_generator.py")
    return f"{command} --n {n_formulas} --timeout {timeout} --min_states {min_states} --min_explored_states {min_explored_states} --model-name {model_name} --model-instance {model_instance}"


def generate_oar(model_name, model_instance, n_formulas, min_states,
                 min_explored_states, timeout, threads, walltime, paths):
    oar_folder = os.path.join(paths['oar'], "formulas", model_name)
    create_folder(oar_folder)
    header = oar_header.format(job_name=f"f_gen_{model_instance}",
                               error=os.path.join(oar_folder,
                                                  f"{model_instance}.err"),
                               output=os.path.join(oar_folder,
                                                   f"{model_instance}.out"),
                               nodes=1,
                               threads=threads,
                               walltime=walltime)

    oar_name = f"{model_instance}.oar"
    oar_file = os.path.join(oar_folder, oar_name)

    with open(oar_file, 'w') as fd:
        fd.write(header)

        srun_command = command(
            model_name, model_instance, n_formulas,
            min_states, min_explored_states, timeout, paths)
        fd.write(srun_command)
        fd.write("\n\n")

    #  give oar script the exec right
    st = os.stat(oar_file)
    os.chmod(oar_file, st.st_mode | stat.S_IEXEC)


def generate_multiple_oars(models, n_formulas, min_states,
                           min_explored_states, timeout, threads, walltime, paths):
    for model_object in models:
        model_name = model_object["name"]
        for model_instance in model_object["instances"]:
            generate_oar(model_name, model_instance, n_formulas, min_states,
                         min_explored_states, timeout, threads, walltime, paths)


if __name__ == '__main__':
    # Default paths
    paths = create_default_paths()

    # Timeout for a batch: 10 hours
    walltime = 10

    # Timeout for an ltsmin run: 5 minutes
    timeout = 5

    # Formulas to be verified
    n_formulas = 100

    # Minimum number of states in the generated state space
    min_states = 1000

    # Minimum number of states explored by the model checker
    min_explored_states = 1000000

    # Number of threads to run the model-checker
    threads = 16

    # Models to be run
    models = [{
        "name": "philo",
        "instances": ["philo5", "philo10", "philo20"]
    }, {
        "name": "train",
        "instances": ["train12", "train24", "train48", "train96"]
    }, {
        "name": "tring",
        "instances": ["tring5", "tring10", "tring20"]
    }, {
        "name":
        "robot",
        "instances": ["robot2", "robot5", "robot10", "robot20", "robot50"]
    }, {
        "name": "spool",
        "instances": ["spool1", "spool2", "spool3", "spool4", "spool5"]
    }]

    generate_multiple_oars(models, n_formulas, min_states,
                           min_explored_states, timeout, threads, walltime, paths)