b-animate-dev

Animate B Machine with probcli

Animate and model-check a B machine using probcli (ProB command line interface).

Input

Arguments: $ARGUMENTS

Parse arguments:

• First positional argument: file path (or search in specs/)
• -v or --verbose: Show full probcli output
• -a N or --animate N: Animation steps (default: 20)
• -s N or --setsize N: Default set size for model checking (default: 2)

Process

0. Check Prerequisites

Verify probcli is installed:

PROBCLI="${PROBCLI:-$HOME/Applications/ProB/probcli}"
if ! which probcli >/dev/null 2>&1 && [ ! -x "$PROBCLI" ]; then
    echo "PROBCLI_NOT_FOUND"
fi

If probcli not found: Stop and tell the user:

probcli is not installed. Run /z-spec-dev:setup-dev probcli first.

1. Locate the Machine

If a file path is provided, use it directly.

If no file specified:

• Look in specs/ for .mch files
• Present options if multiple files exist

2. Run Validation Checks

Execute these checks in sequence:

Check 1: Parse and Initialize

probcli <file>.mch -init

Verifies the machine parses and has valid initial state(s).

Look for:

• Operation listings indicating available operations
• Error messages indicating parse failures
• INITIALISATION execution success

Check 2: Animation

probcli <file>.mch -animate 20

Randomly executes operations to verify they're executable.

Look for:

• ALL OPERATIONS COVERED - all operations were executed
• Partial coverage indicates some operations may have unsatisfiable preconditions

Check 3: Constraint-Based Assertion Check

probcli <file>.mch -cbc_assertions

Checks if any operation can violate assertions defined in the ASSERTIONS clause.

Look for:

• No counter-example to ASSERTION exists - pass
• No ASSERTION to check - no assertions defined
• Counter-example found - potential assertion violation

Check 4: Constraint-Based Deadlock Check

probcli <file>.mch -cbc_deadlock