@@ -8,135 +8,80 @@ type Name = internal Name of int
88
99
1010/// <summary >
11- /// Environment mapping symbolic variable names to concrete values.
11+ /// Environment used for generating unique action IDs and as a capability token
12+ /// to enforce compile-time safety. The presence of an Env parameter indicates
13+ /// the execution phase, where symbolic variables can be resolved.
1214/// The SUT is passed separately to Execute, not stored in Env.
1315/// </summary >
1416type Env = private {
15- values: Map < Name , obj >
1617 nextId: int
1718}
1819
1920
2021/// <summary >
2122/// Symbolic variable referencing a command's output. Symbolic variables are placeholders
2223/// that let us chain commands by using one command's result as input to another, even before execution.
23- /// A symbolic variable is not yet bound to a generated value and is used to represent a value in the model before binding occurs.
24+ /// Variables can be either Symbolic (during generation, with optional default values) or
25+ /// Concrete (during execution, with actual runtime values).
2426/// </summary >
2527[<StructuredFormatDisplay( " {DisplayText}" ) >]
26- type Var < 'T > = private {
28+ type Var < 'T > =
29+ internal
2730 /// <summary >
28- /// The unique integer name of the variable.
31+ /// Symbolic variable with an optional default value.
32+ /// None indicates a placeholder created during generation (not yet executed).
33+ /// Some indicates an initial state default value.
2934/// </summary >
30- Name : int
35+ | Symbolic of 'T option
3136 /// <summary >
32- /// Indicates if the variable is bound to a generated value.
37+ /// Concrete variable with an actual runtime value from execution .
3338/// </summary >
34- : bool
35- /// <summary >
36- /// The optional default value for the variable.
37- /// </summary >
38- : 'T option
39- /// <summary >
40- /// Transform function applied when resolving the variable from the environment.
41- /// Handles unboxing and any projections/mappings applied via Var.map.
42- /// </summary >
43- : obj -> 'T
44- /// <summary >
45- /// Mutable field used internally for displaying resolved values in counterexamples.
46- /// Only mutated during test failure formatting, not during normal test execution.
47- ///
48- /// The purpose is to report failure with the concrete state values,
49- /// to make dev experience better when debugging failed tests.
50- ///
51- /// NOT INTENDED TO BE USED FOR ANY OTHER PURPOSE.
52- /// </summary >
53- mutable ResolvedValue: 'T option
54- }
39+ | Concrete of 'T
5540with
5641 /// <summary >
57- /// Gets the unique integer name of the variable .
42+ /// Gets whether the variable has been bound to a concrete execution value .
5843/// </summary >
59- member this.VarName = this.Name
60-
61- /// <summary >
62- /// Gets whether the variable is bound to a generated value.
63- /// </summary >
64- member this.IsBounded = this.Bounded
44+ member this.IsBounded =
45+ match this with
46+ | Concrete _ -> true
47+ | Symbolic _ -> false
6548
6649 member private this.DisplayText =
67- // If resolved for display (during counterexample formatting), show the resolved value
68- match this.ResolvedValue with
69- | Some resolved -> $" %A "
70- | None ->
71- if this.Bounded then
72- match this.Default with
73- | Some d -> $" %A "
74- | None -> $" Var_%d "
75- else
76- match this.Default with
77- | Some d -> $" %A "
78- | None -> " <no value> (symbolic)"
50+ match this with
51+ | Concrete value -> $" %A "
52+ | Symbolic ( Some defaultValue) -> $" %A "
53+ | Symbolic None -> " <symbolic>"
7954
8055 /// <summary >
81- /// Resolve the variable using its default if not found in the environment.
56+ /// Resolve the variable to its value.
57+ /// Requires Env parameter as a capability token to enforce that resolution
58+ /// only happens during execution phase (Execute, Require, Ensure methods).
8259/// </summary >
83- /// <param name =" env " >The environment to resolve the variable from .</param >
60+ /// <param name =" env " >The environment capability token .</param >
8461/// <returns >The resolved value of the variable.</returns >
8562member this.Resolve ( env : Env ) : 'T =
86- if not this.Bounded then
87- match this.Default with
88- | Some d -> d
89- | None -> failwithf " Symbolic var must have a default value"
90- else
91- match Map.tryFind ( Name this.Name) env.values with
92- | Some v -> this.Transform v
93- | None ->
94- match this.Default with
95- | Some d -> d
96- | None -> failwithf $" Var %A "
63+ match this with
64+ | Concrete value -> value
65+ | Symbolic ( Some defaultValue) -> defaultValue
66+ | Symbolic None -> failwith " Cannot resolve symbolic variable without a default value"
9767
9868 /// <summary >
99- /// Resolve the variable with an explicit fallback value, overriding the variable's default .
69+ /// Resolve the variable with an explicit fallback value.
10070/// </summary >
101- /// <param name =" env " >The environment to resolve the variable from .</param >
102- /// <param name =" fallback " >The fallback value to use if the variable is not found .</param >
103- /// <returns >The resolved value or the fallback if not found .</returns >
71+ /// <param name =" env " >The environment capability token .</param >
72+ /// <param name =" fallback " >The fallback value to use if the variable is symbolic without a default .</param >
73+ /// <returns >The resolved value or the fallback.</returns >
10474member this.ResolveOr ( env : Env , fallback : 'T ) : 'T =
105- if not this.Bounded then
106- fallback // Override default for unbounded
107- else
108- match Map.tryFind ( Name this.Name) env.values with
109- | Some v -> this.Transform v
110- | None -> fallback
111-
112- /// <summary >
113- /// Set the resolved value for display purposes during counterexample formatting.
114- /// This should only be called internally by StateFormatter during test failure formatting.
115- /// </summary >
116- /// <param name =" env " >The environment to resolve the variable from.</param >
117- member internal this.SetResolvedValue ( env : Env ) : unit =
118- try
119- let resolved = this.Resolve( env)
120- this.ResolvedValue <- Some resolved
121- with
122- | _ -> () // If resolution fails, leave ResolvedForDisplay as None
123-
124- static member internal CreateSymbolic ( value : 'T ) : Var < 'T > =
125- { Name = - 1 ; Bounded = false ; Default = Some value; Transform = unbox< 'T>; ResolvedValue = Some value }
75+ match this with
76+ | Concrete value -> value
77+ | Symbolic ( Some defaultValue) -> defaultValue
78+ | Symbolic None -> fallback
12679
12780
12881module internal Env =
12982 /// Empty environment
130- let empty : Env = { values = Map.empty ; nextId = 0 }
83+ let empty : Env = { nextId = 0 }
13184
132- /// Generate a fresh variable name
85+ /// Generate a fresh action ID
13386let freshName ( env : Env ) : Name * Env =
13487 Name env.nextId, { env with nextId = env.nextId + 1 }
135-
136- /// Store a concrete value for a variable
137- let add ( v : Var < 'a >) ( value : 'a ) ( env : Env ) : Env =
138- { env with values = Map.add ( Name v.Name) ( box value) env.values }
139-
140- /// Resolve a variable to its concrete value
141- let resolve < 'T > ( v : Var < 'T >) ( env : Env ) : 'T =
142- v.Resolve( env)
0 commit comments