Class BuchiDegeneralization


  • public final class BuchiDegeneralization
    extends Object
    This class provides a conversion from generalised Büchi automata into Büchi automata. The conversion preserves determinism.

    This class is also an example on how to do the following:

    • How to implement an OwlModule and derive a standalone tool.
    • How to generate an automaton on-the-fly using the symbolic and explicit API.
    • Field Detail

      • MODULE

        public static final OwlModule<OwlModule.Transformer> MODULE
        Instantiation of the module. We give the name, a short description, and a function to be called for construction of an instance of the module. OwlModule.AutomatonTransformer checks the input passed to the instance of the module and does the necessary transformation to obtain a generalized Büchi automaton if possible. If this is not possible an exception is thrown.

        This object has to be imported by the OwlModuleRegistry in order to be available on the Owl CLI interface.

    • Method Detail

      • main

        public static void main​(String... args)
                         throws IOException
        Entry-point for standalone CLI tool. This class has be registered in build.gradle in the "Startup Scripts" section in order to get the necessary scripts for CLI invocation.
        Parameters:
        args - the arguments
        Throws:
        IOException - the exception