Module dev.civl.mc
Package dev.civl.mc.state.IF

Interface State

public interface State
A State represents the (global) state of a CIVL Model. It encodes:
  • a set of process states
  • a set of dynamic scopes
  • a path condition

The data listed above comprise the "intrinsic data" of the state. A State may have additional "extrinsic data" but they should not affect the equals or hashCode methods. Those methods should depend only on the three intrinsic data listed above.

States should be immutable (or something in between). The contract for the state modules does not specify this. However, states must supply a "commit" method. After invoking this method, the state must be essentially immutable, which means its intrinsic data (and therefore hash code) cannot change. The processes and dynamic scopes are ordered within any one State. However their order may change from State to State. In addition, States may participate in the Flyweight Pattern. We say two states are equivalent if the equals method says they are equal. (This means they have "equal" intrinsic data; the extrinsic data are completely ignored.) The point of the Flyweight Pattern is to choose one representative State from each equivalence class. This pattern is provided through a method in the StateFactory,
invalid reference 
StateFactory#canonic(State)
. That method takes any State, and return the State which is the canonic representative of the given State's equivalence class. The canonic State are also given unique "canonic ID numbers".

  • Method Summary

    Modifier and Type
    Method
    Description
    StringBuffer
    callStackToString()
    Gets the call stack information (function, location, but no dyscope) of each process and return it as a string buffer object.
    DynamicScope
    getDyscope(int id)
    Returns the id-th dynamic scope in this state.
    int
    getDyscope(int pid, int scopeID)
    Given a PID and a static scope ID , returns the ID of the first dyscope corresponding to the static scope and reachable from the given process.
    int
    getDyscope(int pid, Scope scope)
    Given a PID and a static scope, returns the ID of the first dyscope corresponding to the static scope and reachable from the given process.
    int
    getDyscopeID(int pid, Variable variable)
    Given a process ID and a variable, finds the first dyscope containing the variable in the path starting from the dyscope of the current (top) frame of the process call stack and following the parent edges of the dyscope tree.
    dev.civl.sarl.IF.expr.SymbolicExpression[]
    getOutputValues(String[] outputNames)
    Returns value of the output variables in the order of the given list of output names.
    int
    getParentId(int dyscopeId)
    Gets the dynamic scope ID (dyscope ID) of the parent of the dynamic scope with the given dyscope ID.
    dev.civl.sarl.IF.expr.BooleanExpression
    getPathCondition(dev.civl.sarl.IF.SymbolicUniverse universe)
    Returns the path condition.
    dev.civl.sarl.IF.expr.BooleanExpression
    getPermanentPathCondition()
    Returns the path condition, excluding the partial path conditions held by the process states.
    ProcessState
    getProcessState(int pid)
    Returns the process state for the pid-th process.
    Iterable<? extends ProcessState>
    getProcessStates()
    Returns the set of process states as an Iterable.
    dev.civl.sarl.IF.expr.SymbolicExpression
    getVariableValue(int dyscopeID, int variableID)
    Given a dyscope ID and a variable ID, returns the value of the first corresponding variable.
    String
    identifier()
    The string of the form canonicId:instanceId.
    boolean
    isFinalState()
    Is this the final state upon execution termination? A state is considered as a final state if it has only one process and the process has empty call stack.
    boolean
    isMonitoringReads(int pid)
     
    boolean
    isMonitoringWrites(int pid)
     
    int
    numberOfReachers(int sid)
    How many processes can reach this dynamic scope? A process p can reach a dynamic scope d iff there is a path starting from a dynamic scope which is referenced in a frame on p's call stack to d, following the "parent" edges in the scope tree.
    int
    numDyscopes()
    Returns the number of dynamic scopes in this state.
    int
    numLiveProcs()
    Returns the number of "live" processes.
    int
    numProcs()
    Returns the number of process states in this state.
    void
    print(PrintStream out)
    Prints the state to a given print stream.
    boolean
    reachableByProcess(int sid, int pid)
    Is this dynamic scope reachable by the process with the given PID?
    int
    rootDyscopeID()
    Returns the dynamic scope ID of the root (or "system") scope.
    dev.civl.sarl.IF.expr.SymbolicExpression
    valueOf(int pid, Variable variable)
    Given a process ID and a variable, returns the value of the variable.

  • Method Details

    • identifier

      String identifier()
      The string of the form canonicId:instanceId. Used to easily identify this instance.
      Returns:
      string canonicId:instanceId

    • numDyscopes

      int numDyscopes()
      Returns the number of dynamic scopes in this state.
      Returns:
      the number of dynamic scopes in this state

    • numProcs

      int numProcs()
      Returns the number of process states in this state.
      Returns:
      the number of process states in this state, including nulls.

    • numLiveProcs

      int numLiveProcs()
      Returns the number of "live" processes. This includes processes which have terminated (i.e., have empty call stack), but have not yet been "waited on". Once a process has been waited on, it is no longer live: it becomes "null" and is eligible for garbage collection.
      Returns:
      the number of non-null process states in this state

    • rootDyscopeID

      int rootDyscopeID()
      Returns the dynamic scope ID of the root (or "system") scope.
      Returns:
      the root dynamic scope ID

    • getPathCondition

      dev.civl.sarl.IF.expr.BooleanExpression getPathCondition(dev.civl.sarl.IF.SymbolicUniverse universe)
      Returns the path condition. This includes the partial path conditions of all process states. See ProcessState.getPartialPathConditions().
      Parameters:
      universe - A reference to a SymbolicUniverse.
      Returns:
      the path condition.

    • getPermanentPathCondition

      dev.civl.sarl.IF.expr.BooleanExpression getPermanentPathCondition()
      Returns the path condition, excluding the partial path conditions held by the process states.
      Returns:
      the permanent path condition.

    • getParentId

      int getParentId(int dyscopeId)
      Gets the dynamic scope ID (dyscope ID) of the parent of the dynamic scope with the given dyscope ID. If the dynamic scope with the given ID is the root scope (which has no parent), the result is -1.
      Parameters:
      dyscopeId - a dynamic scope ID in the range [0,numScopes-1]
      Returns:
      dynamic scope ID of the parent of the dynamic scope specified by scopeId

    • getDyscopeID

      int getDyscopeID(int pid, Variable variable)
      Given a process ID and a variable, finds the first dyscope containing the variable in the path starting from the dyscope of the current (top) frame of the process call stack and following the parent edges of the dyscope tree.
      Parameters:
      pid - The ID of the process whose current dynamic scope is the starting point of the search
      variable - A (static) variable in the model
      Returns:
      the ID of the first dyscope reachable from the process whose static scope is the scope of the given variable, or -1 if there is no such scope (i.e., if the variable is not visible)

    • getVariableValue

      dev.civl.sarl.IF.expr.SymbolicExpression getVariableValue(int dyscopeID, int variableID)
      Given a dyscope ID and a variable ID, returns the value of the first corresponding variable.
      Parameters:
      dyscopeID - The dynamic scope ID.
      variableID - The variable ID
      Returns:
      The value of the corresponding variable.

    • valueOf

      dev.civl.sarl.IF.expr.SymbolicExpression valueOf(int pid, Variable variable)
      Given a process ID and a variable, returns the value of the variable.
      Parameters:
      pid - The ID of the process whose current dynamic scope is the starting point of the searching.
      variable - The variable whose value is to be searched for.
      Returns:

    • callStackToString

      StringBuffer callStackToString()
      Gets the call stack information (function, location, but no dyscope) of each process and return it as a string buffer object.
      Returns:
      the call stack information of each process

    • getProcessState

      ProcessState getProcessState(int pid)
      Returns the process state for the pid-th process. The process state encodes the state of the call stack for the process. The result could be null when the process has terminated but not yet removed from the state. The processes in this state are numbered with consecutive integers starting from 0. This number is the PID.
      Parameters:
      pid - the process ID
      Returns:
      the process state

    • getDyscope

      DynamicScope getDyscope(int id)
      Returns the id-th dynamic scope in this state. The dynamic scopes are numbered starting from 0. The dynamic scope specifies a value (a symbolic expression) for each variable occurring in the static scope of which the dynamic scope is an instance.
      Parameters:
      id - the dyscope ID, an integer in the range [0,numScopes-1]
      Returns:
      the dynamic scope with that ID

    • getDyscope

      int getDyscope(int pid, Scope scope)
      Given a PID and a static scope, returns the ID of the first dyscope corresponding to the static scope and reachable from the given process. The search starts at the dyscope referenced by the top frame of the process's call stack, and walks its way up in the dyscope tree until it finds a dyscope whose lexical scope is the specified one.
      Parameters:
      pid - The ID of the process whose current dynamic scope is the starting point of the searching.
      scope - The static scope
      Returns:
      the ID of the first dynamic scope corresponding to the static scope and reachable from the given process.

    • getDyscope

      int getDyscope(int pid, int scopeID)
      Given a PID and a static scope ID , returns the ID of the first dyscope corresponding to the static scope and reachable from the given process. The search starts at the dyscope referenced by the top frame of the process's call stack, and walks its way up in the dyscope tree until it finds a dyscope whose lexical scope is the specified one.
      Parameters:
      pid - The ID of the process whose current dynamic scope is the starting point of the searching.
      scope - The static scope ID
      Returns:
      the ID of the first dynamic scope corresponding to the static scope and reachable from the given process.

    • getProcessStates

      Iterable<? extends ProcessState> getProcessStates()
      Returns the set of process states as an Iterable. This should not be modified. It is convenient when you want to iterate over the states, e.g., for (ProcessState p : state.getProcessStates()). Alternatively, you can invoke the iterator() method to get an Iterator.
      Returns:
      iterable object yielding all the process states in this state

    • numberOfReachers

      int numberOfReachers(int sid)
      How many processes can reach this dynamic scope? A process p can reach a dynamic scope d iff there is a path starting from a dynamic scope which is referenced in a frame on p's call stack to d, following the "parent" edges in the scope tree.
      Parameters:
      sid - The dynamic scope ID
      Returns:
      the number of processes which can reach this dynamic scope

    • reachableByProcess

      boolean reachableByProcess(int sid, int pid)
      Is this dynamic scope reachable by the process with the given PID?
      Parameters:
      sid - The dynamic scope ID
      pid - the process ID (PID)
      Returns:
      true iff this dynamic scope is reachable from the process with pid PID

    • print

      void print(PrintStream out)
      Prints the state to a given print stream.
      Parameters:
      out - The print stream to be used.

    • getOutputValues

      dev.civl.sarl.IF.expr.SymbolicExpression[] getOutputValues(String[] outputNames)
      Returns value of the output variables in the order of the given list of output names.
      Parameters:
      outputNames -
      Returns:

    • isFinalState

      boolean isFinalState()
      Is this the final state upon execution termination? A state is considered as a final state if it has only one process and the process has empty call stack.
      Returns:

    • isMonitoringWrites

      boolean isMonitoringWrites(int pid)
      Parameters:
      pid - The PID of the process who will be tested if it is monitoring write operations.
      Returns:
      True iff any change of variables and memory heap objects by this process of this state will be recorded.

    • isMonitoringReads

      boolean isMonitoringReads(int pid)
      Parameters:
      pid - The PID of the process who will be tested if it is monitoring read operations.
      Returns:
      True iff any read of objects by this process of this state will be recorded.