diff --git a/models/Application_examples/Euclids_Algorithm.mp b/models/Application_examples/Euclids_Algorithm.mp new file mode 100644 index 0000000000000000000000000000000000000000..a47cc4b4ce2272eb67e2432a7c0e380c4d8336ee --- /dev/null +++ b/models/Application_examples/Euclids_Algorithm.mp @@ -0,0 +1,71 @@ +/*┬────────────────────────────────────────────────────────┠+│*│ ┌─[ 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; \ No newline at end of file