Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 145a6d0c authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

Fix typos all around the code

parent 53c37f52
......@@ -309,7 +309,7 @@ def main():
# https://docs.python.org/dev/library/argparse.html#action
# all_macs to False by default
parser_input_file.add_argument('--all_macs', action='store_true',
help="Solver will try to search all macs with 0 to the maximum of "
help="Solver will try to search all macs from 0 to the maximum of "
"allowed steps.")
# continue to False by default
parser_input_file.add_argument('--continue', action='store_true',
......
......@@ -204,7 +204,7 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
i = len(previous_frontier_places)-1 if previous_frontier_places else 0
#with PyCallGraph(output=GraphvizOutput()):
while True:
print("START PROP:", current_start_prop)
LOGGER.info("%s:: START PROP: %s", final_prop, current_start_prop)
# EXIT
i += 1
......@@ -218,12 +218,12 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
mac_file, mac_step_file, mac_complete_file,
steps, final_prop, current_start_prop, inv_prop)
if ret:
frontier_places, min_steps = ret
else:
if not ret:
# No new solution/not satisfiable
return
frontier_places, min_steps = ret
# Add theese frontier places to set of previous ones
# (tuple is hashable)
previous_frontier_places.add(tuple(frontier_places))
......@@ -254,12 +254,12 @@ def find_macs(mcla,
steps, final_prop, start_prop, inv_prop):
"""__mac_exhaustive_search, on cherche d´abord des solutions non minimales
(lfsol = self.__sq_dimacs_frontier_solutions(query, nb_step, 2))
pour ensuite les élaguer en supprimer les places non essentielles à la
pour ensuite les élaguer en supprimant les places non essentielles à la
satisfiabilité de la propriété
(current_mac = self.__prune_frontier_solution(small_sol, query, nb_step)).
Ce processus récursif est le plus "time-consuming" car nous n´avons pas
le control sur les solutions fournies par SAT et les solutions non minimale
sont en générales tres éloignées de la solution minimale,
le controle sur les solutions fournies par SAT et les solutions non minimales
sont en général très éloignées de la solution minimale,
cad contiennent beaucoup plus de places.
:return: None
......@@ -319,7 +319,7 @@ def find_mac(mcla,
LOGGER.info("%s:: STOP the search!", final_prop)
return
# Find next MAC
# Find next MAC: Get FrontierSolution object
next_mac_object = mcla.next_mac(query, min_step)
if next_mac_object:
LOGGER.debug("%s:: Next MAC object:\n%s", final_prop, next_mac_object)
......
......@@ -2,8 +2,8 @@
## Filename : CLDynSys.py
## Author(s) : Michel Le Borgne
## Created : 05/2011
## Revision :
## Source :
## Revision :
## Source :
##
## Copyright 2011 : IRISA/IRSET
##
......@@ -34,8 +34,8 @@
## IRISA
## Symbiose team
## IRISA Campus de Beaulieu
## 35042 RENNES Cedex, FRANCE
##
## 35042 RENNES Cedex, FRANCE
##
##
## Contributor(s): Geoffroy Andrieux
##
......@@ -49,14 +49,14 @@ class Clause():
"""
def __init__(self, list_lit=[]):
self.list_of_literals = list_lit
def add_lit(self, lit):
"""
add a literal to the clause
@param lit: Literal object
"""
self.list_of_literals.append(lit)
def __str__(self):
"""
To print
......@@ -66,36 +66,36 @@ class Clause():
clause_string += lit.__str__()+', '
clause_string = clause_string + self.list_of_literals[-1].__str__()+'$'
return clause_string
def __repr__(self):
return self.__str__()
def equal(self, cl2):
"""
test if two clauses have the same literals
"""
if len(self.list_of_literals) != len(cl2.list_of_literals):
return False
return False
sc1 = sorted(self.list_of_literals, cmp=lit_cmp)
sc2 = sorted(cl2.list_of_literals, cmp=lit_cmp)
for i in range(len(sc1)):
if not lit_cmp(sc1[i], sc2[i]) == 0:
return False
return True
# helper functions mainly for tests
# helper functions mainly for tests
def clause_cmp(cl1, cl2):
"""
lexicographic order on ordered list of literals
"""
sc1 = sorted(cl1.list_of_literals, cmp=lit_cmp)
sc2 = sorted(cl2.list_of_literals, cmp=lit_cmp)
sc2 = sorted(cl2.list_of_literals, cmp=lit_cmp)
len1 = len(sc1)
len2 = len(sc2)
rlen = min(len1, len2)
for i in range(rlen):
cmp = lit_cmp(sc1[i], sc2[i])
# if not equal - clauses ordered as literals
# if not equal - clauses ordered as literals
if cmp != 0:
return cmp
# the shorter clause is a prefix of the longuest one
......@@ -105,7 +105,7 @@ def clause_cmp(cl1, cl2):
return 1
else:
return 0
def clause_list_equal(lc1, lc2):
"""
compare two clause lists
......@@ -118,37 +118,37 @@ def clause_list_equal(lc1, lc2):
if not slc1[i].equal(slc2[i]):
return False
return True
class Literal():
"""
Object representing literals.
A literal is a pair (string, boolean). The string is the variable name
and the boolean the sign of the literal.
A literal is a pair (string, boolean). The string is the variable name
and the boolean the sign of the literal.
"""
def __init__(self, name, sign):
self.name = name
self.sign = sign
def lit_not(self):
"""
returns the negation of the literal
"""
return Literal(self.name, not self.sign)
def equal(self, lit):
"""
literal equality
"""
return (lit.name == self.name) and (lit.sign == self.sign)
return (lit.name == self.name) and (lit.sign == self.sign)
def opposite(self, lit):
"""
true if one literal is the negation of the other
"""
return (lit.name == self.name) and (lit.sign == (not self.sign))
return (lit.name == self.name) and (lit.sign == (not self.sign))
def __str__(self):
"""
For printing
......@@ -157,7 +157,7 @@ class Literal():
return self.name
else:
return 'not '+self.name
def code_name(self):
"""
returns a string representing the literal
......@@ -166,7 +166,7 @@ class Literal():
return self.name
else:
return '_' + self.name
def __repr__(self):
return self.__str__()
......@@ -188,52 +188,52 @@ def lit_cmp(lit1, lit2):
return -1
else:
return 1
class CLDynSys(object):
"""
This class describe a dynamic system in clause form.
"""Class to describe a dynamic system in clause form.
@param symb_tab: name (string) -> type
@param report: reporter for error reporting
The frontier, free_clock, place_clock list are used for extractiong informations
The frontier, free_clock, place_clock list are used for extracting informations
from solutions. The place_cock list is used for generating the structural constraint
OR(P and h) implying that at least one clock transition must be activated at each step.
"""
def __init__(self, symb_tab, report):
# symbol table of charter model produced by Table_visitor
# completed by add_free_clock
self.symb_tab = symb_tab
self.symb_tab = symb_tab
self.report = report # reporter for errors
# set of variables of the dynamic system (including aux vars)
self.base_var_set = set()
self.base_var_set = set()
self.list_clauses = [] # clause form of the dynamic
# structural constraints valid if there is no timing constraints
self.aux_list_clauses = []
self.frontier = [] # frontier of the model
self.aux_list_clauses = []
self.frontier = [] # frontier of the model
# complement of the frontier in the set of variables
self.no_frontier = []
self.no_frontier = []
self.free_clocks = [] # free clocks inputs
# dictionary clock h -> [place P] where P is the place
# preceding free clock h
self.place_clocks = dict()
# dictionary clock h -> [place P] where P is the place
# preceding free clock h
self.place_clocks = dict()
self.inputs = [] # other inputs
self.lit_compt = 0 # for auxiliary variables generation
def add_var(self, name):
"""
add a logical variable to the dynamic system
@param name: the name of the variable (string)
"""
if name in self.base_var_set:
if name in self.base_var_set:
return
else:
self.base_var_set.add(name)
def add_aux_var(self):
"""
create an auxiliary variable for compiler purpose
......@@ -242,19 +242,19 @@ class CLDynSys(object):
self.lit_compt += 1
self.base_var_set.add(name)
return name
def add_free_clock(self, hname):
"""
add a free clock variable
@param hname: the name of the clock variable (string)
"""
if hname in self.base_var_set:
if hname in self.base_var_set:
return
else:
self.base_var_set.add(hname)
self.free_clocks.append(hname)
self.symb_tab[hname] = ('clock', -1)
def add_place_clock(self, pname, hname):
"""
add an association hname --> pname between a clock and an inductive place
......@@ -265,35 +265,34 @@ class CLDynSys(object):
except:
# clock not registered
self.place_clocks[hname] = [pname]
def add_input(self, name):
"""
add a variable representing an input
@param name: name of the input
@param name: name of the input
"""
if not name in self.base_var_set:
self.base_var_set.add(name)
self.inputs.append(name)
def add_clause(self, cla):
"""
add a clause constraint
"""
#TODO: do not add satisfied clauses (n or not n)
self.list_clauses.append(cla)
def add_aux_clause(self, cla):
"""
add an auxiliary clause constraint
"""
self.aux_list_clauses.append(cla)
def get_var_number(self):
"""
returns the number of variables used in the system (including aux vars)
"""
return len(self.base_var_set)
\ No newline at end of file
# -*- coding: utf-8 -*-
## Filename : CLUnfolder.py
## Author(s) : Michel Le Borgne
## Created : 22 mars 2012
......@@ -64,6 +65,7 @@ class CLUnfolder(object):
========================================
Each variable is coded as an integer (in var_code_table and var_list).
Each clause is represented as a list of signed integers (DIMACS coding).
During unfolding, clauses are shifted either to the future (forward) or
to the past (backward). The shift operator is a simple addition
of self.__shift_step. The shift direction depends only on initializations.
......@@ -859,7 +861,7 @@ class CLUnfolder(object):
def init_backward_unfolding(self):
"""
""" Never used (and backward not implemented in __init_variant_constraints_0)
initialisation before generating constraints - backward trajectory
"""
self.__shift_direction = 'BACKWARD'
......@@ -1034,15 +1036,18 @@ class CLUnfolder(object):
"""
if LOGGER.getEffectiveLevel() == DEBUG:
LOGGER.debug("squery_solve :: vvars : %s", vvars)
# initialization
self.init_forward_unfolding()
# horizon adjustment
if self.__list_variant_constraints:
max_step = min(max_step, len(self.__list_variant_constraints)-1)
# loop
if self.__invariant_property and not self.__final_property :
if self.__invariant_property and not self.__final_property:
# loop
while self.__current_step <= max_step:
self.shift()
# return l_rawsol
return self.__msolve_constraints(max_sol, vvars)
......
# -*- coding: utf-8 -*-
## Filename : MCLAnalyser.py
## Author(s) : Michel Le Borgne
## Created : 03/2012
......@@ -533,7 +534,7 @@ class MCLAnalyser(object):
# helper functions
def only_in_l1(ll1, ll2):
"""
"""(not used)
@param ll1: list<any> - list of element
@param ll2: list<any> - list of element
@return: only_l1 list<any> - list of element that are only in the first list (l1\l2)
......
......@@ -47,9 +47,7 @@ Various solution representations
from _cadbiom import get_unshift_code, unflatten
class MCLException(Exception):
"""
Exception for MCLAnalyser
"""
"""Exception for MCLAnalyser"""
def __init__(self, mess):
self.message = mess
......
......@@ -682,7 +682,7 @@ class TestMCLAnaLyzer(unittest.TestCase):
def test_mac_inhibitor(self):
"""
test
[A1, B1,C1] not strong activator, D is a strong inhibitor
[A1, B1, C1] not strong activator, D is a strong inhibitor
"""
rep = ErrorRep()
mcla = MCLAnalyser(rep)
......
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