modality check

Command: modality check [specification]

This command checks that your SUT behaves as specified over some region of recorded execution. There are three distinct ways in which check can be used:

  1. Manually check a single specification against some given region or against all available sessions.
  2. Check a suite of specifications and produce a report.
  3. Check a specification against an open session (i.e. against a running system), optionally polling until the check is satisfied or a timeout is hit.

If a specification is not satisfied, the verbosity flags can be used to have check explain which part of the specification was unsatisfiable, provide a counter-example, and provide a query to find all counter-examples. If no region expression or session option is provided, check will evaluate the specification against the current default session. For further details on writing specifications, see the SpeQTr language reference.

# Example

$ modality check "EXISTS SENT_HEARTBEAT@CONSUMER" --using example-session
true

$ modality check 'EXISTS SENT_HEARTBEAT@CONSUMER' --all-sessions
SESSION          OUTCOME
failing-session  FAIL
example-session  PASS

$ modality check -v --file failing-measurement-query.tq 
The given check had no matches. Analyzing why…

Violation: Exists
    NEVER
        (RECVD_MSG@MONITOR AND (payload = 2)) AS RecvdMsgA,
        (RECVD_MSG@MONITOR AND (payload = 2)) AS RecvdMsgB
    WHEN
        RecvdMsgA -> RecvdMsgB AFTER 600ms
                                ^^^^^^^^^^^
                                |
                                Changing this limit to 3182ms causes this assertion to pass

# Options

[specification] - The specification to be evaluated and reported on. Mutually exclusive with the --file option.

--all-sessions - Evaluate the given trace expression against all sessions associated with the relevant SUT. The relevant SUT is either the one provided with the --with-sut option or the default one. This option is useful for quickly finding relevant sessions for an investigation or applying newly found tests to historical data to see when a problem arose. Mutually exclusive with the --timeout and --suite options.

--color <always | never | auto> - Whether to color the output. Default is auto, which will autodetect the target output location and whether or not it is capable of handling color escape codes.

--file <specification path> - Path to a file containing a specification. Mutually exclusive with a specification provided directly as a command line argument. Whitespace is ignored in specification files, and # can be used for single line comments.

-f, --format <text | jsonl | json | markdown | html> - The printed output format. Defaults to text for individual specifications and to markdown when used with --suite. The markdown and html options are only valid with the --suite option.

--region-expression <region expression> - Evaluate the specification against the provided region. See here for details on writing region expressions. If neither this option nor the --using option are passed, the check will be evaluated against the current default session.

--suite <suite path> - Path to a check suite file. Evaluate the given suite and produce a report with results. Mutually exclusive with a specification provided directly as a command line argument or the --file flag. The -v and --region-expression options are a no-op in conjunction with this option—verbose output is included automatically where applicable, and suites can only be evaluated against entire sessions, either the default session or one passed with the --using option.

--timeout <timeout> - A duration in seconds for which to reattempt the given check, for use when checking against a currently open session. The check will be retried until it is successful or the timeout expires. Mutually exclusive with the all-sessions flag.

--using <session name> - Evaluate the specification against the given session. If neither this option nor the --region-expression option are passed, defaults to evaluating against the current default session.

-v, -vv, --verbose - Provide (more) verbose output. At level 1 (-v), highlight the part of the specification causing the failure. At level 2 (-vv), additionally provide a counter-example which violates the specification and a query to find all counter-examples with modality query.

--with-sut <sut name> - Use the given SUT rather than the one currently associated with this session.

← config →