try

signal.als

@@ -1,5 +1,9 @@
 
 // Names of you and your partner:
+// 
+//zikai wang
+
+
 // FILL IN HERE
 
 // the type of addresses
@@ -126,6 +130,27 @@ pred user_send_post[m : Message] {
 pred user_recv_post[m : Message] {
   no State.network' and
   // Task 1.1: FILL IN HERE
+	(
+    (m.type = SDPOffer and 
+      State.calls' = State.calls ++ (m.source -> SignallingStart) and
+      State.ringing' = State.ringing and
+      State.audio' = State.audio) or
+
+    (m.type = SDPAnswer and 
+      State.calls' = State.calls ++ (m.source -> SignallingOngoing) and
+      State.ringing' = State.ringing and
+      State.audio' = State.audio) or
+
+    (m.type = SDPCandidates and 
+      State.calls' = State.calls ++ (m.source -> SignallingComplete) and
+      State.ringing' = m.source and
+      State.audio' = State.audio) or
+
+    (m.type = Connect and 
+      State.calls' = State.calls and
+      State.ringing' = State.ringing and
+      State.audio' = m.source)
+  )
 }
 
 // the action of the attacker sending a message
@@ -219,6 +244,9 @@ fact {
 // participant or to answer a call from them
 assert no_bad_states {
  // Task 1.2: FILL IN HERE
+	all a: Address | 
+	    State.audio = a implies 
+	      (State.last_called = a or State.last_answered = a)
 }
 
 // describe the vulnerability that this check identified
@@ -243,21 +271,34 @@ pred successful_run {
     some other : Address | (always no State.calls.SignallingStart) and
     eventually State.audio = other
 }
+
+pred successful_run2 {
+// Task 3.1: FILL IN HERE
+  some other: Address |
+    always no State.calls.SignallingStart and
+    some s: State | s.audio = other
+}
+
+run successful_run2 for 2 but 6 Message, 1..7 steps expect 1
+
 // shows successful run of the protocol in the caller mode
 run successful_run for 2 but 6 Message, 1..7 steps expect 1
 
-pred successful_run2 {
-    // Task 3.1: FILL IN HERE
-}
 
 assert equivalent {
-    // Task 3.2: FILL IN HERE
+  successful_run iff successful_run2
 }
-check equivalent // Task 3.2: CHOOSE BOUND HERE
+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
+ // 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
 }
-run two_rings // Task 3.3: CHOOSE BOUND HERE
+run two_rings for 3 but 8 Message, 1..8 steps // Task 3.3: CHOOSE BOUND HERE