ptolemy.vergil.basic.imprt.g4ltl

Class G4LTL

java.lang.Object

ptolemy.vergil.basic.imprt.g4ltl.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: G4LTL.java 70402 2014-10-23 00:52:20Z cxh $

Author:

Chihhong (Patrick) Cheng (Fortiss), Christopher Brooks. Based on ExportPDFAction by Edward A. Lee

Accepted Rating:

Red (cxh)

Proposed Rating:

Red (cxh)

Constructor Summary

Constructors

Constructor and Description
G4LTL()

Method Summary

Modifier and Type	Method and 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.