From 47391871257559c8d9ac2db78ab2cb1cf97dbfe0 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Wed, 20 Nov 2019 21:12:08 +0100
Subject: [PATCH] [lib] MCLAnalyser: Try to understand undocumented function...
---
.../clause_constraints/mcl/MCLAnalyser.py | 26 +++++++++++++++----
1 file changed, 21 insertions(+), 5 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index 9218924..d3b709f 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/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):
"""
--
GitLab