diff --git a/models/Application_examples/Euclids_Algorithm.mp b/models/Application_examples/Euclids_Algorithm.mp index ee35f1e57d0f724b9b5942b3b5eb6093be15d86a..64a11d5a87253a007695df059a7531f8fcb99175 100644 --- a/models/Application_examples/Euclids_Algorithm.mp +++ b/models/Application_examples/Euclids_Algorithm.mp @@ -1,10 +1,9 @@ /*┬────────────────────────────────────────────────────────┠│*│ ┌─[ 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 ]────────────────────────────────────────┠│ @@ -29,26 +28,26 @@ │*│ │ │*│ ┌─[ Search Terms ]───────────────────────────────────┠│ │*│ │ behavior, Euclid, GCD, Lamport ; │ │ -│*│ │ coordination, event; coordination, conditional; │ │ +│*│ │ 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. │ │ +│*│ │ 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 +61,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