Merge pull request #38 from ybbh/main

sedeve-kit, update .md

README.md

@@ -55,7 +55,7 @@ We incorporate **anchor macros** at appropriate source locations(__Step (4)__).
 During the testing, these macros establish a communication channel with the **Deterministic Player** and reorder actions in a predetermined order as the trace steps generated by the specification.
 When the program is compiled for release, the macros are left empty and have no effect.
 
-Finally, we test the system using our **Deterministic Player** and check the result to detect the [inconsistency between specification and implementation ](doc/deterministic_testing)(__Step (5)__). 
+Finally, we test the system using our **Deterministic Player** and check the result to detect the inconsistency between specification and implementation by conducting [deterministic testing](doc/deterministic_testing.md)(__Step (5)__). 
 
 We repeat this procedure until all the test cases pass successfully.
 

doc/deterministic_testing.md

@@ -19,6 +19,6 @@ Each test case is represented as a trace, a finite sequence of action and state
 
 $${a_1, \pi_1, a_2, \pi_2, ... a_n, \pi_n}$$
 
-where $a_i$ is the $i$th  action of the trace, and ${\pi_i}$ is the system's state after executing action ${a_i}$.
+where $a_i$ is the ${i}$ th action of the trace, and ${\pi_i}$ is the system's state after executing action ${a_i}$.
 The player processes each action ${a_i}$ in sequence $T$. After executing action ${a_i}$, it verifies the system state by asserting that its current state matches the expected state  ${\pi_i}$. 
-If the system receives an action ${a_i}$ , then it yields an action $`{a'_{i+1} }`$ that does not match the expected following action $`{a_{i+1}}`$, the testbed will trigger a timeout to report the inconsistency. 
+If the system receives an action ${a_i}$, then it yields an action $`{a'_{i+1} }`$ that does not match the expected following action $`{a_{i+1}}`$, the testbed will trigger a timeout to report the inconsistency.