Containment Test

You have to choose a target automaton after the function is triggered. This function checks if the language of the current automaton is contained in that of the chosen automaton.

There are two different approaches of checking containment available.

• by Complementation and Intersection: This approach relies on the intersection and complementation operations and the emptiness test. If the containment does not hold, one counterexample (an infinite word) is shown.
• by Rank-Based Approach: This approach relies on the tool developed by Seth Fogarty. To apply this approach, the executable rank (or rank.exe on Microsoft Windows) should be placed somewhere in the search path. The user can also specify the path to the executable by adding the following argument when invoking GOAL.

    -Drank.path=/path/to/rank

  (/path/to/rank should be replaced by the actual path including the filename of the executable)

A sample of the containment test. The test reports that the language
of the "Even p" automaton is not contained in that of the "<>[]p"
automaton.