Commit 50fe2004 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLQuery: fix confusing attribute: dim_variant_prop -> dim_variant

parent 308cb6f6
......@@ -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)
......
......@@ -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)
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment