CONSTANT p1 = p1
CONSTANT p2 = p2
CONSTANT defaultInitValue = defaultInitValue

CONSTANT Edges <- CartEdges
CONSTANT Nodes = {1,2,3}

CONSTANT Threads = {p1, p2}
SYMMETRY SymmetryThreads

SPECIFICATION Spec
INVARIANT Correct

POSTCONDITION PostCondition

CONSTANT p1 = p1
CONSTANT p2 = p2
CONSTANT defaultInitValue = defaultInitValue

CONSTANT Edges <- CartEdges
CONSTANT Nodes = {1,2,3,4}

CONSTANT Threads = {p1, p2}
SYMMETRY SymmetryThreads

SPECIFICATION Spec
INVARIANT Correct

POSTCONDITION PostCondition

Change from Bleoemen model from three to four nodes for performance benchmark to run long enough.
Change from Bleoemen model from three to four nodes for performance
benchmark to run long enough.

[Performance][TLC]