How to use InitOnEntry method of Microsoft.Coyote.Actors.BugFinding.Tests.EventHandlerTests class

Best Coyote code snippet using Microsoft.Coyote.Actors.BugFinding.Tests.EventHandlerTests.InitOnEntry

EventHandlerTests.cs

Source:EventHandlerTests.cs

...115        private class M1 : StateMachine116        {117            private bool Test = false;118            [Start]119            [OnEntry(nameof(InitOnEntry))]120            [OnEventDoAction(typeof(UnitEvent), nameof(HandleUnitEvent))]121            [OnEventDoAction(typeof(E1), nameof(HandleE1))]122            private class Init : State123            {124            }125            private void InitOnEntry()126            {127                this.SendEvent(this.Id, new E1());128                this.RaiseEvent(UnitEvent.Instance);129            }130            private void HandleUnitEvent()131            {132                this.Test = true;133            }134            private void HandleE1()135            {136                this.Assert(this.Test is false, "Reached test assertion.");137            }138        }139        [Fact(Timeout = 5000)]140        public void TestEventHandlerInStateMachine1()141        {142            this.TestWithError(r =>143            {144                r.CreateActor(typeof(M1));145            },146            expectedError: "Reached test assertion.",147            replay: true);148        }149        private class M2 : StateMachine150        {151            [Start]152            [OnEntry(nameof(InitOnEntry))]153            [OnEventDoAction(typeof(E1), nameof(HandleE1))]154            private class Init : State155            {156            }157            private void InitOnEntry()158            {159                this.SendEvent(this.Id, new E1());160            }161            private void HandleE1()162            {163                this.Assert(false, "Reached test assertion.");164            }165        }166        [Fact(Timeout = 5000)]167        public void TestEventHandlerInStateMachine2()168        {169            this.TestWithError(r =>170            {171                r.CreateActor(typeof(M2));172            },173            expectedError: "Reached test assertion.",174            replay: true);175        }176        private class M3 : StateMachine177        {178            [Start]179            [OnEntry(nameof(InitOnEntry))]180            [OnExit(nameof(InitOnExit))]181            [OnEventGotoState(typeof(UnitEvent), typeof(Active))]182            private class Init : State183            {184            }185            private void InitOnEntry()186            {187                this.SendEvent(this.Id, UnitEvent.Instance);188            }189            private void InitOnExit()190            {191                this.SendEvent(this.Id, new E1());192            }193            private class Active : State194            {195            }196        }197        [Fact(Timeout = 5000)]198        public void TestEventHandlerInStateMachine3()199        {200            this.TestWithError(r =>201            {202                r.CreateActor(typeof(M3));203            },204            expectedError: "M3() received event 'E1' that cannot be handled.",205            replay: true);206        }207        private class M4 : StateMachine208        {209            private bool Test = false;210            [Start]211            [OnEntry(nameof(InitOnEntry))]212            [OnExit(nameof(InitOnExit))]213            [OnEventGotoState(typeof(UnitEvent), typeof(Active))]214            private class Init : State215            {216            }217            private void InitOnEntry()218            {219                this.SendEvent(this.Id, UnitEvent.Instance);220            }221            private void InitOnExit()222            {223                this.SendEvent(this.Id, new E1());224            }225            [OnEntry(nameof(ActiveOnEntry))]226            [OnEventDoAction(typeof(E1), nameof(HandleE1))]227            private class Active : State228            {229            }230            private void ActiveOnEntry()231            {232                this.Test = true;233            }234            private void HandleE1()235            {236                this.Assert(this.Test is false, "Reached test assertion.");237            }238        }239        [Fact(Timeout = 5000)]240        public void TestEventHandlerInStateMachine4()241        {242            this.TestWithError(r =>243            {244                r.CreateActor(typeof(M4));245            },246            expectedError: "Reached test assertion.",247            replay: true);248        }249        private class M5 : StateMachine250        {251            [Start]252            [OnEntry(nameof(InitOnEntry))]253            [OnExit(nameof(InitOnExit))]254            [OnEventGotoState(typeof(UnitEvent), typeof(Init))]255            [OnEventDoAction(typeof(E1), nameof(HandleE1))]256            private class Init : State257            {258            }259            private void InitOnEntry()260            {261                this.SendEvent(this.Id, UnitEvent.Instance);262            }263            private void InitOnExit()264            {265                this.SendEvent(this.Id, new E1());266            }267            private void HandleE1()268            {269                this.Assert(false, "Reached test assertion.");270            }271        }272        [Fact(Timeout = 5000)]273        public void TestEventHandlerInStateMachine5()274        {275            this.TestWithError(r =>276            {277                r.CreateActor(typeof(M5));278            },279            expectedError: "Reached test assertion.",280            replay: true);281        }282        private class M6 : StateMachine283        {284            [Start]285            [OnEntry(nameof(InitOnEntry))]286            [OnExit(nameof(InitOnExit))]287            [OnEventGotoState(typeof(UnitEvent), typeof(Init))]288            [OnEventPushState(typeof(E1), typeof(Init))]289            private class Init : State290            {291            }292            private void InitOnEntry()293            {294                this.SendEvent(this.Id, UnitEvent.Instance, options: new SendOptions(assert: 1));295            }296            private void InitOnExit()297            {298                this.SendEvent(this.Id, new E1());299            }300        }301        [Fact(Timeout = 5000)]302        public void TestEventHandlerInStateMachine6()303        {304            this.TestWithError(r =>305            {306                r.CreateActor(typeof(M6));307            },308            expectedError: "There are more than 1 instances of 'Events.UnitEvent' in the input queue of M6().",309            replay: true);310        }311        private class M7 : StateMachine312        {313            [Start]314            [OnEntry(nameof(InitOnEntry))]315            [OnExit(nameof(InitOnExit))]316            [OnEventGotoState(typeof(UnitEvent), typeof(Init))]317            [OnEventPushState(typeof(E1), typeof(Active))]318            private class Init : State319            {320            }321            private void InitOnEntry()322            {323                this.SendEvent(this.Id, UnitEvent.Instance);324            }325            private void InitOnExit()326            {327                this.SendEvent(this.Id, new E1());328            }329            [OnEntry(nameof(ActiveOnEntry))]330            private class Active : State331            {332            }333            private void ActiveOnEntry()334            {335                this.Assert(false, "Reached test assertion.");336            }337        }338        [Fact(Timeout = 5000)]339        public void TestEventHandlerInStateMachine7()340        {341            this.TestWithError(r =>342            {343                r.CreateActor(typeof(M7));344            },345            expectedError: "Reached test assertion.",346            replay: true);347        }348        private class M8 : StateMachine349        {350            private bool Test = false;351            [Start]352            [OnEntry(nameof(InitOnEntry))]353            [OnExit(nameof(InitOnExit))]354            [OnEventGotoState(typeof(UnitEvent), typeof(Init))]355            [OnEventPushState(typeof(E1), typeof(Active))]356            [OnEventDoAction(typeof(E2), nameof(HandleE2))]357            private class Init : State358            {359            }360            private void InitOnEntry()361            {362                this.SendEvent(this.Id, UnitEvent.Instance);363            }364            private void InitOnExit()365            {366                this.SendEvent(this.Id, new E1());367            }368            [OnEntry(nameof(ActiveOnEntry))]369            private class Active : State370            {371            }372            private void ActiveOnEntry()373            {374                this.Test = true;375                this.SendEvent(this.Id, new E2());376            }377            private void HandleE2()378            {379                this.Assert(this.Test is false, "Reached test assertion.");380            }381        }382        [Fact(Timeout = 5000)]383        public void TestEventHandlerInStateMachine8()384        {385            this.TestWithError(r =>386            {387                r.CreateActor(typeof(M8));388            },389            expectedError: "Reached test assertion.",390            replay: true);391        }392        private class M9 : StateMachine393        {394            private bool Test = false;395            [Start]396            [OnEntry(nameof(InitOnEntry))]397            [OnExit(nameof(InitOnExit))]398            [OnEventPushState(typeof(UnitEvent), typeof(Active))]399            [OnEventDoAction(typeof(E2), nameof(HandleE2))]400            private class Init : State401            {402            }403            private void InitOnEntry()404            {405                this.SendEvent(this.Id, UnitEvent.Instance);406            }407            private void InitOnExit()408            {409                this.SendEvent(this.Id, new E1());410            }411            [OnEntry(nameof(ActiveOnEntry))]412            private class Active : State413            {414            }415            private void ActiveOnEntry()416            {417                this.Test = true;418                this.SendEvent(this.Id, new E2());419                this.RaisePopStateEvent();420            }421            private void HandleE2()422            {423                this.Assert(this.Test is false, "Reached test assertion.");424            }425        }426        [Fact(Timeout = 5000)]427        public void TestEventHandlerInStateMachine9()428        {429            this.TestWithError(r =>430            {431                r.CreateActor(typeof(M9));432            },433            expectedError: "Reached test assertion.",434            replay: true);435        }436        private class M10 : StateMachine437        {438            private bool Test = false;439            [Start]440            [OnEntry(nameof(InitOnEntry))]441            [OnExit(nameof(InitOnExit))]442            [OnEventPushState(typeof(UnitEvent), typeof(Active))]443            [OnEventDoAction(typeof(E2), nameof(HandleE2))]444            private class Init : State445            {446            }447            private void InitOnEntry()448            {449                this.SendEvent(this.Id, UnitEvent.Instance);450            }451            private void InitOnExit()452            {453                this.SendEvent(this.Id, new E1());454            }455            [OnEntry(nameof(ActiveOnEntry))]456            private class Active : State457            {458            }459            private void ActiveOnEntry()460            {461                this.Test = true;462                this.SendEvent(this.Id, new E2());463            }464            private void HandleE2()465            {466                this.Assert(this.Test is false, "Reached test assertion.");467            }468        }469        [Fact(Timeout = 5000)]470        public void TestEventHandlerInStateMachine10()471        {472            this.TestWithError(r =>473            {474                r.CreateActor(typeof(M10));475            },476            expectedError: "Reached test assertion.",477            replay: true);478        }479        private class M11 : StateMachine480        {481            private bool Test = false;482            [Start]483            [OnEntry(nameof(InitOnEntry))]484            [OnEventGotoState(typeof(UnitEvent), typeof(Active))]485            [OnEventGotoState(typeof(E2), typeof(Checking))]486            private class Init : State487            {488            }489            private void InitOnEntry()490            {491                this.SendEvent(this.Id, UnitEvent.Instance);492            }493            [OnEntry(nameof(ActiveOnEntry))]494            [OnExit(nameof(ActiveOnExit))]495            [OnEventGotoState(typeof(E2), typeof(Init))]496            private class Active : State497            {498            }499            private void ActiveOnEntry()500            {501                this.Test = true;502                this.SendEvent(this.Id, new E2());503            }504            private void ActiveOnExit()505            {506                this.SendEvent(this.Id, new E2());507            }508            [OnEntry(nameof(CheckingOnEntry))]509            private class Checking : State510            {511            }512            private void CheckingOnEntry()513            {514                this.Assert(this.Test is false, "Reached test assertion.");515            }516        }517        [Fact(Timeout = 5000)]518        public void TestEventHandlerInStateMachine11()519        {520            this.TestWithError(r =>521            {522                r.CreateActor(typeof(M11));523            },524            expectedError: "Reached test assertion.",525            replay: true);526        }527        private class M12 : StateMachine528        {529            private bool Test = false;530            [Start]531            [OnEntry(nameof(InitOnEntry))]532            [OnExit(nameof(InitOnExit))]533            [OnEventGotoState(typeof(UnitEvent), typeof(Init))]534            [OnEventPushState(typeof(E1), typeof(Active))]535            [OnEventDoAction(typeof(E2), nameof(HandleE2))]536            private class Init : State537            {538            }539            private void InitOnEntry()540            {541                this.SendEvent(this.Id, UnitEvent.Instance);542            }543            private void InitOnExit()544            {545                this.SendEvent(this.Id, new E1());546            }547            [OnEntry(nameof(ActiveOnEntry))]548            [OnExit(nameof(ActiveOnExit))]549            [OnEventGotoState(typeof(E2), typeof(Init))]550            private class Active : State551            {552            }553            private void ActiveOnEntry()554            {555                this.Test = true;556                this.SendEvent(this.Id, new E2());557            }558            private void ActiveOnExit()559            {560                this.Assert(this.Test is false, "Reached test assertion.");561            }562#pragma warning disable CA1822 // Mark members as static563            private void HandleE2()564#pragma warning restore CA1822 // Mark members as static565            {566            }567        }568        [Fact(Timeout = 5000)]569        public void TestEventHandlerInStateMachine12()570        {571            this.TestWithError(r =>572            {573                r.CreateActor(typeof(M12));574            },575            expectedError: "Reached test assertion.",576            replay: true);577        }578        private class M13 : StateMachine579        {580            private bool Test = false;581            [Start]582            [OnEntry(nameof(InitOnEntry))]583            [OnExit(nameof(InitOnExit))]584            [OnEventPushState(typeof(UnitEvent), typeof(Active))]585            [OnEventDoAction(typeof(E2), nameof(HandleE2))]586            private class Init : State587            {588            }589            private void InitOnEntry()590            {591                this.SendEvent(this.Id, UnitEvent.Instance);592            }593            private void InitOnExit()594            {595                this.SendEvent(this.Id, new E1());596            }597            [OnEntry(nameof(ActiveOnEntry))]598            [OnExit(nameof(ActiveOnExit))]599            private class Active : State600            {601            }602            private void ActiveOnEntry()603            {604                this.Test = true;605                this.RaisePopStateEvent();606            }607            private void ActiveOnExit()608            {609                this.SendEvent(this.Id, new E2());610            }611            private void HandleE2()612            {613                this.Assert(this.Test is false, "Reached test assertion.");614            }615        }616        [Fact(Timeout = 5000)]617        public void TestEventHandlerInStateMachine13()618        {619            this.TestWithError(r =>620            {621                r.CreateActor(typeof(M13));622            },623            expectedError: "Reached test assertion.",624            replay: true);625        }626        private class M14 : StateMachine627        {628            [Start]629            [OnEntry(nameof(InitOnEntry))]630            [OnExit(nameof(InitOnExit))]631            [OnEventGotoState(typeof(UnitEvent), typeof(Init))]632            [OnEventPushState(typeof(E1), typeof(Active))]633            [OnEventDoAction(typeof(E2), nameof(HandleE2))]634            private class Init : State635            {636            }637            private void InitOnEntry()638            {639                this.SendEvent(this.Id, UnitEvent.Instance, options: new SendOptions(assert: 1));640            }641            private void InitOnExit()642            {643                this.SendEvent(this.Id, new E1());644            }645            [OnEntry(nameof(ActiveOnEntry))]646            private class Active : State647            {648            }649            private void ActiveOnEntry() => this.RaiseEvent(UnitEvent.Instance);650#pragma warning disable CA1822 // Mark members as static651            private void HandleE2()652#pragma warning restore CA1822 // Mark members as static653            {654            }655        }656        [Fact(Timeout = 5000)]657        public void TestEventHandlerInStateMachine14()658        {659            this.TestWithError(r =>660            {661                r.CreateActor(typeof(M14));662            },663            expectedError: "There are more than 1 instances of 'Events.UnitEvent' in the input queue of M14().",664            replay: true);665        }666        private class M15 : StateMachine667        {668            [Start]669            [OnEntry(nameof(InitOnEntry))]670            [OnEventPushState(typeof(UnitEvent), typeof(Active))]671            private class Init : State672            {673            }674            private void InitOnEntry() => this.RaiseEvent(UnitEvent.Instance);675            [OnEntry(nameof(ActiveOnEntry))]676            [OnExit(nameof(ActiveOnExit))]677            private class Active : State678            {679            }680            private void ActiveOnEntry() => this.RaisePopStateEvent();681            private void ActiveOnExit()682            {683                this.Assert(false, "Reached test assertion.");684            }685        }686        [Fact(Timeout = 5000)]687        public void TestEventHandlerInStateMachine15()688        {689            this.TestWithError(r =>690            {691                r.CreateActor(typeof(M15));692            },693            expectedError: "Reached test assertion.",694            replay: true);695        }696        private class M16 : StateMachine697        {698            private bool Test = false;699            [Start]700            [OnEntry(nameof(InitOnEntry))]701            [OnEventPushState(typeof(HaltEvent), typeof(Active))]702            [OnEventDoAction(typeof(UnitEvent), nameof(HandleUnitEvent))]703            private class Init : State704            {705            }706            private void InitOnEntry()707            {708                this.SendEvent(this.Id, UnitEvent.Instance);709                this.RaiseEvent(HaltEvent.Instance);710            }711            [OnEntry(nameof(ActiveOnEntry))]712            private class Active : State713            {714            }715            private void ActiveOnEntry()716            {717                this.Test = true;718            }719            private void HandleUnitEvent()720            {721                this.Assert(this.Test is false, "Reached test assertion.");722            }723        }724        [Fact(Timeout = 5000)]725        public void TestEventHandlerInStateMachine16()726        {727            this.TestWithError(r =>728            {729                r.CreateActor(typeof(M16));730            },731            expectedError: "Reached test assertion.",732            replay: true);733        }734        private class M17 : StateMachine735        {736            private bool Test = false;737            [Start]738            [OnEntry(nameof(InitOnEntry))]739            [OnEventGotoState(typeof(DefaultEvent), typeof(Active))]740            [OnEventDoAction(typeof(UnitEvent), nameof(HandleUnitEvent))]741            [OnEventDoAction(typeof(E1), nameof(HandleE1))]742            private class Init : State743            {744            }745            private void InitOnEntry() => this.RaiseEvent(new E1());746            private void HandleUnitEvent()747            {748                this.Test = true;749            }750            private void HandleE1()751            {752                this.SendEvent(this.Id, UnitEvent.Instance);753            }754            [OnEntry(nameof(ActiveOnEntry))]755            private class Active : State756            {757            }758            private void ActiveOnEntry()759            {760                this.Assert(this.Test is false, "Reached test assertion.");761            }762        }763        [Fact(Timeout = 5000)]764        public void TestEventHandlerInStateMachine17()765        {766            this.TestWithError(r =>767            {768                r.CreateActor(typeof(M17));769            },770            expectedError: "Reached test assertion.",771            replay: true);772        }773        private class M18 : StateMachine774        {775            private readonly bool Test = false;776            [Start]777            [OnEventGotoState(typeof(DefaultEvent), typeof(Active))]778            private class Init : State779            {780            }781            [OnEntry(nameof(ActiveOnEntry))]782            private class Active : State783            {784            }785            private void ActiveOnEntry()786            {787                this.Assert(this.Test is true, "Reached test assertion.");788            }789        }790        [Fact(Timeout = 5000)]791        public void TestEventHandlerInStateMachine18()792        {793            this.TestWithError(r =>794            {795                r.CreateActor(typeof(M18));796            },797            expectedError: "Reached test assertion.",798            replay: true);799        }800        private class M19 : StateMachine801        {802            private int Value;803            [Start]804            [OnEntry(nameof(InitOnEntry))]805            [OnEventPushState(typeof(UnitEvent), typeof(Active))]806            [OnEventDoAction(typeof(DefaultEvent), nameof(DefaultAction))]807            private class Init : State808            {809            }810            private void InitOnEntry()811            {812                this.Value = 0;813                this.RaiseEvent(UnitEvent.Instance);814            }815            private void DefaultAction()816            {817                this.Assert(false, "Reached test assertion.");818            }819            [OnEntry(nameof(ActiveOnEntry))]820            [IgnoreEvents(typeof(UnitEvent))]821            private class Active : State822            {823            }824            private void ActiveOnEntry()825            {826                if (this.Value is 0)827                {828                    this.RaiseEvent(UnitEvent.Instance);829                }830                else831                {832                    this.Value++;833                }834            }835        }836        [Fact(Timeout = 5000)]837        public void TestEventHandlerInStateMachine19()838        {839            this.TestWithError(r =>840            {841                r.CreateActor(typeof(M19));842            },843            expectedError: "Reached test assertion.",844            replay: true);845        }846        private class M20 : StateMachine847        {848            [Start]849            [OnEventGotoState(typeof(DefaultEvent), typeof(Active))]850            private class Init : State851            {852            }853            [OnEntry(nameof(ActiveOnEntry))]854            private class Active : State855            {856            }857            private void ActiveOnEntry(Event e)858            {859                this.Assert(e.GetType() == typeof(DefaultEvent));860            }861        }862        [Fact(Timeout = 5000)]863        public void TestEventHandlerInStateMachine20()864        {865            this.Test(r =>866            {867                r.CreateActor(typeof(M20));868            });869        }870        private class M21a : StateMachine871        {872            private ActorId GhostMachine;873            private bool Test = false;874            [Start]875            [OnEntry(nameof(InitOnEntry))]876            [OnExit(nameof(ExitInit))]877            [OnEventGotoState(typeof(E1), typeof(S1))] // exit actions are performed before transition to S1878            [OnEventDoAction(typeof(E3), nameof(Action1))] // E3, E2 have no effect on reachability of assert(false)879            private class Init : State880            {881            }882            private void InitOnEntry()883            {884                this.GhostMachine = this.CreateActor(typeof(M21b));885                this.SendEvent(this.GhostMachine, new SetupEvent(this.Id));886                this.SendEvent(this.GhostMachine, UnitEvent.Instance);887            }888            private void ExitInit()889            {890                this.Test = true;891            }892            [OnEntry(nameof(EntryS1))]893            [OnEventGotoState(typeof(UnitEvent), typeof(S2))]894            private class S1 : State895            {896            }897            private void EntryS1()898            {899                this.Assert(this.Test is true);900                this.RaiseEvent(UnitEvent.Instance);901            }902            [OnEntry(nameof(EntryS2))]903            private class S2 : State904            {905            }906            private void EntryS2()907            {908                // This assert is reachable: M1A -UnitEvent-> M1B -E1-> M1A;909                // then Real_S1 (assert holds), Real_S2 (assert fails)910                this.Assert(false, "Reached test assertion.");911            }912            private void Action1()913            {914                this.SendEvent(this.GhostMachine, new E2());915            }916        }917        private class M21b : StateMachine918        {919            private ActorId RealMachine;920            [Start]921            [OnEventDoAction(typeof(SetupEvent), nameof(SetupEvent))]922            [OnEventGotoState(typeof(UnitEvent), typeof(S1))]923            private class Init : State924            {925            }926            private void SetupEvent(Event e)927            {928                this.RealMachine = (e as SetupEvent).Id;929            }930            [OnEntry(nameof(EntryS1))]931            [OnEventGotoState(typeof(E2), typeof(S2))]932            private class S1 : State933            {934            }935            private void EntryS1()936            {937                this.SendEvent(this.RealMachine, new E3());938                this.SendEvent(this.RealMachine, new E1());939            }940            private class S2 : State941            {942            }943        }944        [Fact(Timeout = 5000)]945        public void TestEventHandlerInStateMachine21()946        {947            this.TestWithError(r =>948            {949                r.CreateActor(typeof(M21a));950            },951            configuration: this.GetConfiguration().WithDFSStrategy(),952            expectedError: "Reached test assertion.",953            replay: true);954        }955        private class M22a : StateMachine956        {957            private ActorId GhostMachine;958            [Start]959            [OnEntry(nameof(InitOnEntry))]960            [OnEventGotoState(typeof(E3), typeof(S2))]961            [OnEventPushState(typeof(UnitEvent), typeof(S1))]962            [OnEventDoAction(typeof(E1), nameof(Action1))]963            private class Init : State964            {965            }966            private void InitOnEntry()967            {968                this.GhostMachine = this.CreateActor(typeof(M22b));969                this.SendEvent(this.GhostMachine, new SetupEvent(this.Id));970                this.RaiseEvent(UnitEvent.Instance);971            }972            [OnEntry(nameof(EntryS1))]973            private class S1 : State974            {975            }976            private void EntryS1()977            {978                this.SendEvent(this.GhostMachine, UnitEvent.Instance);979                // We wait in this state until E1 comes from M2B,980                // then handle E1 using the inherited handler Action1981                // installed by Init.982                // Then wait until E3 comes from M2B, and since983                // there's no handler for E3 in this pushed state,984                // this state is popped, and E3 goto handler from Init985                // is invoked.986            }987            [OnEntry(nameof(EntryS2))]988            private class S2 : State989            {990            }991            private void EntryS2()992            {993                // This assert is reachable.994                this.Assert(false, "Reached test assertion.");995            }996            private void Action1()997            {998                this.SendEvent(this.GhostMachine, new E2());999            }1000        }1001        private class M22b : StateMachine1002        {1003            private ActorId RealMachine;1004            [Start]1005            [OnEventDoAction(typeof(SetupEvent), nameof(SetupEvent))]1006            [OnEventGotoState(typeof(UnitEvent), typeof(S1))]1007            private class Init : State1008            {1009            }1010            private void SetupEvent(Event e)1011            {1012                this.RealMachine = (e as SetupEvent).Id;1013            }1014            [OnEntry(nameof(EntryS1))]1015            [OnEventGotoState(typeof(E2), typeof(S2))]1016            private class S1 : State1017            {1018            }1019            private void EntryS1()1020            {1021                this.SendEvent(this.RealMachine, new E1());1022            }1023            [OnEntry(nameof(EntryS2))]1024            private class S2 : State1025            {1026            }1027            private void EntryS2()1028            {1029                this.SendEvent(this.RealMachine, new E3());1030            }1031        }1032        [Fact(Timeout = 5000)]1033        public void TestEventHandlerInStateMachine22()1034        {1035            this.TestWithError(r =>1036            {1037                r.CreateActor(typeof(M22a));1038            },1039            configuration: this.GetConfiguration().WithDFSStrategy(),1040            expectedError: "Reached test assertion.",1041            replay: true);1042        }1043        private class M23a : StateMachine1044        {1045            private ActorId GhostMachine;1046            [Start]1047            [OnEntry(nameof(InitOnEntry))]1048            [OnEventGotoState(typeof(E3), typeof(S2))]1049            [OnEventPushState(typeof(UnitEvent), typeof(S1))]1050            [OnEventDoAction(typeof(E4), nameof(Action1))]1051            private class Init : State1052            {1053            }1054            private void InitOnEntry()1055            {1056                this.GhostMachine = this.CreateActor(typeof(M23b));1057                this.SendEvent(this.GhostMachine, new SetupEvent(this.Id));1058                this.RaiseEvent(UnitEvent.Instance);1059            }1060            [OnEntry(nameof(EntryS1))]1061            private class S1 : State1062            {1063            }1064            private void EntryS1()1065            {1066                this.SendEvent(this.GhostMachine, UnitEvent.Instance);1067            }1068            [OnEntry(nameof(EntryS2))]...

InitOnEntry

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.Coyote.Specifications;7using Microsoft.Coyote.SystematicTesting;8using Microsoft.Coyote.Tasks;9{10    {11        static void Main(string[] args)12        {13            var configuration = Configuration.Create();14            configuration.TestingIterations = 1;15            configuration.SchedulingIterations = 1;16            configuration.EnableDataRaceDetection = true;17            var test = new EventHandlerTests();18            test.InitOnEntry(configuration);19        }20    }21}22using System;23using System.Threading.Tasks;24using Microsoft.Coyote;25using Microsoft.Coyote.Actors;26using Microsoft.Coyote.Actors.BugFinding.Tests;27using Microsoft.Coyote.Specifications;28using Microsoft.Coyote.SystematicTesting;29using Microsoft.Coyote.Tasks;30{31    {32        static void Main(string[] args)33        {34            var configuration = Configuration.Create();35            configuration.TestingIterations = 1;36            configuration.SchedulingIterations = 1;37            configuration.EnableDataRaceDetection = true;38            var test = new EventHandlerTests();39            test.InitOnEntry(configuration);40        }41    }42}43using System;44using System.Threading.Tasks;45using Microsoft.Coyote;46using Microsoft.Coyote.Actors;47using Microsoft.Coyote.Actors.BugFinding.Tests;48using Microsoft.Coyote.Specifications;49using Microsoft.Coyote.SystematicTesting;50using Microsoft.Coyote.Tasks;51{52    {53        static void Main(string[] args)54        {55            var configuration = Configuration.Create();56            configuration.TestingIterations = 1;57            configuration.SchedulingIterations = 1;58            configuration.EnableDataRaceDetection = true;59            var test = new EventHandlerTests();60            test.InitOnEntry(configuration);61        }62    }63}

InitOnEntry

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4using Microsoft.Coyote.Actors;5using Microsoft.Coyote.Testing;6using Microsoft.Coyote.Testing.Systematic;7using Microsoft.Coyote.Actors.BugFinding.Tests;8using Microsoft.Coyote.Actors.BugFinding.Tests.Systematic;9{10    {11        static void Main(string[] args)12        {13            RunSystematic();14        }15        static void RunSynchronous()16        {17            SynchronousEngine engine = new SynchronousEngine();18            CoyoteRuntime runtime = CoyoteRuntime.CreateFromConfiguration(19                configuration: Configuration.Create().WithTestingIterations(100),20                testHooks: new EventHandlerTests(),21                engine: engine);22            runtime.CreateActor(typeof(EventHandlerTests), new Event());23        }24        static void RunSystematic()25        {26            SystematicTestingEngine engine = new SystematicTestingEngine();27            CoyoteRuntime runtime = CoyoteRuntime.CreateFromConfiguration(28                configuration: Configuration.Create().WithTestingIterations(100),29                testHooks: new EventHandlerTests(),30                engine: engine);31            runtime.CreateActor(typeof(EventHandlerTests), new Event());32        }33    }34}35using System;36using System.Threading.Tasks;37using Microsoft.Coyote;38using Microsoft.Coyote.Actors;39using Microsoft.Coyote.Testing;40using Microsoft.Coyote.Testing.Systematic;41using Microsoft.Coyote.Actors.BugFinding.Tests;42using Microsoft.Coyote.Actors.BugFinding.Tests.Systematic;43{44    {45        static void Main(string[] args)46        {47            RunSystematic();48        }49        static void RunSynchronous()50        {51            SynchronousEngine engine = new SynchronousEngine();

InitOnEntry

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.Strategies;7using Microsoft.Coyote.Actors.BugFinding.Strategies.Scheduling;8using Microsoft.Coyote.Actors.BugFinding.Strategies.FaultInjection;9using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration;10using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies;11using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.Cache;12using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR;13using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching;14using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Memory;15using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence;16using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores;17using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.Disk;18using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.Memory;19using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.Redis;20using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.SqlServer;21using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.Sqlite;22using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.MongoDB;23using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.AzureStorage;24using Microsoft.Coyote.Actors.BugFinding.Strategies.StateExploration.Strategies.DPOR.StateCaching.Persistence.Stores.AzureCosmosDB;

InitOnEntry

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote.Actors;4using Microsoft.Coyote.Actors.BugFinding;5using Microsoft.Coyote.Actors.BugFinding.Tests;6using Microsoft.Coyote.TestingServices;7using Xunit;8using Xunit.Abstractions;9{10    {11        public BugFindingTests(ITestOutputHelper output)12            : base(output)13        {14        }15        [Fact(Timeout = 5000)]16        public void TestEventHandlerInitOnEntry()17        {18            this.Test(r =>19            {20                r.RegisterMonitor<EventHandlerTests.EventHandlerMonitor>();21                r.CreateActor(typeof(EventHandlerTests.EventHandler));22            },23            configuration: GetConfiguration().WithTestingIterations(100));24        }25    }26}

InitOnEntry

Using AI Code Generation

1using System;2using System.Threading.Tasks;3using Microsoft.Coyote;4using Microsoft.Coyote.Actors;5using Microsoft.Coyote.Specifications;6using Microsoft.Coyote.TestingServices;7using Microsoft.Coyote.TestingServices.Runtime;8using Microsoft.Coyote.TestingServices.Threading;9using Microsoft.Coyote.Tests.Common;10using Microsoft.Coyote.Tests.Common.Actors;11using Microsoft.Coyote.Tests.Common.Actors.BugFinding;12using Microsoft.Coyote.Tests.Common.Actors.BugFinding.Tasks;13using Microsoft.Coyote.Tests.Common.Actors.BugFinding.Utilities;14using Microsoft.Coyote.Tests.Common.Actors.EventHandlers;15using Microsoft.Coyote.Tests.Common.Actors.EventHandlers.BugFinding;16using Microsoft.Coyote.Tests.Common.Actors.EventHandlers.BugFinding.Tasks;17using Microsoft.Coyote.Tests.Common.Actors.EventHandlers.BugFinding.Utilities;18using Microsoft.Coyote.Tests.Common.Actors.Runtime;19using Microsoft.Coyote.Tests.Common.Actors.Runtime.BugFinding;20using Microsoft.Coyote.Tests.Common.Actors.Runtime.BugFinding.Tasks;21using Microsoft.Coyote.Tests.Common.Actors.Runtime.BugFinding.Utilities;22using Microsoft.Coyote.Tests.Common.Actors.StateMachines;23using Microsoft.Coyote.Tests.Common.Actors.StateMachines.BugFinding;24using Microsoft.Coyote.Tests.Common.Actors.StateMachines.BugFinding.Tasks;25using Microsoft.Coyote.Tests.Common.Actors.StateMachines.BugFinding.Utilities;26using Microsoft.Coyote.Tests.Common.Actors.StateMachines.Runtime;27using Microsoft.Coyote.Tests.Common.Actors.StateMachines.Runtime.BugFinding;28using Microsoft.Coyote.Tests.Common.Actors.StateMachines.Runtime.BugFinding.Tasks;29using Microsoft.Coyote.Tests.Common.Actors.StateMachines.Runtime.BugFinding.Utilities;30using Microsoft.Coyote.Tests.Common.Actors.Utilities;31using Microsoft.Coyote.Tests.Common.Actors.Utilities.BugFinding;32using Microsoft.Coyote.Tests.Common.Actors.Utilities.BugFinding.Tasks;33using Microsoft.Coyote.Tests.Common.Actors.Utilities.BugFinding.Utilities;34using Microsoft.Coyote.Tests.Common.Runtime;35using Microsoft.Coyote.Tests.Common.Runtime.BugFinding;36using Microsoft.Coyote.Tests.Common.Runtime.BugFinding.Tasks;37using Microsoft.Coyote.Tests.Common.Runtime.BugFinding.Utilities;38using Microsoft.Coyote.Tests.Common.Threading;39using Microsoft.Coyote.Tests.Common.Threading.BugFinding;40using Microsoft.Coyote.Tests.Common.Threading.BugFinding.Tasks;

InitOnEntry

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using Microsoft.Coyote.Testing;4using System;5using System.Threading.Tasks;6{7    {8        static void Main(string[] args)9        {10            var runtime = RuntimeFactory.Create();11            var test = new EventHandlerTests();12            runtime.Test(r => test.InitOnEntry(r));13        }14    }15}16using Microsoft.Coyote.Actors;17using Microsoft.Coyote.Actors.BugFinding.Tests;18using Microsoft.Coyote.Testing;19using System;20using System.Threading.Tasks;21{22    {23        static void Main(string[] args)24        {25            var runtime = RuntimeFactory.Create();26            var test = new EventHandlerTests();27            runtime.Test(r => test.InitOnEntry(r));28        }29    }30}31using Microsoft.Coyote.Actors;32using Microsoft.Coyote.Actors.BugFinding.Tests;33using Microsoft.Coyote.Testing;34using System;35using System.Threading.Tasks;36{37    {38        static void Main(string[] args)39        {40            var runtime = RuntimeFactory.Create();41            var test = new EventHandlerTests();42            runtime.Test(r => test.InitOnEntry(r));43        }44    }45}46using Microsoft.Coyote.Actors;47using Microsoft.Coyote.Actors.BugFinding.Tests;48using Microsoft.Coyote.Testing;49using System;50using System.Threading.Tasks;51{

InitOnEntry

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using Microsoft.Coyote.Actors.BugFinding.Tests;3using System;4using System.Threading.Tasks;5{6    {7        static void Main(string[] args)8        {9            var config = Configuration.Create();10            config.TestingIterations = 100;11            config.SchedulingIterations = 1000;12            config.MaxFairSchedulingSteps = 1000;13            config.MaxUnfairSchedulingSteps = 1000;14            config.MaxStepsFromEntry = 1000;15            config.MaxStepsFromAnyAction = 1000;16            config.MaxStepsFromAnyChoice = 1000;17            config.MaxStepsFromAnySend = 1000;18            config.MaxStepsFromAnyReceive = 1000;19            config.MaxStepsFromAnyWait = 1000;20            config.MaxStepsFromAnyWaitAsync = 1000;21            config.MaxStepsFromAnyDefer = 1000;22            config.MaxStepsFromAnyPushState = 1000;23            config.MaxStepsFromAnyPopState = 1000;24            config.MaxStepsFromAnyRaiseEvent = 1000;25            config.MaxStepsFromAnyGotoState = 1000;26            config.MaxStepsFromAnyInvoke = 1000;27            config.MaxStepsFromAnyNondet = 1000;28            config.MaxStepsFromAnyNondetChoice = 1000;29            config.MaxStepsFromAnyNondetSend = 1000;30            config.MaxStepsFromAnyNondetReceive = 1000;31            config.MaxStepsFromAnyNondetWait = 1000;32            config.MaxStepsFromAnyNondetWaitAsync = 1000;33            config.MaxStepsFromAnyNondetDefer = 1000;34            config.MaxStepsFromAnyNondetPushState = 1000;35            config.MaxStepsFromAnyNondetPopState = 1000;36            config.MaxStepsFromAnyNondetRaiseEvent = 1000;37            config.MaxStepsFromAnyNondetGotoState = 1000;38            config.MaxStepsFromAnyNondetInvoke = 1000;39            config.MaxStepsFromAnyNondetBooleanChoice = 1000;40            config.MaxStepsFromAnyNondetIntegerChoice = 1000;41            config.MaxStepsFromAnyNondetMachineChoice = 1000;

InitOnEntry

Using AI Code Generation

1using Microsoft.Coyote.Actors.BugFinding.Tests;2EventHandlerTests.InitOnEntry();3using Microsoft.Coyote.Actors.BugFinding.Tests;4StateMachineTests.InitOnEntry();5using Microsoft.Coyote.Actors.BugFinding.Tests;6MachineTests.InitOnEntry();7using Microsoft.Coyote.Actors.BugFinding.Tests;8ActorTests.InitOnEntry();9using Microsoft.Coyote.Actors.BugFinding.Tests;10EventTests.InitOnEntry();11using Microsoft.Coyote.Actors.BugFinding.Tests;12TaskTests.InitOnEntry();13using Microsoft.Coyote.Actors.BugFinding.Tests;14TaskCompletionSourceTests.InitOnEntry();15using Microsoft.Coyote.Actors.BugFinding.Tests;16TaskCompletionSourceTests.InitOnEntry();17using Microsoft.Coyote.Actors.BugFinding.Tests;18TaskCompletionSourceTests.InitOnEntry();19using Microsoft.Coyote.Actors.BugFinding.Tests;20TaskCompletionSourceTests.InitOnEntry();21using Microsoft.Coyote.Actors.BugFinding.Tests;22TaskCompletionSourceTests.InitOnEntry();23using Microsoft.Coyote.Actors.BugFinding.Tests;24TaskCompletionSourceTests.InitOnEntry();

InitOnEntry

Using AI Code Generation

1using Microsoft.Coyote.Actors;2using System.Threading.Tasks;3{4    {5        {6            public ActorId Id;7            public TaskCompletionSource<bool> Tcs;8            public E(ActorId id, TaskCompletionSource<bool> tcs)9            {10                this.Id = id;11                this.Tcs = tcs;12            }13        }14        {15            public ActorId Id;16            public M(ActorId id)17            {18                this.Id = id;19            }20        }21        {22            public ActorId Id;23            public N(ActorId id)24            {25                this.Id = id;26            }27        }28        {29            protected override Task OnInitializeAsync(Event initialEvent)30            {31                this.RegisterEventHandler<E>(this.Handle);32                return Task.CompletedTask;33            }34            private Task Handle(Event e)35            {36                var ee = e as E;37                this.SendEvent(ee.Id, new M(this.Id));38                ee.Tcs.SetResult(true);39                return Task.CompletedTask;40            }41        }42        {43            protected override Task OnInitializeAsync(Event initialEvent)44            {45                this.RegisterEventHandler<M>(this.Handle);46                return Task.CompletedTask;47            }48            private Task Handle(Event e)49            {50                var me = e as M;51                this.SendEvent(me.Id, new N(this.Id));52                return Task.CompletedTask;53            }54        }55        {56            protected override Task OnInitializeAsync(Event initialEvent)57            {58                this.RegisterEventHandler<N>(this.Handle);59                return Task.CompletedTask;60            }61            private Task Handle(Event e)62            {63                var ne = e as N;64                this.SendEvent(ne.Id, new Halt());65                return Task.CompletedTask;66            }67        }68        [Fact(Timeout = 5000)]69        public async Task TestEventHandler()70        {71            var tcs = new TaskCompletionSource<bool>();72            var a = this.CreateActor(typeof(A));73            var b = this.CreateActor(typeof(B));74            var c = this.CreateActor(typeof(C));75            this.SendEvent(a, new E(b, tcs));76            this.SendEvent(b, new M(c));

InitOnEntry

Using AI Code Generation

1using System;2{3    {4        public static void Main(string[] args)5        {6            InitOnEntry();7        }8    }9}

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.