diff --git a/.pydevproject b/.pydevproject
index ad74947..c3434da 100644
--- a/.pydevproject
+++ b/.pydevproject
@@ -3,6 +3,6 @@
/${PROJECT_DIR_NAME}
-python interpreter
+python 3.0
Default
diff --git a/CFRefinement.py b/CFRefinement.py
old mode 100644
new mode 100755
index 8f16aa6..3558414
--- a/CFRefinement.py
+++ b/CFRefinement.py
@@ -21,6 +21,7 @@ def threshold_type(value):
def setArgumentParser():
desc = _name + ": Control Flow refinement."
absdomains = ["none", "interval", "polyhedra"]
+ output_formats = ["fc", "dot", "svg", "koat", "pl", "smt2"]
argParser = argparse.ArgumentParser(
description=desc,
formatter_class=argparse.RawTextHelpFormatter)
@@ -31,8 +32,8 @@ def setArgumentParser():
action='store_true', help="Shows the version.")
argParser.add_argument("--ei-out", required=False, action='store_true',
help="Shows the output supporting ei")
- argParser.add_argument("-of", "--output_formats", required=False, nargs='+',
- choices=["fc", "dot", "koat", "pl", "svg"], default=["fc", "dot", "svg"],
+ argParser.add_argument("-of", "--output-formats", required=False, nargs='+',
+ choices=output_formats, default=output_formats[:3],
help="Formats to print the graphs.")
argParser.add_argument("-od", "--output-destination", required=False,
help="Folder to save output files.")
diff --git a/irankfinder.py b/irankfinder.py
index c494da2..fefeeaf 100755
--- a/irankfinder.py
+++ b/irankfinder.py
@@ -54,14 +54,52 @@ def nontermination_alg_desc():
"\n\t".join(NTAM.options(True)))
+def setCFRArgumentsParser(group):
+ group.add_argument("-cfr-it", "--cfr-iterations", type=int, choices=range(0, 5),
+ help="# times to apply cfr", default=0)
+ group.add_argument("-cfr-mx-t", "--cfr-max-tries", type=int, choices=range(0, 5),
+ help="max tries to apply cfr on scc level", default=4)
+ group.add_argument("-cfr-st-before", "--cfr-strategy-before", action='store_true',
+ help="")
+ group.add_argument("-cfr-st-scc", "--cfr-strategy-scc", action='store_true',
+ help="")
+ group.add_argument("-cfr-st-after", "--cfr-strategy-after", action='store_true',
+ help="")
+ group.add_argument("-cfr-usr", "--cfr-user-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-cone", "--cfr-cone-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-head", "--cfr-head-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-head-var", "--cfr-head-var-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-call", "--cfr-call-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-call-var", "--cfr-call-var-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-john", "--cfr-john-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-split", "--cfr-split-properties", action='store_true',
+ help="")
+ group.add_argument("-cfr-inv", "--cfr-invariants", action='store_true',
+ help="CFR with Invariants.")
+ group.add_argument("-cfr-nodes", "--cfr-nodes", required=False, nargs="*",
+ default=[], help=".")
+ group.add_argument("-cfr-nodes-mode", "--cfr-nodes-mode", required=False,
+ default="all", choices=["john", "cyclecutnodes", "all", "user"], help=".")
+
+
def setArgumentParser():
desc = _name + ": a Ranking Function finder on python."
dt_options = ["never", "iffail", "always"]
+ domains = ["Z", "Q", "user"]
dt_scheme_options = ["default", "inhomogeneous"]
absdomains = ["none", "interval", "polyhedra"]
+ output_formats = ["fc", "dot", "svg", "koat", "pl", "smt2"]
argParser = argparse.ArgumentParser(
description=desc,
formatter_class=argparse.RawTextHelpFormatter)
+ setCFRArgumentsParser(argParser.add_argument_group('cfr', "CFR parameters"))
# Output Parameters
argParser.add_argument("-v", "--verbosity", type=int, choices=range(0, 5),
help="increase output verbosity", default=0)
@@ -70,7 +108,7 @@ def setArgumentParser():
argParser.add_argument("-od", "--output-destination", required=False,
help="Folder to save output files.")
argParser.add_argument("-of", "--output-formats", required=False, nargs='+',
- choices=["fc", "dot", "koat", "pl", "svg"], default=["fc", "dot", "svg"],
+ choices=output_formats, default=output_formats[:3],
help="Formats to print the graphs.")
argParser.add_argument("-si", "--show-with-invariants", required=False, default=False,
action='store_true', help="add invariants to the output formats")
@@ -81,6 +119,9 @@ def setArgumentParser():
argParser.add_argument("--print-graphs", required=False, action='store_true',
help="Shows the output in fc and svg format")
# Algorithm Parameters
+ argParser.add_argument("-d", "--domain", required=False,
+ choices=domains, default=domains[0],
+ help="Domain of the variables")
argParser.add_argument("-dt", "--different-template", required=False,
choices=dt_options, default=dt_options[0],
help="Use different templates on each node")
@@ -101,39 +142,6 @@ def setArgumentParser():
help="Check Invariants with the assertions defined")
argParser.add_argument("-rfs-as-cfr-props", "--rfs-as-cfr-props", action='store_true',
help="Print a graph with rfs as user props.")
- # CFR Parameters
- argParser.add_argument("-cfr-it", "--cfr-iterations", type=int, choices=range(0, 5),
- help="# times to apply cfr", default=0)
- argParser.add_argument("-cfr-mx-t", "--cfr-max-tries", type=int, choices=range(0, 5),
- help="max tries to apply cfr on scc level", default=4)
- argParser.add_argument("-cfr-st-before", "--cfr-strategy-before", action='store_true',
- help="")
- argParser.add_argument("-cfr-st-scc", "--cfr-strategy-scc", action='store_true',
- help="")
- argParser.add_argument("-cfr-st-after", "--cfr-strategy-after", action='store_true',
- help="")
- argParser.add_argument("-cfr-usr", "--cfr-user-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-cone", "--cfr-cone-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-head", "--cfr-head-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-head-var", "--cfr-head-var-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-call", "--cfr-call-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-call-var", "--cfr-call-var-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-john", "--cfr-john-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-split", "--cfr-split-properties", action='store_true',
- help="")
- argParser.add_argument("-cfr-inv", "--cfr-invariants", action='store_true',
- help="CFR with Invariants.")
- argParser.add_argument("-cfr-nodes", "--cfr-nodes", required=False, nargs="*",
- default=[], help=".")
- argParser.add_argument("-cfr-nodes-mode", "--cfr-nodes-mode", required=False,
- default="all", choices=["john", "cyclecutnodes", "all", "user"], help=".")
argParser.add_argument("-scc-pl", "--print-scc-prolog", required=False,
help="File where print, on certain format, sccs that we don't know if terminate.")
# IMPORTANT PARAMETERS
@@ -142,6 +150,9 @@ def setArgumentParser():
argParser.add_argument("-nt", "--nontermination", type=nontermination_alg,
nargs='*', required=False, default=[],
help=nontermination_alg_desc())
+ argParser.add_argument("-nt-reach", "--nt-reachability", required=False,
+ default=False, action='store_true',
+ help="Analyse reachability when NT algorithms says NO.")
argParser.add_argument("-t", "--termination", type=termination_alg, default=[],
nargs='*', required=False,
help=termination_alg_desc())
@@ -188,7 +199,8 @@ def parse_file(f):
return genericparser.parse(f)
-def launch_file(config, f, out):
+def launch_file(gconfig, f, out):
+ config = dict(gconfig)
aux_p = f.split('/')
aux_c = len(aux_p) - 1
while aux_c > 0:
@@ -210,6 +222,8 @@ def launch_file(config, f, out):
OM.printerrf("Parser Error: {}\n{}".format(type(e).__name__, str(e)))
# raise Exception() from e
return
+ if "domain" in config and config["domain"] == "user":
+ config["domain"] = cfg.get_info("domain")
nodeproperties.invariant.set_configuration(config)
OM.restart(odest=out, cdest=r)
remove_no_important_variables(cfg, doit=config["remove_no_important_variables"])
@@ -305,6 +319,7 @@ def check_assertions(config, cfg):
OM.printf("Refining graph...")
from partialevaluation import control_flow_refinement
cfg = control_flow_refinement(cfg, config)
+ cfg.remove_unsat_edges()
OM.printf("Computing and checking invariants...")
nodeproperties.invariant.compute_invariants(cfg, check=True, add_to_polyhedron=False)
showgraph(cfg, config, sufix="cfr_before", console=config["print_graphs"], writef=False, output_formats=["fc", "svg"])
diff --git a/termination/__init__.py b/termination/__init__.py
index 98ba34d..08c798b 100644
--- a/termination/__init__.py
+++ b/termination/__init__.py
@@ -8,6 +8,7 @@
from partialevaluation import control_flow_refinement
from partialevaluation import prepare_scc
from .algorithm.utils import compute_way_nodes
+from termination.algorithm.utils import check_determinism
__all__ = ["NonTermination_Algorithm_Manager", "Termination_Algorithm_Manager", "Output_Manager", "Result", "TerminationResult", "analyse"]
@@ -97,7 +98,7 @@ def analyse(config, cfg):
if not R or not R.get_status().is_terminate():
# analyse NON-termination
if can_be_nonterminate:
- R_nt = analyse_scc_nontermination(nt_algs, scc)
+ R_nt = analyse_scc_nontermination(nt_algs, cfg, scc, domain=config["domain"], do_reachability=config["nt_reachability"])
if R_nt and R_nt.get_status().is_nonterminate():
R_nt.set_response(graph=scc)
nonterminating_sccs.append(R_nt)
@@ -163,20 +164,27 @@ def analyse(config, cfg):
CFGs = new_sccs + CFGs
else:
stop_all = True
-
+ determ = None
status = TerminationResult.UNKNOWN
if can_be_nonterminate and len(nonterminating_sccs) > 0:
status = TerminationResult.NONTERMINATE
elif len(maybe_sccs) > 0:
+ determ = True
+ for scc in maybe_sccs:
+ determ = check_determinism(scc.get_edges(), scc.get_info("global_vars"))
+ if not determ:
+ break
status = TerminationResult.UNKNOWN
elif can_be_terminate:
status = TerminationResult.TERMINATE
response = Result()
+
response.set_response(status=status,
rfs=dict(rfs),
terminate=terminating_sccs[:],
nonterminate=nonterminating_sccs[:],
unknown_sccs=maybe_sccs[:],
+ deterministic=determ,
graph=original_cfg)
return response
@@ -211,7 +219,7 @@ def prepare_cfr_config(config):
return cfr, cfr_before, cfr_scc, cfr_after
-def analyse_scc_nontermination(algs, scc, close_walk_depth=20):
+def analyse_scc_nontermination(algs, cfg, scc, close_walk_depth=20, domain="Z", do_reachability=False):
cw_algs = [a for a in algs if a.use_close_walk()]
nt_algs = [a for a in algs if not a.use_close_walk()]
if len(nt_algs) > 0:
@@ -220,15 +228,43 @@ def analyse_scc_nontermination(algs, scc, close_walk_depth=20):
if response.get_status().is_nonterminate():
return response
if len(cw_algs) > 0:
- for cw in scc.get_close_walks(close_walk_depth):
+ for cw in scc.get_close_walks(close_walk_depth, 1, linear=True):
OM.printif(1, "\nAnalysing Close Walk: {}.".format([t["name"] for t in cw]))
+ determ = check_determinism(cw, scc.get_info("global_vars"))
+ if not determ and domain == "Z":
+ OM.printif(1, "\t- Skiping because is not DET and domain is Z.")
+ continue
for a in cw_algs:
- response = a.run(scc, cw)
+ response = a.run(scc, cw, domain)
+ response.set_response(reachability=False)
+ if do_reachability:
+ response = analyse_reachability(cfg, cw, response, domain)
if response.get_status().is_nonterminate():
+ response.set_response(deterministic=determ)
return response
return False
+def analyse_reachability(cfg, cw, response, domain):
+ if not response.get_status().is_nonterminate():
+ return response
+ ntargument = None
+ if response.has("nt_argument"):
+ ntargument = response.get("nt_argument")
+ else:
+ raise Exception("no nt argument...")
+ from termination.algorithm.nonTermination import reachability
+ from genericparser import constants as gconsts
+ targets = list(set([tr["source"] for tr in cw]))
+
+ if reachability(cfg, ntargument, targets, domain=domain):
+ response.set_response(reachability=True)
+ return response
+ response.set_response(status=TerminationResult.UNKNOWN,
+ info="NTargument not reachable")
+ return response
+
+
def analyse_scc_termination(algs, cfg, dt_modes=[False], dt_scheme="default"):
trans = cfg.get_edges()
answer = Result()
diff --git a/termination/algorithm/nonTermination.py b/termination/algorithm/nonTermination.py
index 5bfcea0..1dea7e1 100644
--- a/termination/algorithm/nonTermination.py
+++ b/termination/algorithm/nonTermination.py
@@ -20,7 +20,7 @@ def __init__(self, properties={}):
def use_close_walk(cls):
return True
- def run(self, cfg, close_walk=[]):
+ def run(self, cfg, close_walk=[], domain="Z"):
"""
looking for a fixpoint in a close walk:
[n0] -(x, xP)-> [n1] -(xP, x2)-> [n2] -(x2, x)-> [n0]
@@ -45,7 +45,10 @@ def run(self, cfg, close_walk=[]):
if c.is_linear()]
cons += cs
tr_idx += Nvars
- s = Solver()
+ if domain == "Z":
+ s = Solver(variable_type="int", coefficient_type="int")
+ else:
+ s = Solver()
s.add(cons)
point, __ = s.get_point(taken_vars)
response = Result()
@@ -55,7 +58,8 @@ def run(self, cfg, close_walk=[]):
response.set_response(status=TerminationResult.NONTERMINATE,
info="FixPoint Found",
close_walk=close_walk,
- fixpoint=fixpointvalue)
+ fixpoint=fixpointvalue,
+ nt_argument=C_Polyhedron(constraints=cons, variables=taken_vars))
else:
OM.printif(1, "No fixpoint found.")
response.set_response(status=TerminationResult.UNKNOWN,
@@ -90,7 +94,7 @@ def generate(cls, data):
return cls(properties)
return None
- def run(self, cfg, close_walk=[]):
+ def run(self, cfg, close_walk=[], domain="Z"):
"""
looking for a Monotonic Recurrent Set in a close walk:
[n0] -(x0, x1)-> [n1] -(x1, x2)-> [n2] -(x2, xP)-> [n0]
@@ -158,7 +162,8 @@ def run(self, cfg, close_walk=[]):
response.set_response(status=TerminationResult.NONTERMINATE,
info="Recurrent Set Found:",
close_walk=close_walk,
- rec_set=tr_poly)
+ rec_set=tr_poly,
+ nt_argument=tr_poly)
return response
tr_poly = tr_poly_p
depth += 1
@@ -186,3 +191,64 @@ def get_algorithm(cls, token):
continue
return alg
raise ValueError("Not Valid token")
+
+
+def reachability(cfg, goal, goal_nodes, source=None, domain="Q"):
+ if source is None:
+ from genericparser import constants
+ source = cfg.get_info(constants.initnode)
+ from lpi import Solver
+ from genericparser import constants as gconsts
+ for cons, path in bfs_paths(cfg, source, goal_nodes, goal):
+ if domain == "Z":
+ s = Solver(variable_type="int", coefficient_type="int")
+ else:
+ s = Solver()
+ s.add(cons)
+ OM.printif(3, s)
+ if s.is_sat():
+ OM.printif(1, "reachable with path", path)
+ OM.printif(1, s.get_point(cfg.get_info(gconsts.variables)))
+ return True
+ else:
+ OM.printif(1, "NO reachable with path", path)
+ return False
+
+
+def bfs_paths(cfg, source, target, goal):
+ from genericparser import constants as gconsts
+ targets = [target] if not isinstance(target, list) else target
+ gvars = cfg.get_info(gconsts.variables)
+ N = int(len(gvars) / 2)
+ _vars = gvars[:N]
+ _pvars = gvars[N:]
+
+ def gen_names(vs, it):
+ return vs[:] if it == 0 else [v + "#" + str(it) for v in vs]
+
+ def gen_local(vs, it):
+ return gen_names(vs, "L" + str(it))
+
+ def add_tr(cons, tr, it):
+ tr_vars = gen_names(_vars, it - 1) + gen_names(_vars, it) + gen_local(tr[gconsts.transition.localvariables], it)
+ cons = cons + [c for c in tr[gconsts.transition.polyhedron].get_constraints(tr_vars)
+ if c.is_linear()]
+ return cons
+
+ trs = {t["name"]: t for t in cfg.get_edges()}
+ trs["#dummy"] = {"target": source}
+ queue = [([], ["#dummy"])]
+
+ while queue:
+ (cons, path) = queue.pop(0)
+ last = path[-1]
+ for tr in cfg.get_edges(source=trs[last]["target"]):
+ if path.count(tr["name"]) >= 2:
+ continue
+ new_cons = add_tr(cons, tr, len(path))
+ if tr["target"] in targets:
+ tr_vars = gen_names(_vars, len(path)) + _pvars + gen_local(goal.get_variables()[2 * N:], len(path))
+ new_cons = new_cons + goal.get_constraints(tr_vars)
+ yield (new_cons, path[1:] + [tr["name"]])
+ else:
+ queue.append((new_cons, path + [tr["name"]]))
diff --git a/termination/algorithm/utils.py b/termination/algorithm/utils.py
index 01209d5..b21e3dc 100644
--- a/termination/algorithm/utils.py
+++ b/termination/algorithm/utils.py
@@ -163,6 +163,16 @@ def showgraph(cfg, config, sufix="", invariant_type="none", console=False, write
OM.writefile(0, completename + ".pl", koatstr)
stream.close()
stream = StringIO()
+ if "smt2" in output_formats:
+ cfg.toSMT2(path=stream, invariant_type=invariant_type)
+ koatstr = stream.getvalue()
+ if console:
+ OM.printif(0, "Graph {}".format(name), consoleid="smt2", consoletitle="smt2 Source")
+ OM.printif(0, koatstr, format="text", consoleid="smt2", consoletitle="smt2 Source")
+ if writef:
+ OM.writefile(0, completename + ".smt2", koatstr)
+ stream.close()
+ stream = StringIO()
stream.close()
@@ -193,3 +203,114 @@ def compute_way_nodes(cfg, target_nodes):
ns = cfg.get_all_nodes_between(init, n)
way_nodes.update(ns)
return way_nodes
+
+
+def is_notdeterministic_1(cons, gvars, usedvs):
+ N = int(len(gvars) / 2)
+ _vars, _pvars = gvars[:N], gvars[N:]
+ pending = [v for v in _pvars if usedvs[v]]
+ for c in cons:
+ pv = False
+ vs = c.get_variables()
+ for v in vs:
+ if not usedvs.get(v, True):
+ continue
+ if v in _pvars:
+ if not c.is_equality():
+ return True
+ if v in pending:
+ pending.remove(v)
+ if pv:
+ return True
+ pv = True
+ cf = c.get_coefficient(v)
+ if cf != 1 and cf != -1:
+ return True
+ elif v not in _vars:
+ return True
+ if len(pending) > 0:
+ return True
+ return False
+
+
+def is_notdeterministic_0(cons, gvars):
+ N = int(len(gvars) / 2)
+ _vars, _pvars = gvars[:N], gvars[N:]
+ pending = _pvars[:]
+ for c in cons:
+ pv = False
+ vs = c.get_variables()
+ for v in vs:
+ if v in _pvars:
+ if not c.is_equality():
+ return True
+ if v in pending:
+ pending.remove(v)
+ if pv:
+ return True
+ pv = True
+ cf = c.get_coefficient(v)
+ if cf != 1 and cf != -1:
+ return True
+ elif v not in _vars:
+ return True
+ if len(pending) > 0:
+ return True
+ return False
+
+
+def used_vars(trs, gvars):
+ from genericparser import constants
+ N = int(len(gvars) / 2)
+ _vars, _pvars = gvars[:N], gvars[N:]
+ unused = gvars[:]
+ used = {v: False for v in gvars}
+ for tr in trs:
+ if len(unused) == 0:
+ break
+ for c in tr[constants.transition.constraints]:
+ if len(unused) == 0:
+ break
+ vs = c.get_variables()
+ if len(vs) == 0:
+ continue
+ elif c.is_equality() and len(vs) == 2:
+ if vs[0] in gvars and vs[1] in gvars:
+ i1 = gvars.index(vs[0])
+ i2 = gvars.index(vs[1])
+ if i1 - i2 == N or i2 - i1 == N:
+ continue
+ for v in vs:
+ if v not in gvars:
+ continue
+ i1 = gvars.index(v)
+ i2 = (i1 + N) % (2 * N)
+ if v in unused:
+ unused.remove(v)
+ if gvars[i2] in unused:
+ unused.remove(gvars[i2])
+ used[v] = True
+ used[gvars[i2]] = True
+ return used
+
+
+def check_determinism(trs, gvars, mode=1):
+ from genericparser import constants
+ usedvs = used_vars(trs, gvars) if mode == 1 else []
+
+ def is_not(cons, mode):
+ if mode == 0:
+ return is_notdeterministic_0(cons, gvars)
+ elif mode == 1:
+ return is_notdeterministic_1(cons, gvars, usedvs)
+
+ def is_deterministic(tr):
+ const_det = constants.transition.isdeterministic
+ if const_det not in tr or tr[const_det] is None:
+ tr[const_det] = not is_not(tr[constants.transition.constraints], mode)
+ return tr[const_det]
+
+ determ = True
+ for tr in trs:
+ determ = determ and is_deterministic(tr)
+ return determ
diff --git a/termination/result.py b/termination/result.py
index 2e2435b..79082f0 100644
--- a/termination/result.py
+++ b/termination/result.py
@@ -122,6 +122,8 @@ def toString(self, vars_name=None):
res_str += self._scc_nonterminate(self._data["nonterminate"], vars_name)
if "unknown_sccs" in self._data:
res_str += self._unknown_sccs(self._data["unknown_sccs"])
+ if "deterministic" in self._data and self._data["deterministic"] is not None:
+ res_str += "deterministic: {}".format(self._data["deterministic"])
return res_str
def _rfs(self, rfs, vars_name=None):
@@ -140,7 +142,7 @@ def toStrRankingFunctions(self, vars_name=None):
def _scc_nonterminate(self, sols_nt, vars_name):
if len(sols_nt) == 0:
return ""
- res_str = "\nNON-Termination: (Didn't check reachability)\n"
+ res_str = "\nNON-Termination:\n"
res_str += "----------------\n"
for sol in sols_nt:
scc = sol.get("graph")
@@ -149,7 +151,13 @@ def _scc_nonterminate(self, sols_nt, vars_name):
res_str += "SCC:\n+--transitions: {}\n+--nodes: {}\n".format(
",".join([t["name"] for t in ts]), ",".join(ns))
if sol.has("close_walk"):
- res_str += "Closed walk: " + len(sol.get("close_walk")) + " -> " + ", ".join([t["name"]for t in sol.get("close_walk")])
+ res_str += "Closed walk: " + str(len(sol.get("close_walk"))) + " -> " + ", ".join([t["name"] for t in sol.get("close_walk")])
+ if sol.has("deterministic"):
+ res_str += "\ndeterministic: {}".format(sol.get("deterministic"))
+ if sol.has("reachability") and sol.get("reachability"):
+ res_str += "\nReachability checked!"
+ else:
+ res_str += "\nDidn't check reachability"
if sol.has("info"):
res_str += "\n- " + sol.get("info") + "\n"
if sol.has("fixpoint"):
diff --git a/test/test.fc b/test/test.fc
index f1289da..b795dc4 100755
--- a/test/test.fc
+++ b/test/test.fc
@@ -2,17 +2,28 @@
vars: [x,y],
pvars: [x',y'],
initnode: n0,
+ domain: Q,
transitions: [
{
+ source: n0,
+ target: n1,
+ name: t0,
+ constraints: [y>=1, x' = 10, y' = y]
+ },{
source: n1,
target: n1,
name: t1,
- constraints: [x >= 0, x' = 10 + y, y' = y]
+ constraints: [y >= 0, x' = x, y' = y - 2]
},{
- source: n0,
- target: n1,
- name: t0,
- constraints: [x' = x, y' = y]
- }
+ source: n1,
+ target: n2,
+ name: t2,
+ constraints: [y <=0, x' = x, y' = y]
+ },{
+ source: n2,
+ target: n2,
+ name: t3,
+ constraints: [x >= 0, x' = x + y, y' = y]
+ },
]
}