From e49cd8cfc93b9dd8e024296615c3fe11eec3c1ef Mon Sep 17 00:00:00 2001 From: toda5603 Date: Mon, 9 Sep 2024 12:47:36 +0900 Subject: [PATCH] fixed bug --- CHANGES.rst | 12 ++++++++++++ examples/recon.py | 48 ++++++++++++++++++++++++----------------------- pygplib/ecc.py | 2 +- pyproject.toml | 2 +- 4 files changed, 39 insertions(+), 25 deletions(-) diff --git a/CHANGES.rst b/CHANGES.rst index 8aac48c..2cecccb 100644 --- a/CHANGES.rst +++ b/CHANGES.rst @@ -3,6 +3,18 @@ CHANGES ======= +Version 2.2.0 - 2024-09-09 +-------------------------- + +Fixed +^^^^^ +- recon.py: trans_type could not be changed from default type "TJ". +- recon.py: the strings of init state and final state were incorrectly computed when these + states are given as sets in a formula file. +- ecc.py: exception unintentially raised when clique encoding is selected and a + graph includes a vertex of degree 1. + + Version 2.1.0 - 2023-11-06 -------------------------- diff --git a/examples/recon.py b/examples/recon.py index 3bd17c9..ac660b3 100644 --- a/examples/recon.py +++ b/examples/recon.py @@ -19,14 +19,16 @@ def get_option(): "--trans", type=str, default="TJ", - help="Specify transition relation (TS or TJ)", + choices=["TS", "TJ"], + help="Specify transition relation", ) ap.add_argument( "-e", "--encoding", type=str, default="edge", - help="Specify ENCODING type (edge, clique, direct, log)", + choices=["edge", "clique", "direct", "log"], + help="Specify ENCODING type", ) ap.add_argument("arg1", help="dimacs graph file") ap.add_argument("arg2", help="formula file") @@ -91,18 +93,18 @@ def convert_ini_str(formula_str: str, variable_name: list) -> str: 3 4 5 Input (variable_name) - ["x1", "x2", "x3"] + ["x01", "x02", "x03", ...,"x10"] Output (equality as sequence) - x1=V3 & x2=V4 & x3=V5 + x01=V3 & x02=V4 & x03=V5 """ for x in formula_str.split(" "): - if len(x) == 0: + if x == "": continue - if not x.isdigit(): - return formula_str - vertex_name = ["V" + f"{x}" for x in formula_str.split(" ") if len(x) != 0] - if len(vertex_name) != len(variable_name): + if f"{int(x)}" != x: + raise Exception() + vertex_name = ["V" + f"{x}" for x in formula_str.split(" ") if x != ""] + if len(vertex_name) > len(variable_name): raise Exception("number of integers in init state is unmatching") return " & ".join([n + "=" + m for n, m in zip(variable_name, vertex_name)]) @@ -115,29 +117,29 @@ def convert_fin_str(formula_str: str, variable_name: list) -> str: 2 7 6 Input (variable_name) - ["x1", "x2", "x3"] + ["x01", "x02", "x03", ...,"x10"] Output (equality as set) - (x1=V2 | x1=V7 | x1=V6) & (x2=V2 | x2=V7 | x2=V6) & \ - (x3=V2 | x3=V7 | x3=V6) & (x1=V2 | x2=V2 | x3=V2) & \ - (x1=V7 | x2=V7 | x3=V7) & (x1=V6 | x2=V6 | x3=V6) + (x01=V2 | x01=V7 | x01=V6) & (x02=V2 | x02=V7 | x02=V6) & \ + (x03=V2 | x03=V7 | x03=V6) & (x01=V2 | x02=V2 | x03=V2) & \ + (x01=V7 | x02=V7 | x03=V7) & (x01=V6 | x02=V6 | x03=V6) """ for x in formula_str.split(" "): - if len(x) == 0: + if x == "": continue - if not x.isdigit(): - return formula_str - vertex_name = ["V" + f"{x}" for x in formula_str.split(" ") if len(x) != 0] - if len(vertex_name) != len(variable_name): + if f"{int(x)}" != x: + raise Exception() + vertex_name = ["V" + f"{x}" for x in formula_str.split(" ") if x != ""] + if len(vertex_name) > len(variable_name): raise Exception("number of integers in fin state is unmatching") tmp = [] # subset relation - for n in variable_name: - tmp.append("(" + " | ".join([n + "=" + m for m in vertex_name]) + ")") + for i in range(len(vertex_name)): + tmp.append("(" + " | ".join([variable_name[i] + "=" + n for n in vertex_name]) + ")") # supset relation - for m in vertex_name: - tmp.append("(" + " | ".join([n + "=" + m for n in variable_name]) + ")") + for n in vertex_name: + tmp.append("(" + " | ".join([n + "=" + variable_name[i] for i in range(len(vertex_name))]) + ")") return " & ".join(tmp) @@ -163,7 +165,7 @@ def convert_fin_str(formula_str: str, variable_name: list) -> str: name_list = [NameMgr.lookup_name(v) for v in op.get_free_vars(state_expr)] ini_expr = Fog.read(convert_ini_str(phi[2], name_list)) fin_expr = Fog.read(convert_fin_str(phi[3], name_list)) -trans_type = "None" if phi[1] != "" else "TJ" +trans_type = "None" if phi[1] != "" else trans_type st = GrSt(vertex_list, edge_list, encoding=encoding_type) bmc = Bmc(state_expr, trans_expr, ini_expr, fin_expr, st, trans_type=trans_type) diff --git a/pygplib/ecc.py b/pygplib/ecc.py index 5ea94b8..57781d5 100644 --- a/pygplib/ecc.py +++ b/pygplib/ecc.py @@ -47,7 +47,7 @@ def __init__(self, vertex_list: list, edge_list: list): self.nof_isolated_edges = 0 """number of isolated edges""" for e in self._edges: - if len(self._N[e[0]]) == 1 and len(self._N[e[1]]): + if len(self._N[e[0]]) == 1 and len(self._N[e[1]]) == 1: self.nof_isolated_edges += 1 if self.nof_isolated_verts > 1: diff --git a/pyproject.toml b/pyproject.toml index d8f492e..4f5e4fd 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "pygplib" -version = "2.1.0" +version = "2.2.0" description = "Python First-Order Graph Property Library" authors = ["Takahisa Toda "] license = "MIT"