Package org.mcp.core

Class ECEngine

java.lang.Object
org.mcp.core.ECEngine
@ParametersAreNonnullByDefault public class ECEngine extends Object
A utility class for computing Equivalence Classes (ECs) from a set of labels.

ECs are the minimal set of labels such that:

  • No EC is logically false.
  • The disjunction of all ECs is logically true.
  • Each EC is disjoint from all others.
  • Each label is equivalent to a disjunction of some subset of the ECs.
This is based on the algorithm described in: "Real-time Verification of Network Properties using ECs" by Yang and Lam.

Since:
2025-02-28
Author:

  • Constructor Details

    • ECEngine

      public ECEngine(Set<Label> labels, Label trueLabel)
      Constructs ECs for the given set of labels.
      Parameters:
      labels - the set of labels to compute ECs for
      trueLabel - a label representing logical "true"

  • Method Details

    • getNumECs

      public int getNumECs()
      Returns the number of computed ECs.
      Returns:
      the number of ECs

    • getECAutomata

      @Nonnull public Map<Integer,OperableLabel> getECAutomata()
      Returns a mapping from EC indices to their semantic representations.
      Returns:
      a map from EC index to OperableLabel

    • getECs

      @Nonnull public Map<Label,Set<Integer>> getECs()
      Returns a mapping from each label to the set of EC indices it covers.
      Returns:
      a map from Label to set of EC indices