Skip to content

ARCHITECTURE.md

Latest commit

 

History

History
78 lines (56 loc) · 3.34 KB

ARCHITECTURE.md

File metadata and controls

78 lines (56 loc) · 3.34 KB
Raw

Architecture of OmegaHyper

The pipeline of OmegaHyper runs through four folders of src/, one per phase; each box of the diagram is a folder and each box inside it a step of the pileline and a file of that folder. The architecture of the tool follows closely the architecture and presentation of the paper, that we recommend to consult for more details.

flowchart TB
    model[/NuSMV models/] --> systr
    phi[/HyperLTL formula/] --> api

    subgraph insys ["Input/Systems/"]
        systr[Translation.fs] --> sysq[Quotient.fs]
    end

    subgraph infor ["Input/Formula/"]
        api[ApInference.fs] --> dec[Decomposition.fs] --> ltl["Translation.fs"]
    end

    subgraph elim ["Elimination/"]
        prod[Product.fs] --> pq[ProductQuotient.fs] --> apc[APCompaction.fs] --> red["Reduction.fs"]
        red -- "quantifier alternation" --> comp["Complement.fs"]
        comp --> prod
    end

    sysq --> prod
    ltl --> apc

    subgraph fin ["FinalCheck/"]
        pre[Premises.fs] --> sym[Symmetry.fs] --> lo[SystemsTranslation.fs] --> chk["InclusionCheck.fs"] --> wit[Witness.fs]
    end

    red -- "last block" --> pre
    wit --> out[/verdict + witness/]
Loading

Phases and Steps

Input/

Instance.fs reads the models and the formula, and interleaves the steps of the two phases below.

Input/Systems/

  • Translation.fs translates each input system once into an OmegaSystem: explicit states for the dynamic variables, and symbolic edges for the frozen and free variables.
  • Quotient.fs replaces each trace's system by its bisimulation quotient under what the formula reads from it.

Input/Formula/

  • ApInference.fs infers the atoms on the systems' domains.
  • Decomposition.fs splits the formula's body into parts in normal form, following the innermost block. Before, it also exchanges the models' specifications and the formula's invariants.
  • Translation.fs translates a formula part into an NBA, when the elimination loop or the final check first needs its automaton.

Elimination/

Loop.fs runs the steps below once per innermost block.

  • APCompaction.fs compacts both APs syntactically and, before a complement, the alphabet semantically.
  • Reduction.fs reduces the size of the NBA parts.
  • Complement.fs, at a quantifier alternation, complements all NBA parts.
  • Product.fs builds the product of the NBA parts with the innermost block.
  • ProductQuotient.fs replaces each product by its bisimulation quotient.

FinalCheck/

  • Premises.fs moves parts of the right (the automaton) to the left (the outermost block's OmegaSystems), as premises on the systems.
  • Symmetry.fs prunes the left parts under identified symmetries.
  • SystemsTranslation.fs converts the left parts into several NBAs.
  • InclusionCheck.fs decides inclusion of the left parts in the right parts.
  • Witness.fs turns an inclusion counterexample into a witness over the input models.

General folders

  • App/: the command line, the configuration, the log and the entry point.
  • Automata/: Büchi automata, their HOA format, runs and lassos.
  • Backends/: one binding per external tool, behind the complementation and inclusion interfaces.
  • Common/: general utilities.
  • Logic/: formula utilities (atomic propositions and HyperLTL formulas).
  • Systems/: system utilities (input formats, translations and common representatio).