update repository

scripts/csv_generator.py

@@ -41,7 +41,7 @@ def get_time(experiment, tool):
         filename = "{}.{}".format(name, 'err')
 
         regex_true = re.compile(r'Empty product with LTL')
-        regex_false = re.compile(r'Accepting cycle FOUND')
+        regex_false = re.compile(r'Accepting cycle FOUND|Non-progress cycle FOUND')
         regex_time = re.compile(r'Total exploration time (\d+(\.\d+)?)')
     else:
         print('{} does not exists'.format(tool))

scripts/formula_generator.py

@@ -161,15 +161,17 @@ def get_default_paths():
     return paths
 
 
-def write_formula(model_name, model_instance, formula, identifier, paths):
+def write_formula(result, model_name, model_instance, formula, identifier, paths):
     """write a formula into a file"""
     base = os.path.join(paths['formulas'], model_name, model_instance)
     create_folder(base)
     filename_ltsmin = f"{model_instance}-{identifier}.ltl"
     filename_pmcsog = f"{filename_ltsmin}.reduced"
+    filename_results = "formula_results"
 
     with open(os.path.join(base, filename_ltsmin), 'w') as ltsmin, \
-        open(os.path.join(base, filename_pmcsog), 'w') as pmcsog:
+        open(os.path.join(base, filename_pmcsog), 'w') as pmcsog, \
+        open(os.path.join(base, filename_results), 'a') as results:
 
         # remove ==1 and add " to atomic propositions
         pmcsog_formula = re.sub(pattern=r'\((\w*\d*)==1\)',
@@ -178,6 +180,29 @@ def write_formula(model_name, model_instance, formula, identifier, paths):
 
         ltsmin.write(formula)
         pmcsog.write(pmcsog_formula)
+        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
 
 
 def generate_formulas(model_name,
@@ -187,28 +212,42 @@ def generate_formulas(model_name,
                       min_states,
                       min_explored_states,
                       paths,
-                      save=True):
+                      save=True,
+                      max_retries=5):
     """Generates N satisfied and N violated formulas"""
     true_formulas = []
     false_formulas = []
+    unknown_formulas = []  #  subset of true_formulas for which ltsmin
+                           #  timed out max_retries times
 
     random_formulas = generate_spot_formulas(model_name, model_instance,
                                              100000, paths)
 
-    formula_id = 1
+    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}.")
     for f in random_formulas:
-        if len(true_formulas) == n and len(false_formulas) == n:
+        if len(true_formulas) + nb_true >= n and len(false_formulas) + nb_false >= n:
             break
 
+        #  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)
 
-        # if timeout or error during the verification
-        if (is_satisfied is None):
-            continue
+            #  run terminated successfuly
+            if is_satisfied is not None:
+                break
+
+        #  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
 
         # add to formulas satisfied
-        if is_satisfied and len(true_formulas) < n:
+        if is_satisfied and len(true_formulas) + nb_true < n:
             # if number of explored states is not satisfied
             has_explored_states = check_explored_states(
                 model_name, model_instance, f, timeout, min_explored_states,
@@ -216,17 +255,23 @@ def generate_formulas(model_name,
             if not has_explored_states:
                 continue
 
+            print('### true formula found: ', f)
             true_formulas.append(f)
-            write_formula(model_name, model_instance, f, formula_id, paths)
+            if is_unknown:
+                unknown_formulas.append(f)
+            write_formula(True, model_name, model_instance, f, formula_id, paths)
             formula_id = formula_id + 1
 
         # add to formulas violated
-        if not is_satisfied and len(false_formulas) < n:
+        if not is_satisfied and len(false_formulas) + nb_false < n:
+            print('### false formula found: ', f)
             false_formulas.append(f)
-            write_formula(model_name, model_instance, f, formula_id, paths)
+            write_formula(False, model_name, model_instance, f, formula_id, paths)
             formula_id = formula_id + 1
 
-    return {'satisfied': true_formulas, 'violated': true_formulas}
+    return {'satisfied': true_formulas,
+            'violated': false_formulas,
+            'unknown': unknown_formulas}
 
 
 def generate_all_formulas(model_name,

scripts/oar_formula_generator.py

+#!/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)