Merge remote-tracking branch 'origin/master' into dev/pexplicit_checker

p-org · Jun 14, 2024 · 6cfb438 · 6cfb438
2 parents 73525f9 + e629bad
commit 6cfb438
Show file tree

Hide file tree

Showing 49 changed files with 149 additions and 125 deletions.
diff --git a/P.sln b/P.sln
@@ -3,8 +3,6 @@ Microsoft Visual Studio Solution File, Format Version 12.00
 # Visual Studio Version 16
 VisualStudioVersion = 16.0.30011.22
 MinimumVisualStudioVersion = 10.0.40219.1
-Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Runtime", "Runtime", "{D641DC13-F2F0-4365-963A-DCFC80BABCAA}"
-EndProject
 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Tests", "Tests", "{31FBBC4D-8756-4D60-B8D5-ED9E0FC8D4C1}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "UnitTests", "Tst\UnitTests\UnitTests.csproj", "{71691381-D3C9-478C-BA37-A94032A536DF}"
@@ -15,8 +13,6 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "PCommandLine", "Src\PCompil
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "CompilerCore", "Src\PCompiler\CompilerCore\CompilerCore.csproj", "{41F39ADD-B75F-473F-AC41-D1A9CDA9A9CD}"
 EndProject
-Project("{9344BDBB-3E7F-41FC-A0DD-8665D75EE146}") = "CSharpRuntime", "Src\PRuntimes\PCSharpRuntime\CSharpRuntime.csproj", "{27E011B3-3995-454A-B200-57800CC941DA}"
-EndProject
 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "PChecker", "PChecker", "{F7D2A6F5-841A-4E22-9ECD-2E1CF736F7EA}"
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CheckerCore", "Src\PChecker\CheckerCore\CheckerCore.csproj", "{37778F65-BDBF-4AEA-BA34-01026A223083}"
@@ -41,10 +37,6 @@ Global
 		{41F39ADD-B75F-473F-AC41-D1A9CDA9A9CD}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{41F39ADD-B75F-473F-AC41-D1A9CDA9A9CD}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{41F39ADD-B75F-473F-AC41-D1A9CDA9A9CD}.Release|Any CPU.Build.0 = Release|Any CPU
-		{27E011B3-3995-454A-B200-57800CC941DA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
-		{27E011B3-3995-454A-B200-57800CC941DA}.Debug|Any CPU.Build.0 = Debug|Any CPU
-		{27E011B3-3995-454A-B200-57800CC941DA}.Release|Any CPU.ActiveCfg = Release|Any CPU
-		{27E011B3-3995-454A-B200-57800CC941DA}.Release|Any CPU.Build.0 = Release|Any CPU
 		{37778F65-BDBF-4AEA-BA34-01026A223083}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
 		{37778F65-BDBF-4AEA-BA34-01026A223083}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{37778F65-BDBF-4AEA-BA34-01026A223083}.Release|Any CPU.ActiveCfg = Release|Any CPU
@@ -56,7 +48,6 @@ Global
 	GlobalSection(NestedProjects) = preSolution
 		{71691381-D3C9-478C-BA37-A94032A536DF} = {31FBBC4D-8756-4D60-B8D5-ED9E0FC8D4C1}
 		{41F39ADD-B75F-473F-AC41-D1A9CDA9A9CD} = {1B21372A-3030-4532-8B30-2A1A3E74527A}
-		{27E011B3-3995-454A-B200-57800CC941DA} = {D641DC13-F2F0-4365-963A-DCFC80BABCAA}
 		{37778F65-BDBF-4AEA-BA34-01026A223083} = {F7D2A6F5-841A-4E22-9ECD-2E1CF736F7EA}
 		{C1A8AF94-F550-4EC7-889A-9D0CCA259502} = {8BAB6184-8545-4E17-8199-86110AC5228F}
 	EndGlobalSection

diff --git a/...me/Exceptions/PFrozenMutationException.cs → ...me/Exceptions/PFrozenMutationException.cs b/...me/Exceptions/PFrozenMutationException.cs → ...me/Exceptions/PFrozenMutationException.cs
@@ -1,7 +1,6 @@
 using System;
-using System.Runtime.Serialization;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public class PFrozenMutationException : Exception
     {

diff --git a/...e/Exceptions/PIllegalCoercionException.cs → ...e/Exceptions/PIllegalCoercionException.cs b/...e/Exceptions/PIllegalCoercionException.cs → ...e/Exceptions/PIllegalCoercionException.cs
@@ -1,7 +1,6 @@
 using System;
-using System.Runtime.Serialization;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public class PIllegalCoercionException : Exception
     {

diff --git a/...pRuntime/Exceptions/PInternalException.cs → ...PRuntime/Exceptions/PInternalException.cs b/...pRuntime/Exceptions/PInternalException.cs → ...PRuntime/Exceptions/PInternalException.cs
@@ -1,7 +1,6 @@
 using System;
-using System.Runtime.Serialization;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public class PInternalException : Exception
     {

diff --git a/...Exceptions/PNonStandardReturnException.cs → ...Exceptions/PNonStandardReturnException.cs b/...Exceptions/PNonStandardReturnException.cs → ...Exceptions/PNonStandardReturnException.cs
@@ -1,7 +1,6 @@
 using System;
-using System.Runtime.Serialization;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public enum NonStandardReturn
     {

diff --git a/...e/Exceptions/PUnReachableCodeException.cs → ...e/Exceptions/PUnReachableCodeException.cs b/...e/Exceptions/PUnReachableCodeException.cs → ...e/Exceptions/PUnReachableCodeException.cs
@@ -1,7 +1,6 @@
 using System;
-using System.Runtime.Serialization;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public class PUnreachableCodeException : Exception
     {

diff --git a/...me/Exceptions/PrtInhabitsTypeException.cs → ...me/Exceptions/PrtInhabitsTypeException.cs b/...me/Exceptions/PrtInhabitsTypeException.cs → ...me/Exceptions/PrtInhabitsTypeException.cs
@@ -1,7 +1,6 @@
 using System;
-using System.Runtime.Serialization;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public class PrtInhabitsTypeException : Exception
     {

diff --git a/...xceptions/UnknownNamedTupleFieldAccess.cs → ...xceptions/UnknownNamedTupleFieldAccess.cs b/...xceptions/UnknownNamedTupleFieldAccess.cs → ...xceptions/UnknownNamedTupleFieldAccess.cs
@@ -1,7 +1,7 @@
 using System;
 using System.Collections.Generic;
 
-namespace Plang.CSharpRuntime.Exceptions
+namespace PChecker.PRuntime.Exceptions
 {
     public class UnknownNamedTupleFieldAccess : Exception
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/GodMachine.cs → ...hecker/CheckerCore/PRuntime/GodMachine.cs b/Src/PRuntimes/PCSharpRuntime/GodMachine.cs → ...hecker/CheckerCore/PRuntime/GodMachine.cs
@@ -2,7 +2,7 @@
 using PChecker.Actors;
 using PChecker.Actors.Events;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public class _GodMachine : StateMachine
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/PEvent.cs → Src/PChecker/CheckerCore/PRuntime/PEvent.cs b/Src/PRuntimes/PCSharpRuntime/PEvent.cs → Src/PChecker/CheckerCore/PRuntime/PEvent.cs
@@ -1,8 +1,8 @@
 using System;
 using PChecker.Actors.Events;
-using Plang.CSharpRuntime.Values;
+using PChecker.PRuntime.Values;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public class PEvent : Event, IPrtValue
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/PInterfaces.cs → ...ecker/CheckerCore/PRuntime/PInterfaces.cs b/Src/PRuntimes/PCSharpRuntime/PInterfaces.cs → ...ecker/CheckerCore/PRuntime/PInterfaces.cs
@@ -1,9 +1,9 @@
 using System.Collections.Generic;
 using System.Linq;
-using Plang.CSharpRuntime.Exceptions;
-using Plang.CSharpRuntime.Values;
+using PChecker.PRuntime.Exceptions;
+using PChecker.PRuntime.Values;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public class PInterfaces
     {

diff --git a/...Runtimes/PCSharpRuntime/PJsonFormatter.cs → ...er/CheckerCore/PRuntime/PJsonFormatter.cs b/...Runtimes/PCSharpRuntime/PJsonFormatter.cs → ...er/CheckerCore/PRuntime/PJsonFormatter.cs
@@ -7,9 +7,9 @@
 using PChecker.Actors;
 using PChecker.Actors.Events;
 using PChecker.Actors.Logging;
-using Plang.CSharpRuntime.Exceptions;
+using PChecker.PRuntime.Exceptions;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     /// <summary>
     /// This class implements IActorRuntimeLog and generates log output in an XML format.

diff --git a/...PRuntimes/PCSharpRuntime/PLogFormatter.cs → ...ker/CheckerCore/PRuntime/PLogFormatter.cs b/...PRuntimes/PCSharpRuntime/PLogFormatter.cs → ...ker/CheckerCore/PRuntime/PLogFormatter.cs
@@ -3,9 +3,9 @@
 using PChecker.Actors;
 using PChecker.Actors.Events;
 using PChecker.Actors.Logging;
-using Plang.CSharpRuntime.Exceptions;
+using PChecker.PRuntime.Exceptions;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     /// <summary>
     ///     Formatter for the runtime log.

diff --git a/Src/PRuntimes/PCSharpRuntime/PMachine.cs → ...PChecker/CheckerCore/PRuntime/PMachine.cs b/Src/PRuntimes/PCSharpRuntime/PMachine.cs → ...PChecker/CheckerCore/PRuntime/PMachine.cs
@@ -6,10 +6,10 @@
 using PChecker.Actors.Events;
 using PChecker.Actors.Exceptions;
 using PChecker.Actors.Logging;
-using Plang.CSharpRuntime.Exceptions;
-using Plang.CSharpRuntime.Values;
+using PChecker.PRuntime.Exceptions;
+using PChecker.PRuntime.Values;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public class PMachine : StateMachine
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/PModule.cs → Src/PChecker/CheckerCore/PRuntime/PModule.cs b/Src/PRuntimes/PCSharpRuntime/PModule.cs → Src/PChecker/CheckerCore/PRuntime/PModule.cs
@@ -2,7 +2,7 @@
 using System.Collections.Generic;
 using PChecker.Actors;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public class PModule
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/PMonitor.cs → ...PChecker/CheckerCore/PRuntime/PMonitor.cs b/Src/PRuntimes/PCSharpRuntime/PMonitor.cs → ...PChecker/CheckerCore/PRuntime/PMonitor.cs
@@ -4,7 +4,7 @@
 using PChecker.Actors.Logging;
 using PChecker.Specifications.Monitors;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public class PMonitor : Monitor
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/PrtTypes.cs → ...PChecker/CheckerCore/PRuntime/PrtTypes.cs b/Src/PRuntimes/PCSharpRuntime/PrtTypes.cs → ...PChecker/CheckerCore/PRuntime/PrtTypes.cs
@@ -3,7 +3,7 @@
 using System.Diagnostics;
 using System.Linq;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public abstract class PrtType
     {

diff --git a/Src/PRuntimes/PCSharpRuntime/PrtValues.cs → ...Checker/CheckerCore/PRuntime/PrtValues.cs b/Src/PRuntimes/PCSharpRuntime/PrtValues.cs → ...Checker/CheckerCore/PRuntime/PrtValues.cs
@@ -1,6 +1,6 @@
-using Plang.CSharpRuntime.Values;
+using PChecker.PRuntime.Values;
 
-namespace Plang.CSharpRuntime
+namespace PChecker.PRuntime
 {
     public static class PrtValues
     {

diff --git a/...times/PCSharpRuntime/Values/HashHelper.cs → ...CheckerCore/PRuntime/Values/HashHelper.cs b/...times/PCSharpRuntime/Values/HashHelper.cs → ...CheckerCore/PRuntime/Values/HashHelper.cs
@@ -1,7 +1,7 @@
 using System.Collections.Generic;
 using System.Linq;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public class HashHelper
     {

diff --git a/...PCSharpRuntime/Values/IPrtMutableValue.cs → ...rCore/PRuntime/Values/IPrtMutableValue.cs b/...PCSharpRuntime/Values/IPrtMutableValue.cs → ...rCore/PRuntime/Values/IPrtMutableValue.cs
@@ -1,4 +1,4 @@
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public interface IPrtMutableValue : IPrtValue
     {

diff --git a/...ntimes/PCSharpRuntime/Values/IPrtValue.cs → .../CheckerCore/PRuntime/Values/IPrtValue.cs b/...ntimes/PCSharpRuntime/Values/IPrtValue.cs → .../CheckerCore/PRuntime/Values/IPrtValue.cs
@@ -1,6 +1,6 @@
 using System;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public interface IPrtValue : IEquatable<IPrtValue>
     {

diff --git a/...PCSharpRuntime/Values/MutabilityHelper.cs → ...rCore/PRuntime/Values/MutabilityHelper.cs b/...PCSharpRuntime/Values/MutabilityHelper.cs → ...rCore/PRuntime/Values/MutabilityHelper.cs
@@ -1,4 +1,4 @@
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public static class MutabilityHelper
     {

diff --git a/...es/PCSharpRuntime/Values/PMachineValue.cs → ...ckerCore/PRuntime/Values/PMachineValue.cs b/...es/PCSharpRuntime/Values/PMachineValue.cs → ...ckerCore/PRuntime/Values/PMachineValue.cs
@@ -2,7 +2,7 @@
 using System.Linq;
 using PChecker.Actors;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public class I_Main : PMachineValue
     {

diff --git a/...Runtimes/PCSharpRuntime/Values/PrtBool.cs → ...er/CheckerCore/PRuntime/Values/PrtBool.cs b/...Runtimes/PCSharpRuntime/Values/PrtBool.cs → ...er/CheckerCore/PRuntime/Values/PrtBool.cs
@@ -1,7 +1,7 @@
 using System;
 using System.Runtime.CompilerServices;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     [Serializable]
     public readonly struct PrtBool : IPrtValue

diff --git a/...Runtimes/PCSharpRuntime/Values/PrtEnum.cs → ...er/CheckerCore/PRuntime/Values/PrtEnum.cs b/...Runtimes/PCSharpRuntime/Values/PrtEnum.cs → ...er/CheckerCore/PRuntime/Values/PrtEnum.cs
@@ -1,7 +1,7 @@
 using System.Collections.Generic;
 using System.Linq;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public class PrtEnum
     {

diff --git a/...untimes/PCSharpRuntime/Values/PrtFloat.cs → ...r/CheckerCore/PRuntime/Values/PrtFloat.cs b/...untimes/PCSharpRuntime/Values/PrtFloat.cs → ...r/CheckerCore/PRuntime/Values/PrtFloat.cs
@@ -1,7 +1,7 @@
 using System;
 using System.Runtime.CompilerServices;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     [Serializable]
     public readonly struct PrtFloat : IPrtValue

diff --git a/...PRuntimes/PCSharpRuntime/Values/PrtInt.cs → ...ker/CheckerCore/PRuntime/Values/PrtInt.cs b/...PRuntimes/PCSharpRuntime/Values/PrtInt.cs → ...ker/CheckerCore/PRuntime/Values/PrtInt.cs
@@ -1,7 +1,7 @@
 using System;
 using System.Runtime.CompilerServices;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     [Serializable]
     public readonly struct PrtInt : IPrtValue

diff --git a/...PRuntimes/PCSharpRuntime/Values/PrtMap.cs → ...ker/CheckerCore/PRuntime/Values/PrtMap.cs b/...PRuntimes/PCSharpRuntime/Values/PrtMap.cs → ...ker/CheckerCore/PRuntime/Values/PrtMap.cs
@@ -2,9 +2,9 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Text;
-using Plang.CSharpRuntime.Exceptions;
+using PChecker.PRuntime.Exceptions;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public sealed class PrtMap : IPrtMutableValue, IDictionary<IPrtValue, IPrtValue>
     {

diff --git a/...PRuntimes/PCSharpRuntime/Values/PrtSeq.cs → ...ker/CheckerCore/PRuntime/Values/PrtSeq.cs b/...PRuntimes/PCSharpRuntime/Values/PrtSeq.cs → ...ker/CheckerCore/PRuntime/Values/PrtSeq.cs
@@ -2,9 +2,9 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Text;
-using Plang.CSharpRuntime.Exceptions;
+using PChecker.PRuntime.Exceptions;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public sealed class PrtSeq : IPrtMutableValue, IReadOnlyList<IPrtValue>
     {

diff --git a/...PRuntimes/PCSharpRuntime/Values/PrtSet.cs → ...ker/CheckerCore/PRuntime/Values/PrtSet.cs b/...PRuntimes/PCSharpRuntime/Values/PrtSet.cs → ...ker/CheckerCore/PRuntime/Values/PrtSet.cs
@@ -3,9 +3,9 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Text;
-using Plang.CSharpRuntime.Exceptions;
+using PChecker.PRuntime.Exceptions;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public sealed class PrtSet : IPrtMutableValue, IReadOnlyList<IPrtValue>, ICollection<IPrtValue>
     {

diff --git a/...ntimes/PCSharpRuntime/Values/PrtString.cs → .../CheckerCore/PRuntime/Values/PrtString.cs b/...ntimes/PCSharpRuntime/Values/PrtString.cs → .../CheckerCore/PRuntime/Values/PrtString.cs
@@ -1,7 +1,7 @@
 using System;
 using System.Runtime.CompilerServices;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     [Serializable]
     public readonly struct PrtString : IPrtValue

diff --git a/...untimes/PCSharpRuntime/Values/PrtTuple.cs → ...r/CheckerCore/PRuntime/Values/PrtTuple.cs b/...untimes/PCSharpRuntime/Values/PrtTuple.cs → ...r/CheckerCore/PRuntime/Values/PrtTuple.cs
@@ -1,9 +1,9 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
-using Plang.CSharpRuntime.Exceptions;
+using PChecker.PRuntime.Exceptions;
 
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     [Serializable]
     public class PrtTuple : IPrtValue

diff --git a/Src/PChecker/CheckerCore/Scheduling/TestingProcessScheduler.cs b/Src/PChecker/CheckerCore/Scheduling/TestingProcessScheduler.cs
@@ -4,6 +4,7 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
+using System.IO;
 using PChecker.SystematicTesting;
 using PChecker.Testing;
 using PChecker.Utilities;
@@ -172,7 +173,14 @@ private void EmitTestReport()
             }
 
             Console.WriteLine(GlobalTestReport.GetText(_checkerConfiguration, "..."));
-            Console.WriteLine($"... Elapsed {Profiler.Results()} sec.");
+
+            var file = Path.GetFileNameWithoutExtension(GlobalTestReport.CheckerConfiguration.AssemblyToBeAnalyzed);
+            var directory = GlobalTestReport.CheckerConfiguration.OutputDirectory;
+            var pintPath = directory + file + "_pchecker_summary.txt";
+            Console.WriteLine($"..... Writing {pintPath}");
+            File.WriteAllText(pintPath, GlobalTestReport.GetSummaryText(Profiler));
+
+            Console.WriteLine($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB.");
 
             if (GlobalTestReport.InternalErrors.Count > 0)
             {