User Guide

What BehaVerify accepts as input, what it produces as output, and how each piece of the DSL is handled across the six generation modes.

---

Tree DSL reference

The .tree grammar: blocks, types, expressions, temporal operators.

The .tree DSL

Components

Composite / decorator / leaf node catalog with memory, parallel policies, and sub-tree reuse.

Components

Generation modes

nuxmv, python, cpp, haskell, latex, trace, grid.

Generation Modes

Specifications

INVAR, CTL, LTL templates; contingency monitors; temporal operators.

Specifications

Neural networks

Embedding ONNX classifiers / regressors as action leaves.

Neural-Network Leaves

Encodings

Fast-forwarding vs naive; staging of blackboard variables.

Encodings

Verification strategies

Model checking, simulation, and runtime monitors.

Verification Strategies