Merge branch 'cleanup/Simplify_PChecker' into cleanup/Simplify_PCheck…

…er_Christine

Src/PChecker/CheckerCore/Actors/StateMachineFactory.cs

@@ -0,0 +1,48 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.Linq.Expressions;
+
+namespace PChecker.Actors
+{
+    /// <summary>
+    /// Factory for creating state machine instances.
+    /// </summary>
+    internal static class StateMachineFactory
+    {
+        /// <summary>
+        /// Cache storing state machine constructors.
+        /// </summary>
+        private static readonly Dictionary<Type, Func<StateMachine>> StateMachineConstructorCache =
+            new Dictionary<Type, Func<StateMachine>>();
+
+        /// <summary>
+        /// Creates a new <see cref="StateMachine"/> instance of the specified type.
+        /// </summary>
+        /// <param name="type">The type of the state machines.</param>
+        /// <returns>The created state machine instance.</returns>
+        public static StateMachine Create(Type type)
+        {
+            Func<StateMachine> constructor = null;
+            lock (StateMachineConstructorCache)
+            {
+                if (!StateMachineConstructorCache.TryGetValue(type, out constructor))
+                {
+                    var constructorInfo = type.GetConstructor(Type.EmptyTypes);
+                    if (constructorInfo == null)
+                    {
+                        throw new Exception("Could not find empty constructor for type " + type.FullName);
+                    }
+
+                    constructor = Expression.Lambda<Func<StateMachine>>(
+                        Expression.New(constructorInfo)).Compile();
+                    StateMachineConstructorCache.Add(type, constructor);
+                }
+            }
+
+            return constructor();
+        }
+    }
+}

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.coverage.txt

@@ -0,0 +1,25 @@
+Total event coverage: 100.0%
+============================
+StateMachine: _GodMachine
+=========================
+Event coverage: 100.0%
+
+	State: Init
+		State has no expected events, so coverage is 100%
+
+StateMachine: Main
+==================
+Event coverage: 100.0%
+
+	State: __InitState__
+		State event coverage: 100.0%
+		Events received: Main+ConstructorEvent
+		Events sent: Main+ConstructorEvent
+		Next states: S
+
+	State: S
+		State event coverage: 100.0%
+		Events received: x
+		Events sent: a, x
+		Previous states: __InitState__
+

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.dgml

@@ -0,0 +1,44 @@
+<DirectedGraph xmlns='http://schemas.microsoft.com/vs/2009/dgml'>
+  <Nodes>
+    <Node Id='PChecker.PRuntime._GodMachine' Category='StateMachine' Group='Expanded'/>
+    <Node Id='PChecker.PRuntime._GodMachine.Init' Label='Init'/>
+    <Node Id='PImplementation.Main' Category='StateMachine' Group='Expanded'/>
+    <Node Id='PImplementation.Main.S' Label='S'/>
+    <Node Id='PImplementation.Main.__InitState__' Label='__InitState__'/>
+  </Nodes>
+  <Links>
+    <Link Source='PChecker.PRuntime._GodMachine' Target='PChecker.PRuntime._GodMachine.Init' Category='Contains'/>
+    <Link Source='PImplementation.Main' Target='PImplementation.Main.S' Category='Contains'/>
+    <Link Source='PImplementation.Main' Target='PImplementation.Main.__InitState__' Category='Contains'/>
+    <Link Source='PImplementation.Main.__InitState__' Target='PImplementation.Main.S' Label='ConstructorEvent' Index='0' EventId='PImplementation.Main+ConstructorEvent'/>
+  </Links>
+  <Styles>
+    <Style TargetType="Node" GroupLabel="Error" ValueLabel="True">
+      <Condition Expression="HasCategory('Error')" />
+      <Setter Property="Background" Value="#FFC15656" />
+    </Style>
+    <Style TargetType="Node" GroupLabel="Actor" ValueLabel="True">
+      <Condition Expression="HasCategory('Actor')" />
+      <Setter Property="Background" Value="#FF57AC56" />
+    </Style>
+    <Style TargetType="Node" GroupLabel="Monitor" ValueLabel="True">
+      <Condition Expression="HasCategory('Monitor')" />
+      <Setter Property="Background" Value="#FF558FDA" />
+    </Style>
+    <Style TargetType="Link" GroupLabel="halt" ValueLabel="True">
+      <Condition Expression="HasCategory('halt')" />
+      <Setter Property="Stroke" Value="#FFFF6C6C" />
+      <Setter Property="StrokeDashArray" Value="4 2" />
+    </Style>
+    <Style TargetType="Link" GroupLabel="push" ValueLabel="True">
+      <Condition Expression="HasCategory('push')" />
+      <Setter Property="Stroke" Value="#FF7380F5" />
+      <Setter Property="StrokeDashArray" Value="4 2" />
+    </Style>
+    <Style TargetType="Link" GroupLabel="pop" ValueLabel="True">
+      <Condition Expression="HasCategory('pop')" />
+      <Setter Property="Stroke" Value="#FF7380F5" />
+      <Setter Property="StrokeDashArray" Value="4 2" />
+    </Style>
+  </Styles>
+</DirectedGraph>

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput.sci

@@ -0,0 +1 @@
+<CoverageInfo z:Id="1" xmlns="http://schemas.datacontract.org/2004/07/PChecker.Coverage" xmlns:i="http://www.w3.org/2001/XMLSchema-instance" xmlns:z="http://schemas.microsoft.com/2003/10/Serialization/"><CoverageGraph z:Id="2"><InternalAllocatedLinkIds z:Id="3" z:Size="1" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringstring><a:Key z:Id="4">PImplementation.Main.__InitState__-&gt;PImplementation.Main.S(0)</a:Key><a:Value z:Id="5">ConstructorEvent</a:Value></a:KeyValueOfstringstring></InternalAllocatedLinkIds><InternalAllocatedLinkIndexes z:Id="6" z:Size="1" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringint><a:Key z:Id="7">PImplementation.Main.__InitState__-&gt;PImplementation.Main.S(ConstructorEvent)</a:Key><a:Value>0</a:Value></a:KeyValueOfstringint></InternalAllocatedLinkIndexes><InternalLinks z:Id="8" z:Size="4" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringGraphLink5QResVQF><a:Key z:Id="9">PChecker.PRuntime._GodMachine-&gt;PChecker.PRuntime._GodMachine.Init</a:Key><a:Value z:Id="10"><AttributeLists i:nil="true"/><Attributes i:nil="true"/><Category z:Id="11">Contains</Category><Index i:nil="true"/><Label i:nil="true"/><Source z:Id="12"><AttributeLists i:nil="true"/><Attributes z:Id="13" z:Size="1"><a:KeyValueOfstringstring><a:Key z:Id="14">Group</a:Key><a:Value z:Id="15">Expanded</a:Value></a:KeyValueOfstringstring></Attributes><Category z:Id="16">StateMachine</Category><Id z:Id="17">PChecker.PRuntime._GodMachine</Id><Label i:nil="true"/></Source><Target z:Id="18"><AttributeLists i:nil="true"/><Attributes i:nil="true"/><Category i:nil="true"/><Id z:Id="19">PChecker.PRuntime._GodMachine.Init</Id><Label z:Id="20">Init</Label></Target></a:Value></a:KeyValueOfstringGraphLink5QResVQF><a:KeyValueOfstringGraphLink5QResVQF><a:Key z:Id="21">PImplementation.Main-&gt;PImplementation.Main.__InitState__</a:Key><a:Value z:Id="22"><AttributeLists i:nil="true"/><Attributes i:nil="true"/><Category z:Ref="11" i:nil="true"/><Index i:nil="true"/><Label i:nil="true"/><Source z:Id="23"><AttributeLists i:nil="true"/><Attributes z:Id="24" z:Size="1"><a:KeyValueOfstringstring><a:Key z:Ref="14" i:nil="true"/><a:Value z:Ref="15" i:nil="true"/></a:KeyValueOfstringstring></Attributes><Category z:Ref="16" i:nil="true"/><Id z:Id="25">PImplementation.Main</Id><Label i:nil="true"/></Source><Target z:Id="26"><AttributeLists i:nil="true"/><Attributes i:nil="true"/><Category i:nil="true"/><Id z:Id="27">PImplementation.Main.__InitState__</Id><Label z:Id="28">__InitState__</Label></Target></a:Value></a:KeyValueOfstringGraphLink5QResVQF><a:KeyValueOfstringGraphLink5QResVQF><a:Key z:Id="29">PImplementation.Main-&gt;PImplementation.Main.S</a:Key><a:Value z:Id="30"><AttributeLists i:nil="true"/><Attributes i:nil="true"/><Category z:Ref="11" i:nil="true"/><Index i:nil="true"/><Label i:nil="true"/><Source z:Ref="23" i:nil="true"/><Target z:Id="31"><AttributeLists i:nil="true"/><Attributes i:nil="true"/><Category i:nil="true"/><Id z:Id="32">PImplementation.Main.S</Id><Label z:Id="33">S</Label></Target></a:Value></a:KeyValueOfstringGraphLink5QResVQF><a:KeyValueOfstringGraphLink5QResVQF><a:Key z:Id="34">PImplementation.Main.__InitState__-&gt;PImplementation.Main.S(0)</a:Key><a:Value z:Id="35"><AttributeLists i:nil="true"/><Attributes z:Id="36" z:Size="1"><a:KeyValueOfstringstring><a:Key z:Id="37">EventId</a:Key><a:Value z:Id="38">PImplementation.Main+ConstructorEvent</a:Value></a:KeyValueOfstringstring></Attributes><Category i:nil="true"/><Index>0</Index><Label z:Ref="5" i:nil="true"/><Source z:Ref="26" i:nil="true"/><Target z:Ref="31" i:nil="true"/></a:Value></a:KeyValueOfstringGraphLink5QResVQF></InternalLinks><InternalNextLinkIndex z:Id="39" z:Size="1" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringint><a:Key z:Id="40">PImplementation.Main.__InitState__-&gt;PImplementation.Main.S</a:Key><a:Value>0</a:Value></a:KeyValueOfstringint></InternalNextLinkIndex><InternalNodes z:Id="41" z:Size="5" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringGraphNode5QResVQF><a:Key z:Ref="17" i:nil="true"/><a:Value z:Ref="12" i:nil="true"/></a:KeyValueOfstringGraphNode5QResVQF><a:KeyValueOfstringGraphNode5QResVQF><a:Key z:Ref="19" i:nil="true"/><a:Value z:Ref="18" i:nil="true"/></a:KeyValueOfstringGraphNode5QResVQF><a:KeyValueOfstringGraphNode5QResVQF><a:Key z:Ref="25" i:nil="true"/><a:Value z:Ref="23" i:nil="true"/></a:KeyValueOfstringGraphNode5QResVQF><a:KeyValueOfstringGraphNode5QResVQF><a:Key z:Ref="27" i:nil="true"/><a:Value z:Ref="26" i:nil="true"/></a:KeyValueOfstringGraphNode5QResVQF><a:KeyValueOfstringGraphNode5QResVQF><a:Key z:Ref="32" i:nil="true"/><a:Value z:Ref="31" i:nil="true"/></a:KeyValueOfstringGraphNode5QResVQF></InternalNodes></CoverageGraph><EventInfo z:Id="42"><EventsReceived z:Id="43" z:Size="2" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Id="44">PImplementation.Main.__InitState__</a:Key><a:Value z:Id="45" z:Size="1"><a:string z:Ref="38" i:nil="true"/></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Id="46">PImplementation.Main.S</a:Key><a:Value z:Id="47" z:Size="1"><a:string z:Id="48">PImplementation.x</a:string></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1></EventsReceived><EventsSent z:Id="49" z:Size="2" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Id="50">PImplementation.Main.__InitState__</a:Key><a:Value z:Id="51" z:Size="1"><a:string z:Ref="38" i:nil="true"/></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Id="52">PImplementation.Main.S</a:Key><a:Value z:Id="53" z:Size="2"><a:string z:Ref="48" i:nil="true"/><a:string z:Id="54">PImplementation.a</a:string></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1></EventsSent></EventInfo><Machines z:Id="55" z:Size="2" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:string z:Ref="17" i:nil="true"/><a:string z:Ref="25" i:nil="true"/></Machines><MachinesToStates z:Id="56" z:Size="2" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Ref="17" i:nil="true"/><a:Value z:Id="57" z:Size="1"><a:string z:Ref="20" i:nil="true"/></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Ref="25" i:nil="true"/><a:Value z:Id="58" z:Size="2"><a:string z:Ref="28" i:nil="true"/><a:string z:Id="59">S</a:string></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1></MachinesToStates><RegisteredEvents z:Id="60" z:Size="2" xmlns:a="http://schemas.microsoft.com/2003/10/Serialization/Arrays"><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Id="61">PImplementation.Main.__InitState__</a:Key><a:Value z:Id="62" z:Size="1"><a:string z:Ref="38" i:nil="true"/></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1><a:KeyValueOfstringArrayOfstringty7Ep6D1><a:Key z:Id="63">PImplementation.Main.S</a:Key><a:Value z:Id="64" z:Size="1"><a:string z:Ref="48" i:nil="true"/></a:Value></a:KeyValueOfstringArrayOfstringty7Ep6D1></RegisteredEvents></CoverageInfo>

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.dgml

@@ -0,0 +1,44 @@
+<DirectedGraph xmlns='http://schemas.microsoft.com/vs/2009/dgml'>
+  <Nodes>
+    <Node Id='PChecker.PRuntime._GodMachine' Category='StateMachine' Group='Expanded'/>
+    <Node Id='PChecker.PRuntime._GodMachine.Init' Label='Init'/>
+    <Node Id='PImplementation.Main' Category='StateMachine' Group='Expanded'/>
+    <Node Id='PImplementation.Main.S' Label='S'/>
+    <Node Id='PImplementation.Main.__InitState__' Label='__InitState__'/>
+  </Nodes>
+  <Links>
+    <Link Source='PChecker.PRuntime._GodMachine' Target='PChecker.PRuntime._GodMachine.Init' Category='Contains'/>
+    <Link Source='PImplementation.Main' Target='PImplementation.Main.S' Category='Contains'/>
+    <Link Source='PImplementation.Main' Target='PImplementation.Main.__InitState__' Category='Contains'/>
+    <Link Source='PImplementation.Main.__InitState__' Target='PImplementation.Main.S' Label='ConstructorEvent' Index='0' EventId='PImplementation.Main+ConstructorEvent'/>
+  </Links>
+  <Styles>
+    <Style TargetType="Node" GroupLabel="Error" ValueLabel="True">
+      <Condition Expression="HasCategory('Error')" />
+      <Setter Property="Background" Value="#FFC15656" />
+    </Style>
+    <Style TargetType="Node" GroupLabel="Actor" ValueLabel="True">
+      <Condition Expression="HasCategory('Actor')" />
+      <Setter Property="Background" Value="#FF57AC56" />
+    </Style>
+    <Style TargetType="Node" GroupLabel="Monitor" ValueLabel="True">
+      <Condition Expression="HasCategory('Monitor')" />
+      <Setter Property="Background" Value="#FF558FDA" />
+    </Style>
+    <Style TargetType="Link" GroupLabel="halt" ValueLabel="True">
+      <Condition Expression="HasCategory('halt')" />
+      <Setter Property="Stroke" Value="#FFFF6C6C" />
+      <Setter Property="StrokeDashArray" Value="4 2" />
+    </Style>
+    <Style TargetType="Link" GroupLabel="push" ValueLabel="True">
+      <Condition Expression="HasCategory('push')" />
+      <Setter Property="Stroke" Value="#FF7380F5" />
+      <Setter Property="StrokeDashArray" Value="4 2" />
+    </Style>
+    <Style TargetType="Link" GroupLabel="pop" ValueLabel="True">
+      <Condition Expression="HasCategory('pop')" />
+      <Setter Property="Stroke" Value="#FF7380F5" />
+      <Setter Property="StrokeDashArray" Value="4 2" />
+    </Style>
+  </Styles>
+</DirectedGraph>

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.schedule

@@ -0,0 +1,6 @@
+--fair-scheduling
+--liveness-temperature-threshold:50000
+(0)
+(1)
+(1)
+(2)

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.trace.json

@@ -0,0 +1,101 @@
+[
+  {
+    "type": "StateTransition",
+    "details": {
+      "log": "Main(2) enters state \u0027S\u0027.",
+      "id": "Main(2)",
+      "state": "S",
+      "payload": "null",
+      "isEntry": true,
+      "clock": {
+        "Main(2)": 1
+      }
+    }
+  },
+  {
+    "type": "RaiseEvent",
+    "details": {
+      "log": "\u0027Main(2)\u0027 raised event \u0027x with payload (\u003Ca,3,\u003E)\u0027 in state \u0027S\u0027.",
+      "id": "Main(2)",
+      "event": "x",
+      "state": "S",
+      "payload": {
+        "0": {},
+        "1": {}
+      },
+      "clock": {
+        "Main(2)": 2
+      }
+    }
+  },
+  {
+    "type": "RaiseEvent",
+    "details": {
+      "log": "\u0027Main(2)\u0027 raised event \u0027a with payload (3)\u0027 in state \u0027S\u0027.",
+      "id": "Main(2)",
+      "event": "a",
+      "state": "S",
+      "payload": 3,
+      "clock": {
+        "Main(2)": 3
+      }
+    }
+  },
+  {
+    "type": "StateTransition",
+    "details": {
+      "log": "Main(2) exits state \u0027S\u0027.",
+      "id": "Main(2)",
+      "state": "S",
+      "payload": "null",
+      "isEntry": false,
+      "clock": {
+        "Main(2)": 4
+      }
+    }
+  },
+  {
+    "type": "PopStateUnhandledEvent",
+    "details": {
+      "log": "Main(2) popped state S due to unhandled event \u0027a\u0027.",
+      "id": "Main(2)",
+      "event": "a",
+      "state": "S",
+      "payload": "null",
+      "clock": {
+        "Main(2)": 5
+      }
+    }
+  },
+  {
+    "type": "ExceptionThrown",
+    "details": {
+      "log": "Main(2) running action \u0027\u0027 in state \u0027S\u0027 threw exception \u0027UnhandledEventException\u0027.",
+      "id": "Main(2)",
+      "state": "S",
+      "payload": "null",
+      "action": "",
+      "exception": "UnhandledEventException",
+      "clock": {
+        "Main(2)": 6
+      }
+    }
+  },
+  {
+    "type": "AssertionFailure",
+    "details": {
+      "log": "Main(2) received event \u0027PImplementation.a\u0027 that cannot be handled.",
+      "error": "Main(2) received event \u0027PImplementation.a\u0027 that cannot be handled.",
+      "payload": "null"
+    }
+  },
+  {
+    "type": "StrategyDescription",
+    "details": {
+      "log": "Found bug using \u0027random\u0027 strategy.",
+      "payload": "null",
+      "strategy": "random",
+      "strategyDescription": "random[seed \u0027769371342\u0027]"
+    }
+  }
+]

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_0_0.txt

@@ -0,0 +1,15 @@
+<TestLog> Running test 'DefaultImpl'.
+<StateLog> Main(2) enters state 'S'.
+<RaiseLog> 'Main(2)' raised event 'x with payload (<a,3,>)' in state 'S'.
+<RaiseLog> 'Main(2)' raised event 'a with payload (3)' in state 'S'.
+<StateLog> Main(2) exits state 'S'.
+<PopLog> Main(2) popped state S due to unhandled event 'PImplementation.a'.
+<ExceptionLog> Main(2) running action '' in state 'S' threw exception 'UnhandledEventException'.
+<ErrorLog> Main(2) received event 'PImplementation.a' that cannot be handled.
+<StrategyLog> Found bug using 'random' strategy.
+<StrategyLog> Checking statistics:
+<StrategyLog> Found 1 bug.
+<StrategyLog> Scheduling statistics:
+<StrategyLog> Explored 1 schedule
+<StrategyLog> Found 100.00% buggy schedules.
+<StrategyLog> Number of scheduling points in terminating schedules: 4 (min), 4 (avg), 4 (max).

Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/bug2/PCheckerOutput/BugFinding1/generatedOutput_pchecker_summary.txt

@@ -0,0 +1,5 @@
+bugs:1
+schedules:1
+max_depth:4
+time_seconds:0.12
+memory_max_mb:0