Collatz

The Collatz recurrence \(x \mapsto x/2\) (even) or \(x \mapsto 3x + 1\) (odd) is the smallest non-trivial behavior tree with genuinely rich dynamics.

Location

examples/Collatz/collatz.tree

Features exercised

• A selector wrapping a three-child sequence.

• loop-constructed set-valued initial assignment (\(x \in [1, 254]\)).

• Integer clamping via (min max_val ...).

• INVARSPEC only — no temporal operators needed.

Invocation

python -m behaverify nuxmv examples/Collatz/collatz.tree ../out/ \
    --generate --invar --nuxmv_path ../nuXmv

Suggested exercise

• Run with --use_encoding naive and compare the generated SMV against the default fastforwarding encoding. See Encodings.

• Render the tree with latex mode on the small variant collatz_small.tree:

  python -m behaverify latex examples/Collatz/collatz_small.tree \
      ./collatz.tex
  pdflatex collatz.tex