diff --git a/termination/algorithm/qlrf.py b/termination/algorithm/qlrf.py index ee17646..d77ad65 100644 --- a/termination/algorithm/qlrf.py +++ b/termination/algorithm/qlrf.py @@ -192,7 +192,7 @@ def run(self, cfg, different_template=False, dt_scheme="default"): dfs = {} for tr in transitions: rf_s = rfs[tr["source"]] - rf_t = rfs[tr["target"]] + rf_t = rfs[tr["target"]].renamed(gvs[:Nvars], gvs[Nvars:]) poly = tr["polyhedron"] df = rf_s - rf_t # ExprTerm(0) constant = (rf_s.get_coeff() - rf_t.get_coeff()) @@ -211,8 +211,8 @@ def run(self, cfg, different_template=False, dt_scheme="default"): for tr in transitions: poly = tr["polyhedron"] cons = poly.get_constraints() - cons.insert(dfs[tr["name"]] == 0) - newpoly = C_Polyhedron(cons) + cons.append(dfs[tr["name"]] == 0) + newpoly = C_Polyhedron(constraints=cons, variables=gvs+tr["local_vars"]) if not newpoly.is_empty(): tr["polyhedron"] = newpoly no_ranked.append(tr)