LTS Termination Proof
by AProVE
Input
Integer Transition System
-
Initial Location:
l0, l2
-
Transitions: (pre-variables and post-variables)
| l0 |
1 |
l1:
|
|
0 ≤ 0 |
| l2 |
2 |
l0:
|
|
0 ≤ 0 |
Proof
1 Switch to Cooperation Termination Proof
We consider the following cutpoint-transitions:
| l0 |
l0 |
l0: |
TRUE
|
| l2 |
l2 |
l2: |
TRUE
|
and for every transition t,
a duplicate t is considered.
2 SCC Decomposition
There exist no SCC in the program graph.
Tool configuration
AProVE
- version: AProVE Commit ID: unknown
- strategy:
Statistics for single proof: 100.00 % (2 real / 0 unknown / 0 assumptions / 2 total proof steps)