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],[1*A>=0,1*A=1],0,0)
sabu_memo_table_1(flip,[A],[1*A>=0,1*A=1,1*A>=0],0,0)
sabu_memo_table_1(case_0,[A],[-1*A>= -2,1*A>=1],1,1)
sabu_memo_table_1(flip,[A],[-1*A>= -2,1*A>=1],2,1)
sabu_memo_table_1(case_0,[A],[-1*A>= -3,1*A>=1],3,2)
sabu_memo_table_1(flip,[A],[-1*A>= -3,1*A>=1],4,2)
sabu_memo_table_1(case_0,[A],[-1*A>= -4,1*A>=1],5,3)
sabu_memo_table_1(flip,[A],[-1*A>= -4,1*A>=1],6,3)
sabu_memo_table_1(case_0,[A],[1*A>=1],7,0)
sabu_memo_table_1(flip,[A],[1*A>=1],8,0)
sabu_memo_table_1(start,[A],[1*A>=0,1*A>=1],0,0)
sabu_memo_table_1(start,[],[],0,0)
:- dynamic sabu_memo_table_1/5.
sabu_memo_table_1(case_0, [A], [1*A>=1], 7, 0).
sabu_memo_table_1(flip, [A], [1*A>=1], 8, 0).
sabu_memo_table_1(start, [A], [1*A>=0, 1*A>=1], 0, 0).
sabu_memo_table_1(start, [], [], 0, 0).
Size analysis performed in 3 ms.
Cost relation system stored in /tmp/costabs/crs.crs
Generated 28 equations
Cost relation system solved by PUBS in 8 ms.
Method start terminates?: YES
- w_1: size of w wrt. XX
UB for start(w_1) = nat(w_1)
Method start terminates?: YES
- w_1: size of w wrt. XX
UB for start(w_1) = nat(w_1)
Method start terminates?: YES
UB for start(w_1) = nat(w_1)
Method start terminates?: YES
UB for start(w_1) = nat(w_1)
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [start/0]
2. recursive : [case_0/1,flip/1]
3. non_recursive : [start/1]
Warning: the following predicates are never called:[and_op/2,eq/2,flip/1,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 start/0
2. SCC is partially evaluated into flip/1
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations start/0
* CE 1 is refined into CE [2]
#### Refined cost equations start/0
* CE 2: start = 1
[]
### Cost equations --> "Loop" of start/0
* CEs [2] --> Loop 2
#### Loops of start/0
* Loop 2: start []
### Ranking functions of CR start
#### Partial ranking functions of CR start
### Resulting Chains:start
* [2]
Computing Bounds
=====================================
#### Cost of chains of start:
* Chain [2]: 1
with precondition: []
Closed-form bounds of start:
-------------------------------------
* Chain [2] with precondition: []
- Lower bound: 1
- Complexity: constant
### Partitioned lower bound of start:
* 1
if []
Possible lower bounds : [1]
Maximum lower bound complexity: constant
* Total analysis performed in 8 ms.