formula_generator.py 9.45 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


164
def write_formula(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
170
171
172
173
    filename_pmcsog = f"{filename_ltsmin}.reduced"

    with open(os.path.join(base, filename_ltsmin), 'w') as ltsmin, \
        open(os.path.join(base, filename_pmcsog), 'w') as pmcsog:

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

179
180
181
182
183
184
185
186
        ltsmin.write(formula)
        pmcsog.write(pmcsog_formula)


def generate_formulas(model_name,
                      model_instance,
                      n,
                      timeout,
187
                      min_states,
188
                      min_explored_states,
189
190
                      paths,
                      save=True):
191
    """Generates N satisfied and N violated formulas"""
192
193
194
    true_formulas = []
    false_formulas = []

195
    random_formulas = generate_spot_formulas(model_name, model_instance,
Jaime Arias's avatar
Jaime Arias committed
196
                                             100000, paths)
197

198
    formula_id = 1
199
200
201
202
203
    for f in random_formulas:
        if len(true_formulas) == n and len(false_formulas) == n:
            break

        is_satisfied = check_formula(model_name, model_instance, f, timeout,
204
                                     min_states, paths)
205
206
207
208
209
210
211

        # if timeout or error during the verification
        if (is_satisfied is None):
            continue

        # add to formulas satisfied
        if is_satisfied and len(true_formulas) < n:
Jaime Arias's avatar
Jaime Arias committed
212
213
214
215
216
217
218
            # 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

219
            true_formulas.append(f)
220
            write_formula(model_name, model_instance, f, formula_id, paths)
221
            formula_id = formula_id + 1
222
223
224
225

        # add to formulas violated
        if not is_satisfied and len(false_formulas) < n:
            false_formulas.append(f)
226
            write_formula(model_name, model_instance, f, formula_id, paths)
227
            formula_id = formula_id + 1
228

229
230
231
    return {'satisfied': true_formulas, 'violated': true_formulas}


232
233
234
235
def generate_all_formulas(model_name,
                          model_instances,
                          n,
                          timeout,
236
                          min_states,
237
                          min_explored_states,
238
239
240
241
                          paths,
                          save=True):
    for model_instance in model_instances:
        formulas = generate_formulas(model_name, model_instance, n, timeout,
242
243
                                     min_states, min_explored_states, paths,
                                     save)
244
        print(model_instance, formulas)
245

246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261

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,
262
                        help='timeout of verification (s)')
263

264
265
266
267
268
269
    parser.add_argument('--min_states',
                        type=int,
                        nargs=1,
                        required=True,
                        help='minimum number of states')

270
271
272
273
274
275
    parser.add_argument('--min_explored_states',
                        type=int,
                        nargs=1,
                        required=True,
                        help='minimum number of explored states')

276
277
278
279
280
281
282
283
284
285
286
287
288
    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()
289
290


291
if __name__ == '__main__':
292
293
    args = parse_arguments()

294
295
296
    # default paths of the project
    paths = get_default_paths()

297
298
    n_formulas = args.n[0]
    timeout = args.timeout[0]
299
    min_states = args.min_states[0]
300
    min_explored_states = args.min_explored_states[0]
301
302
303
304
    model_name = args.model_name[0]
    model_instances = args.model_instance

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