Skip to content

GitLab

Commit f1c6b605 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: Clean; delete useless setters; add doc

parent 83590d6f
Hide whitespace changes
Inline Side-by-side
library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
View file @ f1c6b605
......@@ -91,25 +91,26 @@ class CLUnfolder(object):
# shift_step equal to the total number of coded variables
# shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
self.shift_step_init = dynamic_system.get_var_number() # shift step of system
self.__shift_step = self.shift_step_init # current shift/step
self.__shift_step = self.shift_step_init # current shift/step
self.__locked = False
self.__current_step = 1
self.__steps_before_check = 0
self.__include_aux_clauses = True
self.__lit_cpt = self.__shift_step + 1 # counter for aux. var. coding
# assign a DIMACS code number to each variable (invariant)
self.__lit_cpt = self.__shift_step +1 # counter for aux. var. coding
self.__var_code_table = dict() # name -> DIMACS code
self.__var_list = ['##'] # DIMACS code -> name - != 0
# Create mappings between names and values of the variables of the system
# dynamic_system.base_var_set : Set of ALL variables of the dynamic system
# (including auxiliary ones and clocks/events).
self.__var_code_table = dict() # Mapping: name -> DIMACS code (!= 0)
self.__var_list = ['##'] # Mapping: DIMACS code (!= 0) -> name
# Create mappings between names and variables of the system
# dynamic_system.base_var_set : set of variables of the dynamic system
# (including aux vars)
# Fix order of variables names with a list:
# indexes of __var_list are the values of the variables at these indexes
# keys of __var_code_table are the names of the variables, and the values theirvalues
# - indexes of __var_list are the values of the variables at these indexes
# - values begin from 1 (0 is a blacklisted value)
base_var_set = list(dynamic_system.base_var_set)
self.__var_list += base_var_set
# keys: are the names of the variables, values: their values
self.__var_code_table = {var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}
assert len(self.__var_code_table) == self.__shift_step
......@@ -119,11 +120,12 @@ class CLUnfolder(object):
self.__aux_code_table = dict() # name 2 code
self.__aux_list = [] # code to name
# list no_frontier place DIMACS codes
self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.__dyn_sys.no_frontier]
# ordered list of DIMACS codes of the simple variables/places
# Disable all variables of places (entities) in the model (except frontiers)
self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.__dyn_sys.no_frontiers]
# ordered list of DIMACS code of the frontier place variables
self.frontier_values = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontier]
# ordered list of DIMACS codes of the frontier variables/places
self.frontier_values = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontiers]
self.frontier_values.sort() ## TODO: sort utile ici ???? si non passer en frozenset et supprimer les casts partout ailleurs
# Convenient attribute for RawSolution.extract_frontier_values()
# all frontiers and their opposite version
......@@ -183,20 +185,20 @@ class CLUnfolder(object):
"""Reset the unfolder before a new query
This function is called from the constructor and during
MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions() with the
call of init_with_query().
MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
following the call of init_with_query().
"""
# Properties to be checked
self.__initial_property = None # string
self.__dim_initial = None # list of dimacs clauses
self.__final_property = None # idem
self.__dim_final = None
self.__invariant_property = None # idem
self.__dim_invariant = None
self.__initial_property = None # logical formula - literal boolean expression
self.__dim_initial = None # list of DIMACS clauses
self.__final_property = None # logical formula
self.__dim_final = None # list of DIMACS clauses
self.__invariant_property = None # logical formula
self.__dim_invariant = None # list of DIMACS clauses
self.__variant_property = None # list<logic formulas>
self.__dim_variant = None # list<list<dimacs clauses>>
self.__dim_variant = None # list<list<DIMACS clauses>>
# list of variant temporal constraints in Dimacs ground code
self.__list_variant_constraints = None # list<list<dimacs clauses>>
self.__list_variant_constraints = None # list<list<DIMACS clauses>>
# If called from the constructor, for now these variables are just redefined here
self.__steps_before_check = 0
......@@ -206,50 +208,43 @@ class CLUnfolder(object):
def init_with_query(self, query):
"""Initialise the unfolder with the given query
Following properties are used from the query:
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_reach
"""
# Reset the unfolder before a new query
self.reset()
# Init with properties
self.set_initial_property(query.start_prop)
self.set_dim_initial_property(query.dim_start)
self.set_current_property(query.inv_prop)
self.set_dim_current_property(query.dim_inv)
self.set_final_property(query.final_prop)
self.set_dim_final_property(query.dim_final)
self.set_variant_property(query.variant_prop)
self.set_dim_variant_property(query.dim_variant_prop)
self.set_minimal_steps(query.steps_before_reach) ## TODO check this value
# Init with query properties and clauses
self.__initial_property = query.start_prop
self.__dim_initial = query.dim_start
self.__final_property = query.final_prop
self.__dim_final = query.dim_final
self.__invariant_property = query.inv_prop
self.__dim_invariant = query.dim_inv
# It's the trajectory of events of a solution.
self.__variant_property = query.variant_prop
self.__dim_variant = query.dim_variant_prop
# For reachability optimisation. Number of shift before checking
self.__steps_before_check = query.steps_before_reach
def set_stats(self):
"""
Enable solver statistics
"""
"""Enable solver statistics (for tests)"""
self.__stats = True
self.__nb_vars = 0
self.__nb_clauses = 0
def unset_stats(self):
"""
disable solver statistics
"""
"""Disable solver statistics (never used)"""
self.__stats = False
def _stats(self):
"""
print solver statistics
"""
print "\n NB Variables in solver: ", self.__nb_vars
print "NB Clauses in solver: ", self.__nb_clauses
def set_minimal_steps(self, nb_steps):
"""
For reachability optimisation. number of shift before checking
"""
self.__steps_before_check = nb_steps
"""Display solver statistics"""
print("\n NB Variables in solver:", self.__nb_vars)
print("NB Clauses in solver:", self.__nb_clauses)
def set_include_aux_clauses(self, val):
"""
......@@ -259,38 +254,32 @@ class CLUnfolder(object):
"""
self.__include_aux_clauses = val
# internal variable access for tests
## internal variable access for tests (never used) #########################
def vars_in_clause(self, clause):
"""DEBUG: Return variables names from values in the given clause"""
return [self.get_var_indexed_name(var) for var in clause]
def get_dynamic_constraints(self):
"""
For tests: returns coded dynamic constraints
"""
"""For tests: returns coded dynamic constraints"""
return self.__dynamic_constraints
def get_initial_constraints(self):
"""
For tests: returns coded initial constraints
"""
"""For tests: returns coded initial constraints"""
return self.__initial_constraints
def get_invariant_constraints(self):
"""
For tests: returns coded invariant constraints
"""
"""For tests: returns coded invariant constraints"""
return self.__invariant_constraints
def get_variant_constraints(self):
"""
For tests: returns coded variant constraints
"""
"""For tests: returns coded variant constraints"""
return self.__variant_constraints
def get_final_constraints(self):
"""
For tests: returns coded final constraints
"""
"""For tests: returns coded final constraints"""
self.__final_constraints
# variables management
## variables management ####################################################
def var_dimacs_code(self, var_name):
"""
returns dimacs code of (string) var_name variable
......@@ -668,19 +657,6 @@ class CLUnfolder(object):
self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
return prop_visitor.clauses
def set_initial_property(self, property_text):
"""
@param property_text: string - litteral boolean expression
"""
self.__initial_property = property_text
def set_dim_initial_property(self, dimacs_clause_list):
"""
set initial property with a DIMACS representation
@param dimacs_clause_list:
"""
self.__dim_initial = dimacs_clause_list
def __init_initial_constraint_0(self, no_frontier_init=True):
"""
if initial property is set, generate constraints clauses in numeric form
......@@ -719,19 +695,6 @@ class CLUnfolder(object):
if self.__dim_initial:
self.__initial_constraints += self.__dim_initial
def set_final_property(self, property_text):
"""
@param property_text: string - litteral boolean expression
"""
self.__final_property = property_text
def set_dim_final_property(self, dimacs_clause_list):
"""
set final property with a DIMACS representation
@param dimacs_clause_list:
"""
self.__dim_final = dimacs_clause_list
def __init_final_constraint_0(self):
"""
if final property is set, generate constraints clauses in numeric form
......@@ -752,21 +715,6 @@ class CLUnfolder(object):
if dim_fin:
self.__final_constraints = self.__final_constraints + dim_fin
def set_current_property(self, property_text):
"""
@param property_text: string - litteral boolean expression
"""
self.__invariant_property = property_text
def set_dim_current_property(self, dimacs_clause_list):
"""
set final property with a DIMACS representation
@param dimacs_clause_list:
"""
self.__dim_invariant = dimacs_clause_list
def __init_invariant_constraint_0(self):
"""
if trajectory property is set, generate constraints clauses in numeric form
......@@ -786,22 +734,6 @@ class CLUnfolder(object):
if d_inv:
self.__invariant_constraints = self.__invariant_constraints + d_inv
def set_variant_property(self, var_prop):
"""
@param var_prop: a list of logical formulas representing time varying
constraints. Each constraint uses ground (not shifted) variables.
The order of the list of constraints is always time increasing.
"""
self.__variant_property = var_prop
def set_dim_variant_property(self, dim_var_prop):
"""
@param dim_var_prop: a list list of dimacs clauses representing time
varying constraints. Each constraint uses ground (not shifted)
variable codes.
"""
self.__dim_variant = dim_var_prop
def __init_variant_constraints_0(self):
"""
if variant_property is set, compile each property into clauses and
......@@ -888,17 +820,6 @@ class CLUnfolder(object):
self.__shift_initial()
self.__shift_invariant()
# for debug
def vars_in_clause(self, clause):
"""
DEBUG
"""
lvar = []
for var in clause:
lvar.append(self.get_var_indexed_name(var))
return lvar
# solver interface
def __load_solver(self, solv):
"""
......
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