[lib] MCLAnalyser: Try to understand undocumented function...

library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py

@@ -749,18 +749,34 @@ class MCLAnalyser(object):
 
         final property becomes the invariant property
         => Ex: test if "C3 and C4" will never append if start property is "A1 and C1 and B1"
+        Cf TestMCLAnalyser...
 
         @return: False if the problem is satisfiable, True otherwise
         @param act_sol: FrontierSolution with activation condition
         @param query: the query used for act_sol condition
         """
-        nb_step = len(act_sol.ic_sequence) - 1
-        query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol,
-                                                               self.unfolder)
-        inv_prop = 'not('+query.final_prop+')'
+        max_step = len(act_sol.ic_sequence) - 1
+        print("max steps:", max_step)
+
+        # Same timings, force inactivated frontiers
+        query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol, self.unfolder)
+
+        inv_prop = 'not(' + query.final_prop + ')'
+        #(None, None, 'A1 and C1 and B1', ['', 'h2', '', ''])
+        print("naive query1:", query_1.final_prop, query_1.inv_prop,
+              query_1.start_prop, query_1.variant_prop)
+
         query_2 = MCLSimpleQuery(None, inv_prop, None)
+        #(None, 'not(C3 and C4)', None, [])
+        print("query 2:", query_2.final_prop, query_2.inv_prop,
+              query_2.start_prop, query_2.variant_prop)
         query_1 = query_2.merge(query_1)
-        return not(self.sq_is_satisfiable(query_1, nb_step))
+        #(None, 'not(C3 and C4)', 'A1 and C1 and B1', ['', 'h2', '', '']
+        print("merged query1:", query_1.final_prop, query_1.inv_prop,
+              query_1.start_prop, query_1.variant_prop)
+
+        return not(self.sq_is_satisfiable(query_1, max_step))
+
 
     def next_inhibitor(self, mac, query):
         """