Unlock 30% off on Manual Testing Annual Plans this Holiday Season. 
Use Code: LCMYEARENDEXCL30
Use Code: LCMYEARENDEXCL30Check icon
Copied to Clipboard!
How to use SetupEvent method of Microsoft.Coyote.Actors.BugFinding.Tests.Request class
Best Coyote code snippet using Microsoft.Coyote.Actors.BugFinding.Tests.Request.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;...
ChordTests.cs
Source:ChordTests.cs
...70 var nodeKeys = this.AssignKeysToNodes();71 for (int idx = 0; idx < this.ChordNodes.Count; idx++)72 {73 var keys = nodeKeys[this.NodeIds[idx]];74 this.SendEvent(this.ChordNodes[idx], new ChordNode.SetupEvent(this.NodeIds[idx], new HashSet<int>(keys),75 new List<ActorId>(this.ChordNodes), new List<int>(this.NodeIds), this.Id));76 }77 this.CreateActor(typeof(Client), new Client.SetupEvent(this.Id, new List<int>(this.Keys)));78 this.RaiseEvent(new Local());79 }80 [OnEventDoAction(typeof(ChordNode.FindSuccessor), nameof(ForwardFindSuccessor))]81 [OnEventDoAction(typeof(CreateNewNode), nameof(ProcessCreateNewNode))]82 [OnEventDoAction(typeof(TerminateNode), nameof(ProcessTerminateNode))]83 [OnEventDoAction(typeof(ChordNode.JoinAck), nameof(QueryStabilize))]84 private class Waiting : State85 {86 }87 private void ForwardFindSuccessor(Event e)88 {89 this.SendEvent(this.ChordNodes[0], e);90 }91 private void ProcessCreateNewNode()92 {93 int newId = -1;94 while ((newId < 0 || this.NodeIds.Contains(newId)) &&95 this.NodeIds.Count < this.NumOfIds)96 {97 for (int i = 0; i < this.NumOfIds; i++)98 {99 if (this.RandomBoolean())100 {101 newId = i;102 }103 }104 }105 this.Assert(newId >= 0, "Cannot create a new node, no ids available.");106 var newNode = this.CreateActor(typeof(ChordNode));107 this.NumOfNodes++;108 this.NodeIds.Add(newId);109 this.ChordNodes.Add(newNode);110 this.SendEvent(newNode, new ChordNode.Join(newId, new List<ActorId>(this.ChordNodes),111 new List<int>(this.NodeIds), this.NumOfIds, this.Id));112 }113 private void ProcessTerminateNode()114 {115 int endId = -1;116 while ((endId < 0 || !this.NodeIds.Contains(endId)) &&117 this.NodeIds.Count > 0)118 {119 for (int i = 0; i < this.ChordNodes.Count; i++)120 {121 if (this.RandomBoolean())122 {123 endId = i;124 }125 }126 }127 this.Assert(endId >= 0, "Cannot find a node to terminate.");128 var endNode = this.ChordNodes[endId];129 this.NumOfNodes--;130 this.NodeIds.Remove(endId);131 this.ChordNodes.Remove(endNode);132 this.SendEvent(endNode, new ChordNode.Terminate());133 }134 private void QueryStabilize()135 {136 foreach (var node in this.ChordNodes)137 {138 this.SendEvent(node, new ChordNode.Stabilize());139 }140 }141 private Dictionary<int, List<int>> AssignKeysToNodes()142 {143 var nodeKeys = new Dictionary<int, List<int>>();144 for (int i = this.Keys.Count - 1; i >= 0; i--)145 {146 bool assigned = false;147 for (int j = 0; j < this.NodeIds.Count; j++)148 {149 if (this.Keys[i] <= this.NodeIds[j])150 {151 if (nodeKeys.ContainsKey(this.NodeIds[j]))152 {153 nodeKeys[this.NodeIds[j]].Add(this.Keys[i]);154 }155 else156 {157 nodeKeys.Add(this.NodeIds[j], new List<int>());158 nodeKeys[this.NodeIds[j]].Add(this.Keys[i]);159 }160 assigned = true;161 break;162 }163 }164 if (!assigned)165 {166 if (nodeKeys.ContainsKey(this.NodeIds[0]))167 {168 nodeKeys[this.NodeIds[0]].Add(this.Keys[i]);169 }170 else171 {172 nodeKeys.Add(this.NodeIds[0], new List<int>());173 nodeKeys[this.NodeIds[0]].Add(this.Keys[i]);174 }175 }176 }177 return nodeKeys;178 }179 }180 private class ChordNode : StateMachine181 {182 internal class SetupEvent : Event183 {184 public int Id;185 public HashSet<int> Keys;186 public List<ActorId> Nodes;187 public List<int> NodeIds;188 public ActorId ManagerId;189 public SetupEvent(int id, HashSet<int> keys, List<ActorId> nodes,190 List<int> nodeIds, ActorId managerId)191 : base()192 {193 this.Id = id;194 this.Keys = keys;195 this.Nodes = nodes;196 this.NodeIds = nodeIds;197 this.ManagerId = managerId;198 }199 }200 internal class Join : Event201 {202 public int Id;203 public List<ActorId> Nodes;204 public List<int> NodeIds;205 public int NumOfIds;206 public ActorId ManagerId;207 public Join(int id, List<ActorId> nodes, List<int> nodeIds,208 int numOfIds, ActorId managerId)209 : base()210 {211 this.Id = id;212 this.Nodes = nodes;213 this.NodeIds = nodeIds;214 this.NumOfIds = numOfIds;215 this.ManagerId = managerId;216 }217 }218 internal class FindSuccessor : Event219 {220 public ActorId Sender;221 public int Key;222 public FindSuccessor(ActorId sender, int key)223 : base()224 {225 this.Sender = sender;226 this.Key = key;227 }228 }229 internal class FindSuccessorResp : Event230 {231 public ActorId Node;232 public int Key;233 public FindSuccessorResp(ActorId node, int key)234 : base()235 {236 this.Node = node;237 this.Key = key;238 }239 }240 internal class FindPredecessor : Event241 {242 public ActorId Sender;243 public FindPredecessor(ActorId sender)244 : base()245 {246 this.Sender = sender;247 }248 }249 internal class FindPredecessorResp : Event250 {251 public ActorId Node;252 public FindPredecessorResp(ActorId node)253 : base()254 {255 this.Node = node;256 }257 }258 internal class QueryId : Event259 {260 public ActorId Sender;261 public QueryId(ActorId sender)262 : base()263 {264 this.Sender = sender;265 }266 }267 internal class QueryIdResp : Event268 {269 public int Id;270 public QueryIdResp(int id)271 : base()272 {273 this.Id = id;274 }275 }276 internal class AskForKeys : Event277 {278 public ActorId Node;279 public int Id;280 public AskForKeys(ActorId node, int id)281 : base()282 {283 this.Node = node;284 this.Id = id;285 }286 }287 internal class AskForKeysResp : Event288 {289 public List<int> Keys;290 public AskForKeysResp(List<int> keys)291 : base()292 {293 this.Keys = keys;294 }295 }296 private class NotifySuccessor : Event297 {298 public ActorId Node;299 public NotifySuccessor(ActorId node)300 : base()301 {302 this.Node = node;303 }304 }305 internal class JoinAck : Event306 {307 }308 internal class Stabilize : Event309 {310 }311 internal class Terminate : Event312 {313 }314 private class Local : Event315 {316 }317 private int NodeId;318 private HashSet<int> Keys;319 private int NumOfIds;320 private Dictionary<int, Finger> FingerTable;321 private ActorId Predecessor;322 private ActorId ManagerId;323 [Start]324 [OnEntry(nameof(InitOnEntry))]325 [OnEventGotoState(typeof(Local), typeof(Waiting))]326 [OnEventDoAction(typeof(SetupEvent), nameof(Setup))]327 [OnEventDoAction(typeof(Join), nameof(JoinCluster))]328 [DeferEvents(typeof(AskForKeys), typeof(NotifySuccessor), typeof(Stabilize))]329 private class Init : State330 {331 }332 private void InitOnEntry()333 {334 this.FingerTable = new Dictionary<int, Finger>();335 }336 private void Setup(Event e)337 {338 this.NodeId = (e as SetupEvent).Id;339 this.Keys = (e as SetupEvent).Keys;340 this.ManagerId = (e as SetupEvent).ManagerId;341 var nodes = (e as SetupEvent).Nodes;342 var nodeIds = (e as SetupEvent).NodeIds;343 this.NumOfIds = (int)Math.Pow(2, nodes.Count);344 for (var idx = 1; idx <= nodes.Count; idx++)345 {346 var start = (this.NodeId + (int)Math.Pow(2, idx - 1)) % this.NumOfIds;347 var end = (this.NodeId + (int)Math.Pow(2, idx)) % this.NumOfIds;348 var nodeId = GetSuccessorNodeId(start, nodeIds);349 this.FingerTable.Add(start, new Finger(start, end, nodes[nodeId]));350 }351 for (var idx = 0; idx < nodeIds.Count; idx++)352 {353 if (nodeIds[idx] == this.NodeId)354 {355 this.Predecessor = nodes[WrapSubtract(idx, 1, nodeIds.Count)];356 break;357 }358 }359 this.RaiseEvent(new Local());360 }361 private void JoinCluster(Event e)362 {363 this.NodeId = (e as Join).Id;364 this.ManagerId = (e as Join).ManagerId;365 this.NumOfIds = (e as Join).NumOfIds;366 var nodes = (e as Join).Nodes;367 var nodeIds = (e as Join).NodeIds;368 for (var idx = 1; idx <= nodes.Count; idx++)369 {370 var start = (this.NodeId + (int)Math.Pow(2, idx - 1)) % this.NumOfIds;371 var end = (this.NodeId + (int)Math.Pow(2, idx)) % this.NumOfIds;372 var nodeId = GetSuccessorNodeId(start, nodeIds);373 this.FingerTable.Add(start, new Finger(start, end, nodes[nodeId]));374 }375 var successor = this.FingerTable[(this.NodeId + 1) % this.NumOfIds].Node;376 this.SendEvent(this.ManagerId, new JoinAck());377 this.SendEvent(successor, new NotifySuccessor(this.Id));378 }379 [OnEventDoAction(typeof(FindSuccessor), nameof(ProcessFindSuccessor))]380 [OnEventDoAction(typeof(FindSuccessorResp), nameof(ProcessFindSuccessorResp))]381 [OnEventDoAction(typeof(FindPredecessor), nameof(ProcessFindPredecessor))]382 [OnEventDoAction(typeof(FindPredecessorResp), nameof(ProcessFindPredecessorResp))]383 [OnEventDoAction(typeof(QueryId), nameof(ProcessQueryId))]384 [OnEventDoAction(typeof(AskForKeys), nameof(SendKeys))]385 [OnEventDoAction(typeof(AskForKeysResp), nameof(UpdateKeys))]386 [OnEventDoAction(typeof(NotifySuccessor), nameof(UpdatePredecessor))]387 [OnEventDoAction(typeof(Stabilize), nameof(ProcessStabilize))]388 [OnEventDoAction(typeof(Terminate), nameof(ProcessTerminate))]389 private class Waiting : State390 {391 }392 private void ProcessFindSuccessor(Event e)393 {394 var sender = (e as FindSuccessor).Sender;395 var key = (e as FindSuccessor).Key;396 if (this.Keys.Contains(key))397 {398 this.SendEvent(sender, new FindSuccessorResp(this.Id, key));399 }400 else if (this.FingerTable.ContainsKey(key))401 {402 this.SendEvent(sender, new FindSuccessorResp(this.FingerTable[key].Node, key));403 }404 else if (this.NodeId.Equals(key))405 {406 this.SendEvent(sender, new FindSuccessorResp(407 this.FingerTable[(this.NodeId + 1) % this.NumOfIds].Node, key));408 }409 else410 {411 int idToAsk = -1;412 foreach (var finger in this.FingerTable)413 {414 if (((finger.Value.Start > finger.Value.End) &&415 (finger.Value.Start <= key || key < finger.Value.End)) ||416 ((finger.Value.Start < finger.Value.End) &&417 finger.Value.Start <= key && key < finger.Value.End))418 {419 idToAsk = finger.Key;420 }421 }422 if (idToAsk < 0)423 {424 idToAsk = (this.NodeId + 1) % this.NumOfIds;425 }426 if (this.FingerTable[idToAsk].Node.Equals(this.Id))427 {428 foreach (var finger in this.FingerTable)429 {430 if (finger.Value.End == idToAsk ||431 finger.Value.End == idToAsk - 1)432 {433 idToAsk = finger.Key;434 break;435 }436 }437 this.Assert(!this.FingerTable[idToAsk].Node.Equals(this.Id), "Cannot locate successor of {0}.", key);438 }439 this.SendEvent(this.FingerTable[idToAsk].Node, new FindSuccessor(sender, key));440 }441 }442 private void ProcessFindPredecessor(Event e)443 {444 var sender = (e as FindPredecessor).Sender;445 if (this.Predecessor != null)446 {447 this.SendEvent(sender, new FindPredecessorResp(this.Predecessor));448 }449 }450 private void ProcessQueryId(Event e)451 {452 var sender = (e as QueryId).Sender;453 this.SendEvent(sender, new QueryIdResp(this.NodeId));454 }455 private void SendKeys(Event e)456 {457 var sender = (e as AskForKeys).Node;458 var senderId = (e as AskForKeys).Id;459 this.Assert(this.Predecessor.Equals(sender), "Predecessor is corrupted.");460 List<int> keysToSend = new List<int>();461 foreach (var key in this.Keys)462 {463 if (key <= senderId)464 {465 keysToSend.Add(key);466 }467 }468 if (keysToSend.Count > 0)469 {470 foreach (var key in keysToSend)471 {472 this.Keys.Remove(key);473 }474 this.SendEvent(sender, new AskForKeysResp(keysToSend));475 }476 }477 private void ProcessStabilize()478 {479 var successor = this.FingerTable[(this.NodeId + 1) % this.NumOfIds].Node;480 this.SendEvent(successor, new FindPredecessor(this.Id));481 foreach (var finger in this.FingerTable)482 {483 if (!finger.Value.Node.Equals(successor))484 {485 this.SendEvent(successor, new FindSuccessor(this.Id, finger.Key));486 }487 }488 }489 private void ProcessFindSuccessorResp(Event e)490 {491 var successor = (e as FindSuccessorResp).Node;492 var key = (e as FindSuccessorResp).Key;493 this.Assert(this.FingerTable.ContainsKey(key), "Finger table of {0} does not contain {1}.", this.NodeId, key);494 this.FingerTable[key] = new Finger(this.FingerTable[key].Start, this.FingerTable[key].End, successor);495 }496 private void ProcessFindPredecessorResp(Event e)497 {498 var successor = (e as FindPredecessorResp).Node;499 if (!successor.Equals(this.Id))500 {501 this.FingerTable[(this.NodeId + 1) % this.NumOfIds] = new Finger(502 this.FingerTable[(this.NodeId + 1) % this.NumOfIds].Start,503 this.FingerTable[(this.NodeId + 1) % this.NumOfIds].End,504 successor);505 this.SendEvent(successor, new NotifySuccessor(this.Id));506 this.SendEvent(successor, new AskForKeys(this.Id, this.NodeId));507 }508 }509 private void UpdatePredecessor(Event e)510 {511 var predecessor = (e as NotifySuccessor).Node;512 if (!predecessor.Equals(this.Id))513 {514 this.Predecessor = predecessor;515 }516 }517 private void UpdateKeys(Event e)518 {519 var keys = (e as AskForKeysResp).Keys;520 foreach (var key in keys)521 {522 this.Keys.Add(key);523 }524 }525 private void ProcessTerminate() => this.RaiseHaltEvent();526 private static int GetSuccessorNodeId(int start, List<int> nodeIds)527 {528 var candidate = -1;529 foreach (var id in nodeIds.Where(v => v >= start))530 {531 if (candidate < 0 || id < candidate)532 {533 candidate = id;534 }535 }536 if (candidate < 0)537 {538 foreach (var id in nodeIds.Where(v => v < start))539 {540 if (candidate < 0 || id < candidate)541 {542 candidate = id;543 }544 }545 }546 for (int idx = 0; idx < nodeIds.Count; idx++)547 {548 if (nodeIds[idx] == candidate)549 {550 candidate = idx;551 break;552 }553 }554 return candidate;555 }556 private static int WrapSubtract(int left, int right, int ceiling)557 {558 int result = left - right;559 if (result < 0)560 {561 result = ceiling + result;562 }563 return result;564 }565 }566 private class Client : StateMachine567 {568 internal class SetupEvent : Event569 {570 public ActorId ClusterManager;571 public List<int> Keys;572 public SetupEvent(ActorId clusterManager, List<int> keys)573 : base()574 {575 this.ClusterManager = clusterManager;576 this.Keys = keys;577 }578 }579 private class Local : Event580 {581 }582 private ActorId ClusterManager;583 private List<int> Keys;584 private int QueryCounter;585 [Start]586 [OnEntry(nameof(InitOnEntry))]587 [OnEventGotoState(typeof(Local), typeof(Querying))]588 private class Init : State589 {590 }591 private void InitOnEntry(Event e)592 {593 this.ClusterManager = (e as SetupEvent).ClusterManager;594 this.Keys = (e as SetupEvent).Keys;595 // LIVENESS BUG: can never detect the key, and keeps looping without596 // exiting the process. Enable to introduce the bug.597 this.Keys.Add(17);598 this.QueryCounter = 0;599 this.RaiseEvent(new Local());600 }601 [OnEntry(nameof(QueryingOnEntry))]602 [OnEventGotoState(typeof(Local), typeof(Waiting))]603 private class Querying : State604 {605 }606 private void QueryingOnEntry()607 {608 if (this.QueryCounter < 5)...
ReplicatingStorageTests.cs
Source:ReplicatingStorageTests.cs
...145 private Dictionary<int, int> DataMap;146 private ActorId RepairTimer;147 [Start]148 [OnEntry(nameof(EntryOnInit))]149 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]150 [OnEventGotoState(typeof(LocalEvent), typeof(Active))]151 [DeferEvents(typeof(Client.Request), typeof(RepairTimer.Timeout))]152 private class Init : State153 {154 }155 private void EntryOnInit()156 {157 this.StorageNodes = new List<ActorId>();158 this.StorageNodeMap = new Dictionary<int, bool>();159 this.DataMap = new Dictionary<int, int>();160 this.RepairTimer = this.CreateActor(typeof(RepairTimer));161 this.SendEvent(this.RepairTimer, new RepairTimer.ConfigureEvent(this.Id));162 }163 private void SetupEvent(Event e)164 {165 this.Environment = (e as ConfigureEvent).Environment;166 this.NumberOfReplicas = (e as ConfigureEvent).NumberOfReplicas;167 for (int idx = 0; idx < this.NumberOfReplicas; idx++)168 {169 this.CreateNewNode();170 }171 this.RaiseEvent(new LocalEvent());172 }173 private void CreateNewNode()174 {175 var idx = this.StorageNodes.Count;176 var node = this.CreateActor(typeof(StorageNode));177 this.StorageNodes.Add(node);178 this.StorageNodeMap.Add(idx, true);179 this.SendEvent(node, new StorageNode.ConfigureEvent(this.Environment, this.Id, idx));180 }181 [OnEventDoAction(typeof(Client.Request), nameof(ProcessClientRequest))]182 [OnEventDoAction(typeof(RepairTimer.Timeout), nameof(RepairNodes))]183 [OnEventDoAction(typeof(StorageNode.SyncReport), nameof(ProcessSyncReport))]184 [OnEventDoAction(typeof(NotifyFailure), nameof(ProcessFailure))]185 private class Active : State186 {187 }188 private void ProcessClientRequest(Event e)189 {190 var command = (e as Client.Request).Command;191 var aliveNodeIds = this.StorageNodeMap.Where(n => n.Value).Select(n => n.Key);192 foreach (var nodeId in aliveNodeIds)193 {194 this.SendEvent(this.StorageNodes[nodeId], new StorageNode.StoreRequest(command));195 }196 }197 private void RepairNodes()198 {199 if (this.DataMap.Count is 0)200 {201 return;202 }203 var latestData = this.DataMap.Values.Max();204 var numOfReplicas = this.DataMap.Count(kvp => kvp.Value == latestData);205 if (numOfReplicas >= this.NumberOfReplicas)206 {207 return;208 }209 foreach (var node in this.DataMap)210 {211 if (node.Value != latestData)212 {213 this.SendEvent(this.StorageNodes[node.Key], new StorageNode.SyncRequest(latestData));214 numOfReplicas++;215 }216 if (numOfReplicas == this.NumberOfReplicas)217 {218 break;219 }220 }221 }222 private void ProcessSyncReport(Event e)223 {224 var nodeId = (e as StorageNode.SyncReport).NodeId;225 var data = (e as StorageNode.SyncReport).Data;226 // LIVENESS BUG: can fail to ever repair again as it thinks there227 // are enough replicas. Enable to introduce a bug fix.228 // if (!this.StorageNodeMap.ContainsKey(nodeId))229 // {230 // return;231 // }232 if (!this.DataMap.ContainsKey(nodeId))233 {234 this.DataMap.Add(nodeId, 0);235 }236 this.DataMap[nodeId] = data;237 }238 private void ProcessFailure(Event e)239 {240 var node = (e as NotifyFailure).Node;241 var nodeId = this.StorageNodes.IndexOf(node);242 this.StorageNodeMap.Remove(nodeId);243 this.DataMap.Remove(nodeId);244 this.CreateNewNode();245 }246 }247 private class StorageNode : StateMachine248 {249 public class ConfigureEvent : Event250 {251 public ActorId Environment;252 public ActorId NodeManager;253 public int Id;254 public ConfigureEvent(ActorId env, ActorId manager, int id)255 : base()256 {257 this.Environment = env;258 this.NodeManager = manager;259 this.Id = id;260 }261 }262 public class StoreRequest : Event263 {264 public int Command;265 public StoreRequest(int cmd)266 : base()267 {268 this.Command = cmd;269 }270 }271 public class SyncReport : Event272 {273 public int NodeId;274 public int Data;275 public SyncReport(int id, int data)276 : base()277 {278 this.NodeId = id;279 this.Data = data;280 }281 }282 public class SyncRequest : Event283 {284 public int Data;285 public SyncRequest(int data)286 : base()287 {288 this.Data = data;289 }290 }291 internal class ShutDown : Event292 {293 }294 private class LocalEvent : Event295 {296 }297 private ActorId Environment;298 private ActorId NodeManager;299 private int NodeId;300 private int Data;301 private ActorId SyncTimer;302 [Start]303 [OnEntry(nameof(EntryOnInit))]304 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]305 [OnEventGotoState(typeof(LocalEvent), typeof(Active))]306 [DeferEvents(typeof(SyncTimer.Timeout))]307 private class Init : State308 {309 }310 private void EntryOnInit()311 {312 this.Data = 0;313 this.SyncTimer = this.CreateActor(typeof(SyncTimer));314 this.SendEvent(this.SyncTimer, new SyncTimer.ConfigureEvent(this.Id));315 }316 private void SetupEvent(Event e)317 {318 this.Environment = (e as ConfigureEvent).Environment;319 this.NodeManager = (e as ConfigureEvent).NodeManager;320 this.NodeId = (e as ConfigureEvent).Id;321 this.Monitor<LivenessMonitor>(new LivenessMonitor.NotifyNodeCreated(this.NodeId));322 this.SendEvent(this.Environment, new Environment.NotifyNode(this.Id));323 this.RaiseEvent(new LocalEvent());324 }325 [OnEventDoAction(typeof(StoreRequest), nameof(Store))]326 [OnEventDoAction(typeof(SyncRequest), nameof(Sync))]327 [OnEventDoAction(typeof(SyncTimer.Timeout), nameof(GenerateSyncReport))]328 [OnEventDoAction(typeof(Environment.FaultInject), nameof(Terminate))]329 private class Active : State330 {331 }332 private void Store(Event e)333 {334 var cmd = (e as StoreRequest).Command;335 this.Data += cmd;336 this.Monitor<LivenessMonitor>(new LivenessMonitor.NotifyNodeUpdate(this.NodeId, this.Data));337 }338 private void Sync(Event e)339 {340 var data = (e as SyncRequest).Data;341 this.Data = data;342 this.Monitor<LivenessMonitor>(new LivenessMonitor.NotifyNodeUpdate(this.NodeId, this.Data));343 }344 private void GenerateSyncReport()345 {346 this.SendEvent(this.NodeManager, new SyncReport(this.NodeId, this.Data));347 }348 private void Terminate()349 {350 this.Monitor<LivenessMonitor>(new LivenessMonitor.NotifyNodeFail(this.NodeId));351 this.SendEvent(this.SyncTimer, HaltEvent.Instance);352 this.RaiseHaltEvent();353 }354 }355 private class FailureTimer : StateMachine356 {357 internal class ConfigureEvent : Event358 {359 public ActorId Target;360 public ConfigureEvent(ActorId id)361 : base()362 {363 this.Target = id;364 }365 }366 internal class StartTimerEvent : Event367 {368 }369 internal class CancelTimer : Event370 {371 }372 internal class Timeout : Event373 {374 }375 private class TickEvent : Event376 {377 }378 private ActorId Target;379 [Start]380 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]381 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]382 private class Init : State383 {384 }385 private void SetupEvent(Event e)386 {387 this.Target = (e as ConfigureEvent).Target;388 this.RaiseEvent(new StartTimerEvent());389 }390 [OnEntry(nameof(ActiveOnEntry))]391 [OnEventDoAction(typeof(TickEvent), nameof(Tick))]392 [OnEventGotoState(typeof(CancelTimer), typeof(Inactive))]393 [IgnoreEvents(typeof(StartTimerEvent))]394 private class Active : State395 {396 }397 private void ActiveOnEntry()398 {399 this.SendEvent(this.Id, new TickEvent());400 }401 private void Tick()402 {403 if (this.RandomBoolean())404 {405 this.SendEvent(this.Target, new Timeout());406 }407 this.SendEvent(this.Id, new TickEvent());408 }409 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]410 [IgnoreEvents(typeof(CancelTimer), typeof(TickEvent))]411 private class Inactive : State412 {413 }414 }415 private class RepairTimer : StateMachine416 {417 internal class ConfigureEvent : Event418 {419 public ActorId Target;420 public ConfigureEvent(ActorId id)421 : base()422 {423 this.Target = id;424 }425 }426 internal class StartTimerEvent : Event427 {428 }429 internal class CancelTimer : Event430 {431 }432 internal class Timeout : Event433 {434 }435 private class TickEvent : Event436 {437 }438 private ActorId Target;439 [Start]440 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]441 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]442 private class Init : State443 {444 }445 private void SetupEvent(Event e)446 {447 this.Target = (e as ConfigureEvent).Target;448 this.RaiseEvent(new StartTimerEvent());449 }450 [OnEntry(nameof(ActiveOnEntry))]451 [OnEventDoAction(typeof(TickEvent), nameof(Tick))]452 [OnEventGotoState(typeof(CancelTimer), typeof(Inactive))]453 [IgnoreEvents(typeof(StartTimerEvent))]454 private class Active : State455 {456 }457 private void ActiveOnEntry()458 {459 this.SendEvent(this.Id, new TickEvent());460 }461 private void Tick()462 {463 if (this.RandomBoolean())464 {465 this.SendEvent(this.Target, new Timeout());466 }467 this.SendEvent(this.Id, new TickEvent());468 }469 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]470 [IgnoreEvents(typeof(CancelTimer), typeof(TickEvent))]471 private class Inactive : State472 {473 }474 }475 private class SyncTimer : StateMachine476 {477 internal class ConfigureEvent : Event478 {479 public ActorId Target;480 public ConfigureEvent(ActorId id)481 : base()482 {483 this.Target = id;484 }485 }486 internal class StartTimerEvent : Event487 {488 }489 internal class CancelTimer : Event490 {491 }492 internal class Timeout : Event493 {494 }495 private class TickEvent : Event496 {497 }498 private ActorId Target;499 [Start]500 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]501 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]502 private class Init : State503 {504 }505 private void SetupEvent(Event e)506 {507 this.Target = (e as ConfigureEvent).Target;508 this.RaiseEvent(new StartTimerEvent());509 }510 [OnEntry(nameof(ActiveOnEntry))]511 [OnEventDoAction(typeof(TickEvent), nameof(Tick))]512 [OnEventGotoState(typeof(CancelTimer), typeof(Inactive))]513 [IgnoreEvents(typeof(StartTimerEvent))]514 private class Active : State515 {516 }517 private void ActiveOnEntry()518 {519 this.SendEvent(this.Id, new TickEvent());520 }521 private void Tick()522 {523 if (this.RandomBoolean())524 {525 this.SendEvent(this.Target, new Timeout());526 }527 this.SendEvent(this.Id, new TickEvent());528 }529 [OnEventGotoState(typeof(StartTimerEvent), typeof(Active))]530 [IgnoreEvents(typeof(CancelTimer), typeof(TickEvent))]531 private class Inactive : State532 {533 }534 }535 private class Client : StateMachine536 {537 public class ConfigureEvent : Event538 {539 public ActorId NodeManager;540 public ConfigureEvent(ActorId manager)541 : base()542 {543 this.NodeManager = manager;544 }545 }546 internal class Request : Event547 {548 public ActorId Client;549 public int Command;550 public Request(ActorId client, int cmd)551 : base()552 {553 this.Client = client;554 this.Command = cmd;555 }556 }557 private class LocalEvent : Event558 {559 }560 private ActorId NodeManager;561 private int Counter;562 [Start]563 [OnEntry(nameof(InitOnEntry))]564 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]565 [OnEventGotoState(typeof(LocalEvent), typeof(PumpRequest))]566 private class Init : State567 {568 }569 private void InitOnEntry()570 {571 this.Counter = 0;572 }573 private void SetupEvent(Event e)574 {575 this.NodeManager = (e as ConfigureEvent).NodeManager;576 this.RaiseEvent(new LocalEvent());577 }578 [OnEntry(nameof(PumpRequestOnEntry))]579 [OnEventGotoState(typeof(LocalEvent), typeof(PumpRequest))]580 private class PumpRequest : State581 {582 }583 private void PumpRequestOnEntry()584 {585 int command = this.RandomInteger(100) + 1;586 this.Counter++;587 this.SendEvent(this.NodeManager, new Request(this.Id, command));588 if (this.Counter is 1)589 {590 this.RaiseHaltEvent();591 }592 else593 {594 this.RaiseEvent(new LocalEvent());595 }596 }597 }598 private class LivenessMonitor : Monitor599 {600 public class ConfigureEvent : Event601 {602 public int NumberOfReplicas;603 public ConfigureEvent(int numOfReplicas)604 : base()605 {606 this.NumberOfReplicas = numOfReplicas;607 }608 }609 public class NotifyNodeCreated : Event610 {611 public int NodeId;612 public NotifyNodeCreated(int id)613 : base()614 {615 this.NodeId = id;616 }617 }618 public class NotifyNodeFail : Event619 {620 public int NodeId;621 public NotifyNodeFail(int id)622 : base()623 {624 this.NodeId = id;625 }626 }627 public class NotifyNodeUpdate : Event628 {629 public int NodeId;630 public int Data;631 public NotifyNodeUpdate(int id, int data)632 : base()633 {634 this.NodeId = id;635 this.Data = data;636 }637 }638 private class LocalEvent : Event639 {640 }641 private Dictionary<int, int> DataMap;642 private int NumberOfReplicas;643 [Start]644 [OnEntry(nameof(InitOnEntry))]645 [OnEventDoAction(typeof(ConfigureEvent), nameof(SetupEvent))]646 [OnEventGotoState(typeof(LocalEvent), typeof(Repaired))]647 private class Init : State648 {649 }650 private void InitOnEntry()651 {652 this.DataMap = new Dictionary<int, int>();653 }654 private void SetupEvent(Event e)655 {656 this.NumberOfReplicas = (e as ConfigureEvent).NumberOfReplicas;657 this.RaiseEvent(new LocalEvent());658 }659 [Cold]660 [OnEventDoAction(typeof(NotifyNodeCreated), nameof(ProcessNodeCreated))]661 [OnEventDoAction(typeof(NotifyNodeFail), nameof(FailAndCheckRepair))]662 [OnEventDoAction(typeof(NotifyNodeUpdate), nameof(ProcessNodeUpdate))]663 [OnEventGotoState(typeof(LocalEvent), typeof(Repairing))]664 private class Repaired : State665 {666 }667 private void ProcessNodeCreated(Event e)668 {...
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;6using Microsoft.Coyote.Actors.BugFinding.Services;7using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces;8using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Events;9using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces;10using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces.Events;11using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces.Messages;12using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces.Messages.Events;13{14 {15 static async Task Main(string[] args)16 {17 ActorId actorId = ActorId.CreateRandom();18 var runtime = BugFindingRuntime.Create();19 var request = new Request(actorId, runtime);20 request.SetupEvent(new RequestMessage("1", "2", "3", "4"));21 await runtime.RunAsync();22 }23 }24}25using System;26using System.Collections.Generic;27using System.Linq;28using System.Text;29using System.Threading.Tasks;30{31 {32 public string Id { get; }33 public string From { get; }34 public string To { get; }35 public string Message { get; }36 public RequestMessage(string id, string from, string to, string message)37 {38 this.Id = id;39 this.From = from;40 this.To = to;41 this.Message = message;42 }43 }44}45using System;46using System.Collections.Generic;47using System.Linq;48using System.Text;49using System.Threading.Tasks;50using Microsoft.Coyote.Actors;51using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces;52using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces.Events;53using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces.Messages.Events;54using Microsoft.Coyote.Actors.BugFinding.Services.Interfaces.Interfaces.Messages;
SetupEvent
Using AI Code Generation
1using System;2using System.Threading.Tasks;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Actors.BugFinding.Tests;5using Microsoft.Coyote.TestingServices;6using Microsoft.Coyote.TestingServices.Coverage;7using Microsoft.Coyote.TestingServices.SchedulingStrategies;8using Microsoft.Coyote.TestingServices.Tracing.Schedule;9using Microsoft.Coyote.TestingServices.Tracing.Schedule.Default;10using Microsoft.Coyote.Tests.Common;11using Xunit;12using Xunit.Abstractions;13{14 {15 public RequestTests(ITestOutputHelper output)16 : base(output)17 {18 }19 [Fact(Timeout = 5000)]20 public void TestRequest()21 {22 this.Test(r =>23 {24 r.CreateActor(typeof(Request));25 },26 configuration: GetConfiguration().WithTestingIterations(100),27 replay: true);28 }29 private static Configuration GetConfiguration()30 {31 var configuration = Configuration.Create();32 configuration.SchedulingStrategy = SchedulingStrategy.DFS;33 configuration.LivenessTemperatureThreshold = 100;34 configuration.SchedulingIterations = 1000;35 configuration.MaxFairSchedulingSteps = 1000;36 configuration.MaxUnfairSchedulingSteps = 1000;37 configuration.RandomSchedulingSeed = 1;38 configuration.TestReporters = new ITestReporter[] { new TextLogReporter() };39 configuration.TraceSchedule = true;40 configuration.TraceScheduling = true;41 configuration.TraceFilePath = "trace.log";42 return configuration;43 }44 }45}46using System;47using System.Threading.Tasks;48using Microsoft.Coyote.Actors;49using Microsoft.Coyote.Actors.BugFinding.Tests;50using Microsoft.Coyote.TestingServices;51using Microsoft.Coyote.TestingServices.Coverage;52using Microsoft.Coyote.TestingServices.SchedulingStrategies;53using Microsoft.Coyote.TestingServices.Tracing.Schedule;54using Microsoft.Coyote.TestingServices.Tracing.Schedule.Default;55using Microsoft.Coyote.Tests.Common;56using Xunit;57using Xunit.Abstractions;58{59 {
SetupEvent
Using AI Code Generation
1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using System;4using System.Collections.Generic;5using System.Linq;6using System.Text;7using System.Threading.Tasks;8{9 {10 static void Main(string[] args)11 {12 var runtime = RuntimeFactory.Create();13 var actor = runtime.CreateActor(typeof(MyActor));14 Request req = new Request();15 req.SetupEvent(new Event());16 runtime.SendEvent(actor, req);17 runtime.Dispose();18 }19 }20}
SetupEvent
Using AI Code Generation
1using Microsoft.Coyote.Actors.BugFinding.Tests;2using System;3using System.Collections.Generic;4using System.Linq;5using System.Text;6using System.Threading.Tasks;7{8 {9 static void Main(string[] args)10 {11 Request r = new Request();12 r.SetupEvent("1", "2", "3");13 Console.WriteLine("Request: " + r.ToString());14 Console.ReadLine();15 }16 }17}18Request: Microsoft.Coyote.Actors.BugFinding.Tests.Request: {Source: 1, Destination: 2, Content: 3}19using Microsoft.Coyote.Actors.BugFinding.Tests;20using System;21using System.Collections.Generic;22using System.Linq;23using System.Text;24using System.Threading.Tasks;25{26 {27 static void Main(string[] args)28 {29 Request r = new Request();30 r.Source = "1";31 r.Destination = "2";32 r.Content = "3";33 Console.WriteLine("Request: " + r.ToString());34 Console.ReadLine();35 }36 }37}38Request: Microsoft.Coyote.Actors.BugFinding.Tests.Request: {Source: 1, Destination: 2, Content: 3}39using Microsoft.Coyote.Actors.BugFinding.Tests;40using System;41using System.Collections.Generic;42using System.Linq;43using System.Text;44using System.Threading.Tasks;45{46 {47 static void Main(string[] args)48 {49 Request r = new Request();50 r.SetSource("1");51 r.SetDestination("2");52 r.SetContent("3");53 Console.WriteLine("Request: " + r.ToString());54 Console.ReadLine();55 }56 }57}58Request: Microsoft.Coyote.Actors.BugFinding.Tests.Request: {Source: 1, Destination: 2, Content: 3}
SetupEvent
Using AI Code Generation
1using System;2using System.Collections.Generic;3using System.Linq;4using System.Text;5using System.Threading.Tasks;6using Microsoft.Coyote.Actors.BugFinding.Tests;7using Microsoft.Coyote.Actors.BugFinding.Tests.Actors;8using Microsoft.Coyote.Actors.BugFinding.Tests.Events;9using Microsoft.Coyote.Actors.BugFinding.Tests.Machines;10using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities;11using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote;12using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime;13using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.EventLogs;14using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.EventLogs.Types;15using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies;16using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types;17using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.Events;18using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States;19using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events;20using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs;21using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs.Types;22using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs.Types.Events;23using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs.Types.Events.Types;24using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs.Types.Events.Types.States;25using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs.Types.Events.Types.States.Events;26using Microsoft.Coyote.Actors.BugFinding.Tests.Utilities.Coyote.Runtime.SchedulingStrategies.Types.States.Events.EventLogs.Types.Events.Types.States.Events.Types;
SetupEvent
Using AI Code Generation
1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4using Microsoft.Coyote.Actors;5using Microsoft.Coyote.Actors.BugFinding.Tests;6using Microsoft.VisualStudio.TestTools.UnitTesting;7{8 {9 private static ActorId actorId;10 private static ActorId actorId2;11 private static ActorId actorId3;12 public async Task TestMethod1()13 {14 actorId = ActorId.CreateRandom();15 actorId2 = ActorId.CreateRandom();16 actorId3 = ActorId.CreateRandom();17 var runtime = RuntimeFactory.Create();18 {19 Event = new E1()20 };21 request.SetupEvent();22 await runtime.CreateActorAndExecuteAsync(typeof(Actor1), actorId, request);23 }24 }25}26using System;27using System.Threading.Tasks;28using Microsoft.Coyote;29using Microsoft.Coyote.Actors;30using Microsoft.Coyote.Actors.BugFinding.Tests;31using Microsoft.VisualStudio.TestTools.UnitTesting;32{33 {34 protected override Task OnInitializeAsync(Event initialEvent)35 {36 var request = (Request)initialEvent;37 this.SendEvent(request.ActorId, request.Event);38 this.SendEvent(request.ActorId2, new E2());39 this.SendEvent(request.ActorId3, new E3
SetupEvent
Using AI Code Generation
1using Microsoft.Coyote.Actors.BugFinding.Tests;2using Microsoft.Coyote.Actors.BugFinding.Tests.Request;3using System;4using System.Threading.Tasks;5{6 {7 public int Value;8 public Request(int value)9 {10 Value = value;11 }12 }13 {14 public int Value;15 public Response(int value)16 {17 Value = value;18 }19 }20 {21 public int Value;22 public SetupEvent(int value)23 {24 Value = value;25 }26 }27}28using Microsoft.Coyote.Actors.BugFinding.Tests;29using Microsoft.Coyote.Actors.BugFinding.Tests.Request;30using System;31using System.Threading.Tasks;32{33 {34 public int Value;35 public Request(int value)36 {37 Value = value;38 }39 }40 {41 public int Value;42 public Response(int value)43 {44 Value = value;45 }46 }47 {48 public int Value;49 public SetupEvent(int value)50 {51 Value = value;52 }53 }54}55using Microsoft.Coyote.Actors.BugFinding.Tests;56using Microsoft.Coyote.Actors.BugFinding.Tests.Request;57using System;58using System.Threading.Tasks;59{60 {61 public int Value;62 public Request(int value)63 {64 Value = value;65 }66 }67 {68 public int Value;69 public Response(int value)70 {71 Value = value;72 }73 }74 {75 public int Value;76 public SetupEvent(int value)77 {78 Value = value;79 }80 }81}
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.
Most used method in Request
- Request
- InitOnEntry
- SetupEvent
- PumpRequestOnEntry
- ProcessResponse
- ConfigureEvent
- ActiveOnEntry
- Tick
- NotifyLeaderElected
- ProcessLeaderElected
- TestMultipleLeadersInRaftProtocol
- NotifyNodeCreated
- NotifyNodeFail
- NotifyNodeUpdate
- ProcessNodeCreated
- FailAndCheckRepair
- ProcessNodeUpdate
- ProcessNodeFail
- CheckIfRepaired
- TestReplicatingStorageLivenessBug
Try LambdaTest Now !!
Get 100 minutes of automation test minutes FREE!!
Was this article helpful?
