Update Euclids_Algorithm.mp

models/Application_examples/Euclids_Algorithm.mp

 /*┬────────────────────────────────────────────────────────┐
 │*│ ┌─[ Title and Authors ]──────────────────────────────┐ │
 │*│ │ Model of Euclids Algorithm                         │ │
-│*│ │  Created by Michael Collins                        │ │
-│*│ │  October, 2022.                                    │ │
+│*│ │  Created by Michael Collins in October, 2022.      │ │
 │*│ │  Edited by Pamela Dyer and Kristin Giammarco in    │ │
-│*│ │  October, 2022.                                    │ │
+│*│ │   October, 2022.                                   │ │
 │*│ └────────────────────────────────────────────────────┘ │
 │*│                                                        │
 │*│ ┌─[ Purpose ]────────────────────────────────────────┐ │
 │*│ │ To use MP to model an adaptation of the well-known │ │
-│*│ │ Greatest Common Divisor Algorithm by Euclid.       │ │
+│*│ │ Greatest Common Divisor (GCD) Algorithm by Euclid. │ │
 │*│ └────────────────────────────────────────────────────┘ │
 │*│                                                        │
 │*│ ┌─[ Description ]────────────────────────────────────┐ │
@@ -22,33 +21,31 @@
 │*│ ┌─[ References ]─────────────────────────────────────┐ │
 │*│ │ Leslie Lamport's Introduction to TLA+              | |
 │*│ │ https://www.newsroom.hlf-foundation.org/newsroom/  | |
-│*│ │ https://www.newsroom.hlf-foundation.org/newsroom/  | |
-|*| | lectures/video/lecture-if-youre-not-writing-a-     | |
-|*| | program-dont-use-a-programming-language.html       | | 
+│*│ │ https://www.newsroom.hlf-foundation.org/newsroom/lectures/video/lecture-if-youre-not-writing-a-program-dont-use-a-programming-language.html
 │*│ └────────────────────────────────────────────────────┘ │
 │*│                                                        │
 │*│ ┌─[ Search Terms ]───────────────────────────────────┐ │
-│*│ │ behavior, Euclid, GCD, Lamport ;                   │ │
-│*│ │ coordination, event; coordination, conditional;    │ │
+│*│ │ behavior, Euclid; GCD; Lamport;                    │ │
+│*│ │ coordination, event; ENSURE, conditional           │ │
 │*│ └────────────────────────────────────────────────────┘ │
 │*│                                                        │
 │*│ ┌─[ Instructions ]───────────────────────────────────┐ │
 │*│ │ Run for Scopes 1, 2, and 3.                        │ │
 │*│ ├─[ Run Statistics ]─────────────────────────────────┤ │
 │*│ │ Scope 1:  4 traces in less than 1 sec.             │ │
-│*│ │ Scope 2: 11 traces in less than 1 sec.             │ │
-│*│ │ Scope 3: 26 traces in less than 1 sec.             │ │
+│*│ │ Scope 2: 10 traces in less than 1 sec.             │ │
+│*│ │ Scope 3: 22 traces in less than 1 sec.             │ │
 │*│ └────────────────────────────────────────────────────┘ │
 └*┴───────────────────────────────────────────────────────*/
 
 SCHEMA Euclids_Algorithm
 
-ROOT GCD:	set_initial_value_for_x
-			set_initial_Value_for_y
+ROOT GCD:   set_initial_value_for_x
+            set_initial_Value_for_y
 
 			(*
     			(  	x_has_become_greater_than_y
-       				x_is assigned_new_value_of_y_subtracted_from_x
+       				x_is_assigned_new_value_of_y_subtracted_from_x
        				y_does_not_change_value
     			|
        				y_has_become_greater_than_x
@@ -62,7 +59,8 @@ ROOT GCD:	set_initial_value_for_x
 
 IF #x_equals_y > 0 THEN
 
- ENSURE FOREACH $x:x_equals_y
+ ENSURE #x_equals_y == 1;
+ ENSURE FOREACH $x: x_equals_y
 
    #x_has_become_greater_than_y AFTER $x == 0 AND