Fest scenario coverage: robustness hardening (cold start-state, merge version guard, dead liveness overload)

Src/PChecker/CheckerCore/CheckerCore.csproj

@@ -23,4 +23,11 @@
         <None Include="../../../Icon/icon.png" Pack="true" PackagePath="" />
         <None Include="../../../README.md" Pack="true" PackagePath="" />
     </ItemGroup>
+    <!-- Expose internal types (e.g. ScenarioComplianceObserver, FeedbackGuidedStrategy) to the
+         unit-test assembly so the high-risk runtime seams can be driven directly by tests. -->
+    <ItemGroup>
+        <AssemblyAttribute Include="System.Runtime.CompilerServices.InternalsVisibleToAttribute">
+            <_Parameter1>UnitTests</_Parameter1>
+        </AssemblyAttribute>
+    </ItemGroup>
 </Project>

Src/PChecker/CheckerCore/Runtime/Specifications/Monitor.cs

@@ -640,21 +640,6 @@ internal void CheckLivenessTemperature()
             }
         }
 
-        /// <summary>
-        /// Checks the liveness temperature of the monitor and report
-        /// a potential liveness bug if the temperature passes the
-        /// specified threshold. Only works in a liveness monitor.
-        /// </summary>
-        internal void CheckLivenessTemperature(int livenessTemperature)
-        {
-            if (livenessTemperature > Runtime.CheckerConfiguration.LivenessTemperatureThreshold)
-            {
-                Runtime.Assert(
-                    livenessTemperature <= Runtime.CheckerConfiguration.LivenessTemperatureThreshold,
-                    $"{GetType().FullName} detected infinite execution that violates a liveness property.");
-            }
-        }
-
         /// <summary>
         /// Returns true if the monitor is in a hot state.
         /// </summary>

Src/PChecker/CheckerCore/SystematicTesting/ScenarioCoverageMerger.cs

@@ -93,8 +93,10 @@ public static void Write(TestReport report, string testCaseName, string path)
 
         /// <summary>
         /// Reads every <c>*_scenario_coverage.json</c> artifact under <paramref name="directory"/>
-        /// and produces a unified suite-wide report: per scenario, the total triggers and unique
-        /// satisfying timelines summed across test cases, the number of test cases that covered it,
+        /// and produces a unified suite-wide report: per scenario, the total triggers and
+        /// satisfying timelines SUMMED across test cases (raw timelines are gone by merge time, so
+        /// this is a per-test-case sum, not a global-distinct count), the number of test cases that
+        /// covered it,
         /// and the best partial progress anywhere.
         /// </summary>
         public static string MergeDirectory(string directory)
@@ -110,6 +112,15 @@ public static string MergeDirectory(string directory)
                 {
                     var a = JsonSerializer.Deserialize<ScenarioCoverageArtifact>(File.ReadAllText(file), JsonOptions);
                     if (a == null) continue;
+                    // Forward-compat guard: a newer artifact schema may have changed field
+                    // meanings, so merging it as v1 would silently miscount. Skip it loudly
+                    // rather than produce a wrong number. (This is why Version is written.)
+                    if (a.Version > SchemaVersion)
+                    {
+                        Console.WriteLine($"... Skipping scenario artifact {file}: schema version {a.Version} is " +
+                                          $"newer than this tool supports (v{SchemaVersion}); upgrade P to merge it.");
+                        continue;
+                    }
                     var when = File.GetLastWriteTimeUtc(file);
                     var key = a.TestCase ?? string.Empty;
                     if (!latest.TryGetValue(key, out var cur) || when > cur.when)
@@ -177,7 +188,7 @@ public static string Merge(IReadOnlyList<ScenarioCoverageArtifact> artifacts)
                 report.AppendLine(
                     $"  [covered] {scenario}: covered in {cases.Count}/{testCasesTotal[scenario]} test cases " +
                     $"({string.Join(", ", cases)}); {triggered[scenario]} total triggers, " +
-                    $"{uniqueTimelines[scenario]} unique satisfying timelines");
+                    $"{uniqueTimelines[scenario]} satisfying timelines (summed per test case)");
             }
             foreach (var scenario in gaps)
             {

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/ScenarioComplianceObserver.cs

@@ -31,6 +31,11 @@ internal class ScenarioComplianceObserver : IControlledRuntimeLog
     // Short names (P scenario names) of scenarios satisfied at least once this iteration.
     private readonly HashSet<string> _satisfied = new();
 
+    // Scenarios whose initial (start) state-entry has already been seen. A monitor's very
+    // first state-entry is its start state, logged during RegisterMonitor before any observed
+    // behavior; a cold start state must NOT count as satisfied (see ScenarioSteering.IsSatisfyingEntry).
+    private readonly HashSet<string> _sawStartEntry = new();
+
     // Short name -> distinct states entered this iteration (partial-progress signal).
     private readonly Dictionary<string, HashSet<string>> _statesReached = new();
 
@@ -114,8 +119,11 @@ public void OnMonitorStateTransition(string monitorType, string stateName, bool
         }
         states.Add(stateName);
 
-        // Entering a cold (accepting) state == scenario satisfied.
-        if (isInHotState == false)
+        // Entering a cold (accepting) state == scenario satisfied, EXCEPT the monitor's very
+        // first (start) state entry (logged during RegisterMonitor, before any observed event):
+        // a cold start state is not "covered" until real behavior re-enters an accepting state.
+        var isStartEntry = _sawStartEntry.Add(scenario); // true only on this scenario's first entry
+        if (ScenarioSteering.IsSatisfyingEntry(isInHotState, isStartEntry))
         {
             _satisfied.Add(scenario);
         }

Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/ScenarioSteering.cs

@@ -68,4 +68,17 @@ public static double NoveltyCompliance(
 
         return compliance;
     }
+
+    /// <summary>
+    /// Whether entering a state marks its scenario satisfied. A scenario is satisfied by
+    /// entering an accepting (cold) state (<paramref name="isInHotState"/> == false), EXCEPT
+    /// on the monitor's very first (start) state entry — that entry is logged during
+    /// RegisterMonitor, before any behavior is observed. Without this exception a
+    /// <c>cold start state</c> scenario would be reported "covered" in every schedule with
+    /// zero observed events (a coverage measurement that lies); with it, such a scenario is
+    /// correctly a coverage gap until it re-enters a cold state through observed behavior.
+    /// A hot (true) or unmarked/warm (null) state never satisfies.
+    /// </summary>
+    public static bool IsSatisfyingEntry(bool? isInHotState, bool isStartEntry)
+        => isInHotState == false && !isStartEntry;
 }

Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs

@@ -44,7 +44,11 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
     ///     This compiler has a compilation stage.
     /// </summary>
     public bool HasCompilationStage => true;
-    private static List<Variable> _globalParams = [];
+    // [ThreadStatic] so concurrent in-process compilations do not race on this shared list;
+    // GenerateSource assigns it before any read. (The backend is a shared singleton, so an
+    // instance field would not isolate it.) Mirrors PChecker's already-ThreadStatic _globalParams.
+    [ThreadStatic]
+    private static List<Variable> _globalParams;
 
     private string GetGlobalParamAndLocalVariableName(Variable v)
     {

Src/PCompiler/CompilerCore/Backend/PEx/TransformASTPass.cs

@@ -15,9 +15,11 @@ namespace Plang.Compiler.Backend.PEx;
 
 internal class TransformASTPass
 {
-    private static CompilationContext context;
-    private static int continuationNumber;
-    private static int callNum;
+    // [ThreadStatic] so concurrent in-process compilations do not share the context or interleave
+    // the generated-identifier counters; GetTransformedDecls resets all three before any read.
+    [ThreadStatic] private static CompilationContext context;
+    [ThreadStatic] private static int continuationNumber;
+    [ThreadStatic] private static int callNum;
 
     public static List<IPDecl> GetTransformedDecls(CompilationContext globalContext, Scope globalScope)
     {

Src/PCompiler/CompilerCore/Backend/PObserve/Constants.cs

@@ -277,7 +277,11 @@ internal static string AsFFIComment(string line)
             /*"while",*/
         };
 
-        private static HashSet<string> _reservedWords;
+        // Lazy (thread-safe by default) so concurrent in-process compilations don't race on the
+        // non-atomic lazy init, while preserving the original timing (built on first use, after all
+        // static string fields are initialized, so reflection still captures every reserved word).
+        private static readonly System.Lazy<HashSet<string>> _reservedWords =
+            new(() => ExtractReservedWords().Concat(_javaKeywords).ToHashSet());
 
         /// <summary>
         /// Reflects out all the string fields defined in this class.
@@ -298,10 +302,7 @@ private static HashSet<string> ExtractReservedWords()
         /// </summary>
         public static bool IsReserved(string token)
         {
-            _reservedWords ??= ExtractReservedWords()
-                .Concat(_javaKeywords)
-                .ToHashSet();
-            return _reservedWords.Contains(token);
+            return _reservedWords.Value.Contains(token);
         }
 
         #endregion

Src/PCompiler/CompilerCore/Backend/PVerifier/Uclid5CodeGenerator.cs

@@ -332,6 +332,7 @@ private void ProcessFailureMessages(List<Match> collection, string[] query, stri
 
     public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope globalScope)
     {
+        useLocalPrefix = false;   // reset per-compile so a prior compile on this thread can't leak state
         _ctx = new CompilationContext(job);
         _optionsToDeclare = [];
         _chooseToDeclare = [];
@@ -568,7 +569,10 @@ private void EmitLine(string str)
     private static string StateAdtReceivedSelector => $"{StateAdt}_Received";
     private static string StateAdtMachinesSelector => $"{StateAdt}_Machines";
 
-    private static bool useLocalPrefix = false;
+    // [ThreadStatic] so concurrent in-process compilations do not race on this transient flag
+    // (set true only within a wrapped block and reset false after). GenerateCode also resets it
+    // per-compile below. The backend is a shared singleton, so an instance field would not isolate it.
+    [ThreadStatic] private static bool useLocalPrefix;
 
     private static string StateAdtConstruct(string sent, string received, string machines)
     {

Src/PCompiler/CompilerCore/TypeChecker/InferMachineCreates.cs

@@ -11,7 +11,11 @@ namespace Plang.Compiler.TypeChecker
 {
     public static class InferMachineCreates
     {
-        // hash table used to store the functions inferred, to handle recursive, cyclic functions
+        // hash table used to store the functions inferred, to handle recursive, cyclic functions.
+        // [ThreadStatic] so concurrent in-process compilations (e.g. the parallel test harness)
+        // each get their own set instead of racing on a shared one (Populate reassigns it before
+        // any read, so per-thread default-null is safe). Mirrors the PChecker backend's _globalParams.
+        [ThreadStatic]
         private static HashSet<Function> _visitedFunctions;
         public static void Populate(Machine machine, ITranslationErrorHandler handler)
         {

Src/PCompiler/CompilerCore/TypeChecker/MachineChecker.cs

@@ -24,6 +24,20 @@ public static void Validate(ITranslationErrorHandler handler, Machine machine, I
             // a scenario (coverage monitor) needs an accepting (cold) state, otherwise
             // it can never be marked satisfied and will always report 0 coverage.
             ValidateScenarioHasColdState(machine, job);
+            // and its start state should not be cold, else it is trivially "covered".
+            ValidateScenarioStartStateNotCold(machine, job);
+        }
+
+        private static void ValidateScenarioStartStateNotCold(Machine machine, ICompilerConfiguration job)
+        {
+            if (machine.IsScenario && machine.StartState?.Temperature == StateTemperature.Cold)
+            {
+                job.Output.WriteWarning(
+                    $"[{machine.SourceLocation.Start.Line}] scenario '{machine.Name}' has a 'cold' (accepting) " +
+                    "start state; it accepts before any behavior is observed, so it is NOT counted as covered " +
+                    "until observed events re-enter an accepting state. Mark the start state 'hot' (or leave it " +
+                    "unmarked) and mark the accepting state 'cold'.");
+            }
         }
 
         private static void ValidateScenarioHasColdState(Machine machine, ICompilerConfiguration job)

Tst/UnitTests/FeedbackGuidedStrategyTest.cs

@@ -0,0 +1,125 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Reflection;
+using NUnit.Framework;
+using PChecker;
+using PChecker.Feedback;
+using PChecker.Generator.Object;
+using PChecker.Runtime;
+using PChecker.Runtime.Events;
+using PChecker.Runtime.StateMachines;
+using PChecker.SystematicTesting.Strategies.Feedback;
+using PChecker.SystematicTesting.Strategies.Probabilistic;
+
+namespace UnitTests
+{
+    /// <summary>
+    /// Integration tests for <see cref="FeedbackGuidedStrategy.ObserveRunningResults"/> — the
+    /// scenario-steering seam that the pure <c>ScenarioSteering.NoveltyCompliance</c> tests cannot
+    /// reach. Two properties:
+    ///  (i)  a timeline-redundant (diversity ≤ 0) schedule is DISCARDED before its scenario progress
+    ///       is folded into the suite state, so it can't rob a later kept schedule of the novelty
+    ///       boost (guards the `if (diversity <= 0) return;` ordering before NoveltyCompliance);
+    ///  (ii) suite-state is per-strategy-instance, not shared static (guards the instance fields
+    ///       _scenarioSuiteBestReached / _scenarioSuiteSatisfied).
+    /// Both are asserted by COMPARING two strategies (no brittle absolute priority values).
+    /// </summary>
+    [TestFixture]
+    public class FeedbackGuidedStrategyTest
+    {
+        private static FeedbackGuidedStrategy NewStrategy()
+        {
+            var cfg = CheckerConfiguration.Create();
+            var gen = new ControlledRandom(new System.Random(0));
+            var sched = new RandomScheduler(gen);
+            return new FeedbackGuidedStrategy(cfg, gen, sched);
+        }
+
+        // A TimelineObserver populated by delivering `events` to a receiver named `receiver`.
+        // Identical (receiver, events) yield the identical abstract timeline (the exact-duplicate
+        // novelty gate); a different receiver/events yields a distinct one.
+        private static TimelineObserver Obs(string receiver, params Event[] events)
+        {
+            var id = new StateMachineId(typeof(FeedbackGuidedStrategyTest), receiver, null, useNameForHashing: true);
+            var obs = new TimelineObserver();
+            foreach (var e in events)
+            {
+                obs.OnDequeueEvent(id, "", e, null, new VectorTime(id));
+            }
+            return obs;
+        }
+
+        private static IReadOnlyDictionary<string, int> Reached(string s, int n) => new Dictionary<string, int> { [s] = n };
+        private static IReadOnlyCollection<string> Sat(params string[] s) => s;
+        private static readonly IReadOnlyDictionary<string, int> NoReached = new Dictionary<string, int>();
+        private static readonly IReadOnlyCollection<string> NoSat = Array.Empty<string>();
+
+        // Sorted saved-generator priorities (reflection: _savedGenerators is private; GeneratorRecord
+        // and its Priority are public).
+        private static List<double> Priorities(FeedbackGuidedStrategy s)
+        {
+            var field = typeof(FeedbackGuidedStrategy).GetField("_savedGenerators",
+                BindingFlags.NonPublic | BindingFlags.Instance);
+            var list = (IEnumerable<FeedbackGuidedStrategy.GeneratorRecord>)field.GetValue(s);
+            return list.Select(r => r.Priority).OrderBy(x => x).ToList();
+        }
+
+        private static void AssertPrioritiesEqual(List<double> a, List<double> b)
+        {
+            Assert.AreEqual(a.Count, b.Count, "different number of saved generators");
+            for (var i = 0; i < a.Count; i++)
+            {
+                Assert.AreEqual(a[i], b[i], 1e-9, $"priority #{i} differs");
+            }
+        }
+
+        private class EvA : Event { }
+        private class EvB : Event { }
+
+        [NUnit.Framework.Test]
+        public void DiscardedScheduleDoesNotConsumeNovelty()
+        {
+            // Strategy A: a non-scenario first schedule, then a distinct schedule that first-satisfies S.
+            var a = NewStrategy();
+            a.ObserveRunningResults(Obs("M", new EvA(), new EvB()), NoReached, NoSat);
+            a.ObserveRunningResults(Obs("N", new EvA(), new EvB()), Reached("S", 3), Sat("S"));
+
+            // Strategy B: identical, but with an extra TIMELINE-DUPLICATE schedule (of the first) that
+            // ALSO carries S-progress, inserted before the distinct one. It must be discarded and must
+            // not consume S's novelty — so B ends identical to A.
+            var b = NewStrategy();
+            b.ObserveRunningResults(Obs("M", new EvA(), new EvB()), NoReached, NoSat);
+            b.ObserveRunningResults(Obs("M", new EvA(), new EvB()), Reached("S", 3), Sat("S")); // duplicate → discarded
+            b.ObserveRunningResults(Obs("N", new EvA(), new EvB()), Reached("S", 3), Sat("S"));
+
+            // The duplicate was dropped (both saved exactly two generators, not three)...
+            Assert.AreEqual(2, a.TotalSavedInputs());
+            Assert.AreEqual(2, b.TotalSavedInputs(), "the timeline-duplicate schedule must be discarded");
+            // ...and it consumed no novelty: the distinct S-satisfying schedule earned the same boost
+            // in both, so the saved priorities are identical. (If the discard had folded S into the
+            // suite state, B's last schedule would have earned compliance 0 and a lower priority.)
+            AssertPrioritiesEqual(Priorities(a), Priorities(b));
+        }
+
+        [NUnit.Framework.Test]
+        public void SuiteStateIsPerInstance()
+        {
+            // Two independent strategies each first-satisfy S on their first (identical) schedule.
+            // Each observation is the instance's first, so diversity is 1.0 and — if suite-state is
+            // per-instance — compliance is 1.0, giving priority 1.0*(1+1)=2.0 in BOTH. If suite-state
+            // were a shared static, the second instance would see S already satisfied → compliance 0
+            // → priority 1.0, and the two would differ.
+            var s1 = NewStrategy();
+            s1.ObserveRunningResults(Obs("M", new EvA(), new EvB()), Reached("S", 3), Sat("S"));
+            var s2 = NewStrategy();
+            s2.ObserveRunningResults(Obs("M", new EvA(), new EvB()), Reached("S", 3), Sat("S"));
+
+            var p1 = Priorities(s1);
+            var p2 = Priorities(s2);
+            AssertPrioritiesEqual(p1, p2);
+            Assert.AreEqual(1, p1.Count);
+            Assert.AreEqual(2.0, p1[0], 1e-9, "first-satisfying schedule should earn the novelty boost (priority 2.0)");
+        }
+    }
+}