LTS Termination Proof
by T2Cert
Input
Integer Transition System
-
Initial Location:
2
-
Transitions: (pre-variables and post-variables)
Proof
1 Switch to Cooperation Termination Proof
We consider the following cutpoint-transitions:
and for every transition t,
a duplicate t is considered.
2 Transition Removal
We remove transitions 0, 1
using the following ranking functions, which are bounded by
−8.
|
2:
|
0 |
|
0:
|
0 |
|
1:
|
0 |
|
2:
|
−4 |
|
0:
|
−5 |
|
1:
|
−6 |
Hints:
| 0 |
lexStrict[
[0]
,
[0]
]
|
| 1 |
lexStrict[auto, auto]
|
3 SCC Decomposition
There exist no SCC in the program graph.
Tool configuration
T2Cert