pyfcstm.highlight.bmc_query_lexer

Pygments lexer for FCSTM BMC Query files.

This module defines FcstmBmcQueryLexer, a lightweight lexer for the *.fbmcq query language used by the FCSTM bounded-model-checking workstream. The lexer mirrors the query grammar token surface closely enough for editor and Sphinx highlighting, but it deliberately does not parse or semantically validate queries.

The module contains:

Note

FcstmBmcQueryLexer.analyse_text() is a pure string heuristic. It must not import pyfcstm.bmc.parse, call the ANTLR parser, resolve model paths, or run semantic binding. Pygments may call language detection on arbitrary text, including malformed snippets.

Example:

>>> from pyfcstm.highlight import FcstmBmcQueryLexer
>>> lexer = FcstmBmcQueryLexer()
>>> lexer.name
'FCSTM BMC Query'
>>> query = 'init cold;\ncheck reach <= 2: active("Root.Done");'
>>> FcstmBmcQueryLexer.analyse_text(query) >= 0.8
True

__all__

pyfcstm.highlight.bmc_query_lexer.__all__ = ['FcstmBmcQueryLexer']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

FcstmBmcQueryLexer

class pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer(*args, **kwds)[source]

Lexer for FCSTM BMC Query files.

This lexer highlights the syntax-only *.fbmcq query surface used to express bounded model checking objectives for FCSTM models. It recognizes query clauses, BMC-only atoms, FCSTM-compatible expression operators, literals, strings, comments, and punctuation. It does not validate whether referenced states, events, variables, cases, or unsupported calls are meaningful for a particular pyfcstm.model.StateMachine.

Variables:

  • name – Human-readable Pygments lexer name.

  • aliases – Pygments aliases for lookup by query-language name.

  • filenames – Filename globs recognized by Pygments.

  • mimetypes – MIME types recognized by Pygments.

Example:

>>> from pygments import lex
>>> from pyfcstm.highlight import FcstmBmcQueryLexer
>>> tokens = [(kind, text) for kind, text in lex('init cold;', FcstmBmcQueryLexer()) if text.strip()]
>>> tokens[0]
(Token.Keyword.Declaration, 'init')
aliases = ['fbmcq', 'fcstm-bmc-query']

A list of short, unique identifiers that can be used to look up the lexer from a list, e.g., using get_lexer_by_name().

static analyse_text(text)

Return a heuristic confidence score for *.fbmcq text.

The score is intentionally based on lightweight regular expressions so editor and Pygments discovery can run on incomplete or invalid query snippets. A complete query with init/assume/check clauses receives a high score; unrelated text receives 0.0.

Parameters:

text (str) – Candidate source text.

Returns:

Pygments confidence score between 0.0 and 1.0.

Return type:

float

Example:

>>> FcstmBmcQueryLexer.analyse_text('check cover <= 3: case("A::B");') >= 0.70
True
filenames = ['*.fbmcq']

A list of fnmatch patterns that match filenames which contain content for this lexer. The patterns in this list should be unique among all lexers.

mimetypes = ['text/x-fcstm-bmc-query']

A list of MIME types for content that can be lexed with this lexer.

name = 'FCSTM BMC Query'

Full name of the lexer, in human-readable form

tokens = {'block-comment': [('\\*/', ('Comment', 'Multiline'), '#pop'), ('[^*]+', ('Comment', 'Multiline')), ('\\*', ('Comment', 'Multiline'))], 'comments': [('/\\*', ('Comment', 'Multiline'), 'block-comment'), ('//.*?$', ('Comment', 'Single')), ('#.*?$', ('Comment', 'Single'))], 'numbers': [('0x[0-9a-fA-F]+', ('Literal', 'Number', 'Hex')), ('[0-9]+\\.[0-9]*([eE][+-]?[0-9]+)?', ('Literal', 'Number', 'Float')), ('\\.[0-9]+([eE][+-]?[0-9]+)?', ('Literal', 'Number', 'Float')), ('[0-9]+[eE][+-]?[0-9]+', ('Literal', 'Number', 'Float')), ('[0-9]+', ('Literal', 'Number', 'Integer'))], 'root': ['whitespace', 'comments', 'strings', (<pygments.lexer.words object>, ('Name', 'Builtin')), (<pygments.lexer.words object>, ('Name', 'Builtin')), (<pygments.lexer.words object>, ('Name', 'Builtin')), (<pygments.lexer.words object>, ('Name', 'Builtin')), (<pygments.lexer.words object>, ('Keyword', 'Declaration')), (<pygments.lexer.words object>, ('Keyword', 'Reserved')), (<pygments.lexer.words object>, ('Operator', 'Word')), (<pygments.lexer.words object>, ('Keyword', 'Constant')), (<pygments.lexer.words object>, ('Name', 'Constant')), ('[0-9]+(?=\\.\\.)', ('Literal', 'Number', 'Integer')), 'numbers', ('\\*\\*', ('Operator',)), ('>>|<<', ('Operator',)), ('<=|>=|==|!=', ('Operator',)), ('&&|\\|\\|', ('Operator',)), ('=>|->|\\.\\.', ('Operator',)), ('!', ('Operator', 'Word')), ('[+\\-*/%&|^~<>]', ('Operator',)), ('=|\\?', ('Operator',)), ('[:;,{}()\\[\\]./]', ('Punctuation',)), ('[a-zA-Z_][a-zA-Z0-9_]*', ('Name',))], 'strings': [('"([^"\\\\\\r\\n]|\\\\[btnfr"\\\'\\\\]|\\\\[0-7]{1,3}|\\\\u[0-9a-fA-F]{4}|\\\\x[0-9a-fA-F]{2})*"', ('Literal', 'String', 'Double')), ('\'([^\'\\\\\\r\\n]|\\\\[btnfr\\"\'\\\\]|\\\\[0-7]{1,3}|\\\\u[0-9a-fA-F]{4}|\\\\x[0-9a-fA-F]{2})*\'', ('Literal', 'String', 'Single'))], 'whitespace': [('\\s+', ('Text', 'Whitespace'))]}

At all time there is a stack of states. Initially, the stack contains a single state ‘root’. The top of the stack is called “the current state”.

Dict of {'state': [(regex, tokentype, new_state), ...], ...}

new_state can be omitted to signify no state transition. If new_state is a string, it is pushed on the stack. This ensure the new current state is new_state. If new_state is a tuple of strings, all of those strings are pushed on the stack and the current state will be the last element of the list. new_state can also be combined('state1', 'state2', ...) to signify a new, anonymous state combined from the rules of two or more existing ones. Furthermore, it can be ‘#pop’ to signify going back one step in the state stack, or ‘#push’ to push the current state on the stack again. Note that if you push while in a combined state, the combined state itself is pushed, and not only the state in which the rule is defined.

The tuple can also be replaced with include('state'), in which case the rules from the state named by the string are included in the current one.