left

Liveness

right
AProVE Help SystemUser InterfaceGraphical User InterfaceSelecting OptionsLiveness

The Liveness options panel offers you the possibility to control the details of liveness proving. Therefore it provides you with an additional configuration box .

livenessterm

The Term Configuration box (1)

The Term Configuration box allows the user to enter those terms that he wishes to disappear from future states. For more details on this see the section on Liveness Problems.

The box allows the user too chose, add, and delete terms.

The Top Symbol selector (2)

After loading a rewrite system, AProVE will collect all the top symbols and then display them in the Top Symbol selector(2). The user can select one ore more of the offered top symbols.

The Heuristic checkboxes (3)

AProVE can try a number of simple but efficient heuristics for termination problems stemming from translated liveness problems. Here, the user has three possibilities:
  1. Full search without heuristics (upper checkbox disabled, lower enabled)
  2. First heuristics, then full search (both checkboxes enabled)
  3. Only heuristics (upper checkbox enabled, lower disabled)

Performing a Liveness Proof

When the user starts the proof by pressing the Go button the terms listed in the Term Configuration box and the symbols selected in the Top Symbol selector determine the transformation into a termination problem. The heuristic selection determines the power and the efficiency of the following termination proof.

The TRS and SCC configuration boxes (4)

The rest of the panel does not differ from the normal TRS configuration panel and controls the proving process once the liveness problem is transformed into a the termination problem of a TRS.