feature: add constraint to a minimum of 1000 number of states

scripts/formula_generator.py

@@ -86,7 +86,8 @@ def generate_spot_formulas(model_name, model_instance, n, paths):
     return formulas
 
 
-def check_formula(model_name, model_instance, formula, timeout, paths):
+def check_formula(model_name, model_instance, formula, timeout, min_states,
+                  paths):
     """Check whether a property is satisfied or not"""
     tool = paths['pnml2lts-mc']
 
@@ -102,13 +103,17 @@ def check_formula(model_name, model_instance, formula, timeout, paths):
 
     match_false = re.search(r'Accepting cycle FOUND', ltsmin_out)
     match_time = re.search(r'Total exploration time (\d+(\.\d+)?)', ltsmin_out)
+    match_states = re.search(r'State space has (\d+) states', ltsmin_out)
 
     # ignore formulas with time zero
     if match_time:
-        time = float(match_time.group(1))
-        if (time > 0.0):
+        # time = float(match_time.group(1))
+        nb_states = int(match_states.group(1))
+
+        if (nb_states >= min_states):
             # print("* property: {}\n  - it is satisfied: {}\n  - time: {} s".
             #       format(formula, not match_false, time))
+
             return not match_false
 
     return None
@@ -158,6 +163,7 @@ def generate_formulas(model_name,
                       model_instance,
                       n,
                       timeout,
+                      min_states,
                       paths,
                       save=True):
     """Generates N satisfied and N violated formulas"""
@@ -173,7 +179,7 @@ def generate_formulas(model_name,
             break
 
         is_satisfied = check_formula(model_name, model_instance, f, timeout,
-                                     paths)
+                                     min_states, paths)
 
         # if timeout or error during the verification
         if (is_satisfied is None):
@@ -198,11 +204,12 @@ def generate_all_formulas(model_name,
                           model_instances,
                           n,
                           timeout,
+                          min_states,
                           paths,
                           save=True):
     for model_instance in model_instances:
         formulas = generate_formulas(model_name, model_instance, n, timeout,
-                                     paths, save)
+                                     min_states, paths, save)
         print(model_instance, formulas)
 
 
@@ -223,6 +230,12 @@ def parse_arguments():
                         required=True,
                         help='timeout of verification')
 
+    parser.add_argument('--min_states',
+                        type=int,
+                        nargs=1,
+                        required=True,
+                        help='minimum number of states')
+
     parser.add_argument('--model-name',
                         type=str,
                         nargs=1,
@@ -246,8 +259,9 @@ if __name__ == '__main__':
 
     n_formulas = args.n[0]
     timeout = args.timeout[0]
+    min_states = args.min_states[0]
     model_name = args.model_name[0]
     model_instances = args.model_instance
 
     generate_all_formulas(model_name, model_instances, n_formulas, timeout,
-                          paths)
+                          min_states, paths)