Portfolios
A portfolio selects the backends and backend configurations that verify a case: Theta, nuXmv, Spin, Uppaal, or a combination of them. Choose one with semantifyr verify --portfolio <id>. A single-backend portfolio needs its backend installed, a combined one at least one of its backends; semantifyr portfolios reports which portfolios are available on your machine.
| Portfolio | Description | Legs |
|---|---|---|
smart-full (default) | Races representative configurations of every backend in parallel and takes the first verdict its leg's soundness direction trusts. | nuxmv:bmc-invar Exacttheta:bounded-bmc Exactspin:safe-dfs UnderApproximatinguppaal:default UnderApproximatingnuxmv:ic3-invar Exacttheta:cegar-expl-pred-combined Exacttheta:bounded-kinduction Exacttheta:ic3 Exactuppaal:over-approximation OverApproximatingspin:bitstate UnderApproximating |
all-agree-full | Runs one representative configuration per backend in parallel and requires the trusted verdicts to agree. | theta:cegar-expl-pred-combined Exactnuxmv:ic3-invar Exactuppaal:default UnderApproximatingspin:safe-dfs UnderApproximating |
theta-full | Races the Theta CEGAR and k-induction configurations in parallel and takes the first verdict. | theta:cegar-expl Exacttheta:cegar-expl-pred-combined Exacttheta:cegar-pred-cart Exacttheta:bounded-kinduction Exact |
theta-cegar-expl | Single theta configuration: cegar-expl | theta:cegar-expl Exact |
theta-cegar-expl-pred-combined | Single theta configuration: cegar-expl-pred-combined | theta:cegar-expl-pred-combined Exact |
theta-cegar-pred-cart | Single theta configuration: cegar-pred-cart | theta:cegar-pred-cart Exact |
theta-bounded-kinduction | Single theta configuration: bounded-kinduction | theta:bounded-kinduction Exact |
theta-bounded-bmc | Single theta configuration: bounded-bmc | theta:bounded-bmc Exact |
theta-bounded-imc | Single theta configuration: bounded-imc | theta:bounded-imc Exact |
theta-ic3 | Single theta configuration: ic3 | theta:ic3 Exact |
uppaal-default | Single uppaal configuration: default | uppaal:default UnderApproximating |
uppaal-breadth-first | Single uppaal configuration: breadth-first | uppaal:breadth-first UnderApproximating |
uppaal-depth-first | Single uppaal configuration: depth-first | uppaal:depth-first UnderApproximating |
uppaal-random-depth-first | Single uppaal configuration: random-depth-first | uppaal:random-depth-first UnderApproximating |
uppaal-over-approximation | Single uppaal configuration: over-approximation | uppaal:over-approximation OverApproximating |
uppaal-under-approximation | Single uppaal configuration: under-approximation | uppaal:under-approximation UnderApproximating |
uppaal-under-approximation-large | Single uppaal configuration: under-approximation-large | uppaal:under-approximation-large UnderApproximating |
uppaal-aggressive-inclusion | Single uppaal configuration: aggressive-inclusion | uppaal:aggressive-inclusion UnderApproximating |
nuxmv-ic3-invar | Single nuxmv configuration: ic3-invar | nuxmv:ic3-invar Exact |
nuxmv-bmc-invar | Single nuxmv configuration: bmc-invar | nuxmv:bmc-invar Exact |
nuxmv-bdd-invar | Single nuxmv configuration: bdd-invar | nuxmv:bdd-invar Exact |
spin-exhaustive-dfs | Single spin configuration: exhaustive-dfs | spin:exhaustive-dfs UnderApproximating |
spin-exhaustive-bfs | Single spin configuration: exhaustive-bfs | spin:exhaustive-bfs UnderApproximating |
spin-safe-dfs | Single spin configuration: safe-dfs | spin:safe-dfs UnderApproximating |
spin-fast-dfs | Single spin configuration: fast-dfs | spin:fast-dfs UnderApproximating |
spin-collapse | Single spin configuration: collapse | spin:collapse UnderApproximating |
spin-bitstate | Single spin configuration: bitstate | spin:bitstate UnderApproximating |
spin-hash-compact | Single spin configuration: hash-compact | spin:hash-compact UnderApproximating |
Soundness directions
Each leg of a portfolio is one backend configuration, listed with the direction in which its verdicts can be trusted. An Exact leg is trusted both ways. An UnderApproximating leg explores only part of the behaviour, so it is trusted when it finds a trace (a Failed AG or a Passed EF property) and not when it reports that none exists. An OverApproximating leg is trusted the other way round. Spin and Uppaal are under-approximating, since they choose a havoced value only among candidate values; Theta and nuXmv are exact. Uppaal's over-approximation configuration (-A, the convex hull of clock zones) is over-approximating, and since a run is exact, over-approximating or under-approximating, never both, it reports a case Not supported before it runs when the case havocs an integer that the model reads other than in comparisons with literals, which is where the candidate values would under-approximate. Spin and Uppaal compute with 32-bit integers that wrap. Spin runs a case only when every integer its property depends on has a static bound within 32 bits, and reports it Not supported otherwise. Uppaal declares every integer with its static bound, or with a 31-bit range when it has none within 32 bits, so that an increment or a doubling cannot wrap before Uppaal checks the range. It reports a case Not supported before it runs when arithmetic its property depends on may still leave 32 bits under those ranges, and stops a run as Not supported, naming the variable, when a value leaves its declared range. A trace either finds therefore never passes through a wrapped value.
smart-full and theta-full race their legs and report the first verdict its leg's direction trusts. When no such verdict arrives the case is Inconclusive, Timeout when a leg ran out of time, or Errored when every leg failed, and the message lists what every leg reported. all-agree-full runs every leg and reports the verdict its trusted legs agree on, naming any untrusted leg it overrules; trusted legs that disagree make the case Errored, since one of them is unsound. When no leg decides, it reports as the racing portfolios do. A single-backend portfolio reports its configuration's verdict when the leg's direction trusts it; otherwise the case is Inconclusive without a witness, and the message names the verdict it withheld, such as Spin's Passed on an AG property. When every leg reports a case Not supported, the message names each leg and the constructs it refused.