How to use SetupEvent method of Microsoft.Coyote.Actors.BugFinding.Tests.Success class

Best Coyote code snippet using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent

ChainReplicationTests.cs

Source:ChainReplicationTests.cs

...51 if (i is 0)52 {53 server = this.CreateActor(54 typeof(ChainReplicationServer),55 new ChainReplicationServer.SetupEvent(i, true, false));56 }57 else if (i == this.NumOfServers - 1)58 {59 server = this.CreateActor(60 typeof(ChainReplicationServer),61 new ChainReplicationServer.SetupEvent(i, false, true));62 }63 else64 {65 server = this.CreateActor(66 typeof(ChainReplicationServer),67 new ChainReplicationServer.SetupEvent(i, false, false));68 }69 this.Servers.Add(server);70 }71 this.Monitor<InvariantMonitor>(72 new InvariantMonitor.SetupEvent(this.Servers));73 this.Monitor<ServerResponseSeqMonitor>(74 new ServerResponseSeqMonitor.SetupEvent(this.Servers));75 for (int i = 0; i < this.NumOfServers; i++)76 {77 ActorId pred;78 ActorId succ;79 if (i > 0)80 {81 pred = this.Servers[i - 1];82 }83 else84 {85 pred = this.Servers[0];86 }87 if (i < this.NumOfServers - 1)88 {89 succ = this.Servers[i + 1];90 }91 else92 {93 succ = this.Servers[this.NumOfServers - 1];94 }95 this.SendEvent(this.Servers[i], new ChainReplicationServer.PredSucc(pred, succ));96 }97 this.Clients.Add(this.CreateActor(typeof(Client),98 new Client.SetupEvent(0, this.Servers[0], this.Servers[this.NumOfServers - 1], 1)));99 this.Clients.Add(this.CreateActor(typeof(Client),100 new Client.SetupEvent(1, this.Servers[0], this.Servers[this.NumOfServers - 1], 100)));101 this.CreateActor(typeof(ChainReplicationMaster),102 new ChainReplicationMaster.SetupEvent(this.Servers, this.Clients));103 this.SendEvent(this.Id, HaltEvent.Instance);104 return Task.CompletedTask;105 }106 }107 private class FailureDetector : StateMachine108 {109 internal class SetupEvent : Event110 {111 public ActorId Main;112 public List<ActorId> Servers;113 public SetupEvent(ActorId main, List<ActorId> servers)114 : base()115 {116 this.Main = main;117 this.Servers = servers;118 }119 }120 internal class FailureDetected : Event121 {122 public ActorId Server;123 public FailureDetected(ActorId server)124 : base()125 {126 this.Server = server;127 }128 }129 internal class FailureCorrected : Event130 {131 public List<ActorId> Servers;132 public FailureCorrected(List<ActorId> servers)133 : base()134 {135 this.Servers = servers;136 }137 }138 internal class Ping : Event139 {140 public ActorId Target;141 public Ping(ActorId target)142 : base()143 {144 this.Target = target;145 }146 }147 internal class Pong : Event148 {149 }150 private class InjectFailure : Event151 {152 }153 private class Local : Event154 {155 }156 private ActorId Main;157 private List<ActorId> Servers;158 private int CheckNodeIdx;159 private int Failures;160 [Start]161 [OnEntry(nameof(InitOnEntry))]162 [OnEventGotoState(typeof(Local), typeof(StartMonitoring))]163 private class Init : State164 {165 }166 private void InitOnEntry(Event e)167 {168 this.Main = (e as SetupEvent).Main;169 this.Servers = (e as SetupEvent).Servers;170 this.CheckNodeIdx = 0;171 this.Failures = 100;172 this.RaiseEvent(new Local());173 }174 [OnEntry(nameof(StartMonitoringOnEntry))]175 [OnEventGotoState(typeof(Pong), typeof(StartMonitoring), nameof(HandlePong))]176 [OnEventGotoState(typeof(InjectFailure), typeof(HandleFailure))]177 private class StartMonitoring : State178 {179 }180 private void StartMonitoringOnEntry()181 {182 if (this.Failures < 1)183 {184 this.RaiseHaltEvent();185 }186 else187 {188 this.SendEvent(this.Servers[this.CheckNodeIdx], new Ping(this.Id));189 if (this.Servers.Count > 1)190 {191 if (this.RandomBoolean())192 {193 this.SendEvent(this.Id, new InjectFailure());194 }195 else196 {197 this.SendEvent(this.Id, new Pong());198 }199 }200 else201 {202 this.SendEvent(this.Id, new Pong());203 }204 this.Failures--;205 }206 }207 private void HandlePong()208 {209 this.CheckNodeIdx++;210 if (this.CheckNodeIdx == this.Servers.Count)211 {212 this.CheckNodeIdx = 0;213 }214 }215 [OnEntry(nameof(HandleFailureOnEntry))]216 [OnEventGotoState(typeof(FailureCorrected), typeof(StartMonitoring), nameof(ProcessFailureCorrected))]217 [IgnoreEvents(typeof(Pong), typeof(InjectFailure))]218 private class HandleFailure : State219 {220 }221 private void HandleFailureOnEntry()222 {223 this.SendEvent(this.Main, new FailureDetected(this.Servers[this.CheckNodeIdx]));224 }225 private void ProcessFailureCorrected(Event e)226 {227 this.CheckNodeIdx = 0;228 this.Servers = (e as FailureCorrected).Servers;229 }230 }231 private class ChainReplicationMaster : StateMachine232 {233 internal class SetupEvent : Event234 {235 public List<ActorId> Servers;236 public List<ActorId> Clients;237 public SetupEvent(List<ActorId> servers, List<ActorId> clients)238 : base()239 {240 this.Servers = servers;241 this.Clients = clients;242 }243 }244 internal class BecomeHead : Event245 {246 public ActorId Target;247 public BecomeHead(ActorId target)248 : base()249 {250 this.Target = target;251 }252 }253 internal class BecomeTail : Event254 {255 public ActorId Target;256 public BecomeTail(ActorId target)257 : base()258 {259 this.Target = target;260 }261 }262 internal class Success : Event263 {264 }265 internal class HeadChanged : Event266 {267 }268 internal class TailChanged : Event269 {270 }271 private class HeadFailed : Event272 {273 }274 private class TailFailed : Event275 {276 }277 private class ServerFailed : Event278 {279 }280 private class FixSuccessor : Event281 {282 }283 private class FixPredecessor : Event284 {285 }286 private class Local : Event287 {288 }289 private class Done : Event290 {291 }292 private List<ActorId> Servers;293 private List<ActorId> Clients;294 private ActorId FailureDetector;295 private ActorId Head;296 private ActorId Tail;297 private int FaultyNodeIndex;298 private int LastUpdateReceivedSucc;299 private int LastAckSent;300 [Start]301 [OnEntry(nameof(InitOnEntry))]302 [OnEventGotoState(typeof(Local), typeof(WaitForFailure))]303 private class Init : State304 {305 }306 private void InitOnEntry(Event e)307 {308 this.Servers = (e as SetupEvent).Servers;309 this.Clients = (e as SetupEvent).Clients;310 this.FailureDetector = this.CreateActor(311 typeof(FailureDetector),312 new FailureDetector.SetupEvent(this.Id, this.Servers));313 this.Head = this.Servers[0];314 this.Tail = this.Servers[this.Servers.Count - 1];315 this.RaiseEvent(new Local());316 }317 [OnEventGotoState(typeof(HeadFailed), typeof(CorrectHeadFailure))]318 [OnEventGotoState(typeof(TailFailed), typeof(CorrectTailFailure))]319 [OnEventGotoState(typeof(ServerFailed), typeof(CorrectServerFailure))]320 [OnEventDoAction(typeof(FailureDetector.FailureDetected), nameof(CheckWhichNodeFailed))]321 private class WaitForFailure : State322 {323 }324 private void CheckWhichNodeFailed(Event e)325 {326 this.Assert(this.Servers.Count > 1, "All nodes have failed.");327 var failedServer = (e as FailureDetector.FailureDetected).Server;328 if (this.Head.Equals(failedServer))329 {330 this.RaiseEvent(new HeadFailed());331 }332 else if (this.Tail.Equals(failedServer))333 {334 this.RaiseEvent(new TailFailed());335 }336 else337 {338 for (int i = 0; i < this.Servers.Count - 1; i++)339 {340 if (this.Servers[i].Equals(failedServer))341 {342 this.FaultyNodeIndex = i;343 }344 }345 this.RaiseEvent(new ServerFailed());346 }347 }348 [OnEntry(nameof(CorrectHeadFailureOnEntry))]349 [OnEventGotoState(typeof(Done), typeof(WaitForFailure), nameof(UpdateFailureDetector))]350 [OnEventDoAction(typeof(HeadChanged), nameof(UpdateClients))]351 private class CorrectHeadFailure : State352 {353 }354 private void CorrectHeadFailureOnEntry()355 {356 this.Servers.RemoveAt(0);357 this.Monitor<InvariantMonitor>(358 new InvariantMonitor.UpdateServers(this.Servers));359 this.Monitor<ServerResponseSeqMonitor>(360 new ServerResponseSeqMonitor.UpdateServers(this.Servers));361 this.Head = this.Servers[0];362 this.SendEvent(this.Head, new BecomeHead(this.Id));363 }364 private void UpdateClients()365 {366 for (int i = 0; i < this.Clients.Count; i++)367 {368 this.SendEvent(this.Clients[i], new Client.UpdateHeadTail(this.Head, this.Tail));369 }370 this.RaiseEvent(new Done());371 }372 private void UpdateFailureDetector()373 {374 this.SendEvent(this.FailureDetector, new FailureDetector.FailureCorrected(this.Servers));375 }376 [OnEntry(nameof(CorrectTailFailureOnEntry))]377 [OnEventGotoState(typeof(Done), typeof(WaitForFailure), nameof(UpdateFailureDetector))]378 [OnEventDoAction(typeof(TailChanged), nameof(UpdateClients))]379 private class CorrectTailFailure : State380 {381 }382 private void CorrectTailFailureOnEntry()383 {384 this.Servers.RemoveAt(this.Servers.Count - 1);385 this.Monitor<InvariantMonitor>(386 new InvariantMonitor.UpdateServers(this.Servers));387 this.Monitor<ServerResponseSeqMonitor>(388 new ServerResponseSeqMonitor.UpdateServers(this.Servers));389 this.Tail = this.Servers[this.Servers.Count - 1];390 this.SendEvent(this.Tail, new BecomeTail(this.Id));391 }392 [OnEntry(nameof(CorrectServerFailureOnEntry))]393 [OnEventGotoState(typeof(Done), typeof(WaitForFailure), nameof(UpdateFailureDetector))]394 [OnEventDoAction(typeof(FixSuccessor), nameof(UpdateClients))]395 [OnEventDoAction(typeof(FixPredecessor), nameof(ProcessFixPredecessor))]396 [OnEventDoAction(typeof(ChainReplicationServer.NewSuccInfo), nameof(SetLastUpdate))]397 [OnEventDoAction(typeof(Success), nameof(ProcessSuccess))]398 private class CorrectServerFailure : State399 {400 }401 private void CorrectServerFailureOnEntry()402 {403 this.Servers.RemoveAt(this.FaultyNodeIndex);404 this.Monitor<InvariantMonitor>(405 new InvariantMonitor.UpdateServers(this.Servers));406 this.Monitor<ServerResponseSeqMonitor>(407 new ServerResponseSeqMonitor.UpdateServers(this.Servers));408 this.RaiseEvent(new FixSuccessor());409 }410 private void ProcessFixPredecessor()411 {412 this.SendEvent(this.Servers[this.FaultyNodeIndex - 1], new ChainReplicationServer.NewSuccessor(413 this.Id, this.Servers[this.FaultyNodeIndex], this.LastAckSent, this.LastUpdateReceivedSucc));414 }415 private void SetLastUpdate(Event e)416 {417 this.LastUpdateReceivedSucc = (e as418 ChainReplicationServer.NewSuccInfo).LastUpdateReceivedSucc;419 this.LastAckSent = (e as420 ChainReplicationServer.NewSuccInfo).LastAckSent;421 this.RaiseEvent(new FixPredecessor());422 }423 private void ProcessSuccess() => this.RaiseEvent(new Done());424 }425 private class ChainReplicationServer : StateMachine426 {427 internal class SetupEvent : Event428 {429 public int Id;430 public bool IsHead;431 public bool IsTail;432 public SetupEvent(int id, bool isHead, bool isTail)433 : base()434 {435 this.Id = id;436 this.IsHead = isHead;437 this.IsTail = isTail;438 }439 }440 internal class PredSucc : Event441 {442 public ActorId Predecessor;443 public ActorId Successor;444 public PredSucc(ActorId pred, ActorId succ)445 : base()446 {447 this.Predecessor = pred;448 this.Successor = succ;449 }450 }451 internal class ForwardUpdate : Event452 {453 public ActorId Predecessor;454 public int NextSeqId;455 public ActorId Client;456 public int Key;457 public int Value;458 public ForwardUpdate(ActorId pred, int nextSeqId, ActorId client, int key, int val)459 : base()460 {461 this.Predecessor = pred;462 this.NextSeqId = nextSeqId;463 this.Client = client;464 this.Key = key;465 this.Value = val;466 }467 }468 internal class BackwardAck : Event469 {470 public int NextSeqId;471 public BackwardAck(int nextSeqId)472 : base()473 {474 this.NextSeqId = nextSeqId;475 }476 }477 internal class NewPredecessor : Event478 {479 public ActorId Main;480 public ActorId Predecessor;481 public NewPredecessor(ActorId main, ActorId pred)482 : base()483 {484 this.Main = main;485 this.Predecessor = pred;486 }487 }488 internal class NewSuccessor : Event489 {490 public ActorId Main;491 public ActorId Successor;492 public int LastUpdateReceivedSucc;493 public int LastAckSent;494 public NewSuccessor(ActorId main, ActorId succ,495 int lastUpdateReceivedSucc, int lastAckSent)496 : base()497 {498 this.Main = main;499 this.Successor = succ;500 this.LastUpdateReceivedSucc = lastUpdateReceivedSucc;501 this.LastAckSent = lastAckSent;502 }503 }504 internal class NewSuccInfo : Event505 {506 public int LastUpdateReceivedSucc;507 public int LastAckSent;508 public NewSuccInfo(int lastUpdateReceivedSucc, int lastAckSent)509 : base()510 {511 this.LastUpdateReceivedSucc = lastUpdateReceivedSucc;512 this.LastAckSent = lastAckSent;513 }514 }515 internal class ResponseToQuery : Event516 {517 public int Value;518 public ResponseToQuery(int val)519 : base()520 {521 this.Value = val;522 }523 }524 internal class ResponseToUpdate : Event525 {526 }527 private class Local : Event528 {529 }530 private int ServerId;531 private bool IsHead;532 private bool IsTail;533 private ActorId Predecessor;534 private ActorId Successor;535 private Dictionary<int, int> KeyValueStore;536 private List<int> History;537 private List<SentLog> SentHistory;538 private int NextSeqId;539 [Start]540 [OnEntry(nameof(InitOnEntry))]541 [OnEventGotoState(typeof(Local), typeof(WaitForRequest))]542 [OnEventDoAction(typeof(PredSucc), nameof(SetupPredSucc))]543 [DeferEvents(typeof(Client.Update), typeof(Client.Query),544 typeof(BackwardAck), typeof(ForwardUpdate))]545 private class Init : State546 {547 }548 private void InitOnEntry(Event e)549 {550 this.ServerId = (e as SetupEvent).Id;551 this.IsHead = (e as SetupEvent).IsHead;552 this.IsTail = (e as SetupEvent).IsTail;553 this.KeyValueStore = new Dictionary<int, int>();554 this.History = new List<int>();555 this.SentHistory = new List<SentLog>();556 this.NextSeqId = 0;557 }558 private void SetupPredSucc(Event e)559 {560 this.Predecessor = (e as PredSucc).Predecessor;561 this.Successor = (e as PredSucc).Successor;562 this.RaiseEvent(new Local());563 }564 [OnEventGotoState(typeof(Client.Update), typeof(ProcessUpdate), nameof(ProcessUpdateAction))]565 [OnEventGotoState(typeof(ForwardUpdate), typeof(ProcessFwdUpdate))]566 [OnEventGotoState(typeof(BackwardAck), typeof(ProcessBckAck))]567 [OnEventDoAction(typeof(Client.Query), nameof(ProcessQueryAction))]568 [OnEventDoAction(typeof(NewPredecessor), nameof(UpdatePredecessor))]569 [OnEventDoAction(typeof(NewSuccessor), nameof(UpdateSuccessor))]570 [OnEventDoAction(typeof(ChainReplicationMaster.BecomeHead), nameof(ProcessBecomeHead))]571 [OnEventDoAction(typeof(ChainReplicationMaster.BecomeTail), nameof(ProcessBecomeTail))]572 [OnEventDoAction(typeof(FailureDetector.Ping), nameof(SendPong))]573 private class WaitForRequest : State574 {575 }576 private void ProcessUpdateAction()577 {578 this.NextSeqId++;579 this.Assert(this.IsHead, "Server {0} is not head", this.ServerId);580 }581 private void ProcessQueryAction(Event e)582 {583 var client = (e as Client.Query).Client;584 var key = (e as Client.Query).Key;585 this.Assert(this.IsTail, "Server {0} is not tail", this.Id);586 if (this.KeyValueStore.ContainsKey(key))587 {588 this.Monitor<ServerResponseSeqMonitor>(new ServerResponseSeqMonitor.ResponseToQuery(589 this.Id, key, this.KeyValueStore[key]));590 this.SendEvent(client, new ResponseToQuery(this.KeyValueStore[key]));591 }592 else593 {594 this.SendEvent(client, new ResponseToQuery(-1));595 }596 }597 private void ProcessBecomeHead(Event e)598 {599 this.IsHead = true;600 this.Predecessor = this.Id;601 var target = (e as ChainReplicationMaster.BecomeHead).Target;602 this.SendEvent(target, new ChainReplicationMaster.HeadChanged());603 }604 private void ProcessBecomeTail(Event e)605 {606 this.IsTail = true;607 this.Successor = this.Id;608 for (int i = 0; i < this.SentHistory.Count; i++)609 {610 this.Monitor<ServerResponseSeqMonitor>(new ServerResponseSeqMonitor.ResponseToUpdate(611 this.Id, this.SentHistory[i].Key, this.SentHistory[i].Value));612 this.SendEvent(this.SentHistory[i].Client, new ResponseToUpdate());613 this.SendEvent(this.Predecessor, new BackwardAck(this.SentHistory[i].NextSeqId));614 }615 var target = (e as ChainReplicationMaster.BecomeTail).Target;616 this.SendEvent(target, new ChainReplicationMaster.TailChanged());617 }618 private void SendPong(Event e)619 {620 var target = (e as FailureDetector.Ping).Target;621 this.SendEvent(target, new FailureDetector.Pong());622 }623 private void UpdatePredecessor(Event e)624 {625 var main = (e as NewPredecessor).Main;626 this.Predecessor = (e as NewPredecessor).Predecessor;627 if (this.History.Count > 0)628 {629 if (this.SentHistory.Count > 0)630 {631 this.SendEvent(main, new NewSuccInfo(632 this.History[this.History.Count - 1],633 this.SentHistory[0].NextSeqId));634 }635 else636 {637 this.SendEvent(main, new NewSuccInfo(638 this.History[this.History.Count - 1],639 this.History[this.History.Count - 1]));640 }641 }642 }643 private void UpdateSuccessor(Event e)644 {645 var main = (e as NewSuccessor).Main;646 this.Successor = (e as NewSuccessor).Successor;647 var lastUpdateReceivedSucc = (e as NewSuccessor).LastUpdateReceivedSucc;648 var lastAckSent = (e as NewSuccessor).LastAckSent;649 if (this.SentHistory.Count > 0)650 {651 for (int i = 0; i < this.SentHistory.Count; i++)652 {653 if (this.SentHistory[i].NextSeqId > lastUpdateReceivedSucc)654 {655 this.SendEvent(this.Successor, new ForwardUpdate(this.Id, this.SentHistory[i].NextSeqId,656 this.SentHistory[i].Client, this.SentHistory[i].Key, this.SentHistory[i].Value));657 }658 }659 int tempIndex = -1;660 for (int i = this.SentHistory.Count - 1; i >= 0; i--)661 {662 if (this.SentHistory[i].NextSeqId == lastAckSent)663 {664 tempIndex = i;665 }666 }667 for (int i = 0; i < tempIndex; i++)668 {669 this.SendEvent(this.Predecessor, new BackwardAck(this.SentHistory[0].NextSeqId));670 this.SentHistory.RemoveAt(0);671 }672 }673 this.SendEvent(main, new ChainReplicationMaster.Success());674 }675 [OnEntry(nameof(ProcessUpdateOnEntry))]676 [OnEventGotoState(typeof(Local), typeof(WaitForRequest))]677 private class ProcessUpdate : State678 {679 }680 private void ProcessUpdateOnEntry(Event e)681 {682 var client = (e as Client.Update).Client;683 var key = (e as Client.Update).Key;684 var value = (e as Client.Update).Value;685 if (this.KeyValueStore.ContainsKey(key))686 {687 this.KeyValueStore[key] = value;688 }689 else690 {691 this.KeyValueStore.Add(key, value);692 }693 this.History.Add(this.NextSeqId);694 this.Monitor<InvariantMonitor>(695 new InvariantMonitor.HistoryUpdate(this.Id, new List<int>(this.History)));696 this.SentHistory.Add(new SentLog(this.NextSeqId, client, key, value));697 this.Monitor<InvariantMonitor>(698 new InvariantMonitor.SentUpdate(this.Id, new List<SentLog>(this.SentHistory)));699 this.SendEvent(this.Successor, new ForwardUpdate(this.Id, this.NextSeqId, client, key, value));700 this.RaiseEvent(new Local());701 }702 [OnEntry(nameof(ProcessFwdUpdateOnEntry))]703 [OnEventGotoState(typeof(Local), typeof(WaitForRequest))]704 private class ProcessFwdUpdate : State705 {706 }707 private void ProcessFwdUpdateOnEntry(Event e)708 {709 var pred = (e as ForwardUpdate).Predecessor;710 var nextSeqId = (e as ForwardUpdate).NextSeqId;711 var client = (e as ForwardUpdate).Client;712 var key = (e as ForwardUpdate).Key;713 var value = (e as ForwardUpdate).Value;714 if (pred.Equals(this.Predecessor))715 {716 this.NextSeqId = nextSeqId;717 if (this.KeyValueStore.ContainsKey(key))718 {719 this.KeyValueStore[key] = value;720 }721 else722 {723 this.KeyValueStore.Add(key, value);724 }725 if (!this.IsTail)726 {727 this.History.Add(nextSeqId);728 this.Monitor<InvariantMonitor>(729 new InvariantMonitor.HistoryUpdate(this.Id, new List<int>(this.History)));730 this.SentHistory.Add(new SentLog(this.NextSeqId, client, key, value));731 this.Monitor<InvariantMonitor>(732 new InvariantMonitor.SentUpdate(this.Id, new List<SentLog>(this.SentHistory)));733 this.SendEvent(this.Successor, new ForwardUpdate(this.Id, this.NextSeqId, client, key, value));734 }735 else736 {737 if (!this.IsHead)738 {739 this.History.Add(nextSeqId);740 }741 this.Monitor<ServerResponseSeqMonitor>(new ServerResponseSeqMonitor.ResponseToUpdate(742 this.Id, key, value));743 this.SendEvent(client, new ResponseToUpdate());744 this.SendEvent(this.Predecessor, new BackwardAck(nextSeqId));745 }746 }747 this.RaiseEvent(new Local());748 }749 [OnEntry(nameof(ProcessBckAckOnEntry))]750 [OnEventGotoState(typeof(Local), typeof(WaitForRequest))]751 private class ProcessBckAck : State752 {753 }754 private void ProcessBckAckOnEntry(Event e)755 {756 var nextSeqId = (e as BackwardAck).NextSeqId;757 this.RemoveItemFromSent(nextSeqId);758 if (!this.IsHead)759 {760 this.SendEvent(this.Predecessor, new BackwardAck(nextSeqId));761 }762 this.RaiseEvent(new Local());763 }764 private void RemoveItemFromSent(int seqId)765 {766 int removeIdx = -1;767 for (int i = this.SentHistory.Count - 1; i >= 0; i--)768 {769 if (seqId == this.SentHistory[i].NextSeqId)770 {771 removeIdx = i;772 }773 }774 if (removeIdx != -1)775 {776 this.SentHistory.RemoveAt(removeIdx);777 }778 }779 }780 private class Client : StateMachine781 {782 internal class SetupEvent : Event783 {784 public int Id;785 public ActorId HeadNode;786 public ActorId TailNode;787 public int Value;788 public SetupEvent(int id, ActorId head, ActorId tail, int val)789 : base()790 {791 this.Id = id;792 this.HeadNode = head;793 this.TailNode = tail;794 this.Value = val;795 }796 }797 internal class UpdateHeadTail : Event798 {799 public ActorId Head;800 public ActorId Tail;801 public UpdateHeadTail(ActorId head, ActorId tail)802 : base()803 {804 this.Head = head;805 this.Tail = tail;806 }807 }808 internal class Update : Event809 {810 public ActorId Client;811 public int Key;812 public int Value;813 public Update(ActorId client, int key, int value)814 : base()815 {816 this.Client = client;817 this.Key = key;818 this.Value = value;819 }820 }821 internal class Query : Event822 {823 public ActorId Client;824 public int Key;825 public Query(ActorId client, int key)826 : base()827 {828 this.Client = client;829 this.Key = key;830 }831 }832 private class Local : Event833 {834 }835 private class Done : Event836 {837 }838 private ActorId HeadNode;839 private ActorId TailNode;840 private int StartIn;841 private int Next;842 private Dictionary<int, int> KeyValueStore;843 [Start]844 [OnEntry(nameof(InitOnEntry))]845 [OnEventGotoState(typeof(Local), typeof(PumpUpdateRequests))]846 private class Init : State847 {848 }849 private void InitOnEntry(Event e)850 {851 this.HeadNode = (e as SetupEvent).HeadNode;852 this.TailNode = (e as SetupEvent).TailNode;853 this.StartIn = (e as SetupEvent).Value;854 this.Next = 1;855 this.KeyValueStore = new Dictionary<int, int>856 {857 { 1 * this.StartIn, 100 },858 { 2 * this.StartIn, 200 },859 { 3 * this.StartIn, 300 },860 { 4 * this.StartIn, 400 }861 };862 this.RaiseEvent(new Local());863 }864 [OnEntry(nameof(PumpUpdateRequestsOnEntry))]865 [OnEventGotoState(typeof(Local), typeof(PumpUpdateRequests), nameof(PumpRequestsLocalAction))]866 [OnEventGotoState(typeof(Done), typeof(PumpQueryRequests), nameof(PumpRequestsDoneAction))]867 [IgnoreEvents(typeof(ChainReplicationServer.ResponseToUpdate), typeof(ChainReplicationServer.ResponseToQuery))]868 private class PumpUpdateRequests : State869 {870 }871 private void PumpUpdateRequestsOnEntry()872 {873 this.SendEvent(this.HeadNode, new Update(this.Id, this.Next * this.StartIn,874 this.KeyValueStore[this.Next * this.StartIn]));875 if (this.Next >= 3)876 {877 this.RaiseEvent(new Done());878 }879 else880 {881 this.RaiseEvent(new Local());882 }883 }884 [OnEntry(nameof(PumpQueryRequestsOnEntry))]885 [OnEventGotoState(typeof(Local), typeof(PumpQueryRequests), nameof(PumpRequestsLocalAction))]886 [IgnoreEvents(typeof(ChainReplicationServer.ResponseToUpdate), typeof(ChainReplicationServer.ResponseToQuery))]887 private class PumpQueryRequests : State888 {889 }890 private void PumpQueryRequestsOnEntry()891 {892 this.SendEvent(this.TailNode, new Query(this.Id, this.Next * this.StartIn));893 if (this.Next >= 3)894 {895 this.RaiseHaltEvent();896 }897 else898 {899 this.RaiseEvent(new Local());900 }901 }902 private void PumpRequestsLocalAction()903 {904 this.Next++;905 }906 private void PumpRequestsDoneAction()907 {908 this.Next = 1;909 }910 }911 private class InvariantMonitor : Monitor912 {913 internal class SetupEvent : Event914 {915 public List<ActorId> Servers;916 public SetupEvent(List<ActorId> servers)917 : base()918 {919 this.Servers = servers;920 }921 }922 internal class UpdateServers : Event923 {924 public List<ActorId> Servers;925 public UpdateServers(List<ActorId> servers)926 : base()927 {928 this.Servers = servers;929 }930 }931 internal class HistoryUpdate : Event932 {933 public ActorId Server;934 public List<int> History;935 public HistoryUpdate(ActorId server, List<int> history)936 : base()937 {938 this.Server = server;939 this.History = history;940 }941 }942 internal class SentUpdate : Event943 {944 public ActorId Server;945 public List<SentLog> SentHistory;946 public SentUpdate(ActorId server, List<SentLog> sentHistory)947 : base()948 {949 this.Server = server;950 this.SentHistory = sentHistory;951 }952 }953 private class Local : Event954 {955 }956 private List<ActorId> Servers;957 private Dictionary<ActorId, List<int>> History;958 private Dictionary<ActorId, List<int>> SentHistory;959 private List<int> TempSeq;960 private ActorId Next;961 private ActorId Prev;962 [Start]963 [OnEventGotoState(typeof(Local), typeof(WaitForUpdateMessage))]964 [OnEventDoAction(typeof(SetupEvent), nameof(Setup))]965 private class Init : State966 {967 }968 private void Setup(Event e)969 {970 this.Servers = (e as SetupEvent).Servers;971 this.History = new Dictionary<ActorId, List<int>>();972 this.SentHistory = new Dictionary<ActorId, List<int>>();973 this.TempSeq = new List<int>();974 this.RaiseEvent(new Local());975 }976 [OnEventDoAction(typeof(HistoryUpdate), nameof(CheckUpdatePropagationInvariant))]977 [OnEventDoAction(typeof(SentUpdate), nameof(CheckInprocessRequestsInvariant))]978 [OnEventDoAction(typeof(UpdateServers), nameof(ProcessUpdateServers))]979 private class WaitForUpdateMessage : State980 {981 }982 private void CheckUpdatePropagationInvariant(Event e)983 {984 var server = (e as HistoryUpdate).Server;985 var history = (e as HistoryUpdate).History;986 this.IsSorted(history);987 if (this.History.ContainsKey(server))988 {989 this.History[server] = history;990 }991 else992 {993 this.History.Add(server, history);994 }995 /​/​ HIST(i+1) <= HIST(i)996 this.GetNext(server);997 if (this.Next != null && this.History.ContainsKey(this.Next))998 {999 this.CheckLessOrEqualThan(this.History[this.Next], this.History[server]);1000 }1001 /​/​ HIST(i) <= HIST(i-1)1002 this.GetPrev(server);1003 if (this.Prev != null && this.History.ContainsKey(this.Prev))1004 {1005 this.CheckLessOrEqualThan(this.History[server], this.History[this.Prev]);1006 }1007 }1008 private void CheckInprocessRequestsInvariant(Event e)1009 {1010 this.ClearTempSeq();1011 var server = (e as SentUpdate).Server;1012 var sentHistory = (e as SentUpdate).SentHistory;1013 this.ExtractSeqId(sentHistory);1014 if (this.SentHistory.ContainsKey(server))1015 {1016 this.SentHistory[server] = this.TempSeq;1017 }1018 else1019 {1020 this.SentHistory.Add(server, this.TempSeq);1021 }1022 this.ClearTempSeq();1023 /​/​ HIST(i) == HIST(i+1) + SENT(i)1024 this.GetNext(server);1025 if (this.Next != null && this.History.ContainsKey(this.Next))1026 {1027 this.MergeSeq(this.History[this.Next], this.SentHistory[server]);1028 this.CheckEqual(this.History[server], this.TempSeq);1029 }1030 this.ClearTempSeq();1031 /​/​ HIST(i-1) == HIST(i) + SENT(i-1)1032 this.GetPrev(server);1033 if (this.Prev != null && this.History.ContainsKey(this.Prev))1034 {1035 this.MergeSeq(this.History[server], this.SentHistory[this.Prev]);1036 this.CheckEqual(this.History[this.Prev], this.TempSeq);1037 }1038 this.ClearTempSeq();1039 }1040 private void GetNext(ActorId curr)1041 {1042 this.Next = null;1043 for (int i = 1; i < this.Servers.Count; i++)1044 {1045 if (this.Servers[i - 1].Equals(curr))1046 {1047 this.Next = this.Servers[i];1048 }1049 }1050 }1051 private void GetPrev(ActorId curr)1052 {1053 this.Prev = null;1054 for (int i = 1; i < this.Servers.Count; i++)1055 {1056 if (this.Servers[i].Equals(curr))1057 {1058 this.Prev = this.Servers[i - 1];1059 }1060 }1061 }1062 private void ExtractSeqId(List<SentLog> seq)1063 {1064 this.ClearTempSeq();1065 for (int i = seq.Count - 1; i >= 0; i--)1066 {1067 if (this.TempSeq.Count > 0)1068 {1069 this.TempSeq.Insert(0, seq[i].NextSeqId);1070 }1071 else1072 {1073 this.TempSeq.Add(seq[i].NextSeqId);1074 }1075 }1076 this.IsSorted(this.TempSeq);1077 }1078 private void MergeSeq(List<int> seq1, List<int> seq2)1079 {1080 this.ClearTempSeq();1081 this.IsSorted(seq1);1082 if (seq1.Count is 0)1083 {1084 this.TempSeq = seq2;1085 }1086 else if (seq2.Count is 0)1087 {1088 this.TempSeq = seq1;1089 }1090 else1091 {1092 for (int i = 0; i < seq1.Count; i++)1093 {1094 if (seq1[i] < seq2[0])1095 {1096 this.TempSeq.Add(seq1[i]);1097 }1098 }1099 for (int i = 0; i < seq2.Count; i++)1100 {1101 this.TempSeq.Add(seq2[i]);1102 }1103 }1104 this.IsSorted(this.TempSeq);1105 }1106 private void IsSorted(List<int> seq)1107 {1108 for (int i = 0; i < seq.Count - 1; i++)1109 {1110 this.Assert(seq[i] < seq[i + 1], "Sequence is not sorted.");1111 }1112 }1113 private void CheckLessOrEqualThan(List<int> seq1, List<int> seq2)1114 {1115 this.IsSorted(seq1);1116 this.IsSorted(seq2);1117 for (int i = 0; i < seq1.Count; i++)1118 {1119 if ((i == seq1.Count) || (i == seq2.Count))1120 {1121 break;1122 }1123 this.Assert(seq1[i] <= seq2[i], "{0} not less or equal than {1}.", seq1[i], seq2[i]);1124 }1125 }1126 private void CheckEqual(List<int> seq1, List<int> seq2)1127 {1128 this.IsSorted(seq1);1129 this.IsSorted(seq2);1130 for (int i = 0; i < seq1.Count; i++)1131 {1132 if ((i == seq1.Count) || (i == seq2.Count))1133 {1134 break;1135 }1136 this.Assert(seq1[i] == seq2[i], "{0} not equal with {1}.", seq1[i], seq2[i]);1137 }1138 }1139 private void ClearTempSeq()1140 {1141 this.Assert(this.TempSeq.Count <= 6, "Temp sequence has more than 6 elements.");1142 this.TempSeq.Clear();1143 this.Assert(this.TempSeq.Count is 0, "Temp sequence is not cleared.");1144 }1145 private void ProcessUpdateServers(Event e)1146 {1147 this.Servers = (e as UpdateServers).Servers;1148 }1149 }1150 private class ServerResponseSeqMonitor : Monitor1151 {1152 internal class SetupEvent : Event1153 {1154 public List<ActorId> Servers;1155 public SetupEvent(List<ActorId> servers)1156 : base()1157 {1158 this.Servers = servers;1159 }1160 }1161 internal class UpdateServers : Event1162 {1163 public List<ActorId> Servers;1164 public UpdateServers(List<ActorId> servers)1165 : base()1166 {1167 this.Servers = servers;1168 }1169 }1170 internal class ResponseToUpdate : Event1171 {1172 public ActorId Tail;1173 public int Key;1174 public int Value;1175 public ResponseToUpdate(ActorId tail, int key, int val)1176 : base()1177 {1178 this.Tail = tail;1179 this.Key = key;1180 this.Value = val;1181 }1182 }1183 internal class ResponseToQuery : Event1184 {1185 public ActorId Tail;1186 public int Key;1187 public int Value;1188 public ResponseToQuery(ActorId tail, int key, int val)1189 : base()1190 {1191 this.Tail = tail;1192 this.Key = key;1193 this.Value = val;1194 }1195 }1196 private class Local : Event1197 {1198 }1199 private List<ActorId> Servers;1200 private Dictionary<int, int> LastUpdateResponse;1201 [Start]1202 [OnEventGotoState(typeof(Local), typeof(Wait))]1203 [OnEventDoAction(typeof(SetupEvent), nameof(Setup))]1204 private class Init : State1205 {1206 }1207 private void Setup(Event e)1208 {1209 this.Servers = (e as SetupEvent).Servers;1210 this.LastUpdateResponse = new Dictionary<int, int>();1211 this.RaiseEvent(new Local());1212 }1213 [OnEventDoAction(typeof(ResponseToUpdate), nameof(ResponseToUpdateAction))]1214 [OnEventDoAction(typeof(ResponseToQuery), nameof(ResponseToQueryAction))]1215 [OnEventDoAction(typeof(UpdateServers), nameof(ProcessUpdateServers))]1216 private class Wait : State1217 {1218 }1219 private void ResponseToUpdateAction(Event e)1220 {1221 var tail = (e as ResponseToUpdate).Tail;1222 var key = (e as ResponseToUpdate).Key;1223 var value = (e as ResponseToUpdate).Value;...

RaftTests.cs

Source:RaftTests.cs

...324 /​/​/​ </​summary>325 private Client.Request LastClientRequest;326 [Start]327 [OnEntry(nameof(EntryOnInit))]328 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]329 [OnEventGotoState(typeof(BecomeFollower), typeof(Follower))]330 [DeferEvents(typeof(VoteRequest), typeof(AppendEntriesRequest))]331 private class Init : State332 {333 }334 private void EntryOnInit()335 {336 this.CurrentTerm = 0;337 this.LeaderId = null;338 this.VotedFor = null;339 this.Logs = new List<Log>();340 this.CommitIndex = 0;341 this.LastApplied = 0;342 this.NextIndex = new Dictionary<ActorId, int>();343 this.MatchIndex = new Dictionary<ActorId, int>();344 }345 private void SetupEvent(Event e)346 {347 this.ServerId = (e as ConfigureEvent).Id;348 this.Servers = (e as ConfigureEvent).Servers;349 this.ClusterManager = (e as ConfigureEvent).ClusterManager;350 this.ElectionTimer = this.CreateActor(typeof(ElectionTimer));351 this.SendEvent(this.ElectionTimer, new ElectionTimer.ConfigureEvent(this.Id));352 this.PeriodicTimer = this.CreateActor(typeof(PeriodicTimer));353 this.SendEvent(this.PeriodicTimer, new PeriodicTimer.ConfigureEvent(this.Id));354 this.RaiseEvent(new BecomeFollower());355 }356 [OnEntry(nameof(FollowerOnInit))]357 [OnEventDoAction(typeof(Client.Request), nameof(RedirectClientRequest))]358 [OnEventDoAction(typeof(VoteRequest), nameof(VoteAsFollower))]359 [OnEventDoAction(typeof(VoteResponse), nameof(RespondVoteAsFollower))]360 [OnEventDoAction(typeof(AppendEntriesRequest), nameof(AppendEntriesAsFollower))]361 [OnEventDoAction(typeof(AppendEntriesResponse), nameof(RespondAppendEntriesAsFollower))]362 [OnEventDoAction(typeof(ElectionTimer.Timeout), nameof(StartLeaderElection))]363 [OnEventDoAction(typeof(ShutDown), nameof(ShuttingDown))]364 [OnEventGotoState(typeof(BecomeFollower), typeof(Follower))]365 [OnEventGotoState(typeof(BecomeCandidate), typeof(Candidate))]366 [IgnoreEvents(typeof(PeriodicTimer.Timeout))]367 private class Follower : State368 {369 }370 private void FollowerOnInit()371 {372 this.LeaderId = null;373 this.VotesReceived = 0;374 this.SendEvent(this.ElectionTimer, new ElectionTimer.StartTimerEvent());375 }376 private void RedirectClientRequest(Event e)377 {378 if (this.LeaderId != null)379 {380 this.SendEvent(this.LeaderId, e);381 }382 else383 {384 this.SendEvent(this.ClusterManager, new ClusterManager.RedirectRequest(e));385 }386 }387 private void StartLeaderElection()388 {389 this.RaiseEvent(new BecomeCandidate());390 }391 private void VoteAsFollower(Event e)392 {393 var request = e as VoteRequest;394 if (request.Term > this.CurrentTerm)395 {396 this.CurrentTerm = request.Term;397 this.VotedFor = null;398 }399 this.Vote(e as VoteRequest);400 }401 private void RespondVoteAsFollower(Event e)402 {403 var request = e as VoteResponse;404 if (request.Term > this.CurrentTerm)405 {406 this.CurrentTerm = request.Term;407 this.VotedFor = null;408 }409 }410 private void AppendEntriesAsFollower(Event e)411 {412 var request = e as AppendEntriesRequest;413 if (request.Term > this.CurrentTerm)414 {415 this.CurrentTerm = request.Term;416 this.VotedFor = null;417 }418 this.AppendEntries(e as AppendEntriesRequest);419 }420 private void RespondAppendEntriesAsFollower(Event e)421 {422 var request = e as AppendEntriesResponse;423 if (request.Term > this.CurrentTerm)424 {425 this.CurrentTerm = request.Term;426 this.VotedFor = null;427 }428 }429 [OnEntry(nameof(CandidateOnInit))]430 [OnEventDoAction(typeof(Client.Request), nameof(RedirectClientRequest))]431 [OnEventDoAction(typeof(VoteRequest), nameof(VoteAsCandidate))]432 [OnEventDoAction(typeof(VoteResponse), nameof(RespondVoteAsCandidate))]433 [OnEventDoAction(typeof(AppendEntriesRequest), nameof(AppendEntriesAsCandidate))]434 [OnEventDoAction(typeof(AppendEntriesResponse), nameof(RespondAppendEntriesAsCandidate))]435 [OnEventDoAction(typeof(ElectionTimer.Timeout), nameof(StartLeaderElection))]436 [OnEventDoAction(typeof(PeriodicTimer.Timeout), nameof(BroadcastVoteRequests))]437 [OnEventDoAction(typeof(ShutDown), nameof(ShuttingDown))]438 [OnEventGotoState(typeof(BecomeLeader), typeof(Leader))]439 [OnEventGotoState(typeof(BecomeFollower), typeof(Follower))]440 [OnEventGotoState(typeof(BecomeCandidate), typeof(Candidate))]441 private class Candidate : State442 {443 }444 private void CandidateOnInit()445 {446 this.CurrentTerm++;447 this.VotedFor = this.Id;448 this.VotesReceived = 1;449 this.SendEvent(this.ElectionTimer, new ElectionTimer.StartTimerEvent());450 this.BroadcastVoteRequests();451 }452 private void BroadcastVoteRequests()453 {454 /​/​ BUG: duplicate votes from same follower455 this.SendEvent(this.PeriodicTimer, new PeriodicTimer.StartTimerEvent());456 for (int idx = 0; idx < this.Servers.Length; idx++)457 {458 if (idx == this.ServerId)459 {460 continue;461 }462 var lastLogIndex = this.Logs.Count;463 var lastLogTerm = this.GetLogTermForIndex(lastLogIndex);464 this.SendEvent(this.Servers[idx], new VoteRequest(this.CurrentTerm, this.Id,465 lastLogIndex, lastLogTerm));466 }467 }468 private void VoteAsCandidate(Event e)469 {470 var request = e as VoteRequest;471 if (request.Term > this.CurrentTerm)472 {473 this.CurrentTerm = request.Term;474 this.VotedFor = null;475 this.Vote(e as VoteRequest);476 this.RaiseEvent(new BecomeFollower());477 }478 else479 {480 this.Vote(e as VoteRequest);481 }482 }483 private void RespondVoteAsCandidate(Event e)484 {485 var request = e as VoteResponse;486 if (request.Term > this.CurrentTerm)487 {488 this.CurrentTerm = request.Term;489 this.VotedFor = null;490 this.RaiseEvent(new BecomeFollower());491 }492 else if (request.Term != this.CurrentTerm)493 {494 return;495 }496 if (request.VoteGranted)497 {498 this.VotesReceived++;499 if (this.VotesReceived >= (this.Servers.Length /​ 2) + 1)500 {501 this.VotesReceived = 0;502 this.RaiseEvent(new BecomeLeader());503 }504 }505 }506 private void AppendEntriesAsCandidate(Event e)507 {508 var request = e as AppendEntriesRequest;509 if (request.Term > this.CurrentTerm)510 {511 this.CurrentTerm = request.Term;512 this.VotedFor = null;513 this.AppendEntries(e as AppendEntriesRequest);514 this.RaiseEvent(new BecomeFollower());515 }516 else517 {518 this.AppendEntries(e as AppendEntriesRequest);519 }520 }521 private void RespondAppendEntriesAsCandidate(Event e)522 {523 var request = e as AppendEntriesResponse;524 if (request.Term > this.CurrentTerm)525 {526 this.CurrentTerm = request.Term;527 this.VotedFor = null;528 this.RaiseEvent(new BecomeFollower());529 }530 }531 [OnEntry(nameof(LeaderOnInit))]532 [OnEventDoAction(typeof(Client.Request), nameof(ProcessClientRequest))]533 [OnEventDoAction(typeof(VoteRequest), nameof(VoteAsLeader))]534 [OnEventDoAction(typeof(VoteResponse), nameof(RespondVoteAsLeader))]535 [OnEventDoAction(typeof(AppendEntriesRequest), nameof(AppendEntriesAsLeader))]536 [OnEventDoAction(typeof(AppendEntriesResponse), nameof(RespondAppendEntriesAsLeader))]537 [OnEventDoAction(typeof(ShutDown), nameof(ShuttingDown))]538 [OnEventGotoState(typeof(BecomeFollower), typeof(Follower))]539 [IgnoreEvents(typeof(ElectionTimer.Timeout), typeof(PeriodicTimer.Timeout))]540 private class Leader : State541 {542 }543 private void LeaderOnInit()544 {545 this.Monitor<SafetyMonitor>(new SafetyMonitor.NotifyLeaderElected(this.CurrentTerm));546 this.SendEvent(this.ClusterManager, new ClusterManager.NotifyLeaderUpdate(this.Id, this.CurrentTerm));547 var logIndex = this.Logs.Count;548 var logTerm = this.GetLogTermForIndex(logIndex);549 this.NextIndex.Clear();550 this.MatchIndex.Clear();551 for (int idx = 0; idx < this.Servers.Length; idx++)552 {553 if (idx == this.ServerId)554 {555 continue;556 }557 this.NextIndex.Add(this.Servers[idx], logIndex + 1);558 this.MatchIndex.Add(this.Servers[idx], 0);559 }560 for (int idx = 0; idx < this.Servers.Length; idx++)561 {562 if (idx == this.ServerId)563 {564 continue;565 }566 this.SendEvent(this.Servers[idx], new AppendEntriesRequest(this.CurrentTerm, this.Id,567 logIndex, logTerm, new List<Log>(), this.CommitIndex, null));568 }569 }570 private void ProcessClientRequest(Event e)571 {572 this.LastClientRequest = e as Client.Request;573 var log = new Log(this.CurrentTerm, this.LastClientRequest.Command);574 this.Logs.Add(log);575 this.BroadcastLastClientRequest();576 }577 private void BroadcastLastClientRequest()578 {579 var lastLogIndex = this.Logs.Count;580 this.VotesReceived = 1;581 for (int idx = 0; idx < this.Servers.Length; idx++)582 {583 if (idx == this.ServerId)584 {585 continue;586 }587 var server = this.Servers[idx];588 if (lastLogIndex < this.NextIndex[server])589 {590 continue;591 }592 var logs = this.Logs.GetRange(this.NextIndex[server] - 1, this.Logs.Count - (this.NextIndex[server] - 1));593 var prevLogIndex = this.NextIndex[server] - 1;594 var prevLogTerm = this.GetLogTermForIndex(prevLogIndex);595 this.SendEvent(server, new AppendEntriesRequest(this.CurrentTerm, this.Id, prevLogIndex,596 prevLogTerm, logs, this.CommitIndex, this.LastClientRequest.Client));597 }598 }599 private void VoteAsLeader(Event e)600 {601 var request = e as VoteRequest;602 if (request.Term > this.CurrentTerm)603 {604 this.CurrentTerm = request.Term;605 this.VotedFor = null;606 this.RedirectLastClientRequestToClusterManager();607 this.Vote(e as VoteRequest);608 this.RaiseEvent(new BecomeFollower());609 }610 else611 {612 this.Vote(e as VoteRequest);613 }614 }615 private void RespondVoteAsLeader(Event e)616 {617 var request = e as VoteResponse;618 if (request.Term > this.CurrentTerm)619 {620 this.CurrentTerm = request.Term;621 this.VotedFor = null;622 this.RedirectLastClientRequestToClusterManager();623 this.RaiseEvent(new BecomeFollower());624 }625 }626 private void AppendEntriesAsLeader(Event e)627 {628 var request = e as AppendEntriesRequest;629 if (request.Term > this.CurrentTerm)630 {631 this.CurrentTerm = request.Term;632 this.VotedFor = null;633 this.RedirectLastClientRequestToClusterManager();634 this.AppendEntries(e as AppendEntriesRequest);635 this.RaiseEvent(new BecomeFollower());636 }637 }638 private void RespondAppendEntriesAsLeader(Event e)639 {640 var request = e as AppendEntriesResponse;641 if (request.Term > this.CurrentTerm)642 {643 this.CurrentTerm = request.Term;644 this.VotedFor = null;645 this.RedirectLastClientRequestToClusterManager();646 this.RaiseEvent(new BecomeFollower());647 }648 else if (request.Term != this.CurrentTerm)649 {650 return;651 }652 if (request.Success)653 {654 this.NextIndex[request.Server] = this.Logs.Count + 1;655 this.MatchIndex[request.Server] = this.Logs.Count;656 this.VotesReceived++;657 if (request.ReceiverEndpoint != null &&658 this.VotesReceived >= (this.Servers.Length /​ 2) + 1)659 {660 var commitIndex = this.MatchIndex[request.Server];661 if (commitIndex > this.CommitIndex &&662 this.Logs[commitIndex - 1].Term == this.CurrentTerm)663 {664 this.CommitIndex = commitIndex;665 }666 this.VotesReceived = 0;667 this.LastClientRequest = null;668 this.SendEvent(request.ReceiverEndpoint, new Client.Response());669 }670 }671 else672 {673 if (this.NextIndex[request.Server] > 1)674 {675 this.NextIndex[request.Server] = this.NextIndex[request.Server] - 1;676 }677 var logs = this.Logs.GetRange(this.NextIndex[request.Server] - 1, this.Logs.Count - (this.NextIndex[request.Server] - 1));678 var prevLogIndex = this.NextIndex[request.Server] - 1;679 var prevLogTerm = this.GetLogTermForIndex(prevLogIndex);680 this.SendEvent(request.Server, new AppendEntriesRequest(this.CurrentTerm, this.Id, prevLogIndex,681 prevLogTerm, logs, this.CommitIndex, request.ReceiverEndpoint));682 }683 }684 /​/​/​ <summary>685 /​/​/​ Processes the given vote request.686 /​/​/​ </​summary>687 /​/​/​ <param name="request">VoteRequest.</​param>688 private void Vote(VoteRequest request)689 {690 var lastLogIndex = this.Logs.Count;691 var lastLogTerm = this.GetLogTermForIndex(lastLogIndex);692 if (request.Term < this.CurrentTerm ||693 (this.VotedFor != null && this.VotedFor != request.CandidateId) ||694 lastLogIndex > request.LastLogIndex ||695 lastLogTerm > request.LastLogTerm)696 {697 this.SendEvent(request.CandidateId, new VoteResponse(this.CurrentTerm, false));698 }699 else700 {701 this.VotedFor = request.CandidateId;702 this.LeaderId = null;703 this.SendEvent(request.CandidateId, new VoteResponse(this.CurrentTerm, true));704 }705 }706 /​/​/​ <summary>707 /​/​/​ Processes the given append entries request.708 /​/​/​ </​summary>709 /​/​/​ <param name="request">AppendEntriesRequest.</​param>710 private void AppendEntries(AppendEntriesRequest request)711 {712 if (request.Term < this.CurrentTerm)713 {714 this.SendEvent(request.LeaderId, new AppendEntriesResponse(this.CurrentTerm, false,715 this.Id, request.ReceiverEndpoint));716 }717 else718 {719 if (request.PrevLogIndex > 0 &&720 (this.Logs.Count < request.PrevLogIndex ||721 this.Logs[request.PrevLogIndex - 1].Term != request.PrevLogTerm))722 {723 this.SendEvent(request.LeaderId, new AppendEntriesResponse(this.CurrentTerm, false, this.Id, request.ReceiverEndpoint));724 }725 else726 {727 if (request.Entries.Count > 0)728 {729 var currentIndex = request.PrevLogIndex + 1;730 foreach (var entry in request.Entries)731 {732 if (this.Logs.Count < currentIndex)733 {734 this.Logs.Add(entry);735 }736 else if (this.Logs[currentIndex - 1].Term != entry.Term)737 {738 this.Logs.RemoveRange(currentIndex - 1, this.Logs.Count - (currentIndex - 1));739 this.Logs.Add(entry);740 }741 currentIndex++;742 }743 }744 if (request.LeaderCommit > this.CommitIndex &&745 this.Logs.Count < request.LeaderCommit)746 {747 this.CommitIndex = this.Logs.Count;748 }749 else if (request.LeaderCommit > this.CommitIndex)750 {751 this.CommitIndex = request.LeaderCommit;752 }753 if (this.CommitIndex > this.LastApplied)754 {755 this.LastApplied++;756 }757 this.LeaderId = request.LeaderId;758 this.SendEvent(request.LeaderId, new AppendEntriesResponse(this.CurrentTerm, true, this.Id, request.ReceiverEndpoint));759 }760 }761 }762 private void RedirectLastClientRequestToClusterManager()763 {764 if (this.LastClientRequest != null)765 {766 this.SendEvent(this.ClusterManager, this.LastClientRequest);767 }768 }769 /​/​/​ <summary>770 /​/​/​ Returns the log term for the given log index.771 /​/​/​ </​summary>772 /​/​/​ <param name="logIndex">Index.</​param>773 /​/​/​ <returns>Term.</​returns>774 private int GetLogTermForIndex(int logIndex)775 {776 var logTerm = 0;777 if (logIndex > 0)778 {779 logTerm = this.Logs[logIndex - 1].Term;780 }781 return logTerm;782 }783 private void ShuttingDown()784 {785 this.SendEvent(this.ElectionTimer, HaltEvent.Instance);786 this.SendEvent(this.PeriodicTimer, HaltEvent.Instance);787 this.RaiseHaltEvent();788 }789 }790 private class Client : StateMachine791 {792 /​/​/​ <summary>793 /​/​/​ Used to configure the client.794 /​/​/​ </​summary>795 public class ConfigureEvent : Event796 {797 public ActorId Cluster;798 public ConfigureEvent(ActorId cluster)799 : base()800 {801 this.Cluster = cluster;802 }803 }804 /​/​/​ <summary>805 /​/​/​ Used for a client request.806 /​/​/​ </​summary>807 internal class Request : Event808 {809 public ActorId Client;810 public int Command;811 public Request(ActorId client, int command)812 : base()813 {814 this.Client = client;815 this.Command = command;816 }817 }818 internal class Response : Event819 {820 }821 private class LocalEvent : Event822 {823 }824 private ActorId Cluster;825 private int LatestCommand;826 private int Counter;827 [Start]828 [OnEntry(nameof(InitOnEntry))]829 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]830 [OnEventGotoState(typeof(LocalEvent), typeof(PumpRequest))]831 private class Init : State832 {833 }834 private void InitOnEntry()835 {836 this.LatestCommand = -1;837 this.Counter = 0;838 }839 private void SetupEvent(Event e)840 {841 this.Cluster = (e as ConfigureEvent).Cluster;842 this.RaiseEvent(new LocalEvent());843 }844 [OnEntry(nameof(PumpRequestOnEntry))]845 [OnEventDoAction(typeof(Response), nameof(ProcessResponse))]846 [OnEventGotoState(typeof(LocalEvent), typeof(PumpRequest))]847 private class PumpRequest : State848 {849 }850 private void PumpRequestOnEntry()851 {852 this.LatestCommand = this.RandomInteger(100);853 this.Counter++;854 this.SendEvent(this.Cluster, new Request(this.Id, this.LatestCommand));855 }856 private void ProcessResponse()857 {858 if (this.Counter is 3)859 {860 this.SendEvent(this.Cluster, new ClusterManager.ShutDown());861 this.RaiseHaltEvent();862 }863 else864 {865 this.RaiseEvent(new LocalEvent());866 }867 }868 }869 private class ElectionTimer : StateMachine870 {871 internal class ConfigureEvent : Event872 {873 public ActorId Target;874 public ConfigureEvent(ActorId id)875 : base()876 {877 this.Target = id;878 }879 }880 internal class StartTimerEvent : Event881 {882 }883 internal class CancelTimer : Event884 {885 }886 internal class Timeout : Event887 {888 }889 private class TickEvent : Event890 {891 }892 private ActorId Target;893 [Start]894 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]895 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]896 private class Init : State897 {898 }899 private void SetupEvent(Event e)900 {901 this.Target = (e as ConfigureEvent).Target;902 }903 [OnEntry(nameof(ActiveOnEntry))]904 [OnEventDoAction(typeof(TickEvent), nameof(Tick))]905 [OnEventGotoState(typeof(CancelTimer), typeof(Inactive))]906 [IgnoreEvents(typeof(StartTimerEvent))]907 private class Active : State908 {909 }910 private void ActiveOnEntry()911 {912 this.SendEvent(this.Id, new TickEvent());913 }914 private void Tick()915 {916 if (this.RandomBoolean())917 {918 this.SendEvent(this.Target, new Timeout());919 }920 this.RaiseEvent(new CancelTimer());921 }922 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]923 [IgnoreEvents(typeof(CancelTimer), typeof(TickEvent))]924 private class Inactive : State925 {926 }927 }928 private class PeriodicTimer : StateMachine929 {930 internal class ConfigureEvent : Event931 {932 public ActorId Target;933 public ConfigureEvent(ActorId id)934 : base()935 {936 this.Target = id;937 }938 }939 internal class StartTimerEvent : Event940 {941 }942 internal class CancelTimer : Event943 {944 }945 internal class Timeout : Event946 {947 }948 private class TickEvent : Event949 {950 }951 private ActorId Target;952 [Start]953 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]954 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]955 private class Init : State956 {957 }958 private void SetupEvent(Event e)959 {960 this.Target = (e as ConfigureEvent).Target;961 }962 [OnEntry(nameof(ActiveOnEntry))]963 [OnEventDoAction(typeof(TickEvent), nameof(Tick))]964 [OnEventGotoState(typeof(CancelTimer), typeof(Inactive))]965 [IgnoreEvents(typeof(StartTimerEvent))]966 private class Active : State967 {968 }969 private void ActiveOnEntry()970 {971 this.SendEvent(this.Id, new TickEvent());972 }...

SetupEvent

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using Microsoft.Coyote.Actors.BugFinding;4using System;5{6 {7 public Success()8 {9 this.SetupEvent(typeof(e));10 }11 [OnEventDoAction(typeof(e), nameof(HandleEvent))]12 {13 }14 private void HandleEvent(Event e)15 {16 this.RaiseEvent(new e());17 }18 }19}20using Microsoft.Coyote.Actors;21using Microsoft.Coyote.Actors.BugFinding.Tests;22using Microsoft.Coyote.Actors.BugFinding;23using System;24{25 {26 public Success()27 {28 this.SetupEvent(typeof(e));29 }30 [OnEventDoAction(typeof(e), nameof(HandleEvent))]31 {32 }33 private void HandleEvent(Event e)34 {35 this.RaiseEvent(new e());36 }37 }38}39using Microsoft.Coyote.Actors;40using Microsoft.Coyote.Actors.BugFinding.Tests;41using Microsoft.Coyote.Actors.BugFinding;42using System;43{44 {45 public Success()46 {47 this.SetupEvent(typeof(e));48 }49 [OnEventDoAction(typeof(e), nameof(HandleEvent))]50 {51 }52 private void HandleEvent(Event e)53 {54 this.RaiseEvent(new e());55 }56 }57}58using Microsoft.Coyote.Actors;59using Microsoft.Coyote.Actors.BugFinding.Tests;60using Microsoft.Coyote.Actors.BugFinding;61using System;62{

SetupEvent

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using System;4using System.Threading.Tasks;5{6 {7 public static async Task Main(string[] args)8 {9 var runtime = RuntimeFactory.Create();10 var setupEvent = new SetupEvent();11 setupEvent.SetupEvent1 = 1;12 setupEvent.SetupEvent2 = 2;13 setupEvent.SetupEvent3 = 3;14 setupEvent.SetupEvent4 = 4;15 setupEvent.SetupEvent5 = 5;16 setupEvent.SetupEvent6 = 6;17 setupEvent.SetupEvent7 = 7;18 setupEvent.SetupEvent8 = 8;19 setupEvent.SetupEvent9 = 9;20 setupEvent.SetupEvent10 = 10;21 setupEvent.SetupEvent11 = 11;22 setupEvent.SetupEvent12 = 12;23 setupEvent.SetupEvent13 = 13;24 setupEvent.SetupEvent14 = 14;25 setupEvent.SetupEvent15 = 15;26 setupEvent.SetupEvent16 = 16;27 setupEvent.SetupEvent17 = 17;28 setupEvent.SetupEvent18 = 18;29 setupEvent.SetupEvent19 = 19;30 setupEvent.SetupEvent20 = 20;31 setupEvent.SetupEvent21 = 21;32 setupEvent.SetupEvent22 = 22;33 setupEvent.SetupEvent23 = 23;34 setupEvent.SetupEvent24 = 24;35 setupEvent.SetupEvent25 = 25;36 setupEvent.SetupEvent26 = 26;37 setupEvent.SetupEvent27 = 27;38 setupEvent.SetupEvent28 = 28;39 setupEvent.SetupEvent29 = 29;40 setupEvent.SetupEvent30 = 30;41 setupEvent.SetupEvent31 = 31;42 setupEvent.SetupEvent32 = 32;43 setupEvent.SetupEvent33 = 33;44 setupEvent.SetupEvent34 = 34;45 setupEvent.SetupEvent35 = 35;46 setupEvent.SetupEvent36 = 36;47 setupEvent.SetupEvent37 = 37;48 setupEvent.SetupEvent38 = 38;49 setupEvent.SetupEvent39 = 39;50 setupEvent.SetupEvent40 = 40;51 setupEvent.SetupEvent41 = 41;52 setupEvent.SetupEvent42 = 42;

SetupEvent

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using Microsoft.Coyote.Specifications;4using System;5using System.Threading.Tasks;6{7 {8 static async Task Main(string[] args)9 {10 var config = Configuration.Create();11 config.MaxSchedulingSteps = 100000;12 config.MaxFairSchedulingSteps = 100000;13 config.EnableCycleDetection = true;14 config.EnableDataRaceDetection = true;15 config.EnableIntegerOverflowChecking = true;16 config.EnableActorGarbageCollection = false;17 config.CreateLogFile = true;18 config.LogFileName = "log.txt";19 config.LogToConsole = true;20 config.EnableHotStateDetection = true;21 config.EnableHotStateDetectionInProduction = true;22 config.EnableHotStateDetectionInTesting = true;23 config.EnableHotStateDetectionInMonitoring = true;24 config.EnableHotStateDetectionInBugFinding = true;25 config.EnableHotStateDetectionInDeadlockDetection = true;26 config.EnableHotStateDetectionInLivenessChecking = true;27 config.EnableHotStateDetectionInStateExploration = true;28 config.MaxUnfairSchedulingSteps = 100000;29 config.SchedulingIterations = 100000;30 config.SchedulingStrategy = SchedulingStrategy.DFS;31 config.ScheduleFairly = true;32 config.TestingIterations = 100000;33 config.TestingStrategy = TestingStrategy.Random;34 config.Verbose = 1;35 config.EnableHotStateDetection = true;36 config.EnableHotStateDetectionInProduction = true;37 config.EnableHotStateDetectionInTesting = true;38 config.EnableHotStateDetectionInMonitoring = true;39 config.EnableHotStateDetectionInBugFinding = true;40 config.EnableHotStateDetectionInDeadlockDetection = true;41 config.EnableHotStateDetectionInLivenessChecking = true;42 config.EnableHotStateDetectionInStateExploration = true;43 config.MaxUnfairSchedulingSteps = 100000;44 config.SchedulingIterations = 100000;45 config.SchedulingStrategy = SchedulingStrategy.DFS;46 config.ScheduleFairly = true;47 config.TestingIterations = 100000;48 config.TestingStrategy = TestingStrategy.Random;49 config.Verbose = 1;50 config.EnableHotStateDetection = true;51 config.EnableHotStateDetectionInProduction = true;

SetupEvent

Using AI Code Generation

1var bugFindingTestsSuccess = new Success();2bugFindingTestsSuccess.SetupEvent();3var bugFindingTestsSuccess = new Success();4bugFindingTestsSuccess.SetupEvent();5var bugFindingTestsSuccess = new Success();6bugFindingTestsSuccess.SetupEvent();7var bugFindingTestsSuccess = new Success();8bugFindingTestsSuccess.SetupEvent();9var bugFindingTestsSuccess = new Success();10bugFindingTestsSuccess.SetupEvent();11var bugFindingTestsSuccess = new Success();12bugFindingTestsSuccess.SetupEvent();13var bugFindingTestsSuccess = new Success();14bugFindingTestsSuccess.SetupEvent();15var bugFindingTestsSuccess = new Success();16bugFindingTestsSuccess.SetupEvent();17var bugFindingTestsSuccess = new Success();18bugFindingTestsSuccess.SetupEvent();19var bugFindingTestsSuccess = new Success();20bugFindingTestsSuccess.SetupEvent();21var bugFindingTestsSuccess = new Success();22bugFindingTestsSuccess.SetupEvent();23var bugFindingTestsSuccess = new Success();

SetupEvent

Using AI Code Generation

1using Microsoft.Coyote.Actors.BugFinding.Tests;2using Microsoft.Coyote.Actors.BugFinding.Tests.Success;3using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent;4using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor;5using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine;6using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine;7using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine;8using System;9using System.Collections.Generic;10using System.Linq;11using System.Text;12using System.Threading.Tasks;13using Microsoft.Coyote;14using Microsoft.Coyote.Actors;15using Microsoft.Coyote.Actors.BugFinding;16using Microsoft.Coyote.Actors.BugFinding.Tests;17using Microsoft.Coyote.Actors.BugFinding.Tests.Success;18using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent;19using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor;20using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine;21using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine;22using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine;23using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine.Machine;24using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine.Machine.Machine;25using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine.Machine.Machine.Machine;26using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine.Machine.Machine.Machine.Machine;27using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine.Machine.Machine.Machine.Machine.Machine;28using Microsoft.Coyote.Actors.BugFinding.Tests.Success.SetupEvent.Monitor.Machine.Machine.Machine.Machine.Machine.Machine.Machine.Machine.Machine;

SetupEvent

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using Microsoft.Coyote.Actors.TestingServices;4using Microsoft.Coyote.TestingServices;5using System.Threading.Tasks;6{7 {8 static void Main(string[] args)9 {10 var runtime = TestingEngine.Create();11 var test = new Success();12 runtime.SetupEvent(test, typeof(Start), typeof(Start));13 runtime.RegisterMonitor<SuccessMonitor>();14 runtime.RunAsync(test);15 runtime.WaitCompletion();16 }17 }18}19using Microsoft.Coyote.Actors;20using Microsoft.Coyote.Actors.BugFinding.Tests;21using Microsoft.Coyote.Actors.TestingServices;22using Microsoft.Coyote.TestingServices;23using System.Threading.Tasks;24{25 {26 static void Main(string[] args)27 {28 var runtime = TestingEngine.Create();29 var test = new Success();30 runtime.SetupEvent(test, typeof(Start), typeof(Start));31 runtime.RegisterMonitor<SuccessMonitor>();32 runtime.RunAsync(test);33 runtime.WaitCompletion();34 }35 }36}37using Microsoft.Coyote.Actors;38using Microsoft.Coyote.Actors.BugFinding.Tests;39using Microsoft.Coyote.Actors.TestingServices;40using Microsoft.Coyote.TestingServices;41using System.Threading.Tasks;42{43 {44 static void Main(string[] args)45 {46 var runtime = TestingEngine.Create();47 var test = new Success();48 runtime.SetupEvent(test, typeof(Start), typeof(Start));49 runtime.RegisterMonitor<SuccessMonitor>();50 runtime.RunAsync(test);51 runtime.WaitCompletion();52 }53 }54}55using Microsoft.Coyote.Actors;56using Microsoft.Coyote.Actors.BugFinding.Tests;57using Microsoft.Coyote.Actors.TestingServices;58using Microsoft.Coyote.TestingServices;59using System.Threading.Tasks;60{

SetupEvent

Using AI Code Generation

1using System;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using Microsoft.Coyote.Actors.BugFinding.Tests.Success;4{5 {6 public static void Main(string[] args)7 {8 var setup = new SetupEvent();9 var m = new Success();10 m.SetupEvent(setup);11 }12 }13}14using System;15using Microsoft.Coyote.Actors.BugFinding.Tests;16using Microsoft.Coyote.Actors.BugFinding.Tests.Success;17{18 {19 public static void Main(string[] args)20 {21 var setup = new SetupEvent();22 var m = new Success();23 m.SetupEvent(setup);24 }25 }26}

SetupEvent

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Actors.BugFinding.Tests;5using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote;6using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting;7using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies;8using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.RaceDetection;9using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateExploration;10using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph;11using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies;12using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk;13using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies;14using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies.RandomWalk;15using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies.RandomWalk.Strategies;16using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies.RandomWalk.Strategies.RandomWalk;17using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies.RandomWalk.Strategies.RandomWalk.Strategies;18using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies.RandomWalk.Strategies.RandomWalk.Strategies.RandomWalk;19using Microsoft.Coyote.Actors.BugFinding.Tests.Coyote.SystematicTesting.Strategies.StateGraph.Strategies.RandomWalk.Strategies.RandomWalk.Strategies.RandomWalk.Strategies.RandomWalk.Strategies;

SetupEvent

Using AI Code Generation

1using System;2using System.Reflection;3using System.Threading.Tasks;4using Microsoft.Coyote;5using Microsoft.Coyote.Actors;6using Microsoft.Coyote.Actors.BugFinding.Tests;7{8 {9 public int Value { get; set; }10 }11}12{13 {14 public static void Main(string[] args)15 {16 var assembly = Assembly.GetExecutingAssembly();17 var type = assembly.GetType("Microsoft.Coyote.Actors.BugFinding.Tests.Event");18 var method = typeof(Actor).GetMethod("SetupEvent", BindingFlags.NonPublic | BindingFlags.Static);19 var generic = method.MakeGenericMethod(type);20 generic.Invoke(null, new object[] { args[0] });21 Task.Run(async () =>22 {23 var m = Runtime.CreateMachine(typeof(M));24 await Runtime.SendEvent(m, new Event { Value = 0 });25 }).Wait();26 }27 }28}29{30 {31 [OnEntry(nameof(InitOnEntry))]32 [OnEventDoAction(typeof(Event), nameof(HandleEvent))]33 class Init : State { }34 void InitOnEntry()35 {36 this.Raise(new Event { Value = 1 });37 }38 void HandleEvent(Event e)39 {40 }41 }42}

Automation Testing Tutorials

Learn to execute automation testing from scratch with LambdaTest Learning Hub. Right from setting up the prerequisites to run your first automation test, to following best practices and diving deeper into advanced test scenarios. LambdaTest Learning Hubs compile a list of step-by-step guides to help you be proficient with different test automation frameworks i.e. Selenium, Cypress, TestNG etc.

LambdaTest Learning Hubs:

• JUnit Tutorial
• TestNG Tutorial
• Webdriver Tutorial
• WebDriverIO Tutorial
• Protractor Tutorial
• Selenium 4 Tutorial
• Jenkins Tutorial
• NUnit Tutorial
• Jest Tutorial
• Playwright Tutorial
• Cypress Tutorial
• PyTest Tutorial

YouTube

You could also refer to video tutorials over LambdaTest YouTube channel to get step by step demonstration from industry experts.

Run Coyote automation tests on LambdaTest cloud grid

Perform automation testing on 3000+ real desktop and mobile devices online.

View sample repo View DocumentationSign up Free

›

_

Most used method in Success

• InitOnEntry
• CheckWhichNodeFailed
• CorrectHeadFailureOnEntry
• UpdateClients
• UpdateFailureDetector
• CorrectTailFailureOnEntry
• CorrectServerFailureOnEntry
• ProcessFixPredecessor
• SetLastUpdate
• ProcessSuccess
• SetupEvent
• PredSucc
• ForwardUpdate
• BackwardAck
• NewPredecessor
• NewSuccessor
• NewSuccInfo
• ResponseToQuery
• SetupPredSucc
• ProcessUpdateAction
• ProcessQueryAction
• ProcessBecomeHead
• ProcessBecomeTail
• SendPong
• UpdatePredecessor
• UpdateSuccessor
• ProcessUpdateOnEntry
• ProcessFwdUpdateOnEntry
• ProcessBckAckOnEntry
• RemoveItemFromSent
• UpdateHeadTail
• Update
• Query
• PumpUpdateRequestsOnEntry
• PumpQueryRequestsOnEntry
• PumpRequestsLocalAction
• PumpRequestsDoneAction
• UpdateServers
• HistoryUpdate
• SentUpdate
• Setup
• CheckUpdatePropagationInvariant
• CheckInprocessRequestsInvariant
• GetNext
• GetPrev
• ExtractSeqId
• MergeSeq
• IsSorted
• CheckLessOrEqualThan
• CheckEqual
• ClearTempSeq
• ProcessUpdateServers
• ResponseToUpdate
• ResponseToUpdateAction
• ResponseToQueryAction
• TestSequenceNotSortedInChainReplicationProtocol