Package org.svvrl.goal.core.tran.tester

Class FDS

java.lang.Object
org.svvrl.goal.core.tran.tester.FDS
public class FDS
extends java.lang.Object
Represents Fair Discrete System. Includes all critical components of an FDS.
Author:
Wen-Chin Chan

  • Constructor Details

    • FDS

      public FDS​(FDS fds)
      Constructor of FDS.
      Parameters:
      fds - an FDS

    • FDS

      public FDS​(LTL qptl)
      The constructor of the FDS.
      Parameters:
      qptl - an LTL formula

  • Method Details

    • getFormula

      public LTL getFormula()
      Returns the LTL formula.
      Returns:
      the LTL formula

    • getTransitionFromStateMap

      public java.util.HashMap<FDSState,​java.util.List<FDSTransition>> getTransitionFromStateMap()
      Returns the map from an FDS state to transitions from the state.
      Returns:
      the map from an FDS state to transitions from the state

    • getTransitionToStateMap

      public java.util.HashMap<FDSState,​java.util.List<FDSTransition>> getTransitionToStateMap()
      Returns the map from an FDS state to transitions to the state.
      Returns:
      the map from an FDS state to transitions to the state

    • getTransitionsFromState

      public java.util.List<FDSTransition> getTransitionsFromState​(FDSState from)
      Returns the transitions from a specified FDS state.
      Parameters:
      from - an FDS state
      Returns:
      the transitions from from

    • getTransitionsToState

      public java.util.List<FDSTransition> getTransitionsToState​(FDSState to)
      Returns the transitions to a specified FDS state.
      Parameters:
      to - an FDS state
      Returns:
      the transitions to to

    • getTransitionFromStateToState

      public FDSTransition getTransitionFromStateToState​(FDSState from, FDSState to)
      Returns the transition from a specified source state to a specified destination state.
      Parameters:
      from - a source state
      to - a destination state
      Returns:
      the transition from from to to

    • evaluate

      public boolean evaluate​(LTL qptl, FDSState from, FDSState to) throws java.lang.UnsupportedOperationException
      Evaluates the transition relation between from state and to state. If the states satisfy the transition, the result is true.
      Parameters:
      qptl - an LTL formula
      from - an FDS state
      to - an FDS state
      Returns:
      true if there should be a transition from state from to state to
      Throws:
      java.lang.UnsupportedOperationException - if some operator in qptl is not supported

    • getStateWithID

      public FDSState getStateWithID​(int id)
      This method gets the state by id.
      Parameters:
      id - an ID
      Returns:
      an FDS state with ID id

    • createState

      public FDSState createState()
      This method creates a FDS state.
      Returns:
      a FDS state created

    • getSystemVariable

      public SystemVariable getSystemVariable()
      Returns the system variable.
      Returns:
      the system variable

    • getInitialCondition

      public InitialCondition getInitialCondition()
      Returns the initial condition.
      Returns:
      the initial condition

    • getTransitionRelation

      public TransitionRelation getTransitionRelation()
      Returns the transition relation.
      Returns:
      the transition relation

    • getFairnessRequirement

      public FairnessRequirement getFairnessRequirement()
      Returns the fairness requirement.
      Returns:
      the fairness requirement

    • getStateSet

      public java.util.Set<java.util.Set<LTL>> getStateSet()
      Returns the state set.
      Returns:
      the state set

    • getStates

      public java.util.Set<FDSState> getStates()
      Returns the FDS states
      Returns:
      the FDS states

    • getInitialStates

      public java.util.Set<FDSState> getInitialStates()
      Returns the initial state.
      Returns:
      the initial state

    • getTransitions

      public java.util.Set<FDSTransition> getTransitions()
      Returns the transitions.
      Returns:
      the transitions

    • getFinalStateSet

      public java.util.Set<java.util.Set<FDSState>> getFinalStateSet()
      Returns the final states.
      Returns:
      the final states

    • setSystemVariable

      public void setSystemVariable​(SystemVariable sysVar)
      Sets the system variable.
      Parameters:
      sysVar - a system variable