diff --git a/signal.als b/signal.als index afc7354..c41dad2 100644 --- a/signal.als +++ b/signal.als @@ -292,13 +292,11 @@ check equivalent for 2 but 6 Message, 1..7 steps// Task 3.2: CHOOSE BOUND HERE pred two_rings { // Task 3.3: FILL IN HERE - some a, b: Address | - a != b and - some s, s': State | - s' in s.next and - s.ringing = a and - s'.ringing = b +some disj caller1, caller2: Address | + some s: State | + s.ringing = caller1 and + after s.ringing = caller2 } -run two_rings for 3 but 8 Message, 1..8 steps // Task 3.3: CHOOSE BOUND HERE +run two_rings for 3 but 6 Message, 1..10 steps // Task 3.3: CHOOSE BOUND HERE