Class StateGraphNode

Namespace

Microsoft.Accordant

Assembly

Accordant.dll

A state graph node represents a unique state along with the set of step functions that can be applied to that state (if enabled). The state and set of step functions lead to a unique node fingerprint.

public class StateGraphNode

Inheritance

object

StateGraphNode

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.MemberwiseClone()

object.ReferenceEquals(object, object)

object.ToString()

Properties

Edges

Edges which lead to the outgoing set of state graph nodes.

For lazily explored nodes the outgoing edges are computed and memoized on first access via Microsoft.Accordant.StateGraphNode.EnsureExpanded(). This makes on-the-fly model checking transparent to every consumer that walks the graph through Edges (emptiness checkers, dot visualization, BFS traversals) — the graph materializes only as far as it is actually walked.

public List<StateGraphEdge> Edges { get; set; }

Property Value

List<StateGraphEdge>

State

The system state represented by this node.

public IState State { get; set; }

Property Value

IState

StepFunctions

The set of step functions that can be applied to this state. Once a step function is applied, it is consumed and not part of the updated state (though a step function can produce new step functions that are included in the step function list for the updated state).

public IList<IStepFunction> StepFunctions { get; set; }

Property Value

IList<IStepFunction>

Methods

CreateCountBasedNodeLabelLambda()

This method creates a count based node label lambda, where it returns a a label with a monotonically increasing count each time it's called, so a sequence like N1, N2, N3, ... and so on.

public static Func<StateGraphNode, string> CreateCountBasedNodeLabelLambda()

Returns

Func<StateGraphNode, string>

DefaultNodeLabelLambda(StateGraphNode)

This method prints out the literal contents of the node in the state graph node.

public static string DefaultNodeLabelLambda(StateGraphNode node)

Parameters

node StateGraphNode

Returns

string

GenerateDotFileContent(StateGraphNode, Func<StateGraphNode, string>, bool)

This method generates a GraphViz dot file to help visualize the state graph.

public static string GenerateDotFileContent(StateGraphNode rootNode, Func<StateGraphNode, string> nodeLabelLambda = null, bool showStepFunctionsInNode = true)

Parameters

rootNode StateGraphNode

nodeLabelLambda Func<StateGraphNode, string>

showStepFunctionsInNode bool

Returns

string

GenerateDotFileContent(Func<StateGraphNode, string>, bool)

public string GenerateDotFileContent(Func<StateGraphNode, string> nodeLabelLambda = null, bool showStepFunctionsInNode = true)

Parameters

nodeLabelLambda Func<StateGraphNode, string>

showStepFunctionsInNode bool

Returns

string

GetNodeFingerprint()

Returns the node fingerprint which is a hash computed over the state hash along with the set of step functions that can be applied to this state (if enabled).

public string GetNodeFingerprint()

Returns

string

GetNodeFingerprint(IState, IList<IStepFunction>)

public static string GetNodeFingerprint(IState state, IList<IStepFunction> stepFunctions)

Parameters

state IState

stepFunctions IList<IStepFunction>

Returns

string