diff --git a/Src/PChecker/CheckerCore/CheckerConfiguration.cs b/Src/PChecker/CheckerCore/CheckerConfiguration.cs index e7bf83b154..39d2cd66ea 100644 --- a/Src/PChecker/CheckerCore/CheckerConfiguration.cs +++ b/Src/PChecker/CheckerCore/CheckerConfiguration.cs @@ -11,7 +11,7 @@ namespace PChecker { #pragma warning disable CA1724 // Type names should not match namespaces /// - /// The Coyote project configurations. + /// The checker project configurations. /// [DataContract] [Serializable] @@ -99,7 +99,7 @@ public class CheckerConfiguration public bool IncrementalSchedulingSeed; /// - /// If true, the Coyote tester performs a full exploration, + /// If true, the tester performs a full exploration, /// and does not stop when it finds a bug. /// [DataMember] @@ -141,7 +141,7 @@ public int MaxSchedulingSteps public bool UserExplicitlySetMaxFairSchedulingSteps; /// - /// If true, then the Coyote tester will consider an execution + /// If true, then the tester will consider an execution /// that hits the depth bound as buggy. /// [DataMember] @@ -188,13 +188,13 @@ public int MaxSchedulingSteps public bool IsVerbose { get; set; } /// - /// Enables code coverage reporting of a Coyote program. + /// Enables code coverage reporting of a program. /// [DataMember] public bool ReportCodeCoverage; /// - /// Enables activity coverage reporting of a Coyote program. + /// Enables activity coverage reporting of a program. /// [DataMember] public bool ReportActivityCoverage { get; set; } diff --git a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs index 9a3b2f1d43..40a51bf2cd 100644 --- a/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs +++ b/Src/PChecker/CheckerCore/Coverage/ActivityCoverageReporter.cs @@ -10,7 +10,7 @@ namespace PChecker.Coverage { /// - /// The Coyote code coverage reporter. + /// The code coverage reporter. /// public class ActivityCoverageReporter { @@ -35,17 +35,6 @@ public ActivityCoverageReporter(CoverageInfo coverageInfo) BuiltInEvents.Add(typeof(DefaultEvent).FullName); } - /// - /// Emits the visualization graph. - /// - public void EmitVisualizationGraph(string graphFile) - { - if (CoverageInfo.CoverageGraph != null) - { - CoverageInfo.CoverageGraph.SaveDgml(graphFile, true); - } - } - /// /// Emits the code coverage report. /// diff --git a/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs b/Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogEventCoverage.cs similarity index 97% rename from Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs rename to Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogEventCoverage.cs index f9185b17c7..aae103b016 100644 --- a/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogEventCoverage.cs +++ b/Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogEventCoverage.cs @@ -102,12 +102,12 @@ private static void MergeHashSets(Dictionary> ours, Dict } } - internal class StateMachineRuntimeLogEventCoverage : IStateMachineRuntimeLog + internal class ControlledRuntimeLogEventCoverage : IControlledRuntimeLog { private readonly EventCoverage InternalEventCoverage = new EventCoverage(); private Event Dequeued; - public StateMachineRuntimeLogEventCoverage() + public ControlledRuntimeLogEventCoverage() { } @@ -233,7 +233,7 @@ public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wa } public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted) + Event e, bool isTargetHalted) { var eventName = e.GetType().FullName; EventCoverage.AddEventSent(GetStateId(senderType, senderStateName), eventName); diff --git a/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs b/Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogGraphBuilder.cs similarity index 80% rename from Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs rename to Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogGraphBuilder.cs index 610998bee2..5498a6bf86 100644 --- a/Src/PChecker/CheckerCore/Coverage/StateMachineRuntimeLogGraphBuilder.cs +++ b/Src/PChecker/CheckerCore/Coverage/ControlledRuntimeLogGraphBuilder.cs @@ -14,10 +14,10 @@ namespace PChecker.Coverage { /// - /// Implements the and builds a directed graph + /// Implements the and builds a directed graph /// from the recorded events and state transitions. /// - public class StateMachineRuntimeLogGraphBuilder : IStateMachineRuntimeLog + public class ControlledRuntimeLogGraphBuilder : IControlledRuntimeLog { private Graph CurrentGraph; private readonly Dictionary Dequeued = new Dictionary(); // current dequeued event. @@ -50,7 +50,7 @@ private class PopStateEvent : Event { } - static StateMachineRuntimeLogGraphBuilder() + static ControlledRuntimeLogGraphBuilder() { EventAliases[typeof(GotoStateEvent).FullName] = "goto"; EventAliases[typeof(HaltEvent).FullName] = "halt"; @@ -62,9 +62,9 @@ static StateMachineRuntimeLogGraphBuilder() } /// - /// Initializes a new instance of the class. + /// Initializes a new instance of the class. /// - public StateMachineRuntimeLogGraphBuilder(bool mergeEventLinks) + public ControlledRuntimeLogGraphBuilder(bool mergeEventLinks) { MergeEventLinks = mergeEventLinks; CurrentGraph = new Graph(); @@ -79,9 +79,6 @@ public StateMachineRuntimeLogGraphBuilder(bool mergeEventLinks) /// /// Get or set the underlying logging object. /// - /// - /// See Logging for more information. - /// public TextWriter Logger { get; set; } /// @@ -113,7 +110,7 @@ public void OnCreateStateMachine(StateMachineId id, string creatorName, string c /// public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted) + Event e, bool isTargetHalted) { var eventName = e.GetType().FullName; AddEvent(targetStateMachineId.Name, targetStateMachineId.Type, senderName, senderType, senderStateName, eventName); @@ -662,11 +659,8 @@ private static string GetEventCategory(string fullyQualifiedName) [DataContract] public class Graph { - internal const string DgmlNamespace = "http://schemas.microsoft.com/vs/2009/dgml"; - // These [DataMember] fields are here so we can serialize the Graph across parallel or distributed - // test processes without losing any information. There is more information here than in the serialized - // DGML which is we we can't just use Save/LoadDgml to do the same. + // test processes without losing any information. [DataMember] private readonly Dictionary InternalNodes = new Dictionary(); @@ -797,175 +791,7 @@ internal int GetUniqueLinkIndex(GraphNode source, GraphNode target, string id) return index; } - - /// - /// Serialize the graph to a DGML string. - /// - public override string ToString() - { - using (var writer = new StringWriter()) - { - WriteDgml(writer, false); - return writer.ToString(); - } - } - - internal void SaveDgml(string graphFilePath, bool includeDefaultStyles) - { - using (var writer = new StreamWriter(graphFilePath, false, Encoding.UTF8)) - { - WriteDgml(writer, includeDefaultStyles); - } - } - - /// - /// Serialize the graph to DGML. - /// - public void WriteDgml(TextWriter writer, bool includeDefaultStyles) - { - writer.WriteLine("", DgmlNamespace); - writer.WriteLine(" "); - - if (InternalNodes != null) - { - var nodes = new List(InternalNodes.Keys); - nodes.Sort(); - foreach (var id in nodes) - { - var node = InternalNodes[id]; - writer.Write(" "); - } - } - - writer.WriteLine(" "); - writer.WriteLine(" "); - - if (InternalLinks != null) - { - var links = new List(InternalLinks.Keys); - links.Sort(); - foreach (var id in links) - { - var link = InternalLinks[id]; - writer.Write(" "); - } - } - - writer.WriteLine(" "); - if (includeDefaultStyles) - { - writer.WriteLine( - @" - - - - - - - "); - } - - writer.WriteLine(""); - } - - /// - /// Load a DGML file into a new Graph object. - /// - /// Full path to the DGML file. - /// The loaded Graph object. - public static Graph LoadDgml(string graphFilePath) - { - var doc = XDocument.Load(graphFilePath); - var result = new Graph(); - var ns = doc.Root.Name.Namespace; - if (ns != DgmlNamespace) - { - throw new Exception(string.Format("File '{0}' does not contain the DGML namespace", graphFilePath)); - } - - foreach (var e in doc.Root.Element(ns + "Nodes").Elements(ns + "Node")) - { - var id = (string)e.Attribute("Id"); - var label = (string)e.Attribute("Label"); - var category = (string)e.Attribute("Category"); - - var node = new GraphNode(id, label, category); - node.AddDgmlProperties(e); - result.GetOrCreateNode(node); - } - - foreach (var e in doc.Root.Element(ns + "Links").Elements(ns + "Link")) - { - var srcId = (string)e.Attribute("Source"); - var targetId = (string)e.Attribute("Target"); - var label = (string)e.Attribute("Label"); - var category = (string)e.Attribute("Category"); - var srcNode = result.GetOrCreateNode(srcId); - var targetNode = result.GetOrCreateNode(targetId); - var indexAttr = e.Attribute("index"); - int? index = null; - if (indexAttr != null) - { - index = (int)indexAttr; - } - - var link = result.GetOrCreateLink(srcNode, targetNode, index, label, category); - link.AddDgmlProperties(e); - } - - return result; - } + /// /// Merge the given graph so that this graph becomes a superset of both graphs. @@ -1132,27 +958,6 @@ public GraphNode(string id, string label, string category) Label = label; Category = category; } - - /// - /// Add additional properties from XML element. - /// - /// An XML element representing the graph node in DGML format. - public void AddDgmlProperties(XElement e) - { - foreach (var a in e.Attributes()) - { - switch (a.Name.LocalName) - { - case "Id": - case "Label": - case "Category": - break; - default: - AddAttribute(a.Name.LocalName, a.Value); - break; - } - } - } } /// @@ -1202,27 +1007,5 @@ public GraphLink(GraphNode source, GraphNode target, string label, string catego Label = label; Category = category; } - - /// - /// Add additional properties from XML element. - /// - /// An XML element representing the graph node in DGML format. - public void AddDgmlProperties(XElement e) - { - foreach (var a in e.Attributes()) - { - switch (a.Name.LocalName) - { - case "Source": - case "Target": - case "Label": - case "Category": - break; - default: - AddAttribute(a.Name.LocalName, a.Value); - break; - } - } - } } } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Exceptions/AssertionFailureException.cs b/Src/PChecker/CheckerCore/Exceptions/AssertionFailureException.cs index 779c439ab2..271eca30f8 100644 --- a/Src/PChecker/CheckerCore/Exceptions/AssertionFailureException.cs +++ b/Src/PChecker/CheckerCore/Exceptions/AssertionFailureException.cs @@ -6,7 +6,7 @@ namespace PChecker.Exceptions { /// - /// The exception that is thrown by the Coyote runtime upon assertion failure. + /// The exception that is thrown by the ControlledRuntime upon assertion failure. /// internal sealed class AssertionFailureException : RuntimeException { diff --git a/Src/PChecker/CheckerCore/Exceptions/RuntimeException.cs b/Src/PChecker/CheckerCore/Exceptions/RuntimeException.cs index 802bb68ea9..2b6b4d1011 100644 --- a/Src/PChecker/CheckerCore/Exceptions/RuntimeException.cs +++ b/Src/PChecker/CheckerCore/Exceptions/RuntimeException.cs @@ -8,7 +8,7 @@ namespace PChecker.Exceptions { /// - /// An exception that is thrown by the Coyote runtime. + /// An exception that is thrown by the ControlledRuntime. /// [Serializable] [DebuggerStepThrough] diff --git a/Src/PChecker/CheckerCore/IO/Logging/ConsoleLogger.cs b/Src/PChecker/CheckerCore/IO/Logging/ConsoleLogger.cs index 027e89f7b7..b2cc0598b7 100644 --- a/Src/PChecker/CheckerCore/IO/Logging/ConsoleLogger.cs +++ b/Src/PChecker/CheckerCore/IO/Logging/ConsoleLogger.cs @@ -10,9 +10,6 @@ namespace PChecker.IO.Logging /// /// Logger that writes text to the console. /// - /// - /// See Logging for more information. - /// public sealed class ConsoleLogger : TextWriter { /// diff --git a/Src/PChecker/CheckerCore/PRuntime/Exceptions/PrtInhabitsTypeException.cs b/Src/PChecker/CheckerCore/PRuntime/Exceptions/PrtInhabitsTypeException.cs deleted file mode 100644 index b9c9d5037e..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Exceptions/PrtInhabitsTypeException.cs +++ /dev/null @@ -1,19 +0,0 @@ -using System; - -namespace PChecker.PRuntime.Exceptions -{ - public class PrtInhabitsTypeException : Exception - { - public PrtInhabitsTypeException() - { - } - - public PrtInhabitsTypeException(string message) : base(message) - { - } - - public PrtInhabitsTypeException(string message, Exception innerException) : base(message, innerException) - { - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/PrtTypes.cs b/Src/PChecker/CheckerCore/PRuntime/PTypes.cs similarity index 73% rename from Src/PChecker/CheckerCore/PRuntime/PrtTypes.cs rename to Src/PChecker/CheckerCore/PRuntime/PTypes.cs index 681640a4fd..a1af43028c 100644 --- a/Src/PChecker/CheckerCore/PRuntime/PrtTypes.cs +++ b/Src/PChecker/CheckerCore/PRuntime/PTypes.cs @@ -5,7 +5,7 @@ namespace PChecker.PRuntime { - public abstract class PrtType + public abstract class PType { public override string ToString() { @@ -13,7 +13,7 @@ public override string ToString() } } - public class PrtNullType : PrtType + public class PNullType : PType { public override string ToString() { @@ -21,7 +21,7 @@ public override string ToString() } } - public class PrtAnyType : PrtType + public class PAnyType : PType { public override string ToString() { @@ -29,7 +29,7 @@ public override string ToString() } } - public class PrtMachineType : PrtType + public class PMachineType : PType { public override string ToString() { @@ -37,7 +37,7 @@ public override string ToString() } } - public class PrtIntType : PrtType + public class PIntType : PType { public override string ToString() { @@ -45,7 +45,7 @@ public override string ToString() } } - public class PrtFloatType : PrtType + public class PFloatType : PType { public override string ToString() { @@ -53,12 +53,12 @@ public override string ToString() } } - public class PrtEnumType : PrtType + public class PEnumType : PType { public Dictionary enumConstants; public string name; - public PrtEnumType(string typeName, params object[] args) + public PEnumType(string typeName, params object[] args) { name = typeName; enumConstants = new Dictionary(); @@ -81,12 +81,12 @@ public override string ToString() } } - public class PrtPermissionType : PrtType + public class PPermissionType : PType { public string name; public List permissions; - public PrtPermissionType(string name, IEnumerable perm) + public PPermissionType(string name, IEnumerable perm) { this.name = name; permissions = perm.ToList(); @@ -98,7 +98,7 @@ public override string ToString() } } - public class PrtBoolType : PrtType + public class PBoolType : PType { public override string ToString() { @@ -106,7 +106,7 @@ public override string ToString() } } - public class PrtStringType : PrtType + public class PStringType : PType { public override string ToString() { @@ -114,7 +114,7 @@ public override string ToString() } } - public class PrtEventType : PrtType + public class PEventType : PType { public override string ToString() { @@ -122,12 +122,12 @@ public override string ToString() } } - public class PrtMapType : PrtType + public class PMapType : PType { - public PrtType keyType; - public PrtType valType; + public PType keyType; + public PType valType; - public PrtMapType(PrtType k, PrtType v) + public PMapType(PType k, PType v) { keyType = k; valType = v; @@ -139,11 +139,11 @@ public override string ToString() } } - public class PrtSeqType : PrtType + public class PSeqType : PType { - public PrtType elemType; + public PType elemType; - public PrtSeqType(PrtType s) + public PSeqType(PType s) { elemType = s; } @@ -154,11 +154,11 @@ public override string ToString() } } - public class PrtSetType : PrtType + public class PSetType : PType { - public PrtType elemType; + public PType elemType; - public PrtSetType(PrtType s) + public PSetType(PType s) { elemType = s; } @@ -169,22 +169,22 @@ public override string ToString() } } - public class PrtTupleType : PrtType + public class PTupleType : PType { - public List fieldTypes; + public List fieldTypes; - public PrtTupleType() + public PTupleType() { /* This constructor is added only to prevent the other constructor from being called - when an instance of PrtNamedTupleType is created. + when an instance of PNamedTupleType is created. */ } - public PrtTupleType(params PrtType[] fields) + public PTupleType(params PType[] fields) { Debug.Assert(fields.Any()); - fieldTypes = new List(); + fieldTypes = new List(); foreach (var f in fields) { fieldTypes.Add(f); @@ -204,22 +204,22 @@ public override string ToString() } } - public class PrtNamedTupleType : PrtTupleType + public class PNamedTupleType : PTupleType { public List fieldNames; - public PrtNamedTupleType(params object[] args) + public PNamedTupleType(params object[] args) { Debug.Assert(args.Length > 0); fieldNames = new List(); - fieldTypes = new List(); + fieldTypes = new List(); var index = 0; while (index < args.Length) { fieldNames.Add((string)args[index]); index++; - fieldTypes.Add((PrtType)args[index]); + fieldTypes.Add((PType)args[index]); index++; } } diff --git a/Src/PChecker/CheckerCore/PRuntime/PrtValues.cs b/Src/PChecker/CheckerCore/PRuntime/PrtValues.cs deleted file mode 100644 index 6b56ffff04..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/PrtValues.cs +++ /dev/null @@ -1,56 +0,0 @@ -using PChecker.PRuntime.Values; - -namespace PChecker.PRuntime -{ - public static class PrtValues - { - public static PrtBool Box(bool value) - { - return value; - } - - public static PrtInt Box(long value) - { - return new PrtInt(value); - } - - public static PrtInt Box(int value) - { - return new PrtInt(value); - } - - public static PrtInt Box(short value) - { - return new PrtInt(value); - } - - public static PrtInt Box(byte value) - { - return new PrtInt(value); - } - - public static PrtFloat Box(double value) - { - return new PrtFloat(value); - } - - public static PrtFloat Box(float value) - { - return new PrtFloat(value); - } - - public static PrtBool SafeEquals(IPrtValue val1, IPrtValue val2) - { - return ReferenceEquals(val1, val2) || val1 != null && val1.Equals(val2); - } - - public static IPrtValue PrtCastValue(IPrtValue value, PrtType type) - { - //todo: Needs to be fixed for better error message - /*if (!PrtInhabitsType(value, type)) - throw new PrtInhabitsTypeException( - $"value {value.ToString()} is not a member of type {type.ToString()}");*/ - return value.Clone(); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs index 322b3daebe..17fb6fbb56 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Runtime/ControlledRuntime.cs @@ -95,7 +95,7 @@ public sealed class ControlledRuntime : IDisposable protected internal volatile bool IsRunning; /// - /// Callback that is fired when the Coyote program throws an exception which includes failed assertions. + /// Callback that is fired when the program throws an exception which includes failed assertions. /// public event OnFailureHandler OnFailure; @@ -136,17 +136,17 @@ public sealed class ControlledRuntime : IDisposable private readonly ConcurrentDictionary StateMachineMap; /// - /// Callback that is fired when a Coyote event is dropped. + /// Callback that is fired when an event is dropped. /// public event OnEventDroppedHandler OnEventDropped; /// - /// Responsible for writing to all registered objects. + /// Responsible for writing to all registered objects. /// protected internal LogWriter LogWriter { get; private set; } /// - /// Used to log text messages. Use + /// Used to log text messages. Use /// to replace the logger with a custom one. /// public TextWriter Logger => LogWriter.Logger; @@ -299,26 +299,26 @@ public StateMachineId CreateStateMachineIdFromName(Type type, string name) /// optional . This event can only be used to access its payload, /// and cannot be handled. /// - public StateMachineId CreateStateMachine(Type type, Event initialEvent = null, Guid opGroupId = default) => - CreateStateMachine(null, type, null, initialEvent, opGroupId); + public StateMachineId CreateStateMachine(Type type, Event initialEvent = null) => + CreateStateMachine(null, type, null, initialEvent); /// /// Creates a new state machine of the specified and name, and with the /// specified optional . This event can only be used to access /// its payload, and cannot be handled. /// - public StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => - CreateStateMachine(null, type, name, initialEvent, opGroupId); + public StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null) => + CreateStateMachine(null, type, name, initialEvent); /// /// Creates a new state machine of the specified type, using the specified . /// This method optionally passes an to the new state machine, which can only /// be used to access its payload, and cannot be handled. /// - public StateMachineId CreateStateMachine(StateMachineId id, Type type, Event initialEvent = null, Guid opGroupId = default) + public StateMachineId CreateStateMachine(StateMachineId id, Type type, Event initialEvent = null) { Assert(id != null, "Cannot create an state machine using a null state machine id."); - return CreateStateMachine(id, type, null, initialEvent, opGroupId); + return CreateStateMachine(id, type, null, initialEvent); } /// @@ -327,8 +327,8 @@ public StateMachineId CreateStateMachine(StateMachineId id, Type type, Event ini /// and cannot be handled. The method returns only when the state machine is initialized and /// the (if any) is handled. /// - public Task CreateStateMachineAndExecuteAsync(Type type, Event e = null, Guid opGroupId = default) => - CreateStateMachineAndExecuteAsync(null, type, null, e, opGroupId); + public Task CreateStateMachineAndExecuteAsync(Type type, Event e = null) => + CreateStateMachineAndExecuteAsync(null, type, null, e); /// /// Creates a new state machine of the specified and name, and with the @@ -336,8 +336,8 @@ public Task CreateStateMachineAndExecuteAsync(Type type, Event e /// its payload, and cannot be handled. The method returns only when the state machine is /// initialized and the (if any) is handled. /// - public Task CreateStateMachineAndExecuteAsync(Type type, string name, Event e = null, Guid opGroupId = default) => - CreateStateMachineAndExecuteAsync(null, type, name, e, opGroupId); + public Task CreateStateMachineAndExecuteAsync(Type type, string name, Event e = null) => + CreateStateMachineAndExecuteAsync(null, type, name, e); /// /// Creates a new state machine of the specified , using the specified unbound @@ -346,45 +346,31 @@ public Task CreateStateMachineAndExecuteAsync(Type type, string /// the state machine is initialized and the (if any) /// is handled. /// - public Task CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, Event e = null, Guid opGroupId = default) + public Task CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, Event e = null) { Assert(id != null, "Cannot create an state machine using a null state machine id."); - return CreateStateMachineAndExecuteAsync(id, type, null, e, opGroupId); + return CreateStateMachineAndExecuteAsync(id, type, null, e); } /// /// Sends an asynchronous to a state machine. /// - public void SendEvent(StateMachineId targetId, Event e, Guid opGroupId = default) + public void SendEvent(StateMachineId targetId, Event e) { var senderOp = Scheduler.GetExecutingOperation(); - SendEvent(targetId, e, senderOp?.StateMachine, opGroupId); + SendEvent(targetId, e, senderOp?.StateMachine); } /// /// Sends an to a state machine. Returns immediately if the target was already /// running. Otherwise, blocks until the target handles the event and reaches quiescence. /// - public Task SendEventAndExecuteAsync(StateMachineId targetId, Event e, Guid opGroupId = default) + public Task SendEventAndExecuteAsync(StateMachineId targetId, Event e) { var senderOp = Scheduler.GetExecutingOperation(); - return SendEventAndExecuteAsync(targetId, e, senderOp?.StateMachine, opGroupId); + return SendEventAndExecuteAsync(targetId, e, senderOp?.StateMachine); } - - /// - /// Returns the operation group id of the state machine with the specified id. Returns - /// if the id is not set, or if the is not associated with this runtime. During - /// testing, the runtime asserts that the specified state machine is currently executing. - /// - public Guid GetCurrentOperationGroupId(StateMachineId currentStateMachineId) - { - var callerOp = Scheduler.GetExecutingOperation(); - Assert(callerOp != null && currentStateMachineId == callerOp.StateMachine.Id, - "Trying to access the operation group id of {0}, which is not the currently executing state machine.", - currentStateMachineId); - return callerOp.StateMachine.OperationGroupId; - } - + /// /// Runs the specified test method. /// @@ -461,22 +447,20 @@ internal ulong GetNextOperationId() => /// unbound state machine id, and passes the specified optional . This event /// can only be used to access its payload, and cannot be handled. /// - internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string name, Event initialEvent = null, - Guid opGroupId = default) + internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string name, Event initialEvent = null) { var creatorOp = Scheduler.GetExecutingOperation(); - return CreateStateMachine(id, type, name, initialEvent, creatorOp?.StateMachine, opGroupId); + return CreateStateMachine(id, type, name, initialEvent, creatorOp?.StateMachine); } /// /// Creates a new of the specified . /// - internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string name, Event initialEvent, StateMachine creator, - Guid opGroupId) + internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string name, Event initialEvent, StateMachine creator) { AssertExpectedCallerStateMachine(creator, "CreateStateMachine"); - var stateMachine = CreateStateMachine(id, type, name, creator, opGroupId); + var stateMachine = CreateStateMachine(id, type, name, creator); LogWriter.LogCreateStateMachine(stateMachine.Id, creator?.Id.Name, creator?.Id.Type); RunStateMachineEventHandler(stateMachine, initialEvent, true, null); return stateMachine.Id; @@ -488,11 +472,10 @@ internal StateMachineId CreateStateMachine(StateMachineId id, Type type, string /// can only be used to access its payload, and cannot be handled. The method returns only /// when the state machine is initialized and the (if any) is handled. /// - internal Task CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, string name, Event initialEvent = null, - Guid opGroupId = default) + internal Task CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, string name, Event initialEvent = null) { var creatorOp = Scheduler.GetExecutingOperation(); - return CreateStateMachineAndExecuteAsync(id, type, name, initialEvent, creatorOp?.StateMachine, opGroupId); + return CreateStateMachineAndExecuteAsync(id, type, name, initialEvent, creatorOp?.StateMachine); } /// @@ -501,13 +484,13 @@ internal Task CreateStateMachineAndExecuteAsync(StateMachineId i /// is handled. /// internal async Task CreateStateMachineAndExecuteAsync(StateMachineId id, Type type, string name, - Event initialEvent, StateMachine creator, Guid opGroupId) + Event initialEvent, StateMachine creator) { AssertExpectedCallerStateMachine(creator, "CreateStateMachineAndExecuteAsync"); Assert(creator != null, "Only a state machine can call 'CreateStateMachineAndExecuteAsync': avoid calling " + "it directly from the test method; instead call it through a test driver state machine."); - var stateMachine = CreateStateMachine(id, type, name, creator, opGroupId); + var stateMachine = CreateStateMachine(id, type, name, creator); RunStateMachineEventHandler(stateMachine, initialEvent, true, creator); // Wait until the state machine reaches quiescence. @@ -518,7 +501,7 @@ internal async Task CreateStateMachineAndExecuteAsync(StateMachi /// /// Creates a new state machine of the specified . /// - private StateMachine CreateStateMachine(StateMachineId id, Type type, string name, StateMachine creator, Guid opGroupId) + private StateMachine CreateStateMachine(StateMachineId id, Type type, string name, StateMachine creator) { Assert(type.IsSubclassOf(typeof(StateMachine)), "Type '{0}' is not a state machine.", type.FullName); @@ -538,18 +521,9 @@ private StateMachine CreateStateMachine(StateMachineId id, Type type, string nam id.Value, id.Type, type.FullName); id.Bind(this); } - - // The operation group id of the state machine is set using the following precedence: - // (1) To the specified state machine creation operation group id, if it is non-empty. - // (2) To the operation group id of the creator state machine, if it exists and is non-empty. - // (3) To the empty operation group id. - if (opGroupId == Guid.Empty && creator != null) - { - opGroupId = creator.OperationGroupId; - } - + var stateMachine = Create(type); - IStateMachineManager stateMachineManager = new StateMachineManager(this, stateMachine, opGroupId); + IStateMachineManager stateMachineManager = new StateMachineManager(this, stateMachine); IEventQueue eventQueue = new EventQueue(stateMachineManager, stateMachine); stateMachine.Configure(this, id, stateMachineManager, eventQueue); @@ -599,7 +573,7 @@ public static StateMachine Create(Type type) /// /// Sends an asynchronous to a state machine. /// - internal void SendEvent(StateMachineId targetId, Event e, StateMachine sender, Guid opGroupId) + internal void SendEvent(StateMachineId targetId, Event e, StateMachine sender) { if (e is null) { @@ -620,7 +594,7 @@ internal void SendEvent(StateMachineId targetId, Event e, StateMachine sender, G AssertExpectedCallerStateMachine(sender, "SendEvent"); - var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); + var enqueueStatus = EnqueueEvent(targetId, e, sender, out var target); if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning) { RunStateMachineEventHandler(target, null, false, null); @@ -631,14 +605,13 @@ internal void SendEvent(StateMachineId targetId, Event e, StateMachine sender, G /// Sends an asynchronous to a state machine. Returns immediately if the target was /// already running. Otherwise, blocks until the target handles the event and reaches quiescence. /// - internal async Task SendEventAndExecuteAsync(StateMachineId targetId, Event e, StateMachine sender, - Guid opGroupId) + internal async Task SendEventAndExecuteAsync(StateMachineId targetId, Event e, StateMachine sender) { Assert(e != null, "{0} is sending a null event.", sender.Id); Assert(targetId != null, "{0} is sending event {1} to a null state machine.", sender.Id, e); AssertExpectedCallerStateMachine(sender, "SendEventAndExecuteAsync"); - var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target); + var enqueueStatus = EnqueueEvent(targetId, e, sender, out var target); if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning) { RunStateMachineEventHandler(target, null, false, sender); @@ -657,7 +630,7 @@ internal async Task SendEventAndExecuteAsync(StateMachineId targetId, Even /// /// Enqueues an event to the state machine with the specified id. /// - private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachine sender, Guid opGroupId, out StateMachine target) + private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachine sender, out StateMachine target) { target = Scheduler.GetOperationWithId(targetId.Value)?.StateMachine; Assert(target != null, @@ -667,24 +640,15 @@ private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachin Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Send); ResetProgramCounter(sender); - // The operation group id of this operation is set using the following precedence: - // (1) To the specified send operation group id, if it is non-empty. - // (2) To the operation group id of the sender state machine, if it exists and is non-empty. - // (3) To the empty operation group id. - if (opGroupId == Guid.Empty && sender != null) - { - opGroupId = sender.OperationGroupId; - } - if (target.IsHalted) { LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type, - (sender)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true); + (sender)?.CurrentStateName ?? string.Empty, e, isTargetHalted: true); TryHandleDroppedEvent(e, targetId); return EnqueueStatus.Dropped; } - var enqueueStatus = EnqueueEvent(target, e, sender, opGroupId); + var enqueueStatus = EnqueueEvent(target, e, sender); if (enqueueStatus == EnqueueStatus.Dropped) { TryHandleDroppedEvent(e, targetId); @@ -696,7 +660,7 @@ private EnqueueStatus EnqueueEvent(StateMachineId targetId, Event e, StateMachin /// /// Enqueues an event to the state machine with the specified id. /// - private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMachine sender, Guid opGroupId) + private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMachine sender) { // Directly use sender as a StateMachine var originInfo = new EventOriginInfo(sender.Id, sender.GetType().FullName, @@ -705,9 +669,9 @@ private EnqueueStatus EnqueueEvent(StateMachine stateMachine, Event e, StateMach var eventInfo = new EventInfo(e, originInfo); LogWriter.LogSendEvent(stateMachine.Id, sender.Id.Name, sender.Id.Type, sender.CurrentStateName, - e, opGroupId, isTargetHalted: false); + e, isTargetHalted: false); - return stateMachine.Enqueue(e, opGroupId, eventInfo); + return stateMachine.Enqueue(e, eventInfo); } /// @@ -741,7 +705,7 @@ private void RunStateMachineEventHandler(StateMachine stateMachine, Event initia await stateMachine.RunEventHandlerAsync(); if (syncCaller != null) { - EnqueueEvent(syncCaller, new QuiescentEvent(stateMachine.Id), stateMachine, stateMachine.OperationGroupId); + EnqueueEvent(syncCaller, new QuiescentEvent(stateMachine.Id), stateMachine); } if (!stateMachine.IsHalted) @@ -1313,14 +1277,14 @@ internal void NotifyMonitorError(Monitor monitor) public void SetJsonLogger(JsonWriter jsonLogger) => LogWriter.SetJsonLogger(jsonLogger); /// - /// Use this method to register an . + /// Use this method to register an . /// - public void RegisterLog(IStateMachineRuntimeLog log) => LogWriter.RegisterLog(log); + public void RegisterLog(IControlledRuntimeLog log) => LogWriter.RegisterLog(log); /// - /// Use this method to unregister a previously registered . + /// Use this method to unregister a previously registered . /// - public void RemoveLog(IStateMachineRuntimeLog log) => LogWriter.RemoveLog(log); + public void RemoveLog(IControlledRuntimeLog log) => LogWriter.RemoveLog(log); /// /// Get the coverage graph information (if any). This information is only available @@ -1332,13 +1296,13 @@ public CoverageInfo GetCoverageInfo() var result = CoverageInfo; if (result != null) { - var builder = LogWriter.GetLogsOfType().FirstOrDefault(); + var builder = LogWriter.GetLogsOfType().FirstOrDefault(); if (builder != null) { result.CoverageGraph = builder.SnapshotGraph(CheckerConfiguration.IsDgmlBugGraph); } - var eventCoverage = LogWriter.GetLogsOfType().FirstOrDefault(); + var eventCoverage = LogWriter.GetLogsOfType().FirstOrDefault(); if (eventCoverage != null) { result.EventInfo = eventCoverage.EventCoverage; diff --git a/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs b/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs index 97acb4614e..a97070f584 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Runtime/OnFailureHandler.cs @@ -6,7 +6,7 @@ namespace PChecker.Runtime { /// - /// Handles the event. + /// Handles the event. /// public delegate void OnFailureHandler(Exception ex); } \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs index 2aeb515c85..b4d4337433 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Specifications/Monitor.cs @@ -24,10 +24,6 @@ namespace PChecker.Specifications.Monitors /// /// Abstract class representing a specification monitor. /// - /// - /// See Specifications Overview - /// for more information. - /// public class Monitor { /// @@ -111,9 +107,6 @@ public class Monitor /// /// The logger installed to the runtime. /// - /// - /// See Logging for more information. - /// protected TextWriter Logger => Runtime.Logger; /// @@ -194,7 +187,7 @@ internal void Initialize(ControlledRuntime runtime) /// /// /// This event is not handled until the action that calls this method returns control back - /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox. + /// to the ControlledRuntime. It is handled before any other events are dequeued from the inbox. /// Only one of the following can be called per action: /// , . /// An Assert is raised if you accidentally try and do two of these operations in a single action. @@ -242,7 +235,7 @@ public void Log(string message) /// this.RaiseEvent(new E()); /// /// This event is not handled until the action that calls this method returns control back - /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox. + /// to the ControlledRuntime. It is handled before any other events are dequeued from the inbox. /// Only one of the following can be called per action: /// , . /// An Assert is raised if you accidentally try and do two of these operations in a single action. @@ -268,7 +261,7 @@ public void RaiseGotoStateEvent(object payload = null) where S : State /// this.RaiseEvent(new E()); /// /// This event is not handled until the action that calls this method returns control back - /// to the Coyote runtime. It is handled before any other events are dequeued from the inbox. + /// to the ControlledRuntime. It is handled before any other events are dequeued from the inbox. /// Only one of the following can be called per action: /// , . /// An Assert is raised if you accidentally try and do two of these operations in a single action. @@ -1021,7 +1014,7 @@ internal HashSet> GetAllStateEventPairs() /// Defines the transition that is the /// result of executing an event handler. Transitions are created by using /// , or . - /// The Transition is processed by the Coyote runtime when + /// The Transition is processed by the ControlledRuntime when /// an event handling method returns a Transition object. /// This means such a method can only do one such Transition per method call. /// If the method wants to do a conditional transition it can return diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs index bfa6d5dfe7..c60673d416 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/EventQueue.cs @@ -28,12 +28,12 @@ internal sealed class EventQueue : IEventQueue /// /// The internal queue that contains events with their metadata. /// - private readonly LinkedList<(Event e, Guid opGroupId, EventInfo info)> Queue; + private readonly LinkedList<(Event e, EventInfo info)> Queue; /// /// The raised event and its metadata, or null if no event has been raised. /// - private (Event e, Guid opGroupId, EventInfo info) RaisedEvent; + private (Event e, EventInfo info) RaisedEvent; /// /// Map from the types of events that the owner of the queue is waiting to receive @@ -70,13 +70,13 @@ internal EventQueue(IStateMachineManager stateMachineManager, StateMachine state { StateMachineManager = stateMachineManager; StateMachine = stateMachine; - Queue = new LinkedList<(Event, Guid, EventInfo)>(); + Queue = new LinkedList<(Event, EventInfo)>(); EventWaitTypes = new Dictionary>(); IsClosed = false; } /// - public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) + public EnqueueStatus Enqueue(Event e, EventInfo info) { if (IsClosed) { @@ -87,13 +87,13 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) (predicate is null || predicate(e))) { EventWaitTypes.Clear(); - StateMachineManager.OnReceiveEvent(e, opGroupId, info); + StateMachineManager.OnReceiveEvent(e, info); ReceiveCompletionSource.SetResult(e); return EnqueueStatus.EventHandlerRunning; } - StateMachineManager.OnEnqueueEvent(e, opGroupId, info); - Queue.AddLast((e, opGroupId, info)); + StateMachineManager.OnEnqueueEvent(e, info); + Queue.AddLast((e, info)); if (!StateMachineManager.IsEventHandlerRunning) { @@ -112,13 +112,13 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } /// - public (DequeueStatus status, Event e, Guid opGroupId, EventInfo info) Dequeue() + public (DequeueStatus status, Event e, EventInfo info) Dequeue() { // Try to get the raised event, if there is one. Raised events // have priority over the events in the inbox. if (RaisedEvent != default) { - if (StateMachineManager.IsEventIgnored(RaisedEvent.e, RaisedEvent.opGroupId, RaisedEvent.info)) + if (StateMachineManager.IsEventIgnored(RaisedEvent.e, RaisedEvent.info)) { // TODO: should the user be able to raise an ignored event? // The raised event is ignored in the current state. @@ -128,7 +128,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) { var raisedEvent = RaisedEvent; RaisedEvent = default; - return (DequeueStatus.Raised, raisedEvent.e, raisedEvent.opGroupId, raisedEvent.info); + return (DequeueStatus.Raised, raisedEvent.e, raisedEvent.info); } } @@ -139,11 +139,11 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } // Try to dequeue the next event, if there is one. - var (e, opGroupId, info) = TryDequeueEvent(); + var (e, info) = TryDequeueEvent(); if (e != null) { // Found next event that can be dequeued. - return (DequeueStatus.Success, e, opGroupId, info); + return (DequeueStatus.Success, e, info); } // No event can be dequeued, so check if there is a default event handler. @@ -151,22 +151,22 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) { // There is no default event handler installed, so do not return an event. StateMachineManager.IsEventHandlerRunning = false; - return (DequeueStatus.NotAvailable, null, Guid.Empty, null); + return (DequeueStatus.NotAvailable, null, null); } // TODO: check op-id of default event. // A default event handler exists. var stateName = NameResolver.GetStateNameForLogging(StateMachine.CurrentState.GetType()); var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName); - return (DequeueStatus.Default, DefaultEvent.Instance, Guid.Empty, new EventInfo(DefaultEvent.Instance, eventOrigin)); + return (DequeueStatus.Default, DefaultEvent.Instance, new EventInfo(DefaultEvent.Instance, eventOrigin)); } /// /// Dequeues the next event and its metadata, if there is one available, else returns null. /// - private (Event e, Guid opGroupId, EventInfo info) TryDequeueEvent(bool checkOnly = false) + private (Event e, EventInfo info) TryDequeueEvent(bool checkOnly = false) { - (Event, Guid, EventInfo) nextAvailableEvent = default; + (Event, EventInfo) nextAvailableEvent = default; // Iterates through the events and metadata in the inbox. var node = Queue.First; @@ -175,7 +175,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) var nextNode = node.Next; var currentEvent = node.Value; - if (StateMachineManager.IsEventIgnored(currentEvent.e, currentEvent.opGroupId, currentEvent.info)) + if (StateMachineManager.IsEventIgnored(currentEvent.e, currentEvent.info)) { if (!checkOnly) { @@ -188,7 +188,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } // Skips a deferred event. - if (!StateMachineManager.IsEventDeferred(currentEvent.e, currentEvent.opGroupId, currentEvent.info)) + if (!StateMachineManager.IsEventDeferred(currentEvent.e, currentEvent.info)) { nextAvailableEvent = currentEvent; if (!checkOnly) @@ -206,13 +206,13 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) } /// - public void RaiseEvent(Event e, Guid opGroupId) + public void RaiseEvent(Event e) { var stateName = NameResolver.GetStateNameForLogging(StateMachine.CurrentState.GetType()); var eventOrigin = new EventOriginInfo(StateMachine.Id, StateMachine.GetType().FullName, stateName); var info = new EventInfo(e, eventOrigin); - RaisedEvent = (e, opGroupId, info); - StateMachineManager.OnRaiseEvent(e, opGroupId, info); + RaisedEvent = (e, info); + StateMachineManager.OnRaiseEvent(e, info); } /// @@ -257,7 +257,7 @@ private Task ReceiveEventAsync(Dictionary> eventW { StateMachine.Runtime.NotifyReceiveCalled(StateMachine); - (Event e, Guid opGroupId, EventInfo info) receivedEvent = default; + (Event e, EventInfo info) receivedEvent = default; var node = Queue.First; while (node != null) { @@ -281,7 +281,7 @@ private Task ReceiveEventAsync(Dictionary> eventW return ReceiveCompletionSource.Task; } - StateMachineManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.opGroupId, receivedEvent.info); + StateMachineManager.OnReceiveEventWithoutWaiting(receivedEvent.e, receivedEvent.info); return Task.FromResult(receivedEvent.e); } @@ -291,7 +291,7 @@ public int GetCachedState() unchecked { var hash = 19; - foreach (var (_, _, info) in Queue) + foreach (var (_, info) in Queue) { hash = (hash * 31) + info.EventName.GetHashCode(); } @@ -316,9 +316,9 @@ private void Dispose(bool disposing) return; } - foreach (var (e, opGroupId, info) in Queue) + foreach (var (e, info) in Queue) { - StateMachineManager.OnDropEvent(e, opGroupId, info); + StateMachineManager.OnDropEvent(e, info); } Queue.Clear(); diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/IEventQueue.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/IEventQueue.cs index c449792aef..1b149527a5 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/IEventQueue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/EventQueues/IEventQueue.cs @@ -25,17 +25,17 @@ internal interface IEventQueue : IDisposable /// /// Enqueues the specified event and its optional metadata. /// - EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info); + EnqueueStatus Enqueue(Event e, EventInfo info); /// /// Dequeues the next event, if there is one available. /// - (DequeueStatus status, Event e, Guid opGroupId, EventInfo info) Dequeue(); + (DequeueStatus status, Event e, EventInfo info) Dequeue(); /// /// Enqueues the specified raised event. /// - void RaiseEvent(Event e, Guid opGroupId); + void RaiseEvent(Event e); /// /// Waits to receive an event of the specified type that satisfies an optional predicate. diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/Event.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/Event.cs index 328f29cd70..855a216262 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/Event.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Events/Event.cs @@ -11,25 +11,25 @@ namespace PChecker.StateMachines.Events /// Class representing an event. /// [DataContract] - public class Event: IPrtValue + public class Event: IPValue { public Event() { } - public Event(IPrtValue payload) + public Event(IPValue payload) { Payload = payload; } - public IPrtValue Payload { get; set; } + public IPValue Payload { get; set; } - public bool Equals(IPrtValue other) + public bool Equals(IPValue other) { return other != null && GetType().FullName.Equals(other.GetType().FullName); } - public virtual IPrtValue Clone() + public virtual IPValue Clone() { throw new NotImplementedException(); } @@ -57,7 +57,7 @@ public override string ToString() public class PHalt : Event { - public PHalt(IPrtValue payload) : base(payload) + public PHalt(IPValue payload) : base(payload) { } } diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IControlledRuntimeLog.cs similarity index 99% rename from Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs rename to Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IControlledRuntimeLog.cs index aa933288ac..de0f574858 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IStateMachineRuntimeLog.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/IControlledRuntimeLog.cs @@ -10,7 +10,7 @@ namespace PChecker.StateMachines.Logging /// Interface that allows an external module to track what /// is happening in the . /// - public interface IStateMachineRuntimeLog + public interface IControlledRuntimeLog { /// /// Invoked when the specified state machine has been created. @@ -40,7 +40,7 @@ public interface IStateMachineRuntimeLog /// The id used to identify the send operation. /// Is the target state machine halted. void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted); + Event e, bool isTargetHalted); /// /// Invoked when the specified state machine raises an event. diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs index 7602b8afcb..ac91ff568e 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/JsonWriter.cs @@ -558,7 +558,7 @@ public JsonWriter() /// /// Enum representing the different log types the JSON error trace logs. /// Referenced from PCheckerLogTextFormatter.cs and PCheckerLogTextFormatter.cs - /// to see what those formatter logs. Check IStateMachineRuntimeLog.cs to see + /// to see what those formatter logs. Check IControlledRuntimeLog.cs to see /// each log types' description and when they are invoked. /// public enum LogType diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs index bedd74a389..fdaeb2e754 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/LogWriter.cs @@ -13,14 +13,14 @@ namespace PChecker.StateMachines.Logging { /// /// Manages the installed and all registered - /// objects. + /// objects. /// public sealed class LogWriter { /// /// The set of registered log writers. /// - private readonly HashSet Logs; + private readonly HashSet Logs; /// /// Used to log messages. @@ -37,7 +37,7 @@ public sealed class LogWriter /// internal LogWriter(CheckerConfiguration checkerConfiguration) { - Logs = new HashSet(); + Logs = new HashSet(); if (checkerConfiguration.IsVerbose) { @@ -95,13 +95,13 @@ public void LogExecuteAction(StateMachineId id, string handlingStateName, string /// The id used to identify the send operation. /// Is the target state machine halted. public void LogSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderState, - Event e, Guid opGroupId, bool isTargetHalted) + Event e, bool isTargetHalted) { if (Logs.Count > 0) { foreach (var log in Logs) { - log.OnSendEvent(targetStateMachineId, senderName, senderType, senderState, e, opGroupId, isTargetHalted); + log.OnSendEvent(targetStateMachineId, senderName, senderType, senderState, e, isTargetHalted); } } } @@ -520,7 +520,7 @@ internal void LogCompletion() /// if there are any. /// public IEnumerable GetLogsOfType() - where TStateMachineRuntimeLog : IStateMachineRuntimeLog => + where TStateMachineRuntimeLog : IControlledRuntimeLog => Logs.OfType(); /// @@ -579,9 +579,9 @@ private PCheckerLogTextFormatter GetOrCreateTextLog() } /// - /// Use this method to register an . + /// Use this method to register an . /// - internal void RegisterLog(IStateMachineRuntimeLog log) + internal void RegisterLog(IControlledRuntimeLog log) { if (log == null) { @@ -614,9 +614,9 @@ internal void RegisterLog(IStateMachineRuntimeLog log) } /// - /// Use this method to unregister a previously registered . + /// Use this method to unregister a previously registered . /// - internal void RemoveLog(IStateMachineRuntimeLog log) + internal void RemoveLog(IControlledRuntimeLog log) { if (log != null) { diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs index 36b6d72ed6..939d2ac41d 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs @@ -12,9 +12,9 @@ namespace PChecker.PRuntime { /// - /// This class implements IStateMachineRuntimeLog and generates log output in an XML format. + /// This class implements IControlledRuntimeLog and generates log output in an XML format. /// - public class PCheckerLogJsonFormatter : IStateMachineRuntimeLog + public class PCheckerLogJsonFormatter : IControlledRuntimeLog { /// /// Get or set the JsonWriter to write to. @@ -329,23 +329,21 @@ public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wa /// public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted) + Event e, bool isTargetHalted) { senderStateName = GetShortName(senderStateName); string eventName = GetEventNameWithPayload(e); - var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; var isHalted = isTargetHalted ? $" which has halted" : string.Empty; var sender = !string.IsNullOrEmpty(senderName) ? $"'{senderName}' in state '{senderStateName}'" : $"The runtime"; - var log = $"{sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}."; + var log = $"{sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}."; Writer.AddLogType(JsonWriter.LogType.SendEvent); Writer.LogDetails.Sender = !string.IsNullOrEmpty(senderName) ? senderName : "Runtime"; Writer.LogDetails.State = senderStateName; Writer.LogDetails.Event = GetShortName(e.GetType().Name); Writer.LogDetails.Target = targetStateMachineId.ToString(); - Writer.LogDetails.OpGroupId = opGroupId.ToString(); Writer.LogDetails.IsTargetHalted = isTargetHalted; Writer.LogDetails.Payload = GetEventPayloadInJson(e); Writer.AddLog(log); diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs index 96f8078f51..aea68c03ac 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs @@ -16,7 +16,7 @@ namespace PChecker.PRuntime /// /// Formatter for the runtime log. /// - public class PCheckerLogTextFormatter : IStateMachineRuntimeLog + public class PCheckerLogTextFormatter : IControlledRuntimeLog { /// /// Get or set the TextWriter to write to. @@ -249,14 +249,13 @@ public void OnMonitorRaiseEvent(string monitorType, string stateName, Event e) } /// - public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, Guid opGroupId, bool isTargetHalted) + public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, Event e, bool isTargetHalted) { senderStateName = GetShortName(senderStateName); var eventName = GetEventNameWithPayload(e); - var opGroupIdMsg = opGroupId != Guid.Empty ? $" (operation group '{opGroupId}')" : string.Empty; var isHalted = isTargetHalted ? $" which has halted" : string.Empty; var sender = !string.IsNullOrEmpty(senderName) ? $"'{senderName}' in state '{senderStateName}'" : $"The runtime"; - var text = $" {sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}{opGroupIdMsg}."; + var text = $" {sender} sent event '{eventName}' to '{targetStateMachineId}'{isHalted}."; Logger.WriteLine(text); } diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogXmlFormatter.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogXmlFormatter.cs index 148fc364c3..14fbd1dcac 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogXmlFormatter.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogXmlFormatter.cs @@ -10,9 +10,9 @@ namespace PChecker.StateMachines.Logging { /// - /// This class implements IStateMachineRuntimeLog and generates log output in an XML format. + /// This class implements IControlledRuntimeLog and generates log output in an XML format. /// - internal class PCheckerLogXmlFormatter : IStateMachineRuntimeLog + internal class PCheckerLogXmlFormatter : IControlledRuntimeLog { private readonly XmlWriter Writer; private bool Closed; @@ -292,7 +292,7 @@ public void OnReceiveEvent(StateMachineId id, string stateName, Event e, bool wa } public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName, - Event e, Guid opGroupId, bool isTargetHalted) + Event e, bool isTargetHalted) { if (Closed) { @@ -312,10 +312,6 @@ public void OnSendEvent(StateMachineId targetStateMachineId, string senderName, Writer.WriteAttributeString("senderState", senderStateName); Writer.WriteAttributeString("event", e.GetType().FullName); - if (opGroupId != Guid.Empty) - { - Writer.WriteAttributeString("event", opGroupId.ToString()); - } Writer.WriteAttributeString("isTargetHalted", isTargetHalted.ToString()); Writer.WriteEndElement(); diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/IStateMachineManager.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/IStateMachineManager.cs index a87b75bfd1..fb0e8b2ee7 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/IStateMachineManager.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/IStateMachineManager.cs @@ -16,12 +16,7 @@ internal interface IStateMachineManager /// True if the event handler of the state machine is running, else false. /// bool IsEventHandlerRunning { get; set; } - - /// - /// Id used to identify subsequent operations performed by the state machine. - /// - Guid OperationGroupId { get; set; } - + /// /// Returns the cached state of the state machine. /// @@ -30,12 +25,12 @@ internal interface IStateMachineManager /// /// Checks if the specified event is currently ignored. /// - bool IsEventIgnored(Event e, Guid opGroupId, EventInfo eventInfo); + bool IsEventIgnored(Event e, EventInfo eventInfo); /// /// Checks if the specified event is currently deferred. /// - bool IsEventDeferred(Event e, Guid opGroupId, EventInfo eventInfo); + bool IsEventDeferred(Event e, EventInfo eventInfo); /// /// Checks if a default handler is currently available. @@ -45,12 +40,12 @@ internal interface IStateMachineManager /// /// Notifies the state machine that an event has been enqueued. /// - void OnEnqueueEvent(Event e, Guid opGroupId, EventInfo eventInfo); + void OnEnqueueEvent(Event e, EventInfo eventInfo); /// /// Notifies the state machine that an event has been raised. /// - void OnRaiseEvent(Event e, Guid opGroupId, EventInfo eventInfo); + void OnRaiseEvent(Event e, EventInfo eventInfo); /// /// Notifies the state machine that it is waiting to receive an event of one of the specified types. @@ -60,18 +55,18 @@ internal interface IStateMachineManager /// /// Notifies the state machine that an event it was waiting to receive has been enqueued. /// - void OnReceiveEvent(Event e, Guid opGroupId, EventInfo eventInfo); + void OnReceiveEvent(Event e, EventInfo eventInfo); /// /// Notifies the state machine that an event it was waiting to receive was already in the /// event queue when the state machine invoked the receiving statement. /// - void OnReceiveEventWithoutWaiting(Event e, Guid opGroupId, EventInfo eventInfo); + void OnReceiveEventWithoutWaiting(Event e, EventInfo eventInfo); /// /// Notifies the state machine that an event has been dropped. /// - void OnDropEvent(Event e, Guid opGroupId, EventInfo eventInfo); + void OnDropEvent(Event e, EventInfo eventInfo); /// /// Asserts if the specified condition holds. diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/StateMachineManager.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/StateMachineManager.cs index f648fd050d..46a1de538f 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/StateMachineManager.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/Managers/StateMachineManager.cs @@ -27,9 +27,6 @@ internal sealed class StateMachineManager : IStateMachineManager /// public bool IsEventHandlerRunning { get; set; } - /// - public Guid OperationGroupId { get; set; } - /// /// Program counter used for state-caching. Distinguishes /// scheduling from non-deterministic choices. @@ -39,12 +36,11 @@ internal sealed class StateMachineManager : IStateMachineManager /// /// Initializes a new instance of the class. /// - internal StateMachineManager(ControlledRuntime runtime, StateMachine instance, Guid operationGroupId) + internal StateMachineManager(ControlledRuntime runtime, StateMachine instance) { Runtime = runtime; Instance = instance; IsEventHandlerRunning = true; - OperationGroupId = operationGroupId; ProgramCounter = 0; } @@ -62,12 +58,12 @@ public int GetCachedState() /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool IsEventIgnored(Event e, Guid opGroupId, EventInfo eventInfo) => + public bool IsEventIgnored(Event e, EventInfo eventInfo) => Instance.IsEventIgnoredInCurrentState(e); /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool IsEventDeferred(Event e, Guid opGroupId, EventInfo eventInfo) => + public bool IsEventDeferred(Event e, EventInfo eventInfo) => Instance.IsEventDeferredInCurrentState(e); /// @@ -76,12 +72,12 @@ public bool IsEventDeferred(Event e, Guid opGroupId, EventInfo eventInfo) => /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnEnqueueEvent(Event e, Guid opGroupId, EventInfo eventInfo) => + public void OnEnqueueEvent(Event e, EventInfo eventInfo) => Runtime.LogWriter.LogEnqueueEvent(Instance.Id, e); /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnRaiseEvent(Event e, Guid opGroupId, EventInfo eventInfo) => + public void OnRaiseEvent(Event e, EventInfo eventInfo) => Runtime.NotifyRaisedEvent(Instance, e, eventInfo); /// @@ -90,33 +86,21 @@ public void OnWaitEvent(IEnumerable eventTypes) => Runtime.NotifyWaitEvent(Instance, eventTypes); /// - public void OnReceiveEvent(Event e, Guid opGroupId, EventInfo eventInfo) + public void OnReceiveEvent(Event e, EventInfo eventInfo) { - if (opGroupId != Guid.Empty) - { - // Inherit the operation group id of the receiving operation, if it is non-empty. - OperationGroupId = opGroupId; - } - Runtime.NotifyReceivedEvent(Instance, e, eventInfo); } /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnReceiveEventWithoutWaiting(Event e, Guid opGroupId, EventInfo eventInfo) + public void OnReceiveEventWithoutWaiting(Event e, EventInfo eventInfo) { - if (opGroupId != Guid.Empty) - { - // Inherit the operation group id of the receiving operation, if it is non-empty. - OperationGroupId = opGroupId; - } - Runtime.NotifyReceivedEventWithoutWaiting(Instance, e, eventInfo); } /// [MethodImpl(MethodImplOptions.AggressiveInlining)] - public void OnDropEvent(Event e, Guid opGroupId, EventInfo eventInfo) + public void OnDropEvent(Event e, EventInfo eventInfo) { Runtime.TryHandleDroppedEvent(e, Instance.Id); } diff --git a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs index 5dda0c7fb5..20987657f8 100644 --- a/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs @@ -143,7 +143,7 @@ public abstract class StateMachine /// protected JsonWriter JsonLogger => Runtime.JsonLogger; - protected IPrtValue gotoPayload; + protected IPValue gotoPayload; public List creates = new List(); public string interfaceName; @@ -151,12 +151,12 @@ public abstract class StateMachine public PMachineValue self; public List sends = new List(); - protected virtual Event GetConstructorEvent(IPrtValue value) + protected virtual Event GetConstructorEvent(IPValue value) { throw new NotImplementedException(); } - public PMachineValue CreateInterface(StateMachine creator, IPrtValue payload = null) + public PMachineValue CreateInterface(StateMachine creator, IPValue payload = null) where T : PMachineValue { var createdInterface = PModule.linkMap[creator.interfaceName][typeof(T).Name]; @@ -169,29 +169,29 @@ public PMachineValue CreateInterface(StateMachine creator, IPrtValue payload } - public IPrtValue TryRandom(IPrtValue param) + public IPValue TryRandom(IPValue param) { switch (param) { - case PrtInt maxValue: + case PInt maxValue: { Assert(maxValue <= 10000, $"choose expects a parameter with at most 10000 choices, got {maxValue} choices instead."); - return (PrtInt)RandomInteger(maxValue); + return (PInt)RandomInteger(maxValue); } - case PrtSeq seq: + case PSeq seq: { Assert(seq.Any(), "Trying to choose from an empty sequence!"); Assert(seq.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {seq.Count} choices instead."); return seq[RandomInteger(seq.Count)]; } - case PrtSet set: + case PSet set: { Assert(set.Any(), "Trying to choose from an empty set!"); Assert(set.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {set.Count} choices instead."); return set.ElementAt(RandomInteger(set.Count)); } - case PrtMap map: + case PMap map: { Assert(map.Any(), "Trying to choose from an empty map!"); Assert(map.Keys.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {map.Keys.Count} choices instead."); @@ -227,7 +227,7 @@ public void Announce(Event ev, object payload = null) var oneArgConstructor = ev.GetType().GetConstructors().First(x => x.GetParameters().Length > 0); var @event = (Event)oneArgConstructor.Invoke(new[] { payload }); - var pText = payload == null ? "" : $" with payload {((IPrtValue)payload).ToEscapedString()}"; + var pText = payload == null ? "" : $" with payload {((IPValue)payload).ToEscapedString()}"; Logger.WriteLine($" '{Id}' announced event '{ev.GetType().Name}'{pText}."); @@ -237,7 +237,7 @@ public void Announce(Event ev, object payload = null) JsonLogger.LogDetails.Event = ev.GetType().Name; if (payload != null) { - JsonLogger.LogDetails.Payload = ((IPrtValue)payload).ToDict(); + JsonLogger.LogDetails.Payload = ((IPValue)payload).ToDict(); } JsonLogger.AddLog($"{Id} announced event {ev.GetType().Name}{pText}."); JsonLogger.AddToLogs(updateVcMap: true); @@ -494,24 +494,6 @@ private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, str return Task.CompletedTask; } - - /// - /// ID used to identify subsequent operations performed by this state machine. This value - /// is initially either or the specified - /// upon creation. This value is automatically set to the operation group id of the - /// last dequeue or receive operation, if it is not . This - /// value can also be manually set using the property. - /// - protected internal Guid OperationGroupId - { - get => Manager.OperationGroupId; - - set - { - Manager.OperationGroupId = value; - } - } - /// /// Creates a new state machine of the specified type and name, and with the specified @@ -523,8 +505,8 @@ protected internal Guid OperationGroupId /// Optional initialization event. /// Optional id that can be used to identify this operation. /// The unique state machine id. - protected StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null, Guid opGroupId = default) => - Runtime.CreateStateMachine(null, type, name, initialEvent, this, opGroupId); + protected StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null) => + Runtime.CreateStateMachine(null, type, name, initialEvent, this); /// @@ -533,7 +515,7 @@ protected StateMachineId CreateStateMachine(Type type, string name, Event initia /// The target. /// The event to send. /// Optional id that can be used to identify this operation. - public void SendEvent(PMachineValue target, Event ev, Guid opGroupId = default) + public void SendEvent(PMachineValue target, Event ev) { Assert(ev != null, "Machine cannot send a null event"); Assert(target != null, "Machine in send cannot be null"); @@ -542,7 +524,7 @@ public void SendEvent(PMachineValue target, Event ev, Guid opGroupId = default) Assert(target.Permissions.Contains(ev.GetType().Name), $"Event {ev.GetType().Name} is not in the permissions set of the target machine"); AnnounceInternal(ev); - Runtime.SendEvent(target.Id, ev, this, opGroupId); + Runtime.SendEvent(target.Id, ev, this); } /// @@ -593,13 +575,8 @@ internal async Task RunEventHandlerAsync() Event lastDequeuedEvent = null; while (CurrentStatus != Status.Halted && Runtime.IsRunning) { - (var status, var e, var opGroupId, var info) = Inbox.Dequeue(); - if (opGroupId != Guid.Empty) - { - // Inherit the operation group id of the dequeued operation, if it is non-empty. - Manager.OperationGroupId = opGroupId; - } - + (var status, var e, var info) = Inbox.Dequeue(); + if (status is DequeueStatus.Success) { // Notify the runtime for a new event to handle. This is only used @@ -896,14 +873,14 @@ public override int GetHashCode() /// /// Enqueues the specified event and its metadata. /// - internal EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info) + internal EnqueueStatus Enqueue(Event e, EventInfo info) { if (CurrentStatus is Status.Halted) { return EnqueueStatus.Dropped; } - return Inbox.Enqueue(e, opGroupId, info); + return Inbox.Enqueue(e, info); } /// @@ -988,7 +965,7 @@ public void RaiseEvent(Event e) /// An Assert is raised if you accidentally try and do two of these operations in a single action. /// /// Type of the state. - public void RaiseGotoStateEvent(IPrtValue payload = null) where S : State + public void RaiseGotoStateEvent(IPValue payload = null) where S : State { gotoPayload = payload; RaiseGotoStateEvent(typeof(S)); @@ -1230,12 +1207,12 @@ private Task ApplyEventHandlerTransitionAsync(Transition transition, Event e) else if (transition.TypeValue is Transition.Type.RaiseEvent) { PendingTransition = default; - Inbox.RaiseEvent(transition.Event, OperationGroupId); + Inbox.RaiseEvent(transition.Event); } else if (transition.TypeValue is Transition.Type.GotoState) { PendingTransition = default; - Inbox.RaiseEvent(new GotoStateEvent(transition.State), OperationGroupId); + Inbox.RaiseEvent(new GotoStateEvent(transition.State)); } else if (transition.TypeValue is Transition.Type.Halt) { @@ -1626,15 +1603,12 @@ private protected void ReportUnhandledException(Exception ex, string actionName) /// Defines the transition that is the /// result of executing an event handler. Transitions are created by using /// , and . - /// The Transition is processed by the Coyote runtime when + /// The Transition is processed by the ControlledRuntime when /// an event handling method of a StateMachine returns a Transition object. /// This means such a method can only do one such Transition per method call. /// If the method wants to do a conditional transition it can return /// Transition.None to indicate no transition is to be performed. /// - /// - /// See State machines for more information. - /// internal readonly struct Transition { /// @@ -1704,9 +1678,6 @@ public enum Type /// /// Abstract class representing a state. /// - /// - /// See State machines for more information. - /// public abstract class State { /// diff --git a/Src/PChecker/CheckerCore/PRuntime/Exceptions/PFrozenMutationException.cs b/Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/PFrozenMutationException.cs similarity index 100% rename from Src/PChecker/CheckerCore/PRuntime/Exceptions/PFrozenMutationException.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/PFrozenMutationException.cs diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/PInhabitsTypeException.cs b/Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/PInhabitsTypeException.cs new file mode 100644 index 0000000000..e2d3141b5f --- /dev/null +++ b/Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/PInhabitsTypeException.cs @@ -0,0 +1,19 @@ +using System; + +namespace PChecker.PRuntime.Exceptions +{ + public class PInhabitsTypeException : Exception + { + public PInhabitsTypeException() + { + } + + public PInhabitsTypeException(string message) : base(message) + { + } + + public PInhabitsTypeException(string message, Exception innerException) : base(message, innerException) + { + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs b/Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/UnknownNamedTupleFieldAccess.cs similarity index 100% rename from Src/PChecker/CheckerCore/PRuntime/Exceptions/UnknownNamedTupleFieldAccess.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/Exceptions/UnknownNamedTupleFieldAccess.cs diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/IPMutableValue.cs similarity index 60% rename from Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/IPMutableValue.cs index b8b3d2c153..8cdeafdb58 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/IPrtMutableValue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/IPMutableValue.cs @@ -1,6 +1,6 @@ namespace PChecker.PRuntime.Values { - public interface IPrtMutableValue : IPrtValue + public interface IPMutableValue : IPValue { void Freeze(); } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/IPrtValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/IPValue.cs similarity index 83% rename from Src/PChecker/CheckerCore/PRuntime/Values/IPrtValue.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/IPValue.cs index 6dbc411363..c33105d573 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/IPrtValue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/IPValue.cs @@ -2,9 +2,9 @@ namespace PChecker.PRuntime.Values { - public interface IPrtValue : IEquatable + public interface IPValue : IEquatable { - IPrtValue Clone(); + IPValue Clone(); /// /// Returns a string representation of this Value, such that strings are diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs b/Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs index 8e7860b537..30b697753b 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/MutabilityHelper.cs @@ -3,9 +3,9 @@ public static class MutabilityHelper { public static void EnsureFrozen(T value) - where T : IPrtValue + where T : IPValue { - if (value is IPrtMutableValue mutable) + if (value is IPMutableValue mutable) { mutable.Freeze(); } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtBool.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PBool.cs similarity index 54% rename from Src/PChecker/CheckerCore/PRuntime/Values/PrtBool.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PBool.cs index 9d80012eee..8b63bbfa7a 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtBool.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PBool.cs @@ -4,9 +4,9 @@ namespace PChecker.PRuntime.Values { [Serializable] - public readonly struct PrtBool : IPrtValue + public readonly struct PBool : IPValue { - public bool Equals(PrtBool other) + public bool Equals(PBool other) { return value == other.value; } @@ -18,7 +18,7 @@ public override bool Equals(object obj) return false; } - return obj is PrtBool other && Equals(other); + return obj is PBool other && Equals(other); } public override string ToString() @@ -34,99 +34,99 @@ public object ToDict() private readonly bool value; [MethodImpl(MethodImplOptions.AggressiveInlining)] - private PrtBool(bool value) + private PBool(bool value) { this.value = value; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public IPrtValue Clone() + public IPValue Clone() { return this; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator bool(in PrtBool val) + public static implicit operator bool(in PBool val) { return val.value; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtBool(bool val) + public static implicit operator PBool(bool val) { - return new PrtBool(val); + return new PBool(val); } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator true(in PrtBool pValue) + public static bool operator true(in PBool pValue) { return pValue; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator false(in PrtBool pValue) + public static bool operator false(in PBool pValue) { return !pValue; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator !(in PrtBool pValue) + public static PBool operator !(in PBool pValue) { - return new PrtBool(!pValue.value); + return new PBool(!pValue.value); } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator &(in PrtBool pValue1, in PrtBool pValue2) + public static PBool operator &(in PBool pValue1, in PBool pValue2) { - return new PrtBool(pValue1.value && pValue2.value); + return new PBool(pValue1.value && pValue2.value); } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator |(in PrtBool pValue1, in PrtBool pValue2) + public static PBool operator |(in PBool pValue1, in PBool pValue2) { - return new PrtBool(pValue1.value || pValue2.value); + return new PBool(pValue1.value || pValue2.value); } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator ==(in PrtBool pValue1, in PrtBool pValue2) + public static bool operator ==(in PBool pValue1, in PBool pValue2) { return Equals(pValue1, pValue2); } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator !=(in PrtBool pValue1, in PrtBool pValue2) + public static bool operator !=(in PBool pValue1, in PBool pValue2) { return !Equals(pValue1, pValue2); } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator ==(in PrtBool pValue1, in IPrtValue pValue2) + public static bool operator ==(in PBool pValue1, in IPValue pValue2) { - return pValue2 is PrtBool prtBool && pValue1.value == prtBool.value; + return pValue2 is PBool pBool && pValue1.value == pBool.value; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator !=(in PrtBool pValue1, in IPrtValue pValue2) + public static bool operator !=(in PBool pValue1, in IPValue pValue2) { - return pValue2 is PrtBool prtBool && pValue1.value != prtBool.value; + return pValue2 is PBool pBool && pValue1.value != pBool.value; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator ==(in IPrtValue pValue1, in PrtBool pValue2) + public static bool operator ==(in IPValue pValue1, in PBool pValue2) { - return pValue1 is PrtBool prtBool && pValue2.value == prtBool.value; + return pValue1 is PBool pBool && pValue2.value == pBool.value; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator !=(in IPrtValue pValue1, in PrtBool pValue2) + public static bool operator !=(in IPValue pValue1, in PBool pValue2) { - return pValue1 is PrtBool prtBool && pValue2.value != prtBool.value; + return pValue1 is PBool pBool && pValue2.value != pBool.value; } [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool Equals(IPrtValue obj) + public bool Equals(IPValue obj) { - return obj is PrtBool other && value == other.value; + return obj is PBool other && value == other.value; } public override int GetHashCode() diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtEnum.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PEnum.cs similarity index 77% rename from Src/PChecker/CheckerCore/PRuntime/Values/PrtEnum.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PEnum.cs index b73a11dd23..6028da1f9a 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtEnum.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PEnum.cs @@ -3,11 +3,11 @@ namespace PChecker.PRuntime.Values { - public class PrtEnum + public class PEnum { - private static readonly Dictionary enumElements = new Dictionary(); + private static readonly Dictionary enumElements = new Dictionary(); - public static PrtInt Get(string name) + public static PInt Get(string name) { return enumElements[name]; } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PFloat.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PFloat.cs new file mode 100644 index 0000000000..0c7c3cc3b4 --- /dev/null +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PFloat.cs @@ -0,0 +1,147 @@ +using System; +using System.Runtime.CompilerServices; + +namespace PChecker.PRuntime.Values +{ + [Serializable] + public readonly struct PFloat : IPValue + { + private readonly double value; + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public PFloat(double value) + { + this.value = value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public IPValue Clone() + { + return this; + } + + public override string ToString() + { + return value.ToString(); + } + + public object ToDict() + { + return value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public bool Equals(IPValue other) + { + return other is PFloat f && value == f.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public override bool Equals(object val) + { + return val is PFloat other && Equals(value, other.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public override int GetHashCode() + { + return value.GetHashCode(); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator double(in PFloat val) + { + return val.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PFloat(float val) + { + return new PFloat(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PFloat(double val) + { + return new PFloat(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PFloat(PInt val) + { + return new PFloat(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PFloat operator +(in PFloat pFloat1, in PFloat pFloat2) + { + return new PFloat(pFloat1.value + pFloat2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PFloat operator -(in PFloat pFloat1, in PFloat pFloat2) + { + return new PFloat(pFloat1.value - pFloat2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PFloat operator *(in PFloat pFloat1, in PFloat pFloat2) + { + return new PFloat(pFloat1.value * pFloat2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PFloat operator /(in PFloat pFloat1, in PFloat pFloat2) + { + return new PFloat(pFloat1.value / pFloat2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <(in PFloat pFloat1, in PFloat pFloat2) + { + return pFloat1.value < pFloat2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >(in PFloat pFloat1, in PFloat pFloat2) + { + return pFloat1.value > pFloat2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <=(in PFloat pFloat1, in PFloat pFloat2) + { + return pFloat1.value <= pFloat2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >=(in PFloat pFloat1, in PFloat pFloat2) + { + return pFloat1.value >= pFloat2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator ==(in PFloat pFloat1, in PFloat pFloat2) + { + return Equals(pFloat1.value, pFloat2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator !=(in PFloat pFloat1, in PFloat pFloat2) + { + return Equals(pFloat1.value, pFloat2.value) == false; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PFloat operator +(in PFloat pFloat) + { + return new PFloat(+pFloat.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PFloat operator -(in PFloat pFloat) + { + return new PFloat(-pFloat.value); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PInt.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PInt.cs new file mode 100644 index 0000000000..8a6643d183 --- /dev/null +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PInt.cs @@ -0,0 +1,185 @@ +using System; +using System.Runtime.CompilerServices; + +namespace PChecker.PRuntime.Values +{ + [Serializable] + public readonly struct PInt : IPValue + { + private readonly long value; + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public PInt(long value) + { + this.value = value; + } + + public bool Equals(IPValue other) + { + return other is PInt i && value == i.value; + } + + public IPValue Clone() + { + return this; + } + + public override bool Equals(object val) + { + return val is PInt other && Equals(value, other.value); + } + + public override int GetHashCode() + { + return value.GetHashCode(); + } + + public override string ToString() + { + return value.ToString(); + } + + public object ToDict() + { + return value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PInt(byte val) + { + return new PInt(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PInt(short val) + { + return new PInt(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PInt(int val) + { + return new PInt(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PInt(long val) + { + return new PInt(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PInt(in PFloat val) + { + return new PInt((long)val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator int(in PInt val) + { + return (int)val.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator long(in PInt val) + { + return val.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PInt operator +(in PInt pInt1, in PInt pInt2) + { + return new PInt(pInt1.value + pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PInt operator -(in PInt pInt1, in PInt pInt2) + { + return new PInt(pInt1.value - pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PInt operator *(in PInt pInt1, in PInt pInt2) + { + return new PInt(pInt1.value * pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PInt operator /(in PInt pInt1, in PInt pInt2) + { + return new PInt(pInt1.value / pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <(in PInt pInt1, in PInt pInt2) + { + return pInt1.value < pInt2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >(in PInt pInt1, in PInt pInt2) + { + return pInt1.value > pInt2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <=(in PInt pInt1, in PInt pInt2) + { + return pInt1.value <= pInt2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >=(in PInt pInt1, in PInt pInt2) + { + return pInt1.value >= pInt2.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator ==(in PInt pInt1, in PInt pInt2) + { + return Equals(pInt1.value, pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator ==(in IPValue pInt1, in PInt pInt2) + { + return pInt1 is PInt int1 && Equals(int1.value, pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator !=(in IPValue pInt1, in PInt pInt2) + { + return pInt1 is PInt int1 && !Equals(int1.value, pInt2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator ==(in PInt pInt1, in IPValue pInt2) + { + return pInt2 is PInt int2 && Equals(pInt1.value, int2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator !=(in PInt pInt1, in IPValue pInt2) + { + return pInt2 is PInt int2 && !Equals(pInt1.value, int2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator !=(in PInt pInt1, in PInt pInt2) + { + return Equals(pInt1.value, pInt2.value) == false; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PInt operator +(in PInt pInt) + { + return new PInt(+pInt.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PInt operator -(in PInt pInt) + { + return new PInt(-pInt.value); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs index 624ee4a321..6d41b3cf83 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PMachineValue.cs @@ -11,7 +11,7 @@ public I_Main(StateMachineId machine, List permissions) : base(machine, } } - public class PMachineValue : IPrtValue + public class PMachineValue : IPValue { public PMachineValue(StateMachineId machine, List permissions) { @@ -28,7 +28,7 @@ public PMachineValue(PMachineValue mValue) public StateMachineId Id { get; } public List Permissions { get; } - public bool Equals(IPrtValue other) + public bool Equals(IPValue other) { return other is PMachineValue machine && Equals(Id, machine.Id); } @@ -38,7 +38,7 @@ public override int GetHashCode() return Id.GetHashCode(); } - public IPrtValue Clone() + public IPValue Clone() { return new PMachineValue(Id, new List(Permissions)); } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtMap.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PMap.cs similarity index 75% rename from Src/PChecker/CheckerCore/PRuntime/Values/PrtMap.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PMap.cs index dff333d165..30a1a9becc 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtMap.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PMap.cs @@ -6,20 +6,20 @@ namespace PChecker.PRuntime.Values { - public sealed class PrtMap : IPrtMutableValue, IDictionary + public sealed class PMap : IPMutableValue, IDictionary { - private readonly IDictionary map = new Dictionary(); + private readonly IDictionary map = new Dictionary(); private int hashCode; private bool isDirty; private bool isFrozen; - public PrtMap() + public PMap() { hashCode = ComputeHashCode(); } - public PrtMap(IDictionary map) + public PMap(IDictionary map) { this.map = map; hashCode = ComputeHashCode(); @@ -39,7 +39,7 @@ private bool IsDirty } } - public IEnumerator> GetEnumerator() + public IEnumerator> GetEnumerator() { return map.GetEnumerator(); } @@ -49,7 +49,7 @@ IEnumerator IEnumerable.GetEnumerator() return GetEnumerator(); } - public void Add(KeyValuePair item) + public void Add(KeyValuePair item) { MutabilityHelper.EnsureFrozen(item.Key); map.Add(item.Key?.Clone(), item.Value?.Clone()); @@ -62,12 +62,12 @@ public void Clear() IsDirty = true; } - public bool Contains(KeyValuePair item) + public bool Contains(KeyValuePair item) { return map.Contains(item); } - public void CopyTo(KeyValuePair[] array, int arrayIndex) + public void CopyTo(KeyValuePair[] array, int arrayIndex) { foreach (var kv in map) { @@ -75,7 +75,7 @@ public void CopyTo(KeyValuePair[] array, int arrayIndex) } } - public bool Remove(KeyValuePair item) + public bool Remove(KeyValuePair item) { var removed = map.Remove(item.Key); IsDirty = true; @@ -85,31 +85,31 @@ public bool Remove(KeyValuePair item) public int Count => map.Count; public bool IsReadOnly => false; - public void Add(IPrtValue key, IPrtValue value) + public void Add(IPValue key, IPValue value) { MutabilityHelper.EnsureFrozen(key); map.Add(key?.Clone(), value?.Clone()); IsDirty = true; } - public bool ContainsKey(IPrtValue key) + public bool ContainsKey(IPValue key) { return map.ContainsKey(key); } - public bool Remove(IPrtValue key) + public bool Remove(IPValue key) { var removed = map.Remove(key); IsDirty = true; return removed; } - public bool TryGetValue(IPrtValue key, out IPrtValue value) + public bool TryGetValue(IPValue key, out IPValue value) { return map.TryGetValue(key, out value); } - public IPrtValue this[IPrtValue key] + public IPValue this[IPValue key] { get => map[key]; set @@ -120,20 +120,20 @@ public IPrtValue this[IPrtValue key] } } - public ICollection Keys => map.Keys; - public ICollection Values => map.Values; + public ICollection Keys => map.Keys; + public ICollection Values => map.Values; - public bool Equals(IPrtValue other) + public bool Equals(IPValue other) { - return other is PrtMap otherMap + return other is PMap otherMap && !map.Keys.Except(otherMap.map.Keys).Any() && !otherMap.map.Keys.Except(map.Keys).Any() - && map.All(kv => PrtValues.SafeEquals(otherMap.map[kv.Key], kv.Value)); + && map.All(kv => PValues.SafeEquals(otherMap.map[kv.Key], kv.Value)); } - public IPrtValue Clone() + public IPValue Clone() { - return new PrtMap(map.ToDictionary( + return new PMap(map.ToDictionary( kv => kv.Key?.Clone(), kv => kv.Value?.Clone())); } @@ -148,14 +148,14 @@ public void Freeze() isFrozen = true; } - public PrtSeq CloneKeys() + public PSeq CloneKeys() { - return new PrtSeq(map.Keys.Select(v => v.Clone())); + return new PSeq(map.Keys.Select(v => v.Clone())); } - public PrtSeq CloneValues() + public PSeq CloneValues() { - return new PrtSeq(map.Values.Select(v => v.Clone())); + return new PSeq(map.Values.Select(v => v.Clone())); } public override int GetHashCode() diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtSeq.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PSeq.cs similarity index 82% rename from Src/PChecker/CheckerCore/PRuntime/Values/PrtSeq.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PSeq.cs index 943f9b9994..308d88c87e 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtSeq.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PSeq.cs @@ -6,20 +6,20 @@ namespace PChecker.PRuntime.Values { - public sealed class PrtSeq : IPrtMutableValue, IReadOnlyList + public sealed class PSeq : IPMutableValue, IReadOnlyList { - private readonly List values = new List(); + private readonly List values = new List(); private int hashCode; private bool isDirty; private bool isFrozen; - public PrtSeq() + public PSeq() { hashCode = ComputeHashCode(); } - public PrtSeq(IEnumerable values) + public PSeq(IEnumerable values) { this.values = values.ToList(); hashCode = ComputeHashCode(); @@ -49,17 +49,17 @@ public void Freeze() isFrozen = true; } - public IPrtValue Clone() + public IPValue Clone() { - return new PrtSeq(values.Select(item => item?.Clone())); + return new PSeq(values.Select(item => item?.Clone())); } - public bool Equals(IPrtValue other) + public bool Equals(IPValue other) { - return other is PrtSeq otherValue && Equals(otherValue); + return other is PSeq otherValue && Equals(otherValue); } - public IEnumerator GetEnumerator() + public IEnumerator GetEnumerator() { return values.GetEnumerator(); } @@ -71,7 +71,7 @@ IEnumerator IEnumerable.GetEnumerator() public int Count => values.Count; - public IPrtValue this[int index] + public IPValue this[int index] { get => values[index]; set @@ -90,13 +90,13 @@ private int ComputeHashCode() return HashHelper.ComputeHash(values); } - public void Add(IPrtValue item) + public void Add(IPValue item) { IsDirty = true; values.Add(item?.Clone()); } - public void Insert(int index, IPrtValue item) + public void Insert(int index, IPValue item) { IsDirty = true; values.Insert(index, item?.Clone()); @@ -108,12 +108,12 @@ public void RemoveAt(int index) values.RemoveAt(index); } - public bool Contains(IPrtValue item) + public bool Contains(IPValue item) { return values.Contains(item); } - private bool Equals(PrtSeq other) + private bool Equals(PSeq other) { return other != null && values.SequenceEqual(other.values); } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PSet.cs similarity index 74% rename from Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PSet.cs index 474dc47c4a..1d9f9e9fe0 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PSet.cs @@ -7,20 +7,20 @@ namespace PChecker.PRuntime.Values { - public sealed class PrtSet : IPrtMutableValue, IReadOnlyList, ICollection + public sealed class PSet : IPMutableValue, IReadOnlyList, ICollection { - private readonly ISet set = new HashSet(); + private readonly ISet set = new HashSet(); private int hashCode; private bool isDirty; private bool isFrozen; - public PrtSet() + public PSet() { hashCode = ComputeHashCode(); } - public PrtSet(ISet set) + public PSet(ISet set) { this.set = set; hashCode = ComputeHashCode(); @@ -50,7 +50,7 @@ public override int GetHashCode() return hashCode; } - public IEnumerator GetEnumerator() + public IEnumerator GetEnumerator() { return set.GetEnumerator(); } @@ -60,7 +60,7 @@ IEnumerator IEnumerable.GetEnumerator() return GetEnumerator(); } - public bool Add(IPrtValue item) + public bool Add(IPValue item) { MutabilityHelper.EnsureFrozen(item); IsDirty = true; @@ -73,12 +73,12 @@ public void Clear() IsDirty = true; } - public bool Contains(IPrtValue item) + public bool Contains(IPValue item) { return set.Contains(item); } - public bool Remove(IPrtValue item) + public bool Remove(IPValue item) { var removed = set.Remove(item); IsDirty = true; @@ -88,15 +88,15 @@ public bool Remove(IPrtValue item) public int Count => set.Count; public bool IsReadOnly => false; - public bool Equals(IPrtValue other) + public bool Equals(IPValue other) { - return other is PrtSet otherSet + return other is PSet otherSet && set.SetEquals(otherSet.set); } - public IPrtValue Clone() + public IPValue Clone() { - var clone = new PrtSet(new HashSet()); + var clone = new PSet(new HashSet()); foreach (var item in set) clone.Add(item.Clone()); return clone; } @@ -154,67 +154,67 @@ public object ToDict() return set.Select(value => value == null ? null : value.ToDict()).ToList(); } - public IPrtValue this[int index] + public IPValue this[int index] { get => set.ElementAt(index); set => throw new Exception("Setting set elements using indexing is not allowed!"); } - public void UnionWith(IEnumerable other) + public void UnionWith(IEnumerable other) { set.UnionWith(other.Select(i => i.Clone())); } - public void IntersectWith(IEnumerable other) + public void IntersectWith(IEnumerable other) { set.IntersectWith(other); } - public void ExceptWith(IEnumerable other) + public void ExceptWith(IEnumerable other) { set.ExceptWith(other); } - public void SymmetricExceptWith(IEnumerable other) + public void SymmetricExceptWith(IEnumerable other) { set.SymmetricExceptWith(other); } - public bool IsSubsetOf(IEnumerable other) + public bool IsSubsetOf(IEnumerable other) { return set.IsSubsetOf(other); } - public bool IsSupersetOf(IEnumerable other) + public bool IsSupersetOf(IEnumerable other) { return set.IsSupersetOf(other); } - public bool IsProperSupersetOf(IEnumerable other) + public bool IsProperSupersetOf(IEnumerable other) { return set.IsProperSupersetOf(other); } - public bool IsProperSubsetOf(IEnumerable other) + public bool IsProperSubsetOf(IEnumerable other) { return set.IsProperSubsetOf(other); } - public bool Overlaps(IEnumerable other) + public bool Overlaps(IEnumerable other) { return set.Overlaps(other); } - public bool SetEquals(IEnumerable other) + public bool SetEquals(IEnumerable other) { return set.SetEquals(other); } - void ICollection.Add(IPrtValue item) + void ICollection.Add(IPValue item) { set.Add(item); } - public void CopyTo(IPrtValue[] array, int arrayIndex) + public void CopyTo(IPValue[] array, int arrayIndex) { set.CopyTo(array, arrayIndex); } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PString.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PString.cs new file mode 100644 index 0000000000..4c6737db8a --- /dev/null +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PString.cs @@ -0,0 +1,197 @@ +using System; +using System.Runtime.CompilerServices; + +namespace PChecker.PRuntime.Values +{ + [Serializable] + public readonly struct PString : IPValue + { + public bool Equals(PString other) + { + return string.Equals(value, other.value); + } + + public override bool Equals(object obj) + { + if (ReferenceEquals(null, obj)) + { + return false; + } + + return obj is PString other && Equals(other); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public IPValue Clone() + { + return this; + } + + private readonly string value; + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator PString(string val) + { + return new PString(val); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static implicit operator string(PString val) + { + return val.value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + private PString(string value) + { + this.value = value; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PString operator +(in PString pString1, in PString pString2) + { + return new PString(pString1.value + pString2.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static bool operator ==(in PString pValue1, in PString pValue2) + { + return Equals(pValue1, pValue2); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static bool operator !=(in PString pValue1, in PString pValue2) + { + return !Equals(pValue1, pValue2); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static bool operator ==(in PString pValue1, in IPValue pValue2) + { + return pValue2 is PString pString && string.Equals(pValue1.value, pString.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static bool operator !=(in PString pValue1, in IPValue pValue2) + { + return pValue2 is PString pString && !string.Equals(pValue1.value, pString.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static bool operator ==(in IPValue pValue1, in PString pValue2) + { + return pValue1 is PString pString && string.Equals(pValue2.value, pString.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static bool operator !=(in IPValue pValue1, in PString pValue2) + { + return pValue1 is PString pString && !string.Equals(pValue2.value, pString.value); + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <(in PString pString1, in PString pString2) + { + return string.Compare(pString1.value, pString2.value) == -1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <(in IPValue pValue1, in PString pValue2) + { + return pValue1 is PString pString && string.Compare(pString.value, pValue2.value) == -1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <(in PString pValue1, in IPValue pValue2) + { + return pValue2 is PString pString && string.Compare(pString.value, pValue1.value) == -1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >(in PString pString1, in PString pString2) + { + return string.Compare(pString1.value, pString2.value) == 1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >(in IPValue pValue1, in PString pValue2) + { + return pValue1 is PString pString && string.Compare(pString.value, pValue2.value) == 1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >(in PString pValue1, in IPValue pValue2) + { + return pValue2 is PString pString && string.Compare(pString.value, pValue1.value) == 1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <=(in PString pString1, in PString pString2) + { + return string.Compare(pString1.value, pString2.value) != 1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <=(in IPValue pValue1, in PString pValue2) + { + return pValue1 is PString pString && string.Compare(pString.value, pValue2.value) != 1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator <=(in PString pValue1, in IPValue pValue2) + { + return pValue2 is PString pString && string.Compare(pString.value, pValue1.value) != 1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >=(in PString pString1, in PString pString2) + { + return string.Compare(pString1.value, pString2.value) != -1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >=(in IPValue pValue1, in PString pValue2) + { + return pValue1 is PString pString && string.Compare(pString.value, pValue2.value) != -1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public static PBool operator >=(in PString pValue1, in IPValue pValue2) + { + return pValue2 is PString pString && string.Compare(pString.value, pValue1.value) != -1; + } + + [MethodImpl(MethodImplOptions.AggressiveInlining)] + public bool Equals(IPValue obj) + { + return obj is PString other && string.Equals(value, other.value); + } + + public override int GetHashCode() + { + return value.GetHashCode(); + } + + public override string ToString() + { + return value; + } + + /// + /// Like ToString, but emits a representation of a string literal, surrounded by double-quotes, + /// and where all interior double-quotes are escaped. + /// + /// + public string ToEscapedString() + { + var v = value ?? ""; + return $"\"{v.Replace("\"", "\\\"")}\""; + } + + + public object ToDict() + { + return ToString(); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtTuple.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PTuple.cs similarity index 80% rename from Src/PChecker/CheckerCore/PRuntime/Values/PrtTuple.cs rename to Src/PChecker/CheckerCore/PRuntime/Values/PTuple.cs index a43d53c138..67c9cf9fa9 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtTuple.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PTuple.cs @@ -6,18 +6,18 @@ namespace PChecker.PRuntime.Values { [Serializable] - public class PrtTuple : IPrtValue + public class PTuple : IPValue { - public readonly List fieldValues; + public readonly List fieldValues; - public PrtTuple() + public PTuple() { - fieldValues = new List(); + fieldValues = new List(); } - public PrtTuple(params IPrtValue[] elems) + public PTuple(params IPValue[] elems) { - fieldValues = new List(); + fieldValues = new List(); if (elems == null || elems.Length == 1) { fieldValues.Add(elems?.First()); @@ -31,15 +31,15 @@ public PrtTuple(params IPrtValue[] elems) } } - public IPrtValue this[int key] + public IPValue this[int key] { get => fieldValues[key]; set => fieldValues[key] = value; } - public IPrtValue Clone() + public IPValue Clone() { - var clone = new PrtTuple(); + var clone = new PTuple(); foreach (var val in fieldValues) { clone.fieldValues.Add(val?.Clone()); @@ -48,14 +48,14 @@ public IPrtValue Clone() return clone; } - public bool Equals(IPrtValue val) + public bool Equals(IPValue val) { - if (val is PrtNamedTuple) + if (val is PNamedTuple) { return false; } - var tupValue = val as PrtTuple; + var tupValue = val as PTuple; if (tupValue == null) { return false; @@ -68,7 +68,7 @@ public bool Equals(IPrtValue val) for (var i = 0; i < fieldValues.Count; i++) { - if (!PrtValues.SafeEquals(fieldValues[i], tupValue.fieldValues[i])) + if (!PValues.SafeEquals(fieldValues[i], tupValue.fieldValues[i])) { return false; } @@ -77,7 +77,7 @@ public bool Equals(IPrtValue val) return true; } - public void Update(int index, IPrtValue val) + public void Update(int index, IPValue val) { fieldValues[index] = val; } @@ -115,23 +115,23 @@ public object ToDict() } [Serializable] - public class PrtNamedTuple : IPrtValue + public class PNamedTuple : IPValue { - public readonly List fieldValues; + public readonly List fieldValues; public List fieldNames; - public PrtNamedTuple() + public PNamedTuple() { fieldNames = new List(); - fieldValues = new List(); + fieldValues = new List(); } - public PrtNamedTuple(string[] _fieldNames, params IPrtValue[] _fieldValues) + public PNamedTuple(string[] _fieldNames, params IPValue[] _fieldValues) { fieldNames = _fieldNames.ToList(); if (_fieldValues == null || _fieldValues.Length == 1) { - fieldValues = new List(); + fieldValues = new List(); fieldValues.Add(_fieldValues?.First()); } @@ -141,7 +141,7 @@ public PrtNamedTuple(string[] _fieldNames, params IPrtValue[] _fieldValues) } } - public IPrtValue this[string name] + public IPValue this[string name] { get { @@ -163,9 +163,9 @@ public IPrtValue this[string name] } } - public IPrtValue Clone() + public IPValue Clone() { - var clone = new PrtNamedTuple(); + var clone = new PNamedTuple(); foreach (var name in fieldNames) { clone.fieldNames.Add(name); @@ -179,9 +179,9 @@ public IPrtValue Clone() return clone; } - public bool Equals(IPrtValue val) + public bool Equals(IPValue val) { - if (!(val is PrtNamedTuple tup)) + if (!(val is PNamedTuple tup)) { return false; } @@ -198,7 +198,7 @@ public bool Equals(IPrtValue val) return false; } - if (!PrtValues.SafeEquals(fieldValues[i], tup.fieldValues[i])) + if (!PValues.SafeEquals(fieldValues[i], tup.fieldValues[i])) { return false; } diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PValues.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PValues.cs new file mode 100644 index 0000000000..8ad75e0781 --- /dev/null +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PValues.cs @@ -0,0 +1,56 @@ +using PChecker.PRuntime.Values; + +namespace PChecker.PRuntime +{ + public static class PValues + { + public static PBool Box(bool value) + { + return value; + } + + public static PInt Box(long value) + { + return new PInt(value); + } + + public static PInt Box(int value) + { + return new PInt(value); + } + + public static PInt Box(short value) + { + return new PInt(value); + } + + public static PInt Box(byte value) + { + return new PInt(value); + } + + public static PFloat Box(double value) + { + return new PFloat(value); + } + + public static PFloat Box(float value) + { + return new PFloat(value); + } + + public static PBool SafeEquals(IPValue val1, IPValue val2) + { + return ReferenceEquals(val1, val2) || val1 != null && val1.Equals(val2); + } + + public static IPValue PCastValue(IPValue value, PType type) + { + //todo: Needs to be fixed for better error message + /*if (!PInhabitsType(value, type)) + throw new PInhabitsTypeException( + $"value {value.ToString()} is not a member of type {type.ToString()}");*/ + return value.Clone(); + } + } +} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtFloat.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtFloat.cs deleted file mode 100644 index d46e38daa7..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtFloat.cs +++ /dev/null @@ -1,147 +0,0 @@ -using System; -using System.Runtime.CompilerServices; - -namespace PChecker.PRuntime.Values -{ - [Serializable] - public readonly struct PrtFloat : IPrtValue - { - private readonly double value; - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public PrtFloat(double value) - { - this.value = value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public IPrtValue Clone() - { - return this; - } - - public override string ToString() - { - return value.ToString(); - } - - public object ToDict() - { - return value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool Equals(IPrtValue other) - { - return other is PrtFloat f && value == f.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public override bool Equals(object val) - { - return val is PrtFloat other && Equals(value, other.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public override int GetHashCode() - { - return value.GetHashCode(); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator double(in PrtFloat val) - { - return val.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtFloat(float val) - { - return new PrtFloat(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtFloat(double val) - { - return new PrtFloat(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtFloat(PrtInt val) - { - return new PrtFloat(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtFloat operator +(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return new PrtFloat(prtFloat1.value + prtFloat2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtFloat operator -(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return new PrtFloat(prtFloat1.value - prtFloat2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtFloat operator *(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return new PrtFloat(prtFloat1.value * prtFloat2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtFloat operator /(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return new PrtFloat(prtFloat1.value / prtFloat2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return prtFloat1.value < prtFloat2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return prtFloat1.value > prtFloat2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <=(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return prtFloat1.value <= prtFloat2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >=(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return prtFloat1.value >= prtFloat2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator ==(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return Equals(prtFloat1.value, prtFloat2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator !=(in PrtFloat prtFloat1, in PrtFloat prtFloat2) - { - return Equals(prtFloat1.value, prtFloat2.value) == false; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtFloat operator +(in PrtFloat prtFloat) - { - return new PrtFloat(+prtFloat.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtFloat operator -(in PrtFloat prtFloat) - { - return new PrtFloat(-prtFloat.value); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtInt.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtInt.cs deleted file mode 100644 index f381ec8cd6..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtInt.cs +++ /dev/null @@ -1,185 +0,0 @@ -using System; -using System.Runtime.CompilerServices; - -namespace PChecker.PRuntime.Values -{ - [Serializable] - public readonly struct PrtInt : IPrtValue - { - private readonly long value; - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public PrtInt(long value) - { - this.value = value; - } - - public bool Equals(IPrtValue other) - { - return other is PrtInt i && value == i.value; - } - - public IPrtValue Clone() - { - return this; - } - - public override bool Equals(object val) - { - return val is PrtInt other && Equals(value, other.value); - } - - public override int GetHashCode() - { - return value.GetHashCode(); - } - - public override string ToString() - { - return value.ToString(); - } - - public object ToDict() - { - return value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtInt(byte val) - { - return new PrtInt(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtInt(short val) - { - return new PrtInt(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtInt(int val) - { - return new PrtInt(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtInt(long val) - { - return new PrtInt(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtInt(in PrtFloat val) - { - return new PrtInt((long)val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator int(in PrtInt val) - { - return (int)val.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator long(in PrtInt val) - { - return val.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtInt operator +(in PrtInt prtInt1, in PrtInt prtInt2) - { - return new PrtInt(prtInt1.value + prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtInt operator -(in PrtInt prtInt1, in PrtInt prtInt2) - { - return new PrtInt(prtInt1.value - prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtInt operator *(in PrtInt prtInt1, in PrtInt prtInt2) - { - return new PrtInt(prtInt1.value * prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtInt operator /(in PrtInt prtInt1, in PrtInt prtInt2) - { - return new PrtInt(prtInt1.value / prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <(in PrtInt prtInt1, in PrtInt prtInt2) - { - return prtInt1.value < prtInt2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >(in PrtInt prtInt1, in PrtInt prtInt2) - { - return prtInt1.value > prtInt2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <=(in PrtInt prtInt1, in PrtInt prtInt2) - { - return prtInt1.value <= prtInt2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >=(in PrtInt prtInt1, in PrtInt prtInt2) - { - return prtInt1.value >= prtInt2.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator ==(in PrtInt prtInt1, in PrtInt prtInt2) - { - return Equals(prtInt1.value, prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator ==(in IPrtValue prtInt1, in PrtInt prtInt2) - { - return prtInt1 is PrtInt int1 && Equals(int1.value, prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator !=(in IPrtValue prtInt1, in PrtInt prtInt2) - { - return prtInt1 is PrtInt int1 && !Equals(int1.value, prtInt2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator ==(in PrtInt prtInt1, in IPrtValue prtInt2) - { - return prtInt2 is PrtInt int2 && Equals(prtInt1.value, int2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator !=(in PrtInt prtInt1, in IPrtValue prtInt2) - { - return prtInt2 is PrtInt int2 && !Equals(prtInt1.value, int2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator !=(in PrtInt prtInt1, in PrtInt prtInt2) - { - return Equals(prtInt1.value, prtInt2.value) == false; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtInt operator +(in PrtInt prtInt) - { - return new PrtInt(+prtInt.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtInt operator -(in PrtInt prtInt) - { - return new PrtInt(-prtInt.value); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtString.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtString.cs deleted file mode 100644 index 92ef3fcaaf..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtString.cs +++ /dev/null @@ -1,197 +0,0 @@ -using System; -using System.Runtime.CompilerServices; - -namespace PChecker.PRuntime.Values -{ - [Serializable] - public readonly struct PrtString : IPrtValue - { - public bool Equals(PrtString other) - { - return string.Equals(value, other.value); - } - - public override bool Equals(object obj) - { - if (ReferenceEquals(null, obj)) - { - return false; - } - - return obj is PrtString other && Equals(other); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public IPrtValue Clone() - { - return this; - } - - private readonly string value; - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator PrtString(string val) - { - return new PrtString(val); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static implicit operator string(PrtString val) - { - return val.value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - private PrtString(string value) - { - this.value = value; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtString operator +(in PrtString prtString1, in PrtString prtString2) - { - return new PrtString(prtString1.value + prtString2.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator ==(in PrtString pValue1, in PrtString pValue2) - { - return Equals(pValue1, pValue2); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator !=(in PrtString pValue1, in PrtString pValue2) - { - return !Equals(pValue1, pValue2); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator ==(in PrtString pValue1, in IPrtValue pValue2) - { - return pValue2 is PrtString prtString && string.Equals(pValue1.value, prtString.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator !=(in PrtString pValue1, in IPrtValue pValue2) - { - return pValue2 is PrtString prtString && !string.Equals(pValue1.value, prtString.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator ==(in IPrtValue pValue1, in PrtString pValue2) - { - return pValue1 is PrtString prtString && string.Equals(pValue2.value, prtString.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static bool operator !=(in IPrtValue pValue1, in PrtString pValue2) - { - return pValue1 is PrtString prtString && !string.Equals(pValue2.value, prtString.value); - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <(in PrtString prtString1, in PrtString prtString2) - { - return string.Compare(prtString1.value, prtString2.value) == -1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <(in IPrtValue pValue1, in PrtString pValue2) - { - return pValue1 is PrtString prtString && string.Compare(prtString.value, pValue2.value) == -1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <(in PrtString pValue1, in IPrtValue pValue2) - { - return pValue2 is PrtString prtString && string.Compare(prtString.value, pValue1.value) == -1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >(in PrtString prtString1, in PrtString prtString2) - { - return string.Compare(prtString1.value, prtString2.value) == 1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >(in IPrtValue pValue1, in PrtString pValue2) - { - return pValue1 is PrtString prtString && string.Compare(prtString.value, pValue2.value) == 1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >(in PrtString pValue1, in IPrtValue pValue2) - { - return pValue2 is PrtString prtString && string.Compare(prtString.value, pValue1.value) == 1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <=(in PrtString prtString1, in PrtString prtString2) - { - return string.Compare(prtString1.value, prtString2.value) != 1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <=(in IPrtValue pValue1, in PrtString pValue2) - { - return pValue1 is PrtString prtString && string.Compare(prtString.value, pValue2.value) != 1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator <=(in PrtString pValue1, in IPrtValue pValue2) - { - return pValue2 is PrtString prtString && string.Compare(prtString.value, pValue1.value) != 1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >=(in PrtString prtString1, in PrtString prtString2) - { - return string.Compare(prtString1.value, prtString2.value) != -1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >=(in IPrtValue pValue1, in PrtString pValue2) - { - return pValue1 is PrtString prtString && string.Compare(prtString.value, pValue2.value) != -1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public static PrtBool operator >=(in PrtString pValue1, in IPrtValue pValue2) - { - return pValue2 is PrtString prtString && string.Compare(prtString.value, pValue1.value) != -1; - } - - [MethodImpl(MethodImplOptions.AggressiveInlining)] - public bool Equals(IPrtValue obj) - { - return obj is PrtString other && string.Equals(value, other.value); - } - - public override int GetHashCode() - { - return value.GetHashCode(); - } - - public override string ToString() - { - return value; - } - - /// - /// Like ToString, but emits a representation of a string literal, surrounded by double-quotes, - /// and where all interior double-quotes are escaped. - /// - /// - public string ToEscapedString() - { - var v = value ?? ""; - return $"\"{v.Replace("\"", "\\\"")}\""; - } - - - public object ToDict() - { - return ToString(); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Random/Generator.cs b/Src/PChecker/CheckerCore/Random/Generator.cs index aa7cbaeea9..e7c4f474e6 100644 --- a/Src/PChecker/CheckerCore/Random/Generator.cs +++ b/Src/PChecker/CheckerCore/Random/Generator.cs @@ -12,10 +12,6 @@ namespace PChecker.Random /// During systematic testing, the generation of random values is controlled, which /// allows the runtime to explore combinations of choices to find bugs. /// - /// - /// See Program non-determinism - /// for more information. - /// public class Generator { /// diff --git a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Special/ReplayStrategy.cs b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Special/ReplayStrategy.cs index 47be1170d2..12bfb858af 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Special/ReplayStrategy.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/Strategies/Special/ReplayStrategy.cs @@ -21,7 +21,7 @@ internal sealed class ReplayStrategy : ISchedulingStrategy private readonly CheckerConfiguration _checkerConfiguration; /// - /// The Coyote program schedule trace. + /// The program schedule trace. /// private readonly ScheduleTrace ScheduleTrace; diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestAttributes.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestAttributes.cs index 47748a5e10..0124cf26d9 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestAttributes.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestAttributes.cs @@ -7,7 +7,7 @@ namespace PChecker.SystematicTesting { /// /// Attribute for declaring the entry point to - /// a Coyote program test. + /// a program test. /// [AttributeUsage(AttributeTargets.Method)] public sealed class TestAttribute : Attribute @@ -43,8 +43,8 @@ public sealed class TestIterationDisposeAttribute : Attribute /// /// Attribute for declaring the factory method that creates - /// the Coyote testing runtime. This is an advanced feature, - /// only to be used for replacing the original Coyote testing + /// the testing runtime. This is an advanced feature, + /// only to be used for replacing the original testing /// runtime with an alternative implementation. /// [AttributeUsage(AttributeTargets.Method)] diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs index b729f3e0ed..24befbed6a 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestReport.cs @@ -11,7 +11,7 @@ namespace PChecker.SystematicTesting { /// - /// Class implementing the Coyote test report. + /// Class implementing the test report. /// [DataContract] public class TestReport diff --git a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs index e4ff17006a..d11b86fe9b 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/TestingEngine.cs @@ -72,9 +72,6 @@ public class TestingEngine /// /// The installed logger. /// - /// - /// See Logging for more information. - /// private TextWriter Logger; /// @@ -730,13 +727,6 @@ public void TryEmitTraces(string directory, string file) JsonSerializer.Serialize(jsonStreamFile, JsonLogger.Logs, jsonSerializerConfig); } - if (Graph != null) - { - var graphPath = directory + file + "_" + index + ".dgml"; - Graph.SaveDgml(graphPath, true); - Logger.WriteLine($"..... Writing {graphPath}"); - } - if (!_checkerConfiguration.PerformFullExploration) { // Emits the reproducable trace, if it exists. @@ -768,7 +758,7 @@ private void InitializeCustomLogging(ControlledRuntime runtime) { if (!string.IsNullOrEmpty(_checkerConfiguration.CustomStateMachineRuntimeLogType)) { - var log = Activate(_checkerConfiguration.CustomStateMachineRuntimeLogType); + var log = Activate(_checkerConfiguration.CustomStateMachineRuntimeLogType); if (log != null) { runtime.RegisterLog(log); @@ -778,7 +768,7 @@ private void InitializeCustomLogging(ControlledRuntime runtime) if (_checkerConfiguration.IsDgmlGraphEnabled || _checkerConfiguration.ReportActivityCoverage) { // Registers an activity coverage graph builder. - runtime.RegisterLog(new StateMachineRuntimeLogGraphBuilder(false) + runtime.RegisterLog(new ControlledRuntimeLogGraphBuilder(false) { CollapseMachineInstances = _checkerConfiguration.ReportActivityCoverage }); @@ -787,7 +777,7 @@ private void InitializeCustomLogging(ControlledRuntime runtime) if (_checkerConfiguration.ReportActivityCoverage) { // Need this additional logger to get the event coverage report correct - runtime.RegisterLog(new StateMachineRuntimeLogEventCoverage()); + runtime.RegisterLog(new ControlledRuntimeLogEventCoverage()); } if (_checkerConfiguration.IsXmlLogEnabled) diff --git a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs index 1751632652..bbc45f0ca8 100644 --- a/Src/PChecker/CheckerCore/Testing/TestingProcess.cs +++ b/Src/PChecker/CheckerCore/Testing/TestingProcess.cs @@ -42,7 +42,7 @@ public class TestingProcess private readonly Profiler Profiler; /// - /// Creates a Coyote testing process. + /// Creates a testing process. /// public static TestingProcess Create(CheckerConfiguration checkerConfiguration) { @@ -61,7 +61,7 @@ public TestReport GetTestReport() private readonly TextWriter StdOut = Console.Out; /// - /// Runs the Coyote testing process. + /// Runs the testing process. /// public void Run() { diff --git a/Src/PChecker/CheckerCore/Utilities/Profiler.cs b/Src/PChecker/CheckerCore/Utilities/Profiler.cs index ec9f031ee6..f9a6ba701d 100644 --- a/Src/PChecker/CheckerCore/Utilities/Profiler.cs +++ b/Src/PChecker/CheckerCore/Utilities/Profiler.cs @@ -7,7 +7,7 @@ namespace PChecker.Utilities { /// - /// The Coyote profiler. + /// The profiler. /// public class Profiler { diff --git a/Src/PChecker/CheckerCore/Utilities/Reporter.cs b/Src/PChecker/CheckerCore/Utilities/Reporter.cs index 2089e178a4..e1a0b05d3a 100644 --- a/Src/PChecker/CheckerCore/Utilities/Reporter.cs +++ b/Src/PChecker/CheckerCore/Utilities/Reporter.cs @@ -9,7 +9,7 @@ namespace PChecker.Utilities { /// - /// The Coyote testing reporter. + /// The testing reporter. /// internal static class Reporter { @@ -74,10 +74,6 @@ private static void EmitTestingCoverageOutputFiles(TestReport report, string dir var codeCoverageReporter = new ActivityCoverageReporter(report.CoverageInfo); var filePath = $"{directory}{file}"; - var graphFilePath = $"{filePath}.dgml"; - Console.WriteLine($"..... Writing {graphFilePath}"); - codeCoverageReporter.EmitVisualizationGraph(graphFilePath); - var coverageFilePath = $"{filePath}.coverage.txt"; Console.WriteLine($"..... Writing {coverageFilePath}"); codeCoverageReporter.EmitCoverageReport(coverageFilePath); diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 19be808ec8..031394f96e 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -367,13 +367,13 @@ private void WriteInitializeEnums(CompilationContext context, StringWriter outpu //initialize the interfaces context.WriteLine(output, "public partial class PHelper {"); context.WriteLine(output, "public static void InitializeEnums() {"); - context.WriteLine(output, "PrtEnum.Clear();"); + context.WriteLine(output, "PEnum.Clear();"); foreach (var enumDecl in enums) { var enumElemNames = $"new [] {{{string.Join(",", enumDecl.Values.Select(e => $"\"{context.Names.GetNameForDecl(e)}\""))}}}"; var enumElemValues = $"new [] {{{string.Join(",", enumDecl.Values.Select(e => e.Value))}}}"; - context.WriteLine(output, $"PrtEnum.AddEnumElements({enumElemNames}, {enumElemValues});"); + context.WriteLine(output, $"PEnum.AddEnumElements({enumElemNames}, {enumElemValues});"); } context.WriteLine(output, "}"); @@ -486,7 +486,7 @@ private void WriteEvent(CompilationContext context, StringWriter output, Event p context.WriteLine(output, "{"); context.WriteLine(output, $"public {declName}() : base() {{}}"); context.WriteLine(output, $"public {declName} ({payloadType} payload): base(payload)" + "{ }"); - context.WriteLine(output, $"public override IPrtValue Clone() {{ return new {declName}();}}"); + context.WriteLine(output, $"public override IPValue Clone() {{ return new {declName}();}}"); context.WriteLine(output, "}"); WriteNameSpaceEpilogue(context, output); @@ -510,12 +510,12 @@ private void WriteMachine(CompilationContext context, StringWriter output, Machi var cTorType = GetCSharpType(machine.PayloadType, true); context.Write(output, "public class ConstructorEvent : Event"); context.Write(output, "{"); - context.Write(output, $"public ConstructorEvent(IPrtValue val) : base(val) {{ }}"); + context.Write(output, $"public ConstructorEvent(IPValue val) : base(val) {{ }}"); context.WriteLine(output, "}"); context.WriteLine(output); context.WriteLine(output, - $"protected override Event GetConstructorEvent(IPrtValue value) {{ return new ConstructorEvent((IPrtValue)value); }}"); + $"protected override Event GetConstructorEvent(IPValue value) {{ return new ConstructorEvent((IPValue)value); }}"); // create the constructor to initialize the sends, creates and receives list WriteMachineConstructor(context, output, machine); @@ -857,7 +857,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function if (ctorStmt.Arguments.Count > 1) { //create tuple from rvaluelist - context.Write(output, "new PrtTuple("); + context.Write(output, "new PTuple("); var septor = ""; foreach (var ctorExprArgument in ctorStmt.Arguments) { @@ -926,7 +926,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function break; case AddStmt addStmt: - context.Write(output, "((PrtSet)"); + context.Write(output, "((PSet)"); WriteExpr(context, output, addStmt.Variable); context.Write(output, ").Add("); WriteExpr(context, output, addStmt.Value); @@ -935,7 +935,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function case InsertStmt insertStmt: var isMap = PLanguageType.TypeIsOfKind(insertStmt.Variable.Type, TypeKind.Map); - var castOp = isMap ? "(PrtMap)" : "(PrtSeq)"; + var castOp = isMap ? "(PMap)" : "(PSeq)"; context.Write(output, $"({castOp}"); WriteExpr(context, output, insertStmt.Variable); if (isMap) @@ -1039,10 +1039,10 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function case RemoveStmt removeStmt: { var castOperation = PLanguageType.TypeIsOfKind(removeStmt.Variable.Type, TypeKind.Map) - ? "(PrtMap)" + ? "(PMap)" : PLanguageType.TypeIsOfKind(removeStmt.Variable.Type, TypeKind.Sequence) - ? "(PrtSeq)" - : "(PrtSet)"; + ? "(PSeq)" + : "(PSet)"; context.Write(output, $"({castOperation}"); switch (removeStmt.Variable.Type.Canonicalize()) { @@ -1135,7 +1135,7 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr switch (lvalue) { case MapAccessExpr mapAccessExpr: - context.Write(output, "((PrtMap)"); + context.Write(output, "((PMap)"); WriteLValue(context, output, mapAccessExpr.MapExpr); context.Write(output, ")["); WriteExpr(context, output, mapAccessExpr.IndexExpr); @@ -1143,7 +1143,7 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr break; case SetAccessExpr setAccessExpr: - context.Write(output, "((PrtSet)"); + context.Write(output, "((PSet)"); WriteLValue(context, output, setAccessExpr.SetExpr); context.Write(output, ")["); WriteExpr(context, output, setAccessExpr.IndexExpr); @@ -1151,13 +1151,13 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr break; case NamedTupleAccessExpr namedTupleAccessExpr: - context.Write(output, "((PrtNamedTuple)"); + context.Write(output, "((PNamedTuple)"); WriteExpr(context, output, namedTupleAccessExpr.SubExpr); context.Write(output, $")[\"{namedTupleAccessExpr.FieldName}\"]"); break; case SeqAccessExpr seqAccessExpr: - context.Write(output, "((PrtSeq)"); + context.Write(output, "((PSeq)"); WriteLValue(context, output, seqAccessExpr.SeqExpr); context.Write(output, ")["); WriteExpr(context, output, seqAccessExpr.IndexExpr); @@ -1165,7 +1165,7 @@ private void WriteLValue(CompilationContext context, StringWriter output, IPExpr break; case TupleAccessExpr tupleAccessExpr: - context.Write(output, "((PrtTuple)"); + context.Write(output, "((PTuple)"); WriteExpr(context, output, tupleAccessExpr.SubExpr); context.Write(output, $")[{tupleAccessExpr.FieldNo}]"); break; @@ -1194,10 +1194,10 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p if (binOpExpr.Operation == BinOpType.Eq || binOpExpr.Operation == BinOpType.Neq) { var negate = binOpExpr.Operation == BinOpType.Neq ? "!" : ""; - context.Write(output, $"({negate}PrtValues.SafeEquals("); + context.Write(output, $"({negate}PValues.SafeEquals("); if (PLanguageType.TypeIsOfKind(binOpExpr.Lhs.Type, TypeKind.Enum)) { - context.Write(output, "PrtValues.Box((long) "); + context.Write(output, "PValues.Box((long) "); WriteExpr(context, output, binOpExpr.Lhs); context.Write(output, "),"); } @@ -1209,7 +1209,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p if (PLanguageType.TypeIsOfKind(binOpExpr.Rhs.Type, TypeKind.Enum)) { - context.Write(output, "PrtValues.Box((long) "); + context.Write(output, "PValues.Box((long) "); WriteExpr(context, output, binOpExpr.Rhs); context.Write(output, ")"); } @@ -1242,7 +1242,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case BoolLiteralExpr boolLiteralExpr: - context.Write(output, $"((PrtBool){(boolLiteralExpr.Value ? "true" : "false")})"); + context.Write(output, $"((PBool){(boolLiteralExpr.Value ? "true" : "false")})"); break; case CastExpr castExpr: @@ -1284,7 +1284,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p case ChooseExpr chooseExpr: if (chooseExpr.SubExpr == null) { - context.Write(output, "((PrtBool)currentMachine.RandomBoolean())"); + context.Write(output, "((PBool)currentMachine.RandomBoolean())"); } else { @@ -1297,10 +1297,10 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p case ContainsExpr containsExpr: var isMap = PLanguageType.TypeIsOfKind(containsExpr.Collection.Type, TypeKind.Map); var isSeq = PLanguageType.TypeIsOfKind(containsExpr.Collection.Type, TypeKind.Sequence); - var castOp = isMap ? "(PrtMap)" - : isSeq ? "(PrtSeq)" - : "(PrtSet)"; - context.Write(output, "((PrtBool)("); + var castOp = isMap ? "(PMap)" + : isSeq ? "(PSeq)" + : "(PSet)"; + context.Write(output, "((PBool)("); context.Write(output, $"({castOp}"); WriteExpr(context, output, containsExpr.Collection); if (isMap) @@ -1326,7 +1326,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p if (ctorExpr.Arguments.Count > 1) { //create tuple from rvaluelist - context.Write(output, "new PrtTuple("); + context.Write(output, "new PTuple("); var septor = ""; foreach (var ctorExprArgument in ctorExpr.Arguments) { @@ -1352,7 +1352,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p case EnumElemRefExpr enumElemRefExpr: var enumElem = enumElemRefExpr.Value; - context.Write(output, $"(PrtEnum.Get(\"{context.Names.GetNameForDecl(enumElem)}\"))"); + context.Write(output, $"(PEnum.Get(\"{context.Names.GetNameForDecl(enumElem)}\"))"); break; case EventRefExpr eventRefExpr: @@ -1376,11 +1376,11 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case FairNondetExpr _: - context.Write(output, "((PrtBool)currentMachine.RandomBoolean())"); + context.Write(output, "((PBool)currentMachine.RandomBoolean())"); break; case FloatLiteralExpr floatLiteralExpr: - context.Write(output, $"((PrtFloat){floatLiteralExpr.Value})"); + context.Write(output, $"((PFloat){floatLiteralExpr.Value})"); break; case FunCallExpr funCallExpr: @@ -1407,7 +1407,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case IntLiteralExpr intLiteralExpr: - context.Write(output, $"((PrtInt)({intLiteralExpr.Value}))"); + context.Write(output, $"((PInt)({intLiteralExpr.Value}))"); break; case KeysExpr keysExpr: @@ -1435,7 +1435,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case NondetExpr _: - context.Write(output, "((PrtBool)currentMachine.RandomBoolean())"); + context.Write(output, "((PBool)currentMachine.RandomBoolean())"); break; case NullLiteralExpr _: @@ -1443,13 +1443,13 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case SizeofExpr sizeofExpr: - context.Write(output, "((PrtInt)("); + context.Write(output, "((PInt)("); WriteExpr(context, output, sizeofExpr.Expr); context.Write(output, ").Count)"); break; case StringExpr stringExpr: - context.Write(output, $"((PrtString) String.Format("); + context.Write(output, $"((PString) String.Format("); context.Write(output, $"\"{stringExpr.BaseString}\""); foreach (var arg in stringExpr.Args) { @@ -1512,7 +1512,7 @@ private void WriteClone(CompilationContext context, StringWriter output, IExprTe } var varName = context.Names.GetNameForDecl(variableRef.Variable); - context.Write(output, $"(({GetCSharpType(variableRef.Type)})((IPrtValue){varName})?.Clone())"); + context.Write(output, $"(({GetCSharpType(variableRef.Type)})((IPValue){varName})?.Clone())"); } private string GetCSharpType(PLanguageType type, bool isVar = false) @@ -1520,37 +1520,37 @@ private string GetCSharpType(PLanguageType type, bool isVar = false) switch (type.Canonicalize()) { case DataType _: - return "IPrtValue"; + return "IPValue"; case EnumType _: - return "PrtInt"; + return "PInt"; case ForeignType _: return type.CanonicalRepresentation; case MapType _: - return "PrtMap"; + return "PMap"; case NamedTupleType _: - return "PrtNamedTuple"; + return "PNamedTuple"; case PermissionType _: return "PMachineValue"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Any): - return "IPrtValue"; + return "IPValue"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Bool): - return "PrtBool"; + return "PBool"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Int): - return "PrtInt"; + return "PInt"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Float): - return "PrtFloat"; + return "PFloat"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.String): - return "PrtString"; + return "PString"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Event): return "Event"; @@ -1559,16 +1559,16 @@ private string GetCSharpType(PLanguageType type, bool isVar = false) return "PMachineValue"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Null): - return isVar ? "IPrtValue" : "void"; + return isVar ? "IPValue" : "void"; case SequenceType _: - return "PrtSeq"; + return "PSeq"; case SetType _: - return "PrtSet"; + return "PSet"; case TupleType _: - return "PrtTuple"; + return "PTuple"; default: throw new ArgumentOutOfRangeException(nameof(type)); @@ -1580,7 +1580,7 @@ private string GetDefaultValue(PLanguageType returnType) switch (returnType.Canonicalize()) { case EnumType enumType: - return $"((PrtInt){enumType.EnumDecl.Values.Min(elem => elem.Value)})"; + return $"((PInt){enumType.EnumDecl.Values.Min(elem => elem.Value)})"; case MapType mapType: return $"new {GetCSharpType(mapType)}()"; @@ -1604,16 +1604,16 @@ private string GetDefaultValue(PLanguageType returnType) return $"(new {GetCSharpType(tupleType)}({defaultTupleValues}))"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Bool): - return "((PrtBool)false)"; + return "((PBool)false)"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Int): - return "((PrtInt)0)"; + return "((PInt)0)"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Float): - return "((PrtFloat)0.0)"; + return "((PFloat)0.0)"; case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.String): - return "((PrtString)\"\")"; + return "((PString)\"\")"; case PrimitiveType eventType when eventType.IsSameTypeAs(PrimitiveType.Event): case PermissionType _: diff --git a/Tst/UnitTests/CSharpValuesTest.cs b/Tst/UnitTests/CSharpValuesTest.cs index dccb6e8aad..814526c52a 100644 --- a/Tst/UnitTests/CSharpValuesTest.cs +++ b/Tst/UnitTests/CSharpValuesTest.cs @@ -8,10 +8,10 @@ namespace UnitTests public class CSharpValuesTest { [Test] - public void TestPrtBoolOverloading() + public void TestPBoolOverloading() { - PrtBool boolT = true; - PrtBool boolF = false; + PBool boolT = true; + PBool boolF = false; Assert.AreEqual(boolT, boolF || boolT); Assert.AreEqual(boolT, boolT || boolF); Assert.AreEqual(boolT, !boolF); @@ -20,33 +20,33 @@ public void TestPrtBoolOverloading() } [Test] - public void TestPrtFloatComparisions() + public void TestPFloatComparisions() { - PrtBool boolT = true; - PrtBool boolF = false; - Assert.AreEqual(boolT, PrtValues.Box(1.0) < PrtValues.Box(2.0)); - Assert.AreEqual(boolF, PrtValues.Box(1.0) < PrtValues.Box(1.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) <= PrtValues.Box(1.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) <= PrtValues.Box(2.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) == PrtValues.Box(1.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) != PrtValues.Box(2.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) >= PrtValues.Box(1.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) >= PrtValues.Box(0.0)); - Assert.AreEqual(boolT, PrtValues.Box(1.0) > PrtValues.Box(0.0)); + PBool boolT = true; + PBool boolF = false; + Assert.AreEqual(boolT, PValues.Box(1.0) < PValues.Box(2.0)); + Assert.AreEqual(boolF, PValues.Box(1.0) < PValues.Box(1.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) <= PValues.Box(1.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) <= PValues.Box(2.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) == PValues.Box(1.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) != PValues.Box(2.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) >= PValues.Box(1.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) >= PValues.Box(0.0)); + Assert.AreEqual(boolT, PValues.Box(1.0) > PValues.Box(0.0)); } [Test] - public void TestPrtFloatOverloading() + public void TestPFloatOverloading() { - PrtFloat float1 = 1.0; - PrtFloat float2 = 2.0; - PrtFloat float3 = 3.0; + PFloat float1 = 1.0; + PFloat float2 = 2.0; + PFloat float3 = 3.0; Assert.AreEqual(float3, float1 + float2); Assert.AreEqual(float1, float3 - float2); Assert.AreEqual(float2, float1 * float2); - Assert.AreEqual(PrtValues.Box(1.5), float3 / float2); - Assert.AreEqual(PrtValues.Box(6.0), float1 + float2 + float3); - Assert.AreEqual(PrtValues.Box(6.0), float1 * float2 * float3); + Assert.AreEqual(PValues.Box(1.5), float3 / float2); + Assert.AreEqual(PValues.Box(6.0), float1 + float2 + float3); + Assert.AreEqual(PValues.Box(6.0), float1 * float2 * float3); Assert.AreEqual(float1, float3 / (float1 + float2)); Assert.AreEqual(-float1, float2 - float3); Assert.AreEqual(+float1, float1); @@ -54,33 +54,33 @@ public void TestPrtFloatOverloading() } [Test] - public void TestPrtIntComparisions() + public void TestPIntComparisions() { - PrtBool boolT = true; - PrtBool boolF = false; - Assert.AreEqual(boolT, PrtValues.Box(1) < PrtValues.Box(2)); - Assert.AreEqual(boolF, PrtValues.Box(1) < PrtValues.Box(1)); - Assert.AreEqual(boolT, PrtValues.Box(1) <= PrtValues.Box(1)); - Assert.AreEqual(boolT, PrtValues.Box(1) <= PrtValues.Box(2)); - Assert.AreEqual(boolT, PrtValues.Box(1) == PrtValues.Box(1)); - Assert.AreEqual(boolT, PrtValues.Box(1) != PrtValues.Box(2)); - Assert.AreEqual(boolT, PrtValues.Box(1) >= PrtValues.Box(1)); - Assert.AreEqual(boolT, PrtValues.Box(1) >= PrtValues.Box(0)); - Assert.AreEqual(boolT, PrtValues.Box(1) > PrtValues.Box(0)); + PBool boolT = true; + PBool boolF = false; + Assert.AreEqual(boolT, PValues.Box(1) < PValues.Box(2)); + Assert.AreEqual(boolF, PValues.Box(1) < PValues.Box(1)); + Assert.AreEqual(boolT, PValues.Box(1) <= PValues.Box(1)); + Assert.AreEqual(boolT, PValues.Box(1) <= PValues.Box(2)); + Assert.AreEqual(boolT, PValues.Box(1) == PValues.Box(1)); + Assert.AreEqual(boolT, PValues.Box(1) != PValues.Box(2)); + Assert.AreEqual(boolT, PValues.Box(1) >= PValues.Box(1)); + Assert.AreEqual(boolT, PValues.Box(1) >= PValues.Box(0)); + Assert.AreEqual(boolT, PValues.Box(1) > PValues.Box(0)); } [Test] - public void TestPrtIntOverloading() + public void TestPIntOverloading() { - PrtInt int1 = 1; - PrtInt int2 = 2; - PrtInt int3 = 3; + PInt int1 = 1; + PInt int2 = 2; + PInt int3 = 3; Assert.AreEqual(int3, int1 + int2); Assert.AreEqual(int1, int3 - int2); Assert.AreEqual(int2, int1 * int2); Assert.AreEqual(int1, int3 / int2); - Assert.AreEqual(PrtValues.Box(6), int1 + int2 + int3); - Assert.AreEqual(PrtValues.Box(6), int1 * int2 * int3); + Assert.AreEqual(PValues.Box(6), int1 + int2 + int3); + Assert.AreEqual(PValues.Box(6), int1 * int2 * int3); Assert.AreEqual(int1, int3 / (int1 + int2)); Assert.AreEqual(-int1, int2 - int3); Assert.AreEqual(+int1, int1);