Verifier Support Matrix

The following tables present which features of Verifier should be considered fully, partially, or un- supported, following this guide:

• ✅: Fully supported
• ⚠️: Fully supported within listed limitations
• 🚧: In progress, some features may not work and documentation may be unclear
• ❌: Unsupported

Interoperability Features

Transports

Transport	Verifier in Tangram Pro	Verifier in CI
ActiveMQ	✅	✅
HTTP	❌	❌
Kafka	✅	✅
NATS	✅	✅
RabbitMQ	✅	✅
ZeroMQ	✅	✅
TCP	❌	✅
UDP	❌	✅

Serializers

Transport	Verifier in Tangram Pro	Verifier in CI
CSV	✅	✅
Direct (Binary)	✅	✅
JSON	✅	✅
LMCP	✅	✅
MAVLink	✅	✅
OMS 2.0 (XML)	✅	✅
Protobuf	✅	✅
ROS	✅	✅
STANAG 4586	✅	✅
WOSA	✅	✅
XML	✅	✅

Flex Features

The Flex language has a large surface area, not all of which is currently supported by Verifier. These tables help disambiguate Verifier's current support for features of the Flex language.

Declarations

Declaration	Supported
Imports	🚧
Message	✅
Struct	✅
Variant	✅
Enum	⚠️ ONLY int32 base
type	✅
newtype	❌
Global protocol	❌
Local protocol	✅
Component	✅
System	❌
Connection	✅

Protocol Features

Protocol Feature	Supported
All primitive types (message fields)	✅
All primitive types (protocol variables)	✅
Built-in Functions	🚧
send let	✅
send any	✅
send ... where { ... }	✅
send <var>	⚠️ See linked example for limitations
recv let	✅
recv any	✅
listen	🚧
branch	🚧
loop	❌
do	🚧
@Topic annotation (on recv/send)	✅
@End annotation (on local protocol)	✅

Constraints

Constraints should be specified as a list of boolean checks.

See the examples below as well as in the Flex protocol examples.

The table below shows the current limitations of Verifier with respect to the larger capability list of Flex protocols.

Why are some features supported in send but not recv?

Recall that Verifier acts as the reciprocal of the component: when the component protocol sends a message, Verifier receives it, and when the component recvs a message, Verifier has to generate and send it.

Generating a message from constraints is a difficult task. We continue to add new features to our message generators, so please keep an eye on the supported constraint types shown in this table.

Constraint Feature	send	recv
Single var conditional statements
Non-array primitive types	✅	✅ Full support for boolean operations
Array primitive types	✅	⚠️ arr_field == [] and length(arr_field) == x only
Variant type matching	✅	❌
Enum type matching	✅	✅ Full support for boolean operations
Dependency on prior message	✅	✅
Dependency on variable	✅	✅
Multi var conditional statements	✅	❌

Examples

Valid Single Variable Boolean Expressions

enum DataType int32 {
    Temperature = 0;
    WindSpeed   = 1;
    AirPressure = 2;
    Rainfall    = 3;
}

struct DataRequest {
    id: string;
    time: uint64;
    request: DataType;
}

struct DataRespone {
    id: string;
    time: uint64;
    response: RequestType;
    data: float64;
}

component Dashboard;
component WeatherStation;

local protocol Example for Dashboard {
    send req: DataRequest
        where req.id == "weatherstation_0"
            && req.time > 0
            && req.request == DataType.Rainfall
        to WeatherStation;

    recv res: DataRespone
        assuming res.id == "weatherstation_0"
            && res.time >= req.time
            && res.response == req.request
        from WeatherStation;
}

Invalid Single Variable Array Index Expressions

local protocol X for Component {
    recv msg: Msg
        // Verifier does not support indexing constraints
        assuming msg.array_field[0] == 10
        from Other;
}

Invalid Multi-Variable Boolean Expressions

message struct Position {
    lat: float64;
    long: float64;
}

component A;
component B;

local protocol X for A {
    // Verifier will struggle to generate the message which the component says it must receive
    recv pos: Position
        assuming pos.x + pos.y < 100
        to B;
}

send Constraints

message struct Position {
	lat: float64;
	long: float64;
}

component Component;
component Other;

local protocol X for Component {
    // WRONG: Message blocks are _not_ checked as constraints
    send pos: Position {
            lat = 10,
            long = 20
        }
        to Other;

    // RIGHT: Instead, do:
    send pos: Position
        where pos.lat == 10
           && pos.long == 20
        to Other;
}