 |
.. (לתיקייה המכילה) | |
In question 1, I didn't understand how the alternating bit protocol is related... | |
|
For each of the problematic queues provided, you should explain whether the AB-protocol - if used with two such queues - will function properly. |
In question 1, is the problem indicated in each of the the queues is in addition to loss of messages? | |
| NO, the three problematic queues do not loose message. Each queue has ONE problem as indicated. |
In question 1, may we assume we have the functions head, tail, last and front (similar to Zed)? | |
| Yes, you are allowed to use them and other elementary queue operations. Make sure they are documented if they are not trivial. |
In question 1, how should we demand that all other elements in msgQ are unchanged? | |
| In UNCHANGED you specify only variables and here the variable Queue is changed. So, you should explicitly specify in the operation itself which elements were changed and which were not. |
In question 2, may we assume that... | |
| You may assume reasonable assumptions as long as they do not contradict the requirements, and that follow the spirit of the assignment. Do not forget to document them. |
In question 2, can we assume there's a function "eat(id)", which is kinda of an internal timer or something like that, that we can do something like: eat(id) ; pay(id). Adding to this, can we also assume there's a function which "pay"? | |
| In general, you may define external functions only if you can't use LOTOS structures for that. Specifically in the case of eating you may ignore the actual eating and simply continue to payment (or complaint). There are other LOTOS solutions such as defining an 'eating' process which is probably more elegant. |
In question 2, are we building up a general system, and in the end we need to make it specific for our own needs? Or we can assume that the numbers given to us are our system. Which means, for example, can we say that the Restaurant_Chief (Axrai Mishmeret) can have two internal variables named "waiter_1,waiter_2", and a Waiter can have three internal variables named "costumer_1,customer_2,customer_3"? [We took this idea from the tutorial, in which the Lift Controller has two boolean fields, one for each Lift] | |
| You are building a general system and then instantiate it in a specific setup. |
In question 3, what is the type of 'a' in insert(p, a)? | |
|
You may assume that 'a' is of type Elem, which is a complex type that consists of a value (of type Val) and of a priority (of type Int). Then you may access them through a.val and a.prio. This is only a suggestion and other assumptions are also possible, as long as they are documented. |
In question 1, can we assume that the 'zevel' element is inserted to the end of the queue? | |
| NO. the zevel may be inserted to each location, randomly. |
In question 1, if we proved that the strong fairness is not sufficient and we came up with a temporal logic formula that guarantees the delivery of the message, does this new formula holds in the AB-protocol part of the question? | |
| Yes. |
In question 1, when you say "to suggest another fairness", can we define another temporal logic formula which doesn't have the form of a weak/strong fairness? | |
| Yes. |
In question 2, should we define a general solution that treats any number of cooks, waiters' etc., or can we solve it to the task at hand? | |
| The solution should be general except for the manager where you may assume there is a single one. Only when you compose the processes to a single behavior you should specify the number of processes requested. |
In question 3, do we need to write stuff like implies, implies converts, exempting, | |
| Yes, where applicable. |