• Checklist
• Getting CUBA
• Input Syntax
• Tutorial
• Benchmarks

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:

• -f, -i: pass the input program to the tool.
• -a: pass the target visible state to the tool.
• -x: launch explicit exploration (see below).
• -p: print output, including states and visible states, in each round. The output for stutter-11.pds is shown below (left).

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:

• -p: print the output, include visible states in each round. The output for stutter-11.pds is shown below (right).

Output

Convergence detection: Reachability of the target state 0|1,6: