plt17:assignment_5

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

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