### Site Tools

plt17:assignment_5

# Differences

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

 plt17:assignment_5 [2017/12/05 12:14]hossein [Task 2] plt17:assignment_5 [2017/12/05 20:00] (current)hossein Both sides previous revision Previous revision 2017/12/05 20:00 hossein 2017/12/05 12:14 hossein [Task 2] 2017/11/16 22:58 hossein [Deadline and Deliverables] 2017/11/16 19:01 hossein created 2017/12/05 20:00 hossein 2017/12/05 12:14 hossein [Task 2] 2017/11/16 22:58 hossein [Deadline and Deliverables] 2017/11/16 19:01 hossein created 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 ====