User Tools

Site Tools


plt17:assignment_5

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
plt17:assignment_5 [2017/12/05 12:14]
hossein [Task 2]
plt17:assignment_5 [2017/12/05 20:00] (current)
hossein
Line 102: Line 102:
  
 Find a set of atomic propositions – try to minimize the number of propositions – that are needed to describe the correctness properties of the elevator system as temporal logic formulas. Find a set of atomic propositions – try to minimize the number of propositions – that are needed to describe the correctness properties of the elevator system as temporal logic formulas.
-Write a Promela model for the elevator and verify its correctness. For simplicity consider ​$N=5$.+Write a Promela model for the elevator and verify its correctness. ​ 
 + 
 +(For simplicity consider N=5)
  
 ===== Task 2 ===== ===== Task 2 =====
Line 138: Line 140:
   * Eventually always a leader will be elected.   * Eventually always a leader will be elected.
   * The elected leader will be the process with the highest number.   * The elected leader will be the process with the highest number.
 +
 +(For simplicity consider N=5)
  
 ==== Deadline and Deliverables ==== ==== Deadline and Deliverables ====
plt17/assignment_5.txt · Last modified: 2017/12/05 20:00 by hossein