diff options
Diffstat (limited to 'tex/thesis/implementation/experiments/example-output')
| -rw-r--r-- | tex/thesis/implementation/experiments/example-output | 90 |
1 files changed, 21 insertions, 69 deletions
diff --git a/tex/thesis/implementation/experiments/example-output b/tex/thesis/implementation/experiments/example-output index 5194e12..38ce67a 100644 --- a/tex/thesis/implementation/experiments/example-output +++ b/tex/thesis/implementation/experiments/example-output @@ -39,8 +39,8 @@ Succs (1): B3 [B5] - 1: 1 - 2: int x1 = 1; + 1: 0 + 2: int x1 = 0; 3: 1 4: int x2 = 1; Preds (1): B6 @@ -52,104 +52,56 @@ 0-6-pre = max(-inf, inf) 1-6-pre = max(-inf, inf) 2-6-pre = max(-inf, inf) -3-6-pre = max(-inf, inf) -4-6-pre = max(-inf, inf) -5-6-pre = max(-inf, inf) 0-5-pre = max(-inf, 0-6-pre) 1-5-pre = max(-inf, 1-6-pre) 2-5-pre = max(-inf, 2-6-pre) -3-5-pre = max(-inf, 3-6-pre) -4-5-pre = max(-inf, 4-6-pre) -5-5-pre = max(-inf, 5-6-pre) -0-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -1-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -2-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) -3-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -4-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))) -5-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)) +0-5-0 = max(-inf, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)) +1-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))) +2-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))) 0-2-pre = max(-inf, 0-5-0, 0-3-pre) 1-2-pre = max(-inf, 1-5-0, 1-3-pre) 2-2-pre = max(-inf, 2-5-0, 2-3-pre) -3-2-pre = max(-inf, 3-5-0, 3-3-pre) -4-2-pre = max(-inf, 4-5-0, 4-3-pre) -5-2-pre = max(-inf, 5-5-0, 5-3-pre) 0-4-pre = max(-inf, min(8, 0-2-pre)) 1-4-pre = max(-inf, 1-2-pre) 2-4-pre = max(-inf, 2-2-pre) -3-4-pre = max(-inf, 3-2-pre) -4-4-pre = max(-inf, 4-2-pre) -5-4-pre = max(-inf, 5-2-pre) 0-1-pre = max(-inf, 0-2-pre) -1-1-pre = max(-inf, min(-9, 1-2-pre)) +1-1-pre = max(-inf, 1-2-pre) 2-1-pre = max(-inf, 2-2-pre) -3-1-pre = max(-inf, 3-2-pre) -4-1-pre = max(-inf, 4-2-pre) -5-1-pre = max(-inf, 5-2-pre) -0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -1-4-0 = max(-inf, add(-2, MCF<[1,-1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -2-4-0 = max(-inf, MCF<[0,1,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) -3-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -4-4-0 = max(-inf, add(-2, MCF<[1,0,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))) -5-4-0 = max(-inf, MCF<[0,-1,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)) +0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))) +1-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))) +2-4-0 = max(-inf, MCF<[0,-1,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre)) 0-3-pre = max(-inf, 0-4-0) 1-3-pre = max(-inf, 1-4-0) 2-3-pre = max(-inf, 2-4-0) -3-3-pre = max(-inf, 3-4-0) -4-3-pre = max(-inf, 4-4-0) -5-3-pre = max(-inf, 5-4-0) 0-0-pre = max(-inf, 0-1-pre) 1-0-pre = max(-inf, 1-1-pre) 2-0-pre = max(-inf, 2-1-pre) -3-0-pre = max(-inf, 3-1-pre) -4-0-pre = max(-inf, 4-1-pre) -5-0-pre = max(-inf, 5-1-pre) Block 0: x1 <= 10 - -x1 <= -9 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 1: x1 <= 10 - -x1 <= -9 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 2: x1 <= 10 - -x1 <= -1 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 3: x1 <= 10 - -x1 <= -3 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -3 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 4: x1 <= 8 - -x1 <= -1 - x1 - x2 <= 0 - x2 <= 10 - -x2 <= -1 - x2 - x1 <= 0 + x2 <= 11 + x2-x1 <= 1 Block 5: x1 <= inf - -x1 <= inf - x1 - x2 <= inf x2 <= inf - -x2 <= inf - x2 - x1 <= inf + x2-x1 <= inf Block 6: x1 <= inf - -x1 <= inf - x1 - x2 <= inf x2 <= inf - -x2 <= inf - x2 - x1 <= inf + x2-x1 <= inf |