Skip to content

Commit

Permalink
cleanup state machine
Browse files Browse the repository at this point in the history
  • Loading branch information
Christine Zhou committed Aug 14, 2024
1 parent 99a5f46 commit 44a2831
Show file tree
Hide file tree
Showing 6 changed files with 90 additions and 99 deletions.
4 changes: 2 additions & 2 deletions Src/PChecker/CheckerCore/Actors/ActorRuntime.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,13 +250,13 @@ private EnqueueStatus EnqueueEvent(ActorId targetId, Event e, StateMachine sende
if (target is null || target.IsHalted)
{
LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type,
(sender as StateMachine)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true);
sender?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: true);
TryHandleDroppedEvent(e, targetId);
return EnqueueStatus.Dropped;
}

LogWriter.LogSendEvent(targetId, sender?.Id.Name, sender?.Id.Type,
(sender as StateMachine)?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: false);
sender?.CurrentStateName ?? string.Empty, e, opGroupId, isTargetHalted: false);

var enqueueStatus = target.Enqueue(e, opGroupId, null);
if (enqueueStatus == EnqueueStatus.Dropped)
Expand Down
6 changes: 2 additions & 4 deletions Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,8 +156,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)

// TODO: check op-id of default event.
// A default event handler exists.
var stateName = Actor is StateMachine stateMachine ?
NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty;
var stateName = NameResolver.GetStateNameForLogging(Actor.CurrentState.GetType());
var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName);
return (DequeueStatus.Default, DefaultEvent.Instance, Guid.Empty, new EventInfo(DefaultEvent.Instance, eventOrigin));
}
Expand Down Expand Up @@ -209,8 +208,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)
/// <inheritdoc/>
public void RaiseEvent(Event e, Guid opGroupId)
{
var stateName = Actor is StateMachine stateMachine ?
NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty;
var stateName = NameResolver.GetStateNameForLogging(Actor.CurrentState.GetType());
var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName);
var info = new EventInfo(e, eventOrigin);
RaisedEvent = (e, opGroupId, info);
Expand Down
2 changes: 1 addition & 1 deletion Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ internal class VectorClockGenerator
{
/// <summary>
/// Nested class for handling FIFO send receive requests.
/// NOTE: In the case of sending to a the same machine with the same event and same payload.
/// NOTE: In the case of sending to the same machine with the same event and same payload.
/// </summary>
private class FifoSendReceiveMapping
{
Expand Down
0 ...ckerCore/Actors/Managers/IActorManager.cs → ...e/Actors/Managers/IStateMachineManager.cs
View file
File renamed without changes.
126 changes: 66 additions & 60 deletions Src/PChecker/CheckerCore/Actors/StateMachine.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,10 +66,10 @@ public abstract class StateMachine
private static readonly ConcurrentDictionary<Type, object> ActionCacheLocks =
new ConcurrentDictionary<Type, object>();

/// <summary>
/// Map from event types to cached action delegates.
/// </summary>
private protected readonly Dictionary<Type, CachedDelegate> ActionMap = new Dictionary<Type, CachedDelegate>();
// /// <summary>
// /// Map from event types to cached action delegates.
// /// </summary>
// private protected readonly Dictionary<Type, CachedDelegate> ActionMap = new Dictionary<Type, CachedDelegate>();

/// <summary>
/// Cache of state machine types to a set of all possible states types.
Expand Down Expand Up @@ -390,17 +390,17 @@ protected internal Guid OperationGroupId
}
}

/// <summary>
/// Creates a new actor of the specified type and with the specified optional
/// <see cref="Event"/>. This <see cref="Event"/> can only be used to access
/// its payload, and cannot be handled.
/// </summary>
/// <param name="type">Type of the actor.</param>
/// <param name="initialEvent">Optional initialization event.</param>
/// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
/// <returns>The unique actor id.</returns>
protected ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) =>
Runtime.CreateActor(null, type, null, initialEvent, this, opGroupId);
// /// <summary>
// /// Creates a new actor of the specified type and with the specified optional
// /// <see cref="Event"/>. This <see cref="Event"/> can only be used to access
// /// its payload, and cannot be handled.
// /// </summary>
// /// <param name="type">Type of the actor.</param>
// /// <param name="initialEvent">Optional initialization event.</param>
// /// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
// /// <returns>The unique actor id.</returns>
// protected ActorId CreateActor(Type type, Event initialEvent = null, Guid opGroupId = default) =>
// Runtime.CreateActor(null, type, null, initialEvent, this, opGroupId);

/// <summary>
/// Creates a new actor of the specified type and name, and with the specified
Expand Down Expand Up @@ -633,22 +633,22 @@ private protected async Task InvokeActionAsync(CachedDelegate cachedAction, Even
}
}

/// <summary>
/// Checks if the specified event is ignored.
/// </summary>
internal bool IsEventIgnored(Event e)
{
return false;
}

/// <summary>
/// Returns the set of all registered events (for code coverage).
/// It does not include events that are deferred or ignored.
/// </summary>
internal HashSet<string> GetAllRegisteredEvents()
{
return new HashSet<string>(from key in ActionMap.Keys select key.FullName);
}
// /// <summary>
// /// Checks if the specified event is ignored.
// /// </summary>
// internal bool IsEventIgnored(Event e)
// {
// return false;
// }
//
// /// <summary>
// /// Returns the set of all registered events (for code coverage).
// /// It does not include events that are deferred or ignored.
// /// </summary>
// internal HashSet<string> GetAllRegisteredEvents()
// {
// return new HashSet<string>(from key in StateMachineActionMap.Keys select key);
// }

/// <summary>
/// Returns the action with the specified name.
Expand Down Expand Up @@ -847,34 +847,34 @@ private protected static class UserCallbackType
internal const string OnHalt = nameof(OnHaltAsync);
}

/// <summary>
/// Attribute for declaring which action should be invoked
/// to handle a dequeued event of the specified type.
/// </summary>
[AttributeUsage(AttributeTargets.Class, AllowMultiple = true)]
protected sealed class OnEventDoActionAttribute : Attribute
{
/// <summary>
/// The type of the dequeued event.
/// </summary>
internal Type Event;

/// <summary>
/// The name of the action to invoke.
/// </summary>
internal string Action;

/// <summary>
/// Initializes a new instance of the <see cref="OnEventDoActionAttribute"/> class.
/// </summary>
/// <param name="eventType">The type of the dequeued event.</param>
/// <param name="actionName">The name of the action to invoke.</param>
public OnEventDoActionAttribute(Type eventType, string actionName)
{
Event = eventType;
Action = actionName;
}
}
// /// <summary>
// /// Attribute for declaring which action should be invoked
// /// to handle a dequeued event of the specified type.
// /// </summary>
// [AttributeUsage(AttributeTargets.Class, AllowMultiple = true)]
// protected sealed class OnEventDoActionAttribute : Attribute
// {
// /// <summary>
// /// The type of the dequeued event.
// /// </summary>
// internal Type Event;
//
// /// <summary>
// /// The name of the action to invoke.
// /// </summary>
// internal string Action;
//
// /// <summary>
// /// Initializes a new instance of the <see cref="OnEventDoActionAttribute"/> class.
// /// </summary>
// /// <param name="eventType">The type of the dequeued event.</param>
// /// <param name="actionName">The name of the action to invoke.</param>
// public OnEventDoActionAttribute(Type eventType, string actionName)
// {
// Event = eventType;
// Action = actionName;
// }
// }

/// <summary>
/// Raises the specified <see cref="Event"/> at the end of the current action.
Expand Down Expand Up @@ -1014,7 +1014,7 @@ private protected async Task HandleEventAsync(Event e)
// Then specific event is more recent than any wild card events.
await HandleEventAsync(e, currentState, ehandler);
}
else if (ActionMap.TryGetValue(e.GetType(), out var handler))
else if (StateMachineActionMap.TryGetValue(e.GetType().Name, out var handler))
{
// Allow StateMachine to have class level OnEventDoActions the same way Actor allows.
Runtime.NotifyInvokedAction(this, handler.MethodInfo, CurrentStateName, CurrentStateName, e);
Expand Down Expand Up @@ -1470,6 +1470,12 @@ private void ExtractStateTypes(Type type)
{
StateTypeCache[GetType()].Add(nextType);
}

/* TODO: figure whether this part is needed */
if (nextType.BaseType != null)
{
stack.Push(nextType.BaseType);
}
}
}

Expand Down
51 changes: 19 additions & 32 deletions Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -386,7 +386,7 @@ internal override void SendEvent(ActorId targetId, Event e, StateMachine sender,
if (e is null)
{
var message = sender != null ?
string.Format("{0} is sending a null event.", sender.Id.ToString()) :
string.Format("{0} is sending a null event.", sender.Id) :
"Cannot send a null event.";
Assert(false, message);
}
Expand Down Expand Up @@ -420,10 +420,10 @@ internal override async Task<bool> SendEventAndExecuteAsync(ActorId targetId, Ev
var enqueueStatus = EnqueueEvent(targetId, e, sender, opGroupId, out var target);
if (enqueueStatus is EnqueueStatus.EventHandlerNotRunning)
{
RunActorEventHandler(target, null, false, sender as StateMachine);
RunActorEventHandler(target, null, false, sender);

// Wait until the actor reaches quiescence.
await (sender as StateMachine).ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == targetId);
await sender.ReceiveEventAsync(typeof(QuiescentEvent), rev => (rev as QuiescentEvent).ActorId == targetId);
return true;
}

Expand Down Expand Up @@ -822,7 +822,7 @@ internal override void NotifyDequeuedEvent(StateMachine actor, Event e, EventInf
ResetProgramCounter(actor);
}

var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;
var stateName = actor.CurrentStateName;
LogWriter.LogDequeueEvent(actor.Id, stateName, e);
}

Expand All @@ -842,14 +842,14 @@ internal override void NotifyDefaultEventHandlerCheck(StateMachine actor)
/// <inheritdoc/>
internal override void NotifyRaisedEvent(StateMachine actor, Event e, EventInfo eventInfo)
{
var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;
var stateName = actor.CurrentStateName;
LogWriter.LogRaiseEvent(actor.Id, stateName, e);
}

/// <inheritdoc/>
internal override void NotifyHandleRaisedEvent(StateMachine actor, Event e)
{
var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;
var stateName = actor.CurrentStateName;
LogWriter.LogHandleRaisedEvent(actor.Id, stateName, e);
}

Expand All @@ -862,7 +862,7 @@ internal override void NotifyReceiveCalled(StateMachine actor)
/// <inheritdoc/>
internal override void NotifyReceivedEvent(StateMachine actor, Event e, EventInfo eventInfo)
{
var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;
var stateName = actor.CurrentStateName;
LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: true);
var op = Scheduler.GetOperationWithId<ActorOperation>(actor.Id.Value);
op.OnReceivedEvent();
Expand All @@ -871,7 +871,7 @@ internal override void NotifyReceivedEvent(StateMachine actor, Event e, EventInf
/// <inheritdoc/>
internal override void NotifyReceivedEventWithoutWaiting(StateMachine actor, Event e, EventInfo eventInfo)
{
var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;
var stateName = actor.CurrentStateName;
LogWriter.LogReceiveEvent(actor.Id, stateName, e, wasBlocked: false);
Scheduler.ScheduleNextEnabledOperation(AsyncOperationType.Receive);
ResetProgramCounter(actor);
Expand All @@ -897,7 +897,7 @@ internal override void NotifyWaitTask(StateMachine actor, Task task)
/// <inheritdoc/>
internal override void NotifyWaitEvent(StateMachine actor, IEnumerable<Type> eventTypes)
{
var stateName = actor is StateMachine stateMachine ? stateMachine.CurrentStateName : null;
var stateName = actor.CurrentStateName;
var op = Scheduler.GetOperationWithId<ActorOperation>(actor.Id.Value);
op.OnWaitEvent(eventTypes);

Expand Down Expand Up @@ -1005,32 +1005,19 @@ private void ReportActivityCoverageOfActor(StateMachine actor)
{
return;
}

if (actor is StateMachine stateMachine)

// Fetch states.
var states = actor.GetAllStates();
foreach (var state in states)
{
// Fetch states.
var states = stateMachine.GetAllStates();
foreach (var state in states)
{
CoverageInfo.DeclareMachineState(name, state);
}

// Fetch registered events.
var pairs = stateMachine.GetAllStateEventPairs();
foreach (var tup in pairs)
{
CoverageInfo.DeclareStateEvent(name, tup.Item1, tup.Item2);
}
CoverageInfo.DeclareMachineState(name, state);
}
else
{
var fakeStateName = actor.GetType().Name;
CoverageInfo.DeclareMachineState(name, fakeStateName);

foreach (var eventId in actor.GetAllRegisteredEvents())
{
CoverageInfo.DeclareStateEvent(name, fakeStateName, eventId);
}
// Fetch registered events.
var pairs = actor.GetAllStateEventPairs();
foreach (var tup in pairs)
{
CoverageInfo.DeclareStateEvent(name, tup.Item1, tup.Item2);
}
}

Expand Down

0 comments on commit 44a2831

Please sign in to comment.