Analysis of Counter-examples vs Invariants

In this page we perform a refined analysis that distinguishes two kinds of properties:

INV : A property that requires a proof, that is universal and bears over all states or paths.
CEX : A property you can disprove (or prove) by exhibiting a counter-example (or witness)
UNK : Properties for which no verdict is available, because no tool could treat it, so that we don't know whether it is INV or CEX.

We introduce this decomposition of properties for Global Properties :

ReachabilityDeadlock : if TRUE, there is a deadlock, it is CEX. Otherwise it is considered INV.
StableMarking : if TRUE, there is a place whose marking will never vary, it is CEX. Otherwise it is considered INV.
OneSafe : if FALSE, there is a place whose marking can exceed 1, it is CEX. Otherwise it is considered INV.
QuasiLiveness : if FALSE, there is a transition that can never be fired, it is CEX. Otherwise it is considered INV.
Liveness : if FALSE, there is a transition that is not live, it is CEX. Otherwise it is considered INV.

We introduce also introduce it for Reachability and LTL:

Reachability AG : when the formula is of the form AG(p), and it is FALSE it is CEX. Otherwise it is considered INV.
Reachability EF : when the formula is of the form EF(p), and it is TRUE it is CEX (a witness suffices). Otherwise it is considered INV.
LTL : when the formula is FALSE it is CEX (and we can produce a counter-example). Otherwise it is considered INV since a TRUE LTL property naturally covers all paths.

We first study the decomposition of formulas in the MCC benchmark according to this criterion.