Package ptolemy.vergil.basic.imprt.g4ltl

Class G4LTL

  • public class G4LTL
extends java.lang.Object
    Run the LTL synthesis (G4LTL) tool on a model.

    "G4LTL is a standalone tool and a Java library for automatically generating controllers realizing linear temporal logic (LTL).

    See http://sourceforge.net/projects/g4ltl/

    This class uses classes defined in $PTII/lib/g4ltl.jar. See $PTII/lib/g4ltl-license.htm.

    This class defines static methods for generating moml and updating models based on the contents of an LTL file.

    Since:
    Ptolemy II 10.0
    Version:
    $Id$
    Author:
    Chihhong (Patrick) Cheng (Fortiss), Christopher Brooks. Based on ExportPDFAction by Edward A. Lee
    Pt.AcceptedRating:
    Red (cxh)
    Pt.ProposedRating:
    Red (cxh)

    • Constructor Summary

      Constructors 
      Constructor Description
      G4LTL()  

    • Method Summary

      All Methods Static Methods Concrete Methods 
      Modifier and Type Method Description
      static java.lang.String generateMoML​(java.io.File ltlFile, int optionTechnique, int unrollSteps, boolean findStrategy, NamedObj context)
      Given a Linear Temporal Logic (LTL) file, generate the corresponding MoML and update the MoML.
      static g4ltl.utility.ResultLTLSynthesis synthesizeFromFile​(g4ltl.SolverUtility solver, java.io.File ltlFile, int optionTechnique, int unrollSteps, boolean findStrategy)
      Given a Linear Temporal Logic (LTL) file, generate the corresponding MoML.
      static java.lang.String updateModel​(java.lang.String updatedMoML, NamedObj context)
      Update the model with MoML that was presumably generated by generateMoML().

      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

    • Constructor Detail

      • G4LTL

        public G4LTL()

    • Method Detail

      • synthesizeFromFile

        public static g4ltl.utility.ResultLTLSynthesis synthesizeFromFile​(g4ltl.SolverUtility solver,
                                                                  java.io.File ltlFile,
                                                                  int optionTechnique,
                                                                  int unrollSteps,
                                                                  boolean findStrategy)
                                                           throws java.lang.Exception
        Given a Linear Temporal Logic (LTL) file, generate the corresponding MoML.
        Parameters:
        solver - The G4LTL Solver to use.
        ltlFile - The ltl file.
        optionTechnique - and integer where 0 means CoBeuchi, 1 means Beuchi
        unrollSteps - The number of unroll steps.
        findStrategy - True if a strategy should be found, false if a counter-strategy should be found. Typically a strategy is found first and then if the result does not contain a "<", this method is called with findStrategy set to false to find a counter-strategy.
        Returns:
        The moml of a state machine that represents the LTL file.
        Throws:
        java.lang.Exception - If thrown while synthesizing.

      • generateMoML

        public static java.lang.String generateMoML​(java.io.File ltlFile,
                                            int optionTechnique,
                                            int unrollSteps,
                                            boolean findStrategy,
                                            NamedObj context)
                                     throws java.lang.Exception
        Given a Linear Temporal Logic (LTL) file, generate the corresponding MoML and update the MoML.

        This is the main entry point for non-gui use of the g4ltl package. If finding a strategy fails the gui may want to ask the user if they want to find a counter strategy.

        Parameters:
        ltlFile - The ltl file.
        optionTechnique - and integer where 0 means CoBeuchi, 1 means Beuchi
        unrollSteps - The number of unroll steps.
        findStrategy - True if a strategy should be found, false if a counter-strategy should be found. If a strategy cannot be found, then a counter-strategy is searched for.
        context - The context for the change. One way to get the context is by calling basicGraphFrame.getModel().
        Returns:
        The name of the state machine that was created.
        Throws:
        java.lang.Exception - If thrown while synthesizing.

      • updateModel

        public static java.lang.String updateModel​(java.lang.String updatedMoML,
                                           NamedObj context)
                                    throws java.lang.Exception
        Update the model with MoML that was presumably generated by generateMoML().
        Parameters:
        updatedMoML - The moml from generateMoML()
        context - The context for the change. One way to get the context is by calling basicGraphFrame.getModel().
        Returns:
        The name of the state machine that was created.
        Throws:
        java.lang.Exception - If thrown while synthesizing.