3.2.1.4 Verification Options

3.2.1.4 Verification Options

This section expands the explanation of verification options in Section 2.2.4. According to each type of assertions supported in RTS module, the possible admissiable behaviors and the verification engines provided in PAT are listed in the following.

Note: The numbers attached to each option represents the corresponding options under batch mode verification and command line console.

Deadlock-Freeness, Divergence-Freeness, Deterministic, Nonterminating, Safety-LTL properties, Reachability, Refinement, Failure-Refinement, and Failure/Divergence Refinement (for the meaning of the assertions, please refer to Section 3.1.1.7):

Admissible behaviors: All (0)
Verification engines:
- First witness trace with zone abstraction (0)
- First witness trace with digitalization (1)
- Shortest witness trace with zone abstraction (2)
- Shortest witness trace with digitalization (3)

Liveness Properties: (for the meaning of admissible behaviors with fairness assumption, please refer to Section 4.1)

Admissible behaviors:
- All (0)
- Non-zeno only (1)
- Event-level weak fair only (2)
- Event-level strong fair only (3)
- Process-level weak fair only (4)
- Process-level strong fair only (5)
- Global fair only (6)
Verification engines (same for each admissible behaviors above):
- Strongly connected components based search with zone abstraction (0)
- Strongly connected components based search with digitalization (1)