Package net.automatalib.modelchecker.m3c.transformer

Class AbstractPropertyTransformer<T extends AbstractPropertyTransformer<T,​L,​AP>,​L,​AP>

  • Type Parameters:
    T - property transformer type
    L - edge label type
    AP - atomic proposition type
    Direct Known Subclasses:
    ADDTransformer, BDDTransformer
    public abstract class AbstractPropertyTransformer<T extends AbstractPropertyTransformer<T,​L,​AP>,​L,​AP>
extends Object
    Base class used to represent a property transformer, i.e., a function which maps a subset of formulas to a subset of formulas. Can also be seen as a function which maps bit vectors of length n to bit vectors of length n.

    • Method Detail

      • evaluate

        public abstract BitSet evaluate​(boolean[] input)
        Returns the set of variable numbers of subformulas y with f(input)=y, where f is the property transformer represented by this.
        Parameters:
        input - a boolean array representing a set of subformulas
        Returns:
        the set of variable numbers of subformulas

      • compose

        public abstract T compose​(T other)
        Returns the composition h of this and other such that h(x) = this(other(x)). The isMust attribute of the composition is set to the isMust attribute of this.
        Parameters:
        other - function which is first applied to an input
        Returns:
        the composition of this and other

      • createUpdate

        public abstract T createUpdate​(Set<AP> atomicPropositions,
                               List<T> compositions,
                               EquationalBlock<L,​AP> currentBlock)
        Returns the updated property transformer of a node.
        Parameters:
        atomicPropositions - of the node
        compositions - of the property transformers belonging to the outgoing edges and their target nodes
        currentBlock - the block which is considered during this update
        Returns:
        the updated property transformer of a node

      • isMust

        public boolean isMust()
        Returns whether the property transformer belongs to a node or to a must edge.
        Returns:
        true if the property transformer belongs to a node or to a must edge, false otherwise