Skip to content

Commit

Permalink
Removed push transitions and cleaned up the state machine code.
Browse files Browse the repository at this point in the history
  • Loading branch information
ankushdesai committed Aug 5, 2024
1 parent 298cb50 commit 1d95c31
Show file tree
Hide file tree
Showing 6 changed files with 61 additions and 500 deletions.
14 changes: 1 addition & 13 deletions Src/PChecker/CheckerCore/Actors/Actor.cs
Original file line number Diff line number Diff line change
Expand Up @@ -119,12 +119,6 @@ protected internal virtual Guid OperationGroupId
/// </summary>
protected JsonWriter JsonLogger => Runtime.JsonLogger;

/// <summary>
/// User-defined hashed state of the actor. Override to improve the
/// accuracy of stateful techniques during testing.
/// </summary>
protected virtual int HashedState => 0;

/// <summary>
/// Initializes a new instance of the <see cref="Actor"/> class.
/// </summary>
Expand Down Expand Up @@ -646,12 +640,6 @@ internal virtual int GetHashedState()
hash = (hash * 31) + Manager.GetCachedState();
hash = (hash * 31) + Inbox.GetCachedState();

if (this.HashedState != 0)
{
// Adds the user-defined hashed state.
hash = (hash * 31) + HashedState;
}

return hash;
}
}
Expand Down Expand Up @@ -808,7 +796,7 @@ private void AssertActionValidity(MethodInfo action)
}

/// <summary>
/// Returns the formatted strint to be used with a fair nondeterministic boolean choice.
/// Returns the formatted string to be used with a fair nondeterministic boolean choice.
/// </summary>
private protected virtual string FormatFairRandom(string callerMemberName, string callerFilePath, int callerLineNumber) =>
string.Format(CultureInfo.InvariantCulture, "{0}_{1}_{2}_{3}",
Expand Down
4 changes: 2 additions & 2 deletions Src/PChecker/CheckerCore/Actors/EventQueues/EventQueue.cs
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,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) : string.Empty;
NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty;
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 @@ -210,7 +210,7 @@ public EnqueueStatus Enqueue(Event e, Guid opGroupId, EventInfo info)
public void RaiseEvent(Event e, Guid opGroupId)
{
var stateName = Actor is StateMachine stateMachine ?
NameResolver.GetStateNameForLogging(stateMachine.CurrentState) : string.Empty;
NameResolver.GetStateNameForLogging(stateMachine.CurrentState.GetType()) : string.Empty;
var eventOrigin = new EventOriginInfo(Actor.Id, Actor.GetType().FullName, stateName);
var info = new EventInfo(e, eventOrigin);
RaisedEvent = (e, opGroupId, info);
Expand Down
5 changes: 0 additions & 5 deletions Src/PChecker/CheckerCore/Actors/NameResolver.cs
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,6 @@ internal static string GetQualifiedStateName(Type state)
var nextState = state;
while (nextState.DeclaringType != null)
{
if (!nextState.DeclaringType.IsSubclassOf(typeof(StateMachine.StateGroup)))
{
break;
}

name = string.Format(CultureInfo.InvariantCulture, "{0}.{1}", nextState.DeclaringType.Name, name);
nextState = nextState.DeclaringType;
}
Expand Down
Loading

0 comments on commit 1d95c31

Please sign in to comment.