From 2cab15f63d42534ec1170fe5b4b7b258a6379e04 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Wed, 4 Sep 2024 19:38:18 -0700 Subject: [PATCH] [Cleanup] Merging PMachine with StateMachine --- .../CheckerCore/PRuntime/GodMachine.cs | 4 +- Src/PChecker/CheckerCore/PRuntime/PMachine.cs | 253 ------------------ .../CheckerCore/StateMachines/StateMachine.cs | 163 ++++++++++- .../SystematicTesting/ControlledRuntime.cs | 14 +- .../Backend/CSharp/CSharpCodeGenerator.cs | 63 ++--- .../Backend/Java/MachineGenerator.cs | 2 +- 6 files changed, 184 insertions(+), 315 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/PRuntime/PMachine.cs diff --git a/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs b/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs index 603e6d386..819a16d4b 100644 --- a/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs +++ b/Src/PChecker/CheckerCore/PRuntime/GodMachine.cs @@ -9,9 +9,7 @@ public class _GodMachine : StateMachine private void InitOnEntry(Event e) { var mainMachine = (e as Config).MainMachine; - CreateStateMachine(mainMachine, mainMachine.Name, - new PMachine.InitializeParametersEvent( - new PMachine.InitializeParameters("I_" + mainMachine.Name, null))); + CreateStateMachine(mainMachine, "I_" + mainMachine.Name); } public class Config : Event diff --git a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs deleted file mode 100644 index d778d186e..000000000 --- a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs +++ /dev/null @@ -1,253 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Threading.Tasks; -using PChecker.StateMachines; -using PChecker.StateMachines.Events; -using PChecker.StateMachines.Exceptions; -using PChecker.StateMachines.Logging; -using PChecker.PRuntime.Exceptions; -using PChecker.PRuntime.Values; - -namespace PChecker.PRuntime -{ - public class PMachine : StateMachine - { - public List creates = new List(); - private string interfaceName; - public List receives = new List(); - public PMachineValue self; - public List sends = new List(); - - public void TryAssert(bool predicate) - { - Assert(predicate); - } - - public void TryAssert(bool predicate, string s, params object[] args) - { - Assert(predicate, s, args); - } - - protected void InitializeParametersFunction(Event e) - { - if (!(e is InitializeParametersEvent @event)) - { - throw new ArgumentException("Event type is incorrect: " + e.GetType().Name); - } - - var initParam = @event.Payload as InitializeParameters; - interfaceName = initParam.InterfaceName; - self = new PMachineValue(Id, receives.ToList()); - TryRaiseEvent(GetConstructorEvent(initParam.Payload), initParam.Payload); - } - - protected virtual Event GetConstructorEvent(IPrtValue value) - { - throw new NotImplementedException(); - } - - protected override OnExceptionOutcome OnException(Exception ex, string methodName, Event e) - { - var v = ex is UnhandledEventException; - if (!v) - { - return ex is PNonStandardReturnException - ? OnExceptionOutcome.HandledException - : base.OnException(ex, methodName, e); - } - - return (ex as UnhandledEventException).UnhandledEvent is PHalt - ? OnExceptionOutcome.Halt - : base.OnException(ex, methodName, e); - } - - public PMachineValue CreateInterface(PMachine creator, IPrtValue payload = null) - where T : PMachineValue - { - var createdInterface = PModule.linkMap[creator.interfaceName][typeof(T).Name]; - Assert(creates.Contains(createdInterface), - $"Machine {GetType().Name} cannot create interface {createdInterface}, not in its creates set"); - var createMachine = PModule.interfaceDefinitionMap[createdInterface]; - var machineId = CreateStateMachine(createMachine, createdInterface.Substring(2), - new InitializeParametersEvent(new InitializeParameters(createdInterface, payload))); - return new PMachineValue(machineId, PInterfaces.GetPermissions(createdInterface)); - } - - public void TrySendEvent(PMachineValue target, Event ev, object payload = null) - { - Assert(ev != null, "Machine cannot send a null event"); - Assert(target != null, "Machine in send cannot be null"); - Assert(sends.Contains(ev.GetType().Name), - $"Event {ev.GetType().Name} is not in the sends set of the Machine {GetType().Name}"); - Assert(target.Permissions.Contains(ev.GetType().Name), - $"Event {ev.GetType().Name} is not in the permissions set of the target machine"); - var oneArgConstructor = ev.GetType().GetConstructors().First(x => x.GetParameters().Length > 0); - ev = (Event)oneArgConstructor.Invoke(new[] { payload }); - - AnnounceInternal(ev); - SendEvent(target.Id, ev); - } - - public void TryRaiseEvent(Event ev, object payload = null) - { - Assert(ev != null, "Machine cannot raise a null event"); - var oneArgConstructor = ev.GetType().GetConstructors().First(x => x.GetParameters().Length > 0); - ev = (Event)oneArgConstructor.Invoke(new[] { payload }); - RaiseEvent(ev); - throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Raise }; - } - - public Task TryReceiveEvent(params Type[] events) - { - return ReceiveEventAsync(events); - } - - public int TryRandomInt(int maxValue) - { - return RandomInteger(maxValue); - } - - public int TryRandomInt(int minValue, int maxValue) - { - return minValue + RandomInteger(maxValue - minValue); - } - - public bool TryRandomBool(int maxValue) - { - return RandomBoolean(maxValue); - } - - public bool TryRandomBool() - { - return RandomBoolean(); - } - - public IPrtValue TryRandom(IPrtValue param) - { - switch (param) - { - case PrtInt maxValue: - { - TryAssert(maxValue <= 10000, $"choose expects a parameter with at most 10000 choices, got {maxValue} choices instead."); - return (PrtInt)TryRandomInt(maxValue); - } - - case PrtSeq seq: - { - TryAssert(seq.Any(), "Trying to choose from an empty sequence!"); - TryAssert(seq.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {seq.Count} choices instead."); - return seq[TryRandomInt(seq.Count)]; - } - case PrtSet set: - { - TryAssert(set.Any(), "Trying to choose from an empty set!"); - TryAssert(set.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {set.Count} choices instead."); - return set.ElementAt(TryRandomInt(set.Count)); - } - case PrtMap map: - { - TryAssert(map.Any(), "Trying to choose from an empty map!"); - TryAssert(map.Keys.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {map.Keys.Count} choices instead."); - return map.Keys.ElementAt(TryRandomInt(map.Keys.Count)); - } - default: - throw new PInternalException("This is an unexpected (internal) P exception. Please report to the P Developers"); - } - } - - public void LogLine(string message) - { - Logger.WriteLine($" {message}"); - - // Log message to JSON output - JsonLogger.AddLogType(JsonWriter.LogType.Print); - JsonLogger.AddLog(message); - JsonLogger.AddToLogs(updateVcMap: false); - } - - public void Log(string message) - { - Logger.Write($"{message}"); - } - - public void Announce(Event ev, object payload = null) - { - Assert(ev != null, "Machine cannot announce a null event"); - if (ev is PHalt) - { - ev = HaltEvent.Instance; - } - - 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()}"; - - Logger.WriteLine($" '{Id}' announced event '{ev.GetType().Name}'{pText}."); - - // Log message to JSON output - JsonLogger.AddLogType(JsonWriter.LogType.Announce); - JsonLogger.LogDetails.Id = $"{Id}"; - JsonLogger.LogDetails.Event = ev.GetType().Name; - if (payload != null) - { - JsonLogger.LogDetails.Payload = ((IPrtValue)payload).ToDict(); - } - JsonLogger.AddLog($"{Id} announced event {ev.GetType().Name}{pText}."); - JsonLogger.AddToLogs(updateVcMap: true); - - AnnounceInternal(@event); - } - - private void AnnounceInternal(Event ev) - { - Assert(ev != null, "cannot send a null event"); - if (!PModule.monitorMap.ContainsKey(interfaceName)) - { - return; - } - - foreach (var monitor in PModule.monitorMap[interfaceName]) - { - if (PModule.monitorObserves[monitor.Name].Contains(ev.GetType().Name)) - { - Monitor(monitor, ev); - } - } - } - - public class InitializeParameters : IPrtValue - { - public InitializeParameters(string interfaceName, IPrtValue payload) - { - InterfaceName = interfaceName; - Payload = payload; - } - - public string InterfaceName { get; } - public IPrtValue Payload { get; } - - public bool Equals(IPrtValue other) - { - throw new NotImplementedException(); - } - - public IPrtValue Clone() - { - throw new NotImplementedException(); - } - - public object ToDict() - { - throw new NotImplementedException(); - } - } - - public class InitializeParametersEvent : Event - { - public InitializeParametersEvent(InitializeParameters payload) : base(payload) - { - } - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs index a95eaffdc..693632382 100644 --- a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs @@ -20,6 +20,7 @@ using PChecker.StateMachines.StateTransitions; using PChecker.Exceptions; using PChecker.IO.Debugging; +using PChecker.PRuntime; using PChecker.PRuntime.Exceptions; using PChecker.PRuntime.Values; using PChecker.SystematicTesting; @@ -144,7 +145,123 @@ public abstract class StateMachine protected IPrtValue gotoPayload; + public List creates = new List(); + public string interfaceName; + public List receives = new List(); + public PMachineValue self; + public List sends = new List(); + + protected virtual Event GetConstructorEvent(IPrtValue value) + { + throw new NotImplementedException(); + } + + public PMachineValue CreateInterface(StateMachine creator, IPrtValue payload = null) + where T : PMachineValue + { + var createdInterface = PModule.linkMap[creator.interfaceName][typeof(T).Name]; + Assert(creates.Contains(createdInterface), + $"Machine {GetType().Name} cannot create interface {createdInterface}, not in its creates set"); + var createMachine = PModule.interfaceDefinitionMap[createdInterface]; + var machineId = CreateStateMachine(createMachine, createdInterface, + GetConstructorEvent(payload)); + return new PMachineValue(machineId, PInterfaces.GetPermissions(createdInterface)); + } + + + public IPrtValue TryRandom(IPrtValue param) + { + switch (param) + { + case PrtInt maxValue: + { + Assert(maxValue <= 10000, $"choose expects a parameter with at most 10000 choices, got {maxValue} choices instead."); + return (PrtInt)RandomInteger(maxValue); + } + + case PrtSeq 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: + { + 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: + { + 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."); + return map.Keys.ElementAt(RandomInteger(map.Keys.Count)); + } + default: + throw new PInternalException("This is an unexpected (internal) P exception. Please report to the P Developers"); + } + } + + public void LogLine(string message) + { + Logger.WriteLine($" {message}"); + + // Log message to JSON output + JsonLogger.AddLogType(JsonWriter.LogType.Print); + JsonLogger.AddLog(message); + JsonLogger.AddToLogs(updateVcMap: false); + } + + public void Log(string message) + { + Logger.Write($"{message}"); + } + public void Announce(Event ev, object payload = null) + { + Assert(ev != null, "Machine cannot announce a null event"); + if (ev is PHalt) + { + ev = HaltEvent.Instance; + } + + 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()}"; + + Logger.WriteLine($" '{Id}' announced event '{ev.GetType().Name}'{pText}."); + + // Log message to JSON output + JsonLogger.AddLogType(JsonWriter.LogType.Announce); + JsonLogger.LogDetails.Id = $"{Id}"; + JsonLogger.LogDetails.Event = ev.GetType().Name; + if (payload != null) + { + JsonLogger.LogDetails.Payload = ((IPrtValue)payload).ToDict(); + } + JsonLogger.AddLog($"{Id} announced event {ev.GetType().Name}{pText}."); + JsonLogger.AddToLogs(updateVcMap: true); + + AnnounceInternal(@event); + } + + private void AnnounceInternal(Event ev) + { + Assert(ev != null, "cannot send a null event"); + if (!PModule.monitorMap.ContainsKey(interfaceName)) + { + return; + } + + foreach (var monitor in PModule.monitorMap[interfaceName]) + { + if (PModule.monitorObserves[monitor.Name].Contains(ev.GetType().Name)) + { + Monitor(monitor, ev); + } + } + } + /// /// Initializes a new instance of the class. /// @@ -174,7 +291,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach /// controlled during analysis or testing. /// /// The controlled nondeterministic choice. - protected bool RandomBoolean() => Runtime.GetNondeterministicBooleanChoice(2, Id.Name, Id.Type); + public bool RandomBoolean() => Runtime.GetNondeterministicBooleanChoice(2, Id.Name, Id.Type); /// /// Returns a nondeterministic boolean choice, that can be @@ -184,7 +301,7 @@ internal void Configure(ControlledRuntime runtime, StateMachineId id, IStateMach /// /// The max value. /// The controlled nondeterministic choice. - protected bool RandomBoolean(int maxValue) => + public bool RandomBoolean(int maxValue) => Runtime.GetNondeterministicBooleanChoice(maxValue, Id.Name, Id.Type); /// @@ -194,8 +311,13 @@ protected bool RandomBoolean(int maxValue) => /// /// The max value. /// The controlled nondeterministic integer. - protected int RandomInteger(int maxValue) => + public int RandomInteger(int maxValue) => Runtime.GetNondeterministicIntegerChoice(maxValue, Id.Name, Id.Type); + + public int RandomInteger(int minValue, int maxValue) + { + return minValue + RandomInteger(maxValue - minValue); + } /// /// Invokes the specified monitor with the specified . @@ -408,11 +530,20 @@ protected StateMachineId CreateStateMachine(Type type, string name, Event initia /// /// Sends an asynchronous to a target. /// - /// The id of the target. + /// The target. /// The event to send. /// Optional id that can be used to identify this operation. - protected void SendEvent(StateMachineId id, Event e, Guid opGroupId = default) => - Runtime.SendEvent(id, e, this, opGroupId); + public void SendEvent(PMachineValue target, Event ev, Guid opGroupId = default) + { + Assert(ev != null, "Machine cannot send a null event"); + Assert(target != null, "Machine in send cannot be null"); + Assert(sends.Contains(ev.GetType().Name), + $"Event {ev.GetType().Name} is not in the sends set of the Machine {GetType().Name}"); + 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); + } /// /// Waits to receive an of the specified type @@ -421,7 +552,7 @@ protected void SendEvent(StateMachineId id, Event e, Guid opGroupId = default) = /// The event type. /// The optional predicate. /// The received event. - protected internal Task ReceiveEventAsync(Type eventType, Func predicate = null) + public Task ReceiveEventAsync(Type eventType, Func predicate = null) { Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); Runtime.NotifyReceiveCalled(this); @@ -433,7 +564,7 @@ protected internal Task ReceiveEventAsync(Type eventType, Func /// The event types to wait for. /// The received event. - protected internal Task ReceiveEventAsync(params Type[] eventTypes) + public Task ReceiveEventAsync(params Type[] eventTypes) { Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); Runtime.NotifyReceiveCalled(this); @@ -446,7 +577,7 @@ protected internal Task ReceiveEventAsync(params Type[] eventTypes) /// /// Event types and predicates. /// The received event. - protected internal Task ReceiveEventAsync(params Tuple>[] events) + public Task ReceiveEventAsync(params Tuple>[] events) { Assert(CurrentStatus is Status.Active, "{0} invoked ReceiveEventAsync while halting.", Id); Runtime.NotifyReceiveCalled(this); @@ -725,9 +856,19 @@ private bool OnUnhandledEventExceptionHandler(UnhandledEventException ex, Event /// The handler (outermost) that threw the exception. /// The event being handled when the exception was thrown. /// The action that the runtime should take. - protected virtual OnExceptionOutcome OnException(Exception ex, string methodName, Event e) + protected OnExceptionOutcome OnException(Exception ex, string methodName, Event e) { - return OnExceptionOutcome.ThrowException; + var v = ex is UnhandledEventException; + if (!v) + { + return ex is PNonStandardReturnException + ? OnExceptionOutcome.HandledException + : OnExceptionOutcome.ThrowException; + } + + return (ex as UnhandledEventException).UnhandledEvent is PHalt + ? OnExceptionOutcome.Halt + : OnExceptionOutcome.ThrowException; } /// diff --git a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs index 69c75d0cd..5734bee74 100644 --- a/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs +++ b/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs @@ -21,6 +21,8 @@ using PChecker.StateMachines.Managers.Mocks; using PChecker.Coverage; using PChecker.Exceptions; +using PChecker.PRuntime; +using PChecker.PRuntime.Values; using PChecker.Random; using PChecker.Runtime; using PChecker.Specifications.Monitors; @@ -30,6 +32,7 @@ using PChecker.SystematicTesting.Traces; using Debug = PChecker.IO.Debugging.Debug; using EventInfo = PChecker.StateMachines.Events.EventInfo; +using PMachineValue = PChecker.PRuntime.Values.PMachineValue; namespace PChecker.SystematicTesting { @@ -457,7 +460,14 @@ private StateMachine CreateStateMachine(StateMachineId id, Type type, string nam if (id is null) { - id = new StateMachineId(type, name, this); + if (name != null) + { + id = new StateMachineId(type, name.Substring(2), this); + } + else + { + id = new StateMachineId(type, name, this); + } } else { @@ -482,6 +492,8 @@ private StateMachine CreateStateMachine(StateMachineId id, Type type, string nam IEventQueue eventQueue = new EventQueue(stateMachineManager, stateMachine); stateMachine.Configure(this, id, stateMachineManager, eventQueue); stateMachine.SetupEventHandlers(); + stateMachine.self = new PMachineValue(id, stateMachine.receives.ToList()); + stateMachine.interfaceName = name; if (CheckerConfiguration.ReportActivityCoverage) { diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 3143c83b4..eaaf86a25 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -496,7 +496,7 @@ private void WriteMachine(CompilationContext context, StringWriter output, Machi WriteNameSpacePrologue(context, output); var declName = context.Names.GetNameForDecl(machine); - context.WriteLine(output, $"internal partial class {declName} : PMachine"); + context.WriteLine(output, $"internal partial class {declName} : StateMachine"); context.WriteLine(output, "{"); foreach (var field in machine.Fields) @@ -509,12 +509,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({cTorType} val) : base(val) {{ }}"); + context.Write(output, $"public ConstructorEvent(IPrtValue val) : base(val) {{ }}"); context.WriteLine(output, "}"); context.WriteLine(output); context.WriteLine(output, - $"protected override Event GetConstructorEvent(IPrtValue value) {{ return new ConstructorEvent(({cTorType})value); }}"); + $"protected override Event GetConstructorEvent(IPrtValue value) {{ return new ConstructorEvent((IPrtValue)value); }}"); // create the constructor to initialize the sends, creates and receives list WriteMachineConstructor(context, output, machine); @@ -559,17 +559,7 @@ private static void WriteMachineConstructor(CompilationContext context, StringWr private void WriteState(CompilationContext context, StringWriter output, State state) { - if (state.IsStart && !state.OwningMachine.IsSpec) - { - context.WriteLine(output, "[Start]"); - context.WriteLine(output, "[OnEntry(nameof(InitializeParametersFunction))]"); - context.WriteLine(output, - $"[OnEventGotoState(typeof(ConstructorEvent), typeof({context.Names.GetNameForDecl(state)}))]"); - context.WriteLine(output, "class __InitState__ : State { }"); - context.WriteLine(output); - } - - if (state.IsStart && state.OwningMachine.IsSpec) + if (state.IsStart) { context.WriteLine(output, "[Start]"); } @@ -730,7 +720,7 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func { // for machine var seperator = functionParameters == "" ? "" : ", "; - var functionParameters_machine = functionParameters + string.Concat(seperator, "PMachine currentMachine"); + var functionParameters_machine = functionParameters + string.Concat(seperator, "StateMachine currentMachine"); context.WriteLine(output, $"public {staticKeyword}{asyncKeyword}{returnType} {functionName}({functionParameters_machine})"); WriteFunctionBody(context, output, function); @@ -1008,7 +998,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function .ToHashSet(); eventTypeNames.Add("PHalt"); // halt as a special case for receive var recvArgs = string.Join(", ", eventTypeNames.Select(name => $"typeof({name})")); - context.WriteLine(output, $"var {eventName} = await currentMachine.TryReceiveEvent({recvArgs});"); + context.WriteLine(output, $"var {eventName} = await currentMachine.ReceiveEventAsync({recvArgs});"); context.WriteLine(output, $"switch ({eventName}) {{"); // add halt as a special case if doesnt exist if (receiveStmt.Cases.All(kv => kv.Key.Name != "PHalt")) @@ -1101,36 +1091,17 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function break; case SendStmt sendStmt: - context.Write(output, "currentMachine.TrySendEvent("); - WriteExpr(context, output, sendStmt.MachineExpr); - context.Write(output, ", (Event)"); - WriteExpr(context, output, sendStmt.Evt); - if (sendStmt.Arguments.Any()) { - context.Write(output, ", "); - if (sendStmt.Arguments.Count > 1) - { - //create tuple from rvaluelist - var argTypes = string.Join(",", - sendStmt.Arguments.Select(a => GetCSharpType(a.Type))); - var tupleType = $"PrtTuple"; - context.Write(output, $"new {tupleType}("); - var septor = ""; - foreach (var ctorExprArgument in sendStmt.Arguments) - { - context.Write(output, septor); - WriteExpr(context, output, ctorExprArgument); - septor = ","; - } - - context.Write(output, ")"); - } - else - { - WriteExpr(context, output, sendStmt.Arguments.First()); - } + WriteExpr(context, output, sendStmt.Evt); + context.Write(output, ".Payload = "); + WriteExpr(context, output, sendStmt.Arguments.First()); + context.WriteLine(output, ";"); } + context.Write(output, "currentMachine.SendEvent("); + WriteExpr(context, output, sendStmt.MachineExpr); + context.Write(output, ", (Event)"); + WriteExpr(context, output, sendStmt.Evt); context.WriteLine(output, ");"); break; @@ -1312,7 +1283,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p case ChooseExpr chooseExpr: if (chooseExpr.SubExpr == null) { - context.Write(output, "((PrtBool)currentMachine.TryRandomBool())"); + context.Write(output, "((PrtBool)currentMachine.RandomBoolean())"); } else { @@ -1404,7 +1375,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case FairNondetExpr _: - context.Write(output, "((PrtBool)currentMachine.TryRandomBool())"); + context.Write(output, "((PrtBool)currentMachine.RandomBoolean())"); break; case FloatLiteralExpr floatLiteralExpr: @@ -1463,7 +1434,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p break; case NondetExpr _: - context.Write(output, "((PrtBool)currentMachine.TryRandomBool())"); + context.Write(output, "((PrtBool)currentMachine.RandomBoolean())"); break; case NullLiteralExpr _: diff --git a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs index 8356b1ff3..30d5e4d39 100644 --- a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs @@ -69,7 +69,7 @@ protected override void GenerateCodeImpl() private void WriteMachineDecl() { - WriteLine($"// PMachine {_currentMachine.Name} elided "); + WriteLine($"// StateMachine {_currentMachine.Name} elided "); } private void WriteMonitorDecl()