From 50fe2004448176b155f559db2c3d3ba9a2cb9321 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Fri, 20 Dec 2019 00:45:03 +0100
Subject: [PATCH] [lib] MCLQuery: fix confusing attribute: dim_variant_prop ->
dim_variant
---
.../models/clause_constraints/mcl/CLUnfolder.py | 10 +++++-----
.../models/clause_constraints/mcl/MCLAnalyser.py | 4 ++--
.../cadbiom/models/clause_constraints/mcl/MCLQuery.py | 8 ++++----
3 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 40796b9..6091095 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -52,7 +52,7 @@ MCLSimpleQuery (reminder):
Ex: start_prop, inv_prop, final_prop, variant_prop
- Attributes in DIMACS format: These are logical formulas encoded in
the form of clauses containing numerical values.
- Ex: dim_start, dim_inv, dim_final, dim_variant_prop
+ Ex: dim_start, dim_inv, dim_final, dim_variant
---
@@ -428,10 +428,10 @@ class CLUnfolder(object):
values = set(it.chain(*query.dim_start))
values.update(it.chain(*query.dim_final))
values.update(it.chain(*query.dim_inv))
- if query.dim_variant_prop:
+ if query.dim_variant:
# Handle empty steps:
# Ex: [[], [[4]], [[6], [7]], []]
- g = (step for step in query.dim_variant_prop if step)
+ g = (step for step in query.dim_variant if step)
[values.update(it.chain(*step)) for step in g]
# Get all values that are not in the initial dynamic system
@@ -453,7 +453,7 @@ class CLUnfolder(object):
Following attributes are used from the query:
start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
- variant_prop, dim_variant_prop, steps_before_check
+ variant_prop, dim_variant, steps_before_check
Textual properties of query are compiled into numeric clauses in
init_forward_unfolding(), just at the beginning of squery_is_satisfied()
@@ -491,7 +491,7 @@ class CLUnfolder(object):
# It's the trajectory of events of a solution.
self.__variant_property = query.variant_prop # logical formula in text
- self.__dimacs_variant = query.dim_variant_prop
+ self.__dimacs_variant = query.dim_variant
# For reachability optimisation. Number of shifts before checking
# the final property (default 0)
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index ece3473..15b2075 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
@@ -489,7 +489,7 @@ class MCLAnalyser(object):
# Initialise the unfolder with the given query
# Following properties are used from the query:
# start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
- # variant_prop, dim_variant_prop, steps_before_check
+ # variant_prop, dim_variant, steps_before_check
self.unfolder.init_with_query(query, check_query=False)
# go
return self.unfolder.squery_is_satisfied(max_step)
@@ -559,7 +559,7 @@ class MCLAnalyser(object):
# Initialise the unfolder with the given query
# Following properties are used from the query:
# start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
- # variant_prop, dim_variant_prop, steps_before_check
+ # variant_prop, dim_variant, steps_before_check
self.unfolder.init_with_query(query, check_query=False)
# go
return self.unfolder.squery_solve(vvars, max_step, max_sol)
diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py b/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
index 94b0c8b..7dc6929 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLQuery.py
@@ -59,7 +59,7 @@ class MCLSimpleQuery(object):
Ex: start_prop, inv_prop, final_prop, variant_prop
- Attributes in DIMACS format: These are logical formulas encoded in
the form of clauses containing numerical values.
- Ex: dim_start, dim_inv, dim_final, dim_variant_prop
+ Ex: dim_start, dim_inv, dim_final, dim_variant
Textual properties of query are compiled into numeric clauses in the unfolder
with init_forward_unfolding(), just at the beginning of squery_is_satisfied()
@@ -78,7 +78,7 @@ class MCLSimpleQuery(object):
:param dim_start: start property in DIMACS form - optional
:param dim_inv: invariant property in DIMACS form - optional
:param dim_final: final property in DIMACS form - optional
- :param dim_variant_prop: list of lists of dimacs clauses
+ :param dim_variant: list of lists of dimacs clauses
:param steps_before_check: Number of shifts before testing the
final property - optional
@@ -90,7 +90,7 @@ class MCLSimpleQuery(object):
:type dim_start: <list <DClause>>, default []
:type dim_inv: <list <DClause>>, default []
:type dim_final: <list <DClause>>, default []
- :type dim_variant_prop: <list <list <DClause>>
+ :type dim_variant: <list <list <DClause>>
:type steps_before_check: <int>, default value 0
NB: DClause: A clause coded as a list of DIMACS coded literals: <list <int>>
@@ -122,7 +122,7 @@ class MCLSimpleQuery(object):
self.dim_start = [] # list<DClause>
self.dim_inv = [] # list<DClause>
self.dim_final = [] # list<DClause>
- self.dim_variant_prop = [] # list<list<DClause>>
+ self.dim_variant = [] # list<list<DClause>>
self.steps_before_check = 0
--
GitLab