Package modelcounter

Class EmersonLeiAutomatonBasedModelCounting<S>

  • Type Parameters:
    S - the state type of the underlying automaton
    public class EmersonLeiAutomatonBasedModelCounting<S>
extends Object
    AuRUS's approximate bounded LTL model counter (the ApMC of the paper): estimates the number of satisfying traces of bounded length of an LTL formula by a single linear-algebra computation over the formula's automaton.

    The pipeline has three steps:

    1. LTL → automaton. The formula is translated, with OWL's DELAG construction (DelagBuilder), into a deterministic automaton with an EmersonLeiAcceptance condition — an arbitrary boolean combination of Inf/Fin atoms over acceptance sets.
    2. Automaton → transfer matrix. The automaton is encoded as an n x n matrix T where entry T[i][j] is the number of propositional valuations (letters of the alphabet 2^AP) that move state s_i to state s_j (see buildTransferMatrix()).
    3. Counting by matrix exponentiation. The number of accepted words of length k is 
         #̂(φ, k)  =  u · T^k · v
      where u is the indicator row vector of the initial states and v the indicator column vector of the accepting states (see count(int)).

    What is being approximated. The computation counts the accepted finite words of length k — the bases of lasso traces — rather than the lasso traces themselves. A single base may close its loop at several positions (under-counting), and a base may reach an "accepting" state although no loop actually satisfies the infinitary acceptance condition (over-counting; see buildFinalStates()). The approximation is nevertheless sufficient for the fitness function, which only needs the relative ordering of candidates — empirically preserved in 9 out of 10 benchmark sets at a small fraction of the cost of exact counting.

    Arithmetic is exact: matrix entries are BigFractions and the result a BigInteger, so the astronomically large counts that arise at higher bounds neither overflow nor lose precision, as floating point would. Both the automaton translation and the counting run in worker threads guarded by timeouts (Settings.PARSING_TIMEOUT and Settings.MC_TIMEOUT); on timeout the counter degrades gracefully by returning null, which callers treat as a failed count.

    This counter is the central technical contribution of: Brizzio, Cordy, Papadakis, Sánchez, Aguirre, Degiovanni. "Automated Repair of Unrealisable LTL Specifications Guided by Model Counting", GECCO 2023 (doi:10.1145/3583131.3590454). Please cite the paper if you reuse or reimplement the technique. A standalone evolution of this counter is maintained as EstiMate.

    Author:
    Matías Brizzio
    See Also:
    AutomataBasedModelCountingSpecificationFitness

    • Constructor Summary

      Constructors 
      Constructor Description
      EmersonLeiAutomatonBasedModelCounting​(owl.ltl.LabelledFormula formula)
      Creates a counter for the given formula and immediately translates it into its Emerson-Lei automaton.

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      boolean accConditionIsSatisfied​(jhoafparser.ast.BooleanExpression<jhoafparser.ast.AtomAcceptance> acceptanceCondition, it.unimi.dsi.fastutil.ints.IntArrayList acceptanceSets)
      Recursively evaluates the automaton's Emerson-Lei acceptance condition — an arbitrary boolean expression in HOA format over Inf/Fin atoms — against the acceptance sets visited by a single edge.
      org.apache.commons.math3.linear.FieldMatrix buildFinalStates()
      Builds the indicator column vector v of the accepting states — and this is where the finite-word abstraction (and hence the approximation) lives.
      org.apache.commons.math3.linear.FieldMatrix buildInitialStates()
      Builds the indicator row vector u of the initial states: u[0][j] = 1 iff states[j] is an initial state of the automaton, 0 otherwise.
      org.apache.commons.math3.linear.FieldMatrix buildTransferMatrix()
      Builds the weighted transfer matrix T of the automaton: entry T[i][j] is the number of propositional valuations sigma in 2^AP whose edge carries state s_i to state s_j.
      BigInteger count​(int bound)
      Computes the approximate bounded model count #&#770;(formula, bound) = u * T^bound * v.
      org.apache.commons.math3.linear.FieldMatrix createMatrix​(int row, int column)
      Creates a zero matrix of the given dimensions with exact BigFraction entries.
      void printMatrix​(org.apache.commons.math3.linear.FieldMatrix<org.apache.commons.math3.fraction.BigFraction> M)
      Debug helper: prints a matrix to standard output, one row per line.

    • Constructor Detail

      • EmersonLeiAutomatonBasedModelCounting

        public EmersonLeiAutomatonBasedModelCounting​(owl.ltl.LabelledFormula formula)
        Creates a counter for the given formula and immediately translates it into its Emerson-Lei automaton.

        The translation runs in a separate worker thread and is abandoned after Settings.PARSING_TIMEOUT seconds; in that case the automaton stays unbuilt and every subsequent count(int) returns null. The translation is done once here so that repeated counts at different bounds pay it only once.

        Parameters:
        formula - the labelled LTL formula to count models of

    • Method Detail

      • count

        public BigInteger count​(int bound)
        Computes the approximate bounded model count #&#770;(formula, bound) = u * T^bound * v.

        The computation runs in a worker thread guarded by Settings.MC_TIMEOUT seconds. It returns null — rather than throwing — when the automaton was never built (translation timeout), when the count itself times out, or when the worker fails; callers such as the fitness function treat null as a failed count and fall back to a neutral score.

        Parameters:
        bound - the trace-length bound k
        Returns:
        the number of accepted words of length bound, or null if the count could not be completed

      • buildTransferMatrix

        public org.apache.commons.math3.linear.FieldMatrix buildTransferMatrix()
        Builds the weighted transfer matrix T of the automaton: entry T[i][j] is the number of propositional valuations sigma in 2^AP whose edge carries state s_i to state s_j. Weighting each transition by its valuation count is what lets a single matrix power count words rather than mere paths.

        Cost: for each of the n^2 state pairs the full valuation universe is enumerated, giving O(n^2 * 2^|AP|) — this construction, done once per formula, dominates the counter's cost, while each additional bound afterwards is only a matrix power.

        Returns:
        the n x n transfer matrix with exact BigFraction entries

      • buildInitialStates

        public org.apache.commons.math3.linear.FieldMatrix buildInitialStates()
        Builds the indicator row vector u of the initial states: u[0][j] = 1 iff states[j] is an initial state of the automaton, 0 otherwise.
        Returns:
        the 1 x n initial-state vector

      • buildFinalStates

        public org.apache.commons.math3.linear.FieldMatrix buildFinalStates()
        Builds the indicator column vector v of the accepting states — and this is where the finite-word abstraction (and hence the approximation) lives.

        An Emerson-Lei automaton accepts infinite runs through a condition over the acceptance sets its edges visit infinitely often; finite prefixes have no acceptance of their own. This method derives a finite-word notion of "accepting state" from the accepting edges: a state is marked final iff it is the successor of some edge whose acceptance-set membership satisfies the automaton's boolean acceptance condition (evaluated by accConditionIsSatisfied(BooleanExpression, IntArrayList)). Intuitively, a base ending in such a state can plausibly be extended into an accepted lasso. This is precisely the over-approximation discussed in the paper: reaching such a state does not guarantee that a valid loop actually exists from it.

        Returns:
        the n x 1 accepting-state vector

      • createMatrix

        public org.apache.commons.math3.linear.FieldMatrix createMatrix​(int row,
                                                                int column)
        Creates a zero matrix of the given dimensions with exact BigFraction entries.
        Parameters:
        row - number of rows
        column - number of columns
        Returns:
        a row x column matrix filled with zeros

      • printMatrix

        public void printMatrix​(org.apache.commons.math3.linear.FieldMatrix<org.apache.commons.math3.fraction.BigFraction> M)
        Debug helper: prints a matrix to standard output, one row per line.
        Parameters:
        M - the matrix to print

      • accConditionIsSatisfied

        public boolean accConditionIsSatisfied​(jhoafparser.ast.BooleanExpression<jhoafparser.ast.AtomAcceptance> acceptanceCondition,
                                       it.unimi.dsi.fastutil.ints.IntArrayList acceptanceSets)
        Recursively evaluates the automaton's Emerson-Lei acceptance condition — an arbitrary boolean expression in HOA format over Inf/Fin atoms — against the acceptance sets visited by a single edge.

        An Inf(i) atom is satisfied iff the edge belongs to acceptance set i; a Fin(i) atom iff it does not; AND/OR/NOT compose recursively (the operand of the unary NOT is stored as the right child, following the jhoafparser AST convention). Evaluating the infinitary condition on a single edge is the per-edge heuristic behind the finite-word abstraction of buildFinalStates().

        Parameters:
        acceptanceCondition - the boolean acceptance expression of the automaton
        acceptanceSets - the acceptance sets the edge belongs to
        Returns:
        true iff the edge satisfies the condition