You signed in with another tab or window.Reload to refresh your session.You signed out in another tab or window.Reload to refresh your session.You switched accounts on another tab or window.Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Aug 26, 2022. It is now read-only.
Copy file name to clipboardExpand all lines: Docs/Testing/UnitTesting.md
+49-44Lines changed: 49 additions & 44 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -4,21 +4,24 @@ The `MachineTestKit` API provides the capability to _unit-test_ a machine of typ
4
4
5
5
We will now discuss how to use`MachineTestKit` by going through some simple examples.
6
6
7
-
Say that you have the following machine`M`, whichhas a method`Add(int m, int k)` that takes two integers, adds them, and returnstheresult:
7
+
Say that you have the following machine`M`, whichwaits to receive an event of type`E` (via the`Receive` statement) in the`InitOnEntry` handler ofthe`Start` state`Init`:
8
8
```C#
9
+
privateclassE :Event {}
10
+
9
11
privateclassM :Machine
10
12
{
11
13
[Start]
14
+
[OnEntry(nameof(InitOnEntry))]
12
15
privateclassInit :MachineState {}
13
16
14
-
internalintAdd(intm,intk)
17
+
privateasyncTaskInitOnEntry()
15
18
{
16
-
returnm+k;
19
+
awaitthis.Receive(typeof(E));
17
20
}
18
21
}
19
22
```
20
23
21
-
To unit-test the above`Add` machine method, first import the`Microsoft.PSharp.TestingServices` library:
24
+
To unit-test the abovelogic, first import the`Microsoft.PSharp.TestingServices` library:
22
25
```C#
23
26
usingMicrosoft.PSharp.TestingServices;
24
27
```
@@ -33,7 +36,46 @@ public void Test()
33
36
34
37
When`MachineTestKit<M>` is instantiated, it creates an instance of the machine`M`, which executes in a special runtime that provides isolation. The internals of the machine (e.g. the queue) are properly initialized, as if the machine was executing in production. However, if the machine is trying to create other machines, it will get a_dummy_`MachineId`, and if the machine tries to send an event to a machine other than itself, that event will be dropped. Talking to external APIs (e.g. network or storage) might still require mocking (as is the case in regular unit-testing).
35
38
36
-
The`MachineTestKit<M>` instance gives you access to the machine reference through the`MachineTestKit.Machine` property, as seen below. You can use this referene to directly invoke methods of the machine, in a unit-testing fashion. We also provide`MachineTestKit.Assert`, which is a generic assertion that you can use for checking correctness, as well as several build-in assertions, e.g. for asserting state transitions, or if the inbox is empty (and more assertions can be added based on user feedback).
39
+
The`MachineTestKit` provides two APIs that allow someone to asynchronously (but sequentially) interact with the machine via its inbox, and thus test how the machine transitions to different states and handles events. These two APIs are`StartMachineAsync(Event initialEvent = null)` and`SendEventAsync(Event e)`.
40
+
41
+
The`StartMachineAsync` method transitions the machine to its`Start` state, passes the optional specified event (`initialEvent`) and invokes its`OnEntry` handler, if there is one available. This method returns a task that completes when the machine reaches quiescence (typically when the event handler finishes executing because there are not more events to dequeue, or when the machine asynchronously waits to receive an event). This method should only be called in the beginning of the unit-test, since a machine only transitions to its`Start` state once.
42
+
43
+
The`SendEventAsync` method sends an event to the machine and starts its event handler. Similar to`StartMachineAsync`, this method returns a task that completes when the machine reaches quiescence (typically when the event handler finishes executing because there are not more events to dequeue, or when the machine asynchronously waits to receive an event).
44
+
45
+
The`MachineTestKit<M>` also provides`Assert`, which is a generic assertion that you can use for checking correctness, as well as several other specialized assertions, e.g. for asserting state transitions, or to check if the inbox is empty. We plan to add more assertions in the future.
46
+
47
+
The following code snippet shows how to use these APIs to test the machine`M` of the above example:
48
+
```C#
49
+
publicasyncTaskTest()
50
+
{
51
+
vartest=newMachineTestKit<M>();
52
+
53
+
awaittest.StartMachineAsync();
54
+
test.AssertIsWaitingToReceiveEvent(true);
55
+
56
+
awaittest.SendEventAsync(newE());
57
+
test.AssertIsWaitingToReceiveEvent(false);
58
+
test.AssertInboxSize(0);
59
+
}
60
+
```
61
+
62
+
The above unit-test creates a new instance of the machine`M`, then transitions the machine to its`Start` state using`StartMachineAsync`, and then asserts that the machine is asynchronously waiting to receive an event of type`E` by invoking the`AssertIsWaitingToReceiveEvent(true)` assertion. Next, the test is sending the expected event`E` using`SendEventAsync`, and finally asserts that the machine is not waiting any event, by calling`AssertIsWaitingToReceiveEvent(false)`, and that its inbox is empty, by calling`AssertInboxSize(0)`.
63
+
64
+
Besides providing the capability to drive the execution of a machine via the`StartMachineAsync` and`SendEventAsync` APIs, the`MachineTestKit` also allows someone to directly call machine methods. Lets see how this can be done in a simple example. Say that you have the following machine`M`, which has a method`Add(int m, int k)` that takes two integers, adds them, and returns the result:
65
+
```C#
66
+
privateclassM :Machine
67
+
{
68
+
[Start]
69
+
privateclassInit :MachineState {}
70
+
71
+
internalintAdd(intm,intk)
72
+
{
73
+
returnm+k;
74
+
}
75
+
}
76
+
```
77
+
78
+
To unit-test the above`Add` machine method, the`MachineTestKit<M>` instance gives you access to the machine reference through the`MachineTestKit.Machine` property. You can then use this reference to directly invoke methods of the machine, as seen below.
37
79
```C#
38
80
publicvoidTest()
39
81
{
@@ -43,7 +85,7 @@ public void Test()
43
85
}
44
86
```
45
87
46
-
Note that directly calling machine methods(as above)only works if these methods are declared as`public` or`internal`. This is typically not recommended for machines (and actors, in general), since the only way to interact with them should be by sending messages. However, it can be very useful to unit-test private machine methods, and for this reason the`MachineTestKit` provides the`Invoke` and`InvokeAsync` APIs, which accept the name of the method (and, optionally, parameter types for distinguishing overloaded methods), as well as the parameters to invoke the method, if any. The following example shows how to use these APIs to invoke private machine methods:
88
+
Note that directly calling machine methods only works if these methods are declared as`public` or`internal`. This is typically not recommended for machines (and actors, in general), since the only way to interact with them should be by sending messages. However, it can be very useful to unit-test private machine methods, and for this reason the`MachineTestKit` provides the`Invoke` and`InvokeAsync` APIs, which accept the name of the method (and, optionally, parameter types for distinguishing overloaded methods), as well as the parameters to invoke the method, if any. The following example shows how to use these APIs to invoke private machine methods:
47
89
48
90
```C#
49
91
privateclassM :Machine
@@ -85,41 +127,4 @@ public async Task TestAsync()
85
127
}
86
128
```
87
129
88
-
Besides allowing the user to directly call machine methods, the`MachineTestKit` also provides access to two APIs that allow the user to asynchronously (but sequentially) interact with the machine via its inbox, and thus test how the machine transitions to different states and handles events. These two APIs are`StartMachineAsync(Event initialEvent = null)` and`SendEventAsync(Event e)`.
89
-
90
-
The`StartMachineAsync` method transitions the machine to its`Start` state, passes the optional specified event (`initialEvent`) and invokes its`OnEntry` handler, if there is one available. This method returns a task that completes when the machine reaches quiescence (typically when the event handler finishes executing because there are not more events to dequeue, or when the machine asynchronously waits to receive an event). This method should only be called in the beginning of the unit-test, since a machine only transitions to its`Start` state once.
91
-
92
-
The`SendEventAsync` method sends an event to the machine and starts its event handler. Similar to`StartMachineAsync`, this method returns a task that completes when the machine reaches quiescence (typically when the event handler finishes executing because there are not more events to dequeue, or when the machine asynchronously waits to receive an event).
93
-
94
-
An example of using these two methods is the following:
95
-
```C#
96
-
privateclassE :Event {}
97
-
98
-
privateclassM :Machine
99
-
{
100
-
[Start]
101
-
[OnEntry(nameof(InitOnEntry))]
102
-
privateclassInit :MachineState {}
103
-
104
-
privateasyncTaskInitOnEntry()
105
-
{
106
-
awaitthis.Receive(typeof(E));
107
-
}
108
-
}
109
-
110
-
publicasyncTaskTest()
111
-
{
112
-
vartest=newMachineTestKit<M>();
113
-
114
-
awaittest.StartMachineAsync();
115
-
test.AssertIsWaitingToReceiveEvent(true);
116
-
117
-
awaittest.SendEventAsync(newE());
118
-
test.AssertIsWaitingToReceiveEvent(false);
119
-
test.AssertInboxSize(0);
120
-
}
121
-
```
122
-
123
-
The above unit-test, creates a new instance of the machine`M`, then transitions the machine to its`Start` state using`StartMachineAsync`, and then asserts that the machine is asynchronously waiting to receive an event of type`E` (via the`Receive` statement) by invoking the`AssertIsWaitingToReceiveEvent(true)` assertion. Next, the test is sending the expected event`E` using`SendEventAsync`, and finally asserts that the machine is not waiting any event, by calling`AssertIsWaitingToReceiveEvent(false)`, and that its inbox is empty, by calling`AssertInboxSize(0)`.
124
-
125
-
Note that its possible to use both the`StartMachineAsync` and`SendEventAsync`, as well as invoke directly methods by accessing the`MachineTestKit.Machine` property, based on the testing scenario.
130
+
Note that its possible to use both the`StartMachineAsync` and`SendEventAsync`, as well as invoke directly machine methods by accessing the`MachineTestKit.Machine` property, based on the testing scenario.