formula_generator.py 11.5 KB
Newer Older
1
2
3
4
5
6
#!/usr/bin/env python3

import os
import xml.etree.ElementTree as etree
import subprocess
import re
7
import argparse
8
9


10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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)


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
def execute_command(command):
    """Run a command in the shell"""
    output = None
    try:
        output = subprocess.check_output(
            command, shell=True, stderr=subprocess.STDOUT).decode("utf-8")
    except Exception as e:
        output = e.output.decode("utf-8")
    except KeyboardInterrupt:
        pass

    return output


def get_atomic_propositions(pnml_file):
    """Returns the atomic propositions from a PNML file"""
    xml_tree = etree.parse(pnml_file)
    root = xml_tree.getroot()
    ns = {'pnml': root.tag[1:].split("}")[0]}

    places = [p.get('id') for p in root.findall('.//pnml:place', ns)]
    transitions = [t.get('id') for t in root.findall('.//pnml:transition', ns)]

    return {'places': places, 'transitions': transitions}


def generate_spot_formulas(model_name, model_instance, n, paths):
    """Generates a number of formulas for a specific PNML model

    Parameters
    ----------
    model_name : str
        Name of model
    model_instance : str
        Instance of the model
    n : int
        Number of formulas to be generated
    paths : dict of str
        Paths of the project

    Returns
    -------
    list of str
        list with formulas
    """
    ignored_operators = "X=0,xor=0,W=0,M=0,R=0,U=0"

    pnml_file = os.path.join(paths['models'], model_name,
                             f'{model_instance}.pnml')

    atomic_propositions = get_atomic_propositions(pnml_file)
78
79
    atomic_propositions = " ".join(
        [f"{ap}==1" for ap in atomic_propositions['places']])
80
81
82
83
84
85
86
87
88

    command = f'{paths["randltl"]} -L -s -p -n{n} --ltl-priorities="{ignored_operators}" {atomic_propositions}'

    output = execute_command(command)
    formulas = output.split('\n')[:-1]

    return formulas


89
90
def check_formula(model_name, model_instance, formula, timeout, min_states,
                  paths):
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
    """Check whether a property is satisfied or not"""
    tool = paths['pnml2lts-mc']

    model_file = os.path.join(paths['models'], model_name,
                              f"{model_instance}.pnml")

    command = f'{tool} --strategy=ndfs --timeout={timeout} --ltl="{formula}" {model_file}'
    ltsmin_out = execute_command(command)

    # timeout or error found
    if (ltsmin_out is None):
        return None

    match_false = re.search(r'Accepting cycle FOUND', ltsmin_out)
    match_time = re.search(r'Total exploration time (\d+(\.\d+)?)', ltsmin_out)
106
    match_states = re.search(r'State space has (\d+) states', ltsmin_out)
107
108
109

    # ignore formulas with time zero
    if match_time:
110
111
112
        nb_states = int(match_states.group(1))

        if (nb_states >= min_states):
Jaime Arias's avatar
Jaime Arias committed
113
            print("# states (state space):", nb_states)
114
115
116
117
118
            return not match_false

    return None


119
120
121
122
123
124
125
126
127
128
129
130
def check_explored_states(model_name, model_instance, formula, time_out,
                          min_explored_states, paths):
    """Checks the number of states visited by the model checker"""
    tool = paths['pnml2lts-mc']
    model_file = os.path.join(paths['models'], model_name,
                              f"{model_instance}.pnml")

    command = f'{tool} --strategy=dfs --timeout={timeout*60} --ltl="{formula}" {model_file}'
    ltsmin_out = execute_command(command)

    # timeout or error found
    if (ltsmin_out is None):
Jaime Arias's avatar
Jaime Arias committed
131
        return False
132
133
134
135
136

    match_regex_explored = re.search(r'Explored (\d+) states', ltsmin_out)

    if match_regex_explored:
        nb_explored_states = int(match_regex_explored.group(1))
Jaime Arias's avatar
Jaime Arias committed
137
        print("# explored states: ", nb_explored_states)
Jaime Arias's avatar
Jaime Arias committed
138
        return nb_explored_states >= min_explored_states
139

Jaime Arias's avatar
Jaime Arias committed
140
    return False
141
142


143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
def get_default_paths():
    """Returns the default path of the project"""

    # Absolute path where are stored the formulas, models
    base_folder = os.path.abspath(
        os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))

    paths = {
        # randltl path: this tool generates random formulas
        "randltl": "randltl",
        # tool to verify the property
        'pnml2lts-mc': os.path.join(base_folder, "tools", "pnml2lts-mc"),
        # Folder where the models are saved
        'models': os.path.join(base_folder, "models"),
        # Folder where the formulas are saved
        'formulas': os.path.join(base_folder, "formulas"),
    }

    return paths


Jaime Arias's avatar
Jaime Arias committed
164
def write_formula(result, model_name, model_instance, formula, identifier, paths):
165
166
    """write a formula into a file"""
    base = os.path.join(paths['formulas'], model_name, model_instance)
167
168
    create_folder(base)
    filename_ltsmin = f"{model_instance}-{identifier}.ltl"
169
    filename_pmcsog = f"{filename_ltsmin}.reduced"
Jaime Arias's avatar
Jaime Arias committed
170
    filename_results = "formula_results"
171
172

    with open(os.path.join(base, filename_ltsmin), 'w') as ltsmin, \
Jaime Arias's avatar
Jaime Arias committed
173
174
        open(os.path.join(base, filename_pmcsog), 'w') as pmcsog, \
        open(os.path.join(base, filename_results), 'a') as results:
175

176
177
178
179
180
        # remove ==1 and add " to atomic propositions
        pmcsog_formula = re.sub(pattern=r'\((\w*\d*)==1\)',
                                repl='("\\1")',
                                string=formula)

181
182
        ltsmin.write(formula)
        pmcsog.write(pmcsog_formula)
Jaime Arias's avatar
Jaime Arias committed
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
        results.write(f"{identifier};{result}\n")

        
def get_instance_stats(model_name, model_instance):
    """get the next formula id for a model instance and the number of true
    and false formulas already computed."""
    base = os.path.join(paths['formulas'], model_name, model_instance)
    filename_results = os.path.join(base, "formula_results")
    if not os.path.exists(filename_results):
        return 1, 0, 0
    true_formulas = 0
    false_formulas = 0
    with open(filename_results, 'r') as fd:
        formulas = fd.read().split('\n')
        for line in formulas:
            id_result = line.split(';')
            if len(id_result) != 2:
                break
            if id_result[1].lower() == 'true':
                true_formulas += 1
            else:
                false_formulas += 1
        return len(formulas), true_formulas, false_formulas
206
207
208
209
210
211


def generate_formulas(model_name,
                      model_instance,
                      n,
                      timeout,
212
                      min_states,
213
                      min_explored_states,
214
                      paths,
Jaime Arias's avatar
Jaime Arias committed
215
216
                      save=True,
                      max_retries=5):
217
    """Generates N satisfied and N violated formulas"""
218
219
    true_formulas = []
    false_formulas = []
Jaime Arias's avatar
Jaime Arias committed
220
221
    unknown_formulas = []  #  subset of true_formulas for which ltsmin
                           #  timed out max_retries times
222

223
    random_formulas = generate_spot_formulas(model_name, model_instance,
Jaime Arias's avatar
Jaime Arias committed
224
                                             100000, paths)
225

Jaime Arias's avatar
Jaime Arias committed
226
227
228
229
    formula_id, nb_true, nb_false = get_instance_stats(model_name, model_instance)
    print(f"I still have {max(0, n - nb_true)} true formulas, " +
          f"and {max(0, n - nb_false)} false formulas to generate.\n" +
          f"I will start from formula id {formula_id}.")
230
    for f in random_formulas:
Jaime Arias's avatar
Jaime Arias committed
231
        if len(true_formulas) + nb_true >= n and len(false_formulas) + nb_false >= n:
232
233
            break

Jaime Arias's avatar
Jaime Arias committed
234
235
236
237
238
239
240
241
        #  launch ltsmin at most max_retries times until a run terminates
        for _ in range(max_retries):
            is_satisfied = check_formula(model_name, model_instance, f, timeout,
                                         min_states, paths)

            #  run terminated successfuly
            if is_satisfied is not None:
                break
242

Jaime Arias's avatar
Jaime Arias committed
243
244
245
246
247
        #  no run terminated after max_retries attempts => claim the
        #  property is verified (even if we're not sure)
        is_unknown = is_satisfied is None
        if is_satisfied is None:
            is_satisfied = True
248
249

        # add to formulas satisfied
Jaime Arias's avatar
Jaime Arias committed
250
        if is_satisfied and len(true_formulas) + nb_true < n:
Jaime Arias's avatar
Jaime Arias committed
251
252
253
254
255
256
257
            # if number of explored states is not satisfied
            has_explored_states = check_explored_states(
                model_name, model_instance, f, timeout, min_explored_states,
                paths)
            if not has_explored_states:
                continue

Jaime Arias's avatar
Jaime Arias committed
258
            print('### true formula found: ', f)
259
            true_formulas.append(f)
Jaime Arias's avatar
Jaime Arias committed
260
261
262
            if is_unknown:
                unknown_formulas.append(f)
            write_formula(True, model_name, model_instance, f, formula_id, paths)
263
            formula_id = formula_id + 1
264
265

        # add to formulas violated
Jaime Arias's avatar
Jaime Arias committed
266
267
        if not is_satisfied and len(false_formulas) + nb_false < n:
            print('### false formula found: ', f)
268
            false_formulas.append(f)
Jaime Arias's avatar
Jaime Arias committed
269
            write_formula(False, model_name, model_instance, f, formula_id, paths)
270
            formula_id = formula_id + 1
271

Jaime Arias's avatar
Jaime Arias committed
272
273
274
    return {'satisfied': true_formulas,
            'violated': false_formulas,
            'unknown': unknown_formulas}
275
276


277
278
279
280
def generate_all_formulas(model_name,
                          model_instances,
                          n,
                          timeout,
281
                          min_states,
282
                          min_explored_states,
283
284
285
286
                          paths,
                          save=True):
    for model_instance in model_instances:
        formulas = generate_formulas(model_name, model_instance, n, timeout,
287
288
                                     min_states, min_explored_states, paths,
                                     save)
289
        print(model_instance, formulas)
290

291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306

def parse_arguments():
    """Creates the command line interface"""
    parser = argparse.ArgumentParser(
        description='Generates formulas for a model')

    parser.add_argument('--n',
                        type=int,
                        nargs=1,
                        required=True,
                        help='number of formulas')

    parser.add_argument('--timeout',
                        type=int,
                        nargs=1,
                        required=True,
307
                        help='timeout of verification (s)')
308

309
310
311
312
313
314
    parser.add_argument('--min_states',
                        type=int,
                        nargs=1,
                        required=True,
                        help='minimum number of states')

315
316
317
318
319
320
    parser.add_argument('--min_explored_states',
                        type=int,
                        nargs=1,
                        required=True,
                        help='minimum number of explored states')

321
322
323
324
325
326
327
328
329
330
331
332
333
    parser.add_argument('--model-name',
                        type=str,
                        nargs=1,
                        required=True,
                        help='Name of the model (e.g. philo)')

    parser.add_argument('--model-instance',
                        type=str,
                        nargs='+',
                        required=True,
                        help='Instances of the model (e.g. philo10)')

    return parser.parse_args()
334
335


336
if __name__ == '__main__':
337
338
    args = parse_arguments()

339
340
341
    # default paths of the project
    paths = get_default_paths()

342
343
    n_formulas = args.n[0]
    timeout = args.timeout[0]
344
    min_states = args.min_states[0]
345
    min_explored_states = args.min_explored_states[0]
346
347
348
349
    model_name = args.model_name[0]
    model_instances = args.model_instance

    generate_all_formulas(model_name, model_instances, n_formulas, timeout,
350
                          min_states, min_explored_states, paths)