Given: Sept. 23 - - Due: Sept. 30
Q1 - In the system of Assignment 1, the behavior of CreateC is not live: We consider the temporal logic formula (in linear temporal logic) newC implies <> startC , which says that once an interaction newC happens, eventually startC will happen. Please explain why this formula is not true for the system of Assignment 1.
Q2 - Introducing fairness for jobs of type C: Please change the behavior of the components PerformA and PerformB is such a manner that they participate in rendezvous with the interaction newC of the CreateC component. The behavior of PerformA and PerformB should be such that the newC interaction would be possible whenever CreateC would like to perform this action, and once this action is performed, the interaction startC should have priority over the actions startA and startB such that the action startC could be eventually executed after a newC interaction has taken place.
Q3 - Please explain why the temporal formula of Q1 is true for your revised system of Q2.