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

Interface ProcessState

public interface ProcessState
A ProcessState represents the state of a process (thread of execution) in a CIVL model. The process has an integer ID number, the PID, unique among the processes in the state. The state of the process is essentially a call stack. The entries on the stack are "activation frames", instances of StackEntry.

  • Method Details

    • hasEmptyStack

      boolean hasEmptyStack()
      Does this process state have an empty call stack?
      Returns:
      true iff the call stack is empty

    • getLocation

      Location getLocation()
      Returns the location at the top of the call stack of this process. Undefined behavior if stack is empty.
      Returns:
      location at top of call stack

    • getPid

      int getPid()
      Returns the process ID (pid) of this process state. Within a fixed state, every process is assigned an integer ID which is unique. It does not necessarily stay the same from state to state though.
      Returns:
      the PID of the process

    • getDyscopeId

      int getDyscopeId()
      The ID of the dynamic scope of the top frame on the call stack. Undefined behavior if call stack is empty.
      Returns:
      the dyscope id of the dyscope on the top frame of the call stack

    • getPartialPathConditions

      dev.civl.sarl.IF.expr.BooleanExpression[] getPartialPathConditions()

    • peekStack

      StackEntry peekStack()
      Returns the top frame on the call stack. Undefined behavior if call stack is empty.
      Returns:
      top frame on call stack.

    • peekSecondLastStack

      StackEntry peekSecondLastStack()
      Returns the second top frame on the call stack. Return NULL if the process has fewer than two stacks.
      Returns:
      top frame on call stack.

    • stackSize

      int stackSize()
      Returns the length of the call stack.
      Returns:
      the length of the call stack

    • getStackEntries

      Iterable<? extends StackEntry> getStackEntries()
      Returns an iterable object over the entries in this stack. Order is fixed from top to bottom.
      Returns:
      the entries in the stack

    • bottomToTopIterator

      Iterator<? extends StackEntry> bottomToTopIterator()
      Returns an iterator over the entries in the call stack from the bottom to the top.
      Returns:
      iterator from bottom to top

    • print

      void print(PrintStream out, String prefix)
      Prints a human-readable form of this process state.
      Parameters:
      out - print stream to which the output is sent
      prefix - a string to prepend to each line of output

    • incrementAtomicCount

      ProcessState incrementAtomicCount()
      Increase the atomic block counter. Invoked when encountering a new atomic block.
      Returns:
      A new process state with the atomic block counter increased by one and other fields remain unchanged.

    • decrementAtomicCount

      ProcessState decrementAtomicCount()
      Decrease the atomic block counter. Invoked when reaching the end of a certain atomic block.
      Returns:
      A new process state with the atomic block counter decreased by one and other fields remain unchanged.

    • inAtomic

      boolean inAtomic()
      Check if the current process is in the execution of some atomic block.
      Returns:
      True if the current process is executing some atomic block.

    • isSelfDestructable

      boolean isSelfDestructable()
      Returns:
      True if and only if this process is "self-destructable" i.e. This process doesn't need an explicit $wait to destroy it. It will destroy itself after it terminates.

    • atomicCount

      int atomicCount()
      Returns:
      The number of $atomic blocks that are currently being executed in this process

    • toStringBuffer

      StringBuffer toStringBuffer(String prefix)

    • name

      String name()
      This name is not part of the state.
      Returns:
      The name of this process, in the form of ,p +PID, e.g. p2, p3.

    • getReachableMemUnitsWoPointer

      Map<dev.civl.sarl.IF.expr.SymbolicExpression,Boolean> getReachableMemUnitsWoPointer()

    • getReachableMemUnitsWtPointer

      Map<dev.civl.sarl.IF.expr.SymbolicExpression,Boolean> getReachableMemUnitsWtPointer()

    • toSBrieftringBuffer

      StringBuffer toSBrieftringBuffer()