Interface DependsNode

All Superinterfaces:
ASTNode, ContractNode

public interface DependsNode extends ContractNode
A depends clause specifies part of the dependence relation used in partial order reduction (POR). It has the syntax
 $depends event0, event1, ...;
 
, where event0, event1, ... are depends events DependsEventNode.

For each process p, the event can be evaluated in the context of p. If event evaluates to be valid, then p must be included in an ample set containing a call to this function. The event e hence defines a predicate d(s,p), where s ranges over states, and p over processes.

See Also:
  • Method Details

    • getEventList

      Gets the list of events specified by this depends clause
      Returns:
      the list of events specified by this depends clause
    • copy

      DependsNode copy()
      Description copied from interface: ASTNode
      Returns a deep copy of this AST node. The node and all of its descendants will be cloned. The cloning does not copy analysis or attribute information.
      Specified by:
      copy in interface ASTNode
      Specified by:
      copy in interface ContractNode
      Returns:
      deep copy of this node