Merge branch 'experimental/pverifier' into master

Docs/docs/manual/expressions.md

@@ -342,3 +342,12 @@ The choose operation can be used to model nondeterministic environment machines
 
 !!! note ""
     Performing a `choose` over an empty collection leads to an error. Also, `choose` from a `map` value returns a random key from the map.
+
+Note that the maximum number of choices allowed in a `choose(expr)` is 10,000. Performing a `choose` with an `int` value greater than 10000 or over a collection with more than 10000 elements leads to an error.
+
+``` java
+choose(10001) // throws a compile-time error
+choose(x)     // throws a runtime error if x is of integer type and has value greater than 10000
+choose(x)     // throws a runtime error if x is of seq/set/map type and has size greater than 10000 elements
+```
+

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

Src/PRuntimes/PCSharpRuntime/Exceptions/PFrozenMutationException.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Exceptions/PIllegalCoercionException.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Exceptions/PInternalException.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Exceptions/PNonStandardReturnException.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Exceptions/PUnReachableCodeException.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Exceptions/PrtInhabitsTypeException.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/GodMachine.cs → 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
     {

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
     {

Src/PRuntimes/PCSharpRuntime/PInterfaces.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/PJsonFormatter.cs → 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
 {
     /// <summary>
     /// This class implements IActorRuntimeLog and generates log output in an XML format.

Src/PRuntimes/PCSharpRuntime/PLogFormatter.cs → 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
 {
     /// <summary>
     ///     Formatter for the runtime log.

Src/PRuntimes/PCSharpRuntime/PMachine.cs → 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
     {
@@ -136,21 +136,27 @@ public IPrtValue TryRandom(IPrtValue param)
             switch (param)
             {
                 case PrtInt maxValue:
+                {
+                    TryAssert(maxValue <= 10000, $"choose expects a parameter with at most 10000 choices, got {maxValue} choices instead.");
                     return (PrtInt)TryRandomInt(maxValue);
+                }
 
                 case PrtSeq seq:
                 {
                     TryAssert(seq.Any(), "Trying to choose from an empty sequence!");
+                    TryAssert(seq.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {seq.Count} choices instead.");
                     return seq[TryRandomInt(seq.Count)];
                 }
                 case PrtSet set:
                 {
                     TryAssert(set.Any(), "Trying to choose from an empty set!");
+                    TryAssert(set.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {set.Count} choices instead.");
                     return set.ElementAt(TryRandomInt(set.Count));
                 }
                 case PrtMap map:
                 {
                     TryAssert(map.Any(), "Trying to choose from an empty map!");
+                    TryAssert(map.Keys.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {map.Keys.Count} choices instead.");
                     return map.Keys.ElementAt(TryRandomInt(map.Keys.Count));
                 }
                 default:

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
     {

Src/PRuntimes/PCSharpRuntime/PMonitor.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/PrtTypes.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/PrtValues.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Values/HashHelper.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Values/IPrtMutableValue.cs → Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs

@@ -1,4 +1,4 @@
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public interface IPrtMutableValue : IPrtValue
     {

Src/PRuntimes/PCSharpRuntime/Values/IPrtValue.cs → 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<IPrtValue>
     {

Src/PRuntimes/PCSharpRuntime/Values/MutabilityHelper.cs → Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs

@@ -1,4 +1,4 @@
-namespace Plang.CSharpRuntime.Values
+namespace PChecker.PRuntime.Values
 {
     public static class MutabilityHelper
     {

Src/PRuntimes/PCSharpRuntime/Values/PMachineValue.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Values/PrtBool.cs → 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

Src/PRuntimes/PCSharpRuntime/Values/PrtEnum.cs → 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
     {

Src/PRuntimes/PCSharpRuntime/Values/PrtFloat.cs → 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

Src/PRuntimes/PCSharpRuntime/Values/PrtInt.cs → 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

Src/PRuntimes/PCSharpRuntime/Values/PrtMap.cs → 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<IPrtValue, IPrtValue>
     {

Src/PRuntimes/PCSharpRuntime/Values/PrtSeq.cs → 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<IPrtValue>
     {

Src/PRuntimes/PCSharpRuntime/Values/PrtSet.cs → 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<IPrtValue>, ICollection<IPrtValue>
     {
@@ -37,6 +37,19 @@ private bool IsDirty
             }
         }
 
+        public override int GetHashCode()
+        {
+            if (!IsDirty)
+            {
+                return hashCode;
+            }
+
+            hashCode = ComputeHashCode();
+            IsDirty = false;
+
+            return hashCode;
+        }
+
         public IEnumerator<IPrtValue> GetEnumerator()
         {
             return set.GetEnumerator();

Src/PRuntimes/PCSharpRuntime/Values/PrtString.cs → 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

Src/PRuntimes/PCSharpRuntime/Values/PrtTuple.cs → 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