Package ptolemy.domains.modal.kernel.fmv

Class FmvAutomaton

  • All Implemented Interfaces:
    java.lang.Cloneable, Actor, Executable, Initializable, TypedActor, ExplicitChangeContext, Changeable, Debuggable, DebugListener, Derivable, Instantiable, ModelErrorHandler, MoMLExportable, Moveable, Nameable
    @Deprecated
public class FmvAutomaton
extends FSMActor
    Deprecated.
    ptolemy.de.lib.TimedDelay is deprecated, use ptolemy.actor.lib.TimeDelay.
    A Formal Method Verification (FMV) Automaton. An FmvAutomaton is not different from a regular FSM, but the class definition provides a specialized environment to convert into format acceptable by model checker NuSMV. Also, the state insertion of FmvAutomaton supports the inserting of FmvState, where these specialized states are able to have property indicating whether it is a risk state.
    Since:
    Ptolemy II 8.0
    Version:
    $Id$
    Author:
    Chihhong Patrick Cheng, Contributor: Edward A. Lee
    See Also:
    State, Transition, FmvState
    Pt.AcceptedRating:
    Red (patrickj)
    Pt.ProposedRating:
    Red (patrickj)

    • Constructor Detail

      • FmvAutomaton

        public FmvAutomaton()
        Deprecated.
        Construct an FmvAutomaton in the default workspace with an empty string as its name. Add the actor to the workspace directory. Increment the version number of the workspace.

      • FmvAutomaton

        public FmvAutomaton​(Workspace workspace)
        Deprecated.
        Construct an FmvAutomaton in the specified workspace with an empty string as its name. The name can be changed later with setName(). If the workspace argument is null, then use the default workspace. Add the actor to the workspace directory. Increment the version number of the workspace.
        Parameters:
        workspace - The workspace that will list the actor.

      • FmvAutomaton

        public FmvAutomaton​(CompositeEntity container,
                    java.lang.String name)
             throws IllegalActionException,
                    NameDuplicationException
        Deprecated.
        Create an FmvAutomaton in the specified container with the specified name. The name must be unique within the container or an exception is thrown. The container argument must not be null, or a NullPointerException will be thrown.
        Parameters:
        container - The container.
        name - The name of this automaton within the container.
        Throws:
        IllegalActionException - If the entity cannot be contained by the proposed container.
        NameDuplicationException - If the name coincides with an entity already in the container.

    • Method Detail

      • convertToSMVFormat

        public java.lang.StringBuffer convertToSMVFormat​(java.lang.String formula,
                                                 MathematicalModelConverter.FormulaType choice,
                                                 int span)
                                          throws IllegalActionException
        Deprecated.
        Return an StringBuffer that contains the .smv format of the FmvAutomaton.
        Parameters:
        formula - The temporal formula used to be attached in the .smv file.
        choice - The type of the formula. It may be either a CTL or LTL formula.
        span - A constant used to expand the size of the rough domain.
        Returns:
        The .smv format of the FmvAutomaton.
        Throws:
        IllegalActionException - If there is a problem with the conversion.