diff --git a/P.sln b/P.sln index d0dc8294c..594592b00 100644 --- 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/Src/PRuntimes/PCSharpRuntime/Exceptions/PFrozenMutationException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PFrozenMutationException.cs similarity index 75% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/PFrozenMutationException.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/PFrozenMutationException.cs index 488f282f9..c00dddfee 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/PFrozenMutationException.cs +++ b/Src/PChecker/CheckerCore/PRuntime/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/Src/PRuntimes/PCSharpRuntime/Exceptions/PIllegalCoercionException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PIllegalCoercionException.cs similarity index 83% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/PIllegalCoercionException.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/PIllegalCoercionException.cs index 82275024a..bea5bb900 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/PIllegalCoercionException.cs +++ b/Src/PChecker/CheckerCore/PRuntime/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/Src/PRuntimes/PCSharpRuntime/Exceptions/PInternalException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PInternalException.cs similarity index 82% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/PInternalException.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/PInternalException.cs index df6a978c8..eb52b9c48 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/PInternalException.cs +++ b/Src/PChecker/CheckerCore/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/Src/PRuntimes/PCSharpRuntime/Exceptions/PNonStandardReturnException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PNonStandardReturnException.cs similarity index 87% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/PNonStandardReturnException.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/PNonStandardReturnException.cs index 0b734ef70..482d4cec5 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/PNonStandardReturnException.cs +++ b/Src/PChecker/CheckerCore/PRuntime/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/Src/PRuntimes/PCSharpRuntime/Exceptions/PUnReachableCodeException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PUnReachableCodeException.cs similarity index 83% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/PUnReachableCodeException.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/PUnReachableCodeException.cs index 46272e7c0..1d2316f77 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/PUnReachableCodeException.cs +++ b/Src/PChecker/CheckerCore/PRuntime/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/Src/PRuntimes/PCSharpRuntime/Exceptions/PrtInhabitsTypeException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PrtInhabitsTypeException.cs similarity index 83% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/PrtInhabitsTypeException.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/PrtInhabitsTypeException.cs index 668782be2..b9c9d5037 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/PrtInhabitsTypeException.cs +++ b/Src/PChecker/CheckerCore/PRuntime/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/Src/PRuntimes/PCSharpRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs similarity index 93% rename from Src/PRuntimes/PCSharpRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs rename to Src/PChecker/CheckerCore/PRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs index 2c8a38070..a9982f30b 100644 --- a/Src/PRuntimes/PCSharpRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Exceptions/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 b/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs similarity index 96% rename from Src/PRuntimes/PCSharpRuntime/GodMachine.cs rename to Src/PChecker/CheckerCore/PRuntime/GodMachine.cs index 73ce29e62..a629d66cd 100644 --- a/Src/PRuntimes/PCSharpRuntime/GodMachine.cs +++ b/Src/PChecker/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 b/Src/PChecker/CheckerCore/PRuntime/PEvent.cs similarity index 94% rename from Src/PRuntimes/PCSharpRuntime/PEvent.cs rename to Src/PChecker/CheckerCore/PRuntime/PEvent.cs index 78767414a..33af7d679 100644 --- a/Src/PRuntimes/PCSharpRuntime/PEvent.cs +++ b/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 b/Src/PChecker/CheckerCore/PRuntime/PInterfaces.cs similarity index 90% rename from Src/PRuntimes/PCSharpRuntime/PInterfaces.cs rename to Src/PChecker/CheckerCore/PRuntime/PInterfaces.cs index a689d07ca..de3c2d878 100644 --- a/Src/PRuntimes/PCSharpRuntime/PInterfaces.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs rename to Src/PChecker/CheckerCore/PRuntime/PJsonFormatter.cs index e42ac4d2c..f654ff132 100644 --- a/Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs +++ b/Src/PChecker/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 { /// /// This class implements IActorRuntimeLog and generates log output in an XML format. diff --git a/Src/PRuntimes/PCSharpRuntime/PLogFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/PLogFormatter.cs rename to Src/PChecker/CheckerCore/PRuntime/PLogFormatter.cs index a9983dd6b..5e70ab79c 100644 --- a/Src/PRuntimes/PCSharpRuntime/PLogFormatter.cs +++ b/Src/PChecker/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 { /// /// Formatter for the runtime log. diff --git a/Src/PRuntimes/PCSharpRuntime/PMachine.cs b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs similarity index 98% rename from Src/PRuntimes/PCSharpRuntime/PMachine.cs rename to Src/PChecker/CheckerCore/PRuntime/PMachine.cs index 0925c1e9f..92014533a 100644 --- a/Src/PRuntimes/PCSharpRuntime/PMachine.cs +++ b/Src/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 b/Src/PChecker/CheckerCore/PRuntime/PModule.cs similarity index 95% rename from Src/PRuntimes/PCSharpRuntime/PModule.cs rename to Src/PChecker/CheckerCore/PRuntime/PModule.cs index dd3803b25..16cc35cee 100644 --- a/Src/PRuntimes/PCSharpRuntime/PModule.cs +++ b/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 b/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs similarity index 98% rename from Src/PRuntimes/PCSharpRuntime/PMonitor.cs rename to Src/PChecker/CheckerCore/PRuntime/PMonitor.cs index 1f175fb1c..08289f4cc 100644 --- a/Src/PRuntimes/PCSharpRuntime/PMonitor.cs +++ b/Src/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 b/Src/PChecker/CheckerCore/PRuntime/PrtTypes.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/PrtTypes.cs rename to Src/PChecker/CheckerCore/PRuntime/PrtTypes.cs index d6294bb04..681640a4f 100644 --- a/Src/PRuntimes/PCSharpRuntime/PrtTypes.cs +++ b/Src/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 b/Src/PChecker/CheckerCore/PRuntime/PrtValues.cs similarity index 95% rename from Src/PRuntimes/PCSharpRuntime/PrtValues.cs rename to Src/PChecker/CheckerCore/PRuntime/PrtValues.cs index 99552fad5..6b56ffff0 100644 --- a/Src/PRuntimes/PCSharpRuntime/PrtValues.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/HashHelper.cs b/Src/PChecker/CheckerCore/PRuntime/Values/HashHelper.cs similarity index 92% rename from Src/PRuntimes/PCSharpRuntime/Values/HashHelper.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/HashHelper.cs index 731dc64b1..36dc42ca4 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/HashHelper.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/IPrtMutableValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs similarity index 68% rename from Src/PRuntimes/PCSharpRuntime/Values/IPrtMutableValue.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs index 2163d256e..b8b3d2c15 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/IPrtMutableValue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs @@ -1,4 +1,4 @@ -namespace Plang.CSharpRuntime.Values +namespace PChecker.PRuntime.Values { public interface IPrtMutableValue : IPrtValue { diff --git a/Src/PRuntimes/PCSharpRuntime/Values/IPrtValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/IPrtValue.cs similarity index 92% rename from Src/PRuntimes/PCSharpRuntime/Values/IPrtValue.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/IPrtValue.cs index 7f6d185f4..6dbc41136 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/IPrtValue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/IPrtValue.cs @@ -1,6 +1,6 @@ using System; -namespace Plang.CSharpRuntime.Values +namespace PChecker.PRuntime.Values { public interface IPrtValue : IEquatable { diff --git a/Src/PRuntimes/PCSharpRuntime/Values/MutabilityHelper.cs b/Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs similarity index 87% rename from Src/PRuntimes/PCSharpRuntime/Values/MutabilityHelper.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs index 14cc68b98..8e7860b53 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/MutabilityHelper.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs @@ -1,4 +1,4 @@ -namespace Plang.CSharpRuntime.Values +namespace PChecker.PRuntime.Values { public static class MutabilityHelper { diff --git a/Src/PRuntimes/PCSharpRuntime/Values/PMachineValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs similarity index 97% rename from Src/PRuntimes/PCSharpRuntime/Values/PMachineValue.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs index d537362de..16c758c4d 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PMachineValue.cs +++ b/Src/PChecker/CheckerCore/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/Src/PRuntimes/PCSharpRuntime/Values/PrtBool.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtBool.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtBool.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtBool.cs index c2f25f1de..9d80012ee 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtBool.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/PrtEnum.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtEnum.cs similarity index 95% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtEnum.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtEnum.cs index cf7adabf5..b73a11dd2 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtEnum.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/PrtFloat.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtFloat.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtFloat.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtFloat.cs index 7d66f6ead..d46e38daa 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtFloat.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/PrtInt.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtInt.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtInt.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtInt.cs index 451bff831..f381ec8cd 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtInt.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/PrtMap.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtMap.cs similarity index 98% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtMap.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtMap.cs index a79525c60..dff333d16 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtMap.cs +++ b/Src/PChecker/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 { diff --git a/Src/PRuntimes/PCSharpRuntime/Values/PrtSeq.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtSeq.cs similarity index 98% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtSeq.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtSeq.cs index 3f93e16e1..943f9b999 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtSeq.cs +++ b/Src/PChecker/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 { diff --git a/Src/PRuntimes/PCSharpRuntime/Values/PrtSet.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs similarity index 98% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtSet.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs index 2e070ac2d..6d5c3ff27 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtSet.cs +++ b/Src/PChecker/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, ICollection { diff --git a/Src/PRuntimes/PCSharpRuntime/Values/PrtString.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtString.cs similarity index 99% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtString.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtString.cs index eaaf7728b..92ef3fcaa 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtString.cs +++ b/Src/PChecker/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/Src/PRuntimes/PCSharpRuntime/Values/PrtTuple.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtTuple.cs similarity index 98% rename from Src/PRuntimes/PCSharpRuntime/Values/PrtTuple.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PrtTuple.cs index 5a191b4a4..a43d53c13 100644 --- a/Src/PRuntimes/PCSharpRuntime/Values/PrtTuple.cs +++ b/Src/PChecker/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 index fa59f57ec..4e1cf63a5 100644 --- 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) { diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs index 81ee7583a..b729f3e0e 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs @@ -6,6 +6,7 @@ using System.Runtime.Serialization; using System.Text; using PChecker.Coverage; +using PChecker.Utilities; namespace PChecker.SystematicTesting { @@ -178,6 +179,31 @@ public bool Merge(TestReport testReport) return true; } + /// + /// Returns a simple string testing report with only the keys and values. + /// + public string GetSummaryText(Profiler Profiler) { + var report = new StringBuilder(); + + report.AppendFormat("bugs:{0}", NumOfFoundBugs); + report.AppendLine(); + + var totalExploredSchedules = NumOfExploredFairSchedules + + NumOfExploredUnfairSchedules; + report.AppendFormat("schedules:{0}", totalExploredSchedules); + report.AppendLine(); + + report.AppendFormat("max_depth:{0}", MaxExploredFairSteps < 0 ? 0 : MaxExploredFairSteps); + report.AppendLine(); + + report.AppendFormat($"time_seconds:{Profiler.GetElapsedTime():0.##}"); + report.AppendLine(); + + report.AppendFormat($"memory_max_mb:{Profiler.GetMaxMemoryUsage():0.##}"); + + return report.ToString(); + } + /// /// Returns the testing report as a string, given a checkerConfiguration and an optional prefix. /// diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index 3a54d5e47..b753ad029 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -362,20 +362,28 @@ public void Run() } catch (AggregateException aex) { - aex.Handle((ex) => + if (aex.InnerException is OutOfMemoryException) { - Debug.WriteLine(ex.Message); - Debug.WriteLine(ex.StackTrace); - return true; - }); - - if (aex.InnerException is FileNotFoundException) - { - Error.ReportAndExit($"{aex.InnerException.Message}"); + Logger.WriteLine("... Checker ran out of memory."); } + else + { + aex.Handle((ex) => + { + Debug.WriteLine(ex.Message); + Debug.WriteLine(ex.StackTrace); + return true; + }); + + if (aex.InnerException is FileNotFoundException) + { + Error.ReportAndExit($"{aex.InnerException.Message}"); + } - Error.ReportAndExit("Exception thrown during testing outside the context of an actor, " + - "possibly in a test method. Please use /debug /v:2 to print more information."); + + Error.ReportAndExit("Exception thrown during testing outside the context of an actor, " + + "possibly in a test method. Please use /debug /v:2 to print more information."); + } } catch (Exception ex) { @@ -422,11 +430,20 @@ _checkerConfiguration.SchedulingStrategy is "probabilistic" || break; } + if (Profiler.GetCurrentMemoryUsage() > _checkerConfiguration.MemoryLimit) + { + if (_checkerConfiguration.MemoryLimit != 0) + { + throw new OutOfMemoryException(); + } + } + // Runs a new testing schedule. RunNextIteration(i); if (IsReplayModeEnabled || (!_checkerConfiguration.PerformFullExploration && - TestReport.NumOfFoundBugs > 0) || !Strategy.PrepareForNextIteration()) + TestReport.NumOfFoundBugs > 0) || + !Strategy.PrepareForNextIteration()) { break; } @@ -620,7 +637,7 @@ public string GetReport() report.AppendFormat("... Reproduced {0} bug{1}.", TestReport.NumOfFoundBugs, TestReport.NumOfFoundBugs == 1 ? string.Empty : "s"); report.AppendLine(); - report.Append($"... Elapsed {Profiler.Results()} sec."); + report.Append($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB."); return report.ToString(); } @@ -744,7 +761,7 @@ public void TryEmitTraces(string directory, string file) } } - Logger.WriteLine($"... Elapsed {Profiler.Results()} sec."); + Logger.WriteLine($"... Elapsed {Profiler.GetElapsedTime():0.##} sec and used {Profiler.GetMaxMemoryUsage():0.##} GB."); } /// diff --git a/Src/PChecker/CheckerCore/Utilities/Profiler.cs b/Src/PChecker/CheckerCore/Utilities/Profiler.cs index 9aa0ca469..ec9f031ee 100644 --- a/Src/PChecker/CheckerCore/Utilities/Profiler.cs +++ b/Src/PChecker/CheckerCore/Utilities/Profiler.cs @@ -1,6 +1,7 @@ // Copyright (c) Microsoft Corporation. // Licensed under the MIT License. +using System; using System.Diagnostics; namespace PChecker.Utilities @@ -11,6 +12,7 @@ namespace PChecker.Utilities public class Profiler { private Stopwatch StopWatch; + private static double maxMemoryUsed = 0.0; /// /// Starts measuring execution time. @@ -33,9 +35,28 @@ public void StopMeasuringExecutionTime() } /// - /// Returns profilling results. + /// Returns profiling results. /// - public double Results() => + public double GetElapsedTime() => StopWatch != null ? StopWatch.Elapsed.TotalSeconds : 0; + + /// + /// Get memory usage in gigabytes. + /// + public double GetCurrentMemoryUsage() + { + double memUsed = GC.GetTotalMemory(false) / 1024.0 / 1024.0 / 1024.0; + if (memUsed > maxMemoryUsed) + maxMemoryUsed = memUsed; + return memUsed; + } + + /// + /// Get max memory usage in gigabytes. + /// + public static double GetMaxMemoryUsage() + { + return maxMemoryUsed; + } } } \ No newline at end of file diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 69e5343d4..181e3a80b 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -159,9 +159,9 @@ private void WriteSourcePrologue(CompilationContext context, StringWriter output context.WriteLine(output, "using System.Collections.Generic;"); context.WriteLine(output, "using System.Linq;"); context.WriteLine(output, "using System.IO;"); - context.WriteLine(output, "using Plang.CSharpRuntime;"); - context.WriteLine(output, "using Plang.CSharpRuntime.Values;"); - context.WriteLine(output, "using Plang.CSharpRuntime.Exceptions;"); + context.WriteLine(output, "using PChecker.PRuntime.Values;"); + context.WriteLine(output, "using PChecker.PRuntime;"); + context.WriteLine(output, "using PChecker.PRuntime.Exceptions;"); context.WriteLine(output, "using System.Threading;"); context.WriteLine(output, "using System.Threading.Tasks;"); context.WriteLine(output); diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs index 7d87bb767..595f3073e 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/Constants.cs @@ -14,9 +14,6 @@ internal class Constants -foreign-include- - - -assembly-path-/PCSharpRuntime.dll - -assembly-path-/PCheckerCore.dll diff --git a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs index 5d8beb352..cae6177f1 100644 --- a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs @@ -76,7 +76,7 @@ private void WriteMonitorDecl() { var cname = Names.GetNameForDecl(_currentMachine); - WriteLine($"public static class {cname} extends prt.Monitor<{cname}.{Constants.StateEnumName}> {{"); + WriteLine($"public static class {cname} extends prt.Monitor<{cname}.{Constants.StateEnumName}> implements Serializable {{"); WriteLine(); WriteSupplierCDef(cname); diff --git a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs index ca7d95141..d45b1d5fd 100644 --- a/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs +++ b/Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs @@ -40,7 +40,7 @@ internal PCheckerOptions() var basicGroup = Parser.GetOrCreateGroup("Basic", "Basic options"); basicGroup.AddArgument("timeout", "t", "Timeout in seconds (disabled by default)", typeof(uint)); - basicGroup.AddArgument("memout", null, "Memory limit in Giga bytes (disabled by default)", typeof(double)).IsHidden = true; + basicGroup.AddArgument("memout", "m", "Memory limit in Giga bytes (disabled by default)", typeof(double)); basicGroup.AddArgument("outdir", "o", "Dump output to directory (absolute or relative path)"); basicGroup.AddArgument("verbose", "v", "Enable verbose log output during exploration", typeof(bool)); basicGroup.AddArgument("debug", "d", "Enable debugging", typeof(bool)).IsHidden = true; diff --git a/Src/PCompiler/PCommandLine/PCommandLine.csproj b/Src/PCompiler/PCommandLine/PCommandLine.csproj index 9e943ed1e..fe01545cc 100644 --- a/Src/PCompiler/PCommandLine/PCommandLine.csproj +++ b/Src/PCompiler/PCommandLine/PCommandLine.csproj @@ -23,7 +23,6 @@ - diff --git a/Src/PRuntimes/PCSharpRuntime/CSharpRuntime.csproj b/Src/PRuntimes/PCSharpRuntime/CSharpRuntime.csproj deleted file mode 100644 index 7016776aa..000000000 --- a/Src/PRuntimes/PCSharpRuntime/CSharpRuntime.csproj +++ /dev/null @@ -1,27 +0,0 @@ - - - net8.0 - latest - $(PSdkFolder)\Binaries - Plang.CSharpRuntime - PCSharpRuntime - MIT - The P Programming Language C# Runtime - https://github.com/p-org/P - The P team - P programming language;safe asynchrony;state machines;model checkers - 1.0.0 - P C# Runtime - The P team - icon.png - https://github.com/p-org/P - README.md - - - - - - - - - \ No newline at end of file diff --git a/Tst/UnitTests/CSharpValuesTest.cs b/Tst/UnitTests/CSharpValuesTest.cs index 86193ad2d..dccb6e8aa 100644 --- a/Tst/UnitTests/CSharpValuesTest.cs +++ b/Tst/UnitTests/CSharpValuesTest.cs @@ -1,6 +1,6 @@ using NUnit.Framework; -using Plang.CSharpRuntime; -using Plang.CSharpRuntime.Values; +using PChecker.PRuntime; +using PChecker.PRuntime.Values; namespace UnitTests { diff --git a/Tst/UnitTests/Runners/PCheckerRunner.cs b/Tst/UnitTests/Runners/PCheckerRunner.cs index e4b79b29f..6dddbf82e 100644 --- a/Tst/UnitTests/Runners/PCheckerRunner.cs +++ b/Tst/UnitTests/Runners/PCheckerRunner.cs @@ -95,7 +95,6 @@ private void CreateCSProjFile(DirectoryInfo scratchDirectory) . - "; diff --git a/Tst/UnitTests/UnitTests.csproj b/Tst/UnitTests/UnitTests.csproj index ab0f30fc4..6c0ab746a 100644 --- a/Tst/UnitTests/UnitTests.csproj +++ b/Tst/UnitTests/UnitTests.csproj @@ -16,6 +16,5 @@ - diff --git a/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs b/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs index c8b9af5a1..8c9ce3176 100644 --- a/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs +++ b/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs @@ -3,9 +3,9 @@ using System.Collections.Generic; using System.Linq; using System.IO; -using Plang.CSharpRuntime; -using Plang.CSharpRuntime.Values; -using Plang.CSharpRuntime.Exceptions; +using PChecker.PRuntime; +using PChecker.PRuntime.Values; +using PChecker.PRuntime.Exceptions; using System.Threading; using System.Threading.Tasks; diff --git a/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs b/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs index f12dd4a6e..a9d0170b5 100644 --- a/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs +++ b/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs @@ -1,5 +1,5 @@ using System.Collections; -using Plang.CSharpRuntime.Values; +using PChecker.PRuntime.Values; namespace PImplementation { diff --git a/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs b/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs index 898a68a54..986c7d0f9 100644 --- a/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs +++ b/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs @@ -4,9 +4,9 @@ using System.Linq; using System.IO; using System.Linq.Expressions; -using Plang.CSharpRuntime; -using Plang.CSharpRuntime.Values; -using Plang.CSharpRuntime.Exceptions; +using PChecker.PRuntime; +using PChecker.PRuntime.Values; +using PChecker.PRuntime.Exceptions; using System.Threading; using System.Threading.Tasks; diff --git a/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs b/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs index 7d77991fe..9f69a5ad6 100644 --- a/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs +++ b/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs @@ -7,9 +7,9 @@ using System.Collections.Generic; using System.Linq; using System.IO; -using Plang.CSharpRuntime; -using Plang.CSharpRuntime.Values; -using Plang.CSharpRuntime.Exceptions; +using PChecker.PRuntime; +using PChecker.PRuntime.Values; +using PChecker.PRuntime.Exceptions; using System.Threading; using System.Threading.Tasks;