Module dev.civl.abc

Package dev.civl.abc.ast.node.IF.acsl

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:

• ContractNode

Nested Class Summary

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.ASTNode

ASTNode.NodeKind

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.acsl.ContractNode

ContractNode.ContractKind

Method Summary

Modifier and Type	Method	Description
DependsNode	copy()	Returns a deep copy of this AST node.
SequenceNode<DependsEventNode>	getEventList()	Gets the list of events specified by this depends clause

Methods inherited from interface dev.civl.abc.ast.node.IF.ASTNode

addAllTransformAnnotations, addTransformAnnotation, child, childIndex, children, diff, equiv, getAttribute, getOwner, getScope, getSource, id, keepOnly, nextDFS, nodeKind, numChildren, parent, prettyPrint, prettyRepresentation, prettyRepresentation, print, remove, removeChild, removeTransformAnnotation, setAttribute, setChild, setId, setOwner, setScope, toString, transformAnnotations

Methods inherited from interface dev.civl.abc.ast.node.IF.acsl.ContractNode

contractKind

Method Details

getEventList

SequenceNode<DependsEventNode> 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