Artifact:

CUBA: Interprocedural Context-Unbounded Analysis of Concurrent Programs

Tutorial

To have the CUBA executable readily available, we suggest you add its location to your PATH variable:
PATH=$PATH:/your-path-to/bin

1. Help Info

The following command prints usage help info:
cuba -h

We illustrate tool usage through the simple example stutter-11.pds, included here. Let the initial state be 0|1,4. You can either input the initial state directly via the command line, or store it in a file like stutter-11.init and pass the file to CUBA (we show both ways below). Similarly, we have a target state 0|1,6 and a file named stutter-11.spec. The reachability of the target state is the property of interest.

2. Run explicit CUBA

Computation of all reachable visible states:
cuba -f stutter-11.pds -i "0|1,4" -x -p
or
cuba -f stutter-11.pds -i stutter-11.init -x -p
Reachability of a given target visible state:
cuba -f stutter-11.pds -i "0|1,4" -a "0|1,6" -x -p
or
cuba -f stutter-11.pds -i stutter-11.init -a stutter-11.spec -x -p

Explanation: Remark: the -x flag will cause an error message if the input does not satisfy the Finite-Context Reachability condition, which ensures that the set of states reachable per round is finite and can therefore be explicitly enumerated. See Section 5 of the paper for details.

3. Run symbolic CUBA

Computation of all reachable visible states:
cuba -f stutter-11.pds -i "0|1,4" -p
or
cuba -f stutter-11.pds -i stutter-11.init -p
Reachability of a given target state:
cuba -f stutter-11.pds -i "0|1,4" -a "0|1,6" -p
or
cuba -f stutter-11.pds -i stutter-11.init -a stutter-11.spec -p

Explanation:

Output

Convergence detection:

Explicit Exploration (with -x, -p flags)

Explicit exploration

Symbolic Exploration (without -x flag)

Symbolic exploration
Reachability of the target state 0|1,6:

Explicit Exploration (with -x, -p flags)

Explicit exploration

Symbolic Exploration (without -x flag)

Symbolic exploration