diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py index 7bcd7af..73d412a 100644 --- a/smt/smt_checker_rsc_param.py +++ b/smt/smt_checker_rsc_param.py @@ -14,6 +14,9 @@ from logics import rsLTL_Encoder # def simplify(x): # return x +def MAX(a, b): + return If(a > b, a, b) + class SmtCheckerRSCParam(object): def __init__(self, rsca): @@ -131,7 +134,7 @@ class SmtCheckerRSCParam(object): entities_dict[entity] = varname all_entities_dict.setdefault(entity, []) - all_entities_dict[entity].append((conc,varname)) + all_entities_dict[entity].append(varname) reactions_dict[reaction_id] = entities_dict @@ -238,31 +241,30 @@ class SmtCheckerRSCParam(object): # enc_max_single_ent = True - sorted_vars_by_conc = sorted(per_reaction_vars, key=lambda conc_var: conc_var[0]) - list_of_vars = [v for c,v in sorted_vars_by_conc] + #sorted_vars_by_conc = sorted(per_reaction_vars, key=lambda conc_var: conc_var[0]) + #list_of_vars = [v for c,v in sorted_vars_by_conc] - print(list_of_vars) + print(per_reaction_vars, "--->", self.enc_max(per_reaction_vars)) return enc_trans - # def enc_max(self, elements): - # - # if len(elements) == 1: - # return elements[0] - # - # elif len(elements) > 1: - # - # # If(a > b, a, b) - # def MAX(a, b): - # return If(a > b, a, b) - # - # for i in range(1,len(elements)): - # MAX(elements[]) - # - # else: - # return None - # + def enc_max(self, elements): + + if len(elements) == 1: + return MAX(0, elements[0]) + + elif len(elements) > 1: + + enc = 0 + for i in range(len(elements) - 1): + enc = MAX(enc, MAX(elements[i], elements[i + 1])) + + return enc + + else: + return None + def enc_automaton_trans(self, level): """Encodes the transition relation for the context automaton"""