Abs program loaded in 3 ms.

Rule based representation generated in 0 ms.

Rule based representation stored in /tmp/costabs/rbr.rbr

RBR properties stored in /tmp/costabs/rbr.properties

Class invariants generated and loaded in 0 ms.
Size abstraction not supported for native

Abstract compilation performed in 0 ms.
sabu_memo_table_1(case_0,[A,B],[1*B=1,1*A=1],0,0)
sabu_memo_table_1(case_0,[A,B],[-1*A+1*B>= -1,1*B>=1,1*A+ -1*B>=0],0,1)
sabu_memo_table_1(pred,[A,B],[1*A+ -1*B>=0,1*B>=1,-1*A+1*B>= -1],0,0)
sabu_memo_table_1(start,[A,B],[-1*A+1*B>= -1,1*B>=1,1*A+ -1*B>=0],0,0)
sabu_memo_table_1(start,[A,B],[],0,1)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_0, [A, B], [-1*A+1*B>= -1, 1*B>=1, 1*A+ -1*B>=0], 0, 1).
sabu_memo_table_1(pred, [A, B], [1*A+ -1*B>=0, 1*B>=1, -1*A+1*B>= -1], 0, 0).
sabu_memo_table_1(start, [_, _], [], 0, 1).


Size analysis performed in 1 ms.

Cost relation system stored in /tmp/costabs/crs.crs

Generated 27 equations 

Cost relation system solved by PUBS in 4 ms.

Method start terminates?: YES

UB for start(x) = 1


Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. non_recursive  : [case_0/1]
1. non_recursive  : [pred/1]
2. non_recursive  : [start/1]
Warning: the following predicates are never called:[and_op/2,eq/2,geq/2,gt/2,leq/2,lt/2,maxNorm/2,neg/1,neq/2,or/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into case_0/1
1. SCC is completely evaluated into other SCCs
2. SCC is partially evaluated into start/1

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations case_0/1 
* CE 3 is refined into CE [5] 
* CE 4 is refined into CE [6] 


#### Refined cost equations case_0/1 
* CE 5: case_0(A) = 2
     [A>=2] 
* CE 6: case_0(A) = 2
     [A=1] 

### Cost equations --> "Loop" of case_0/1 
* CEs [5] --> Loop 5 
* CEs [6] --> Loop 6 

#### Loops of case_0/1 
* Loop 5: case_0(A) [A>=2] 
* Loop 6: case_0(A) [A=1] 

### Ranking functions of CR case_0(A) 

#### Partial ranking functions of CR case_0(A) 


### Resulting Chains:case_0(A) 
* [6]
* [5]


### Specialization of cost equations start/1 
* CE 2 is refined into CE [7,8] 
* CE 1 is refined into CE [9] 


#### Refined cost equations start/1 
* CE 7: start(A) = 2+ case_0(B):[6]
     [B=1,A=1] 
* CE 8: start(A) = 2+ case_0(A):[5]
     [A>=2] 
* CE 9: start(A) = 1
     [] 

### Cost equations --> "Loop" of start/1 
* CEs [8] --> Loop 7 
* CEs [7] --> Loop 8 
* CEs [9] --> Loop 9 

#### Loops of start/1 
* Loop 7: start(A) [A>=2] 
* Loop 8: start(A) [A=1] 
* Loop 9: start(A) [] 

### Ranking functions of CR start(A) 

#### Partial ranking functions of CR start(A) 


### Resulting Chains:start(A) 
* [9]
* [8]
* [7]


Computing Bounds
=====================================

#### Cost of chains of case_0(A):
* Chain [6]: 2
  with precondition: [A=1] 

* Chain [5]: 2
  with precondition: [A>=2] 


#### Cost of chains of start(A):
* Chain [9]: 1
  with precondition: [] 

* Chain [8]: 4
  with precondition: [A=1] 

* Chain [7]: 4
  with precondition: [A>=2] 


Closed-form bounds of start(A): 
-------------------------------------
* Chain [9] with precondition: [] 
    - Lower bound: 1 
    - Complexity: constant
 * Chain [8] with precondition: [A=1] 
    - Lower bound: 4 
    - Complexity: constant
 * Chain [7] with precondition: [A>=2] 
    - Lower bound: 4 
    - Complexity: constant
 
### Partitioned lower bound of start(A): 
* 1 
 if []
Possible lower bounds : [1]
Maximum lower bound complexity: constant
* Total analysis performed in 12 ms.