Update models/Application_examples/Euclids_Algorithm.mp

models/Application_examples/Euclids_Algorithm.mp

+/*┬────────────────────────────────────────────────────────┐
+│*│ ┌─[ Title and Authors ]──────────────────────────────┐ │
+│*│ │ Model of Euclids Algorithm                         │ │
+│*│ │  Created by Michael Collins                        │ │
+│*│ │  October, 2022.                                    │ │
+│*│ │  Edited by Pamela Dyer and Kristin Giammarco in    │ │
+│*│ │  October, 2022.                                    │ │
+│*│ └────────────────────────────────────────────────────┘ │
+│*│                                                        │
+│*│ ┌─[ Purpose ]────────────────────────────────────────┐ │
+│*│ │ To use MP to model an adaptation of the well-known │ │
+│*│ │ Greatest Common Divisor Algorithm by Euclid.       │ │
+│*│ └────────────────────────────────────────────────────┘ │
+│*│                                                        │
+│*│ ┌─[ Description ]────────────────────────────────────┐ │
+│*│ │ This models Euclid's algorithm to compute a GCD    | |
+│*│ │ Inspired by Leslie Lamports discussions about TLA+ │ │
+|*| | The constraints handle undesirable traces in such a| | 
+|*| | computation.                                       | |
+│*│ └────────────────────────────────────────────────────┘ │
+│*│                                                        │
+│*│ ┌─[ 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       | |                       │ │
+│*│ └────────────────────────────────────────────────────┘ │
+│*│                                                        │
+│*│ ┌─[ Search Terms ]───────────────────────────────────┐ │
+│*│ │ behavior, Euclid, GCD, Lamport ;                   │ │
+│*│ │ coordination, event; coordination, 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.             │ │
+│*│ └────────────────────────────────────────────────────┘ │
+└*┴───────────────────────────────────────────────────────*/
+
+SCHEMA Euclids_Algorithm
+
+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
+       				y_does_not_change_value
+    			|
+       				y_has_become_greater_than_x
+       				y_is_assigned_new_value_of_x_subtracted_from_y
+       				x_does_not_change_value
+    			|  
+       				x_equals_y
+    			)
+			*)
+;
+
+IF #x_equals_y > 0 THEN
+
+ ENSURE FOREACH $x:x_equals_y
+
+   #x_has_become_greater_than_y AFTER $x == 0 AND
+
+   #y_has_become_greater_than_x AFTER $x == 0;
+
+FI;