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	✅	✅
MQTT	✅	✅
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	✅

Annotations

Annotation	Supported
@Topic(name: string)	✅
@End(term: string)	✅

NOTE: Annotations must be defined at top of Flex file. See any of the annotation details below for examples of usage.

Topic Annotation

For transports which use Publish/Subscribe models with topics, the @Topic annotation tells Verifier which topic a message should be sent or received on. Topics which aren't listed in any protocol will not be watched, and messages which arrive on the incorrect topic will be marked invalid.

All annotations which are placed on send or recv statements must be placed at the end of the expression, just before the closing ;.

annotation Topic(name: string)

component Test;
component Other;

local protocol basicFlow in Test {
    recv let msg1: RequestNumber
        from Other
        @Topic("messages.RequestNumber");

    send let msg2: GiveNumber
        where msg2.id == msg1.id
        to Other
        @Topic("messages.GiveNumber");
}

End Annotation

@End specifies the conditions on which Verifier should mark a protocol as completed, after all sends and recvs have occured. The value for this annotation can be any one of:

• Exit - The component program should exit before the protocol can succeed
• Timeout - Verifier should wait for a message timeout after receiving all messages (program exit would result in an error)
• ExitOrTimeout - Either of the above conditions is considered successful
• LastMessage - The protocol is considered successful after the last specified send or recv occurs

annotation End(term: string)

@End("LastMessage")
local protocol basicFlow in Test {
    recv let msg1: RequestNumber
        from Other;

    send let msg2: GiveNumber
        where msg2.id == msg1.id
        to Other;
}

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	🚧

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?

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.

Type & Variable Features

Feature	send	recv
Single var conditional statements
Non-array primitive types	✅	✅ Full support for boolean operations
Array/List 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	✅	❌

Flex Std Lib Features

The Flex Standard Library supports a large number of functions & operators. The below table shows support for standard library features specifically in send and recv constraint clauses (i.e. assuming and where). The list of std lib features supported by Verifier is constantly growing:

Std Lib Feature	send	recv
Literals/Primitive Types	⚠️ Custom length (u)intN aren't supported, only standard lengths (8, 16, 32, 64)	⚠️
Built-in Functions	⚠️ Currently, only length is supported for lists as shown in Type & Variable Features	⚠️
Custom function definitions	✅	❌
transform definitions	❌	❌
match	✅	❌
assert	❌	❌
for	❌	❌
scan/fold/try/filter	❌	❌
Operators	✅	⚠️ Bitwise & bit shift operators are not supported

Examples

Primitive Type Constraints

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 in Dashboard {
    send let req: DataRequest
        where req.id == "weatherstation_0"
            && req.time > 0
            && req.request == DataType.Rainfall
        to WeatherStation;

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

List Constraints

Valid Constraints

local protocol X in Component {
    recv let first: MsgOne
        assuming length(first.array_field) == 10
        from Other;

    recv let second: MsgTwo
        assuming second.array_field == [1, 2, 3, 4, 5]
        from Other;
}

Invalid Single Variable Array Index Expressions

local protocol X in Component {
    recv let 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 in A {
    // Verifier will struggle to generate the message which the component says it must receive
    recv let 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 in Component {
    // WRONG: Message blocks are _not_ checked as constraints
    send Position {
            lat = 10,
            long = 20
        }
        to Other;

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