LTS Termination Proof
by T2Cert
Input
Integer Transition System
-
Initial Location:
0
-
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 transition 0
using the following ranking functions, which are bounded by
−6.
Hints:
3 SCC Decomposition
There exist no SCC in the program graph.
Tool configuration
T2Cert