Harden state exploration with fail-fast validation and immutable graph diagnostics

Accordant.Operations/GenerationAlgorithms/ConcurrentTestCaseAlgorithms.cs

@@ -103,7 +103,7 @@ void Recurse(StateGraphNode node, HashSet<ulong> visitedHashes, List<OperationCa
                 else
                 {
                     var concurrentEdgeList = GetCombinations(
-                        edgeList,
+                        edgeList.ToList(),
                         maxConcurrencyLevel);
 
                     foreach (var subset in concurrentEdgeList)

Accordant/Exceptions/StepFunctionApplicationException.cs

@@ -5,6 +5,7 @@ namespace Microsoft.Accordant;
 
 using System;
 using System.Collections.Generic;
+using System.Linq;
 
 /// <summary>
 /// This is an exception thrown during state graph exploration
@@ -22,28 +23,36 @@ public class StepFunctionApplicationException : Exception
     /// The state graph node at which applying one of its step
     /// functions lead to the exception.
     /// </summary>
-    public StateGraphNode ExceptionEncounteringNode { get; set; }
+    public StateGraphNode ExceptionEncounteringNode { get; }
 
     /// <summary>
     /// The path from the root node to the node at which the exception
     /// was encountered. The initial step function is null for the starting node.
     /// </summary>
-    public IList<(IStepFunction stepFunction, StateGraphNode node)> PathToNode { get; set; }
+    public IReadOnlyList<(IStepFunction stepFunction, StateGraphNode node)> PathToNode { get; }
 
     /// <summary>
     /// The step function that lead to the exception.
     /// </summary>
-    public IStepFunction ExceptionEncounteringStepFunction { get; set; }
+    public IStepFunction ExceptionEncounteringStepFunction { get; }
 
     public StepFunctionApplicationException(
         Exception exception,
         StateGraphNode node,
-        IList<(IStepFunction stepFunction, StateGraphNode node)> pathToNode,
+        IReadOnlyList<(IStepFunction stepFunction, StateGraphNode node)> pathToNode,
         IStepFunction stepFunction)
         : base("Encountered an exception when applying a step function at a node", exception)
     {
-        ExceptionEncounteringNode = node;
-        PathToNode = pathToNode;
-        ExceptionEncounteringStepFunction = stepFunction;
+        if (exception == null)
+        {
+            throw new ArgumentNullException(nameof(exception));
+        }
+
+        ExceptionEncounteringNode = node ?? throw new ArgumentNullException(nameof(node));
+        PathToNode = (pathToNode ?? throw new ArgumentNullException(nameof(pathToNode)))
+            .ToList()
+            .AsReadOnly();
+        ExceptionEncounteringStepFunction = stepFunction ??
+            throw new ArgumentNullException(nameof(stepFunction));
     }
 }

Accordant/State/State.cs

@@ -20,14 +20,13 @@ namespace Microsoft.Accordant;
 /// </summary>
 public abstract class State : IState
 {
-    public static Random Random { get; } = new Random();
-
     /// <summary>
-    /// Controls whether <see cref="ValidateNotMutated"/> performs validation.
-    /// Set to false to disable validation for performance in production scenarios.
+    /// Controls whether <see cref="ValidateNotMutated"/> performs validation
+    /// for this state instance. Set to false only when the caller explicitly
+    /// accepts the loss of mutation detection for this state.
     /// Default is true.
     /// </summary>
-    public static bool EnableFreezeValidation { get; set; } = true;
+    public bool EnableFreezeValidation { get; set; } = true;
 
     protected string stringRepresentation = null;
     protected ulong? stateHash = null;
@@ -93,6 +92,9 @@ public State Clone(Dictionary<object, object> clonedMap)
 
         if (clonedMap[this] is State state)
         {
+            // Validation is an instance option and should follow the state
+            // when it is cloned, while the clone remains unfrozen.
+            state.EnableFreezeValidation = EnableFreezeValidation;
             return state;
         }
         else
@@ -296,6 +298,14 @@ public void Freeze()
 
     public void Freeze(HashSet<object> visited)
     {
+        if (IsFrozen)
+        {
+            // A frozen state is already baselined. Re-freezing must validate
+            // it rather than silently accepting a mutation as the new baseline.
+            ValidateNotMutated();
+            return;
+        }
+
         if (visited.Contains(this))
         {
             return;