tools/verification/rvgen/rvgen/ltl2k.py

Source file repositories/reference/linux-study-clean/tools/verification/rvgen/rvgen/ltl2k.py

File Facts

System
Linux kernel
Corpus path
tools/verification/rvgen/rvgen/ltl2k.py
Extension
.py
Size
8226 bytes
Lines
278
Domain
Support Tooling And Documentation
Bucket
tools
Inferred role
Support Tooling And Documentation: tools
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

#!/usr/bin/env python3
# SPDX-License-Identifier: GPL-2.0-only

from pathlib import Path
from . import generator
from . import ltl2ba
from .automata import AutomataError

COLUMN_LIMIT = 100

def line_len(line: str) -> int:
    tabs = line.count('\t')
    return tabs * 7 + len(line)

def break_long_line(line: str, indent='') -> list[str]:
    result = []
    while line_len(line) > COLUMN_LIMIT:
        i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ')
        result.append(line[:i])
        line = indent + line[i + 1:]
    if line:
        result.append(line)
    return result

def build_condition_string(node: ltl2ba.GraphNode):
    if not node.labels:
        return "(true)"

    result = "("

    first = True
    for label in sorted(node.labels):
        if not first:
            result += " && "
        result += label
        first = False

    result += ")"

    return result

def abbreviate_atoms(atoms: list[str]) -> list[str]:
    def shorten(s: str) -> str:
        skip = ["is", "by", "or", "and"]
        return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip])

    def find_share_length(atom: str) -> int:
        for i in range(len(atom), -1, -1):
            if sum(a.startswith(atom[:i]) for a in atoms) > 1:
                return i
        return 0

    abbrs = []
    for atom in atoms:
        share_len = find_share_length(atom)
        share = atom[:share_len]
        unique = atom[share_len:]
        abbrs.append((shorten(share) + shorten(unique)))
    return abbrs

class ltl2k(generator.Monitor):
    template_dir = "ltl2k"

    def __init__(self, file_path, MonitorType, extra_params={}):
        if MonitorType != "per_task":
            raise NotImplementedError("Only per_task monitor is supported for LTL")
        super().__init__(extra_params)
        try:
            with open(file_path) as f:
                self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())

Annotation

Implementation Notes