代做COMP2111 Assignment 2 2023 Term 1代写C/C++程序

COMP2111

Assignment 2

2023 Term 1

Due: Wed 10 April, 23:59

Submission is through give and should consist of:

1. A single pdf file with typeset answers, maximum size 4Mb. Prose should be typed, not handwritten. Use of LATEX is strongly encouraged, but not required.

2. A file partner.txt with a single line on the format. z<digits> . This must be the zID of your group partner. For individual submissions, write your own zID.

Submit your work using the web interface linked on the course website, or by running the following on a CSE machine

give cs2111 assn2 assn2.pdf partner.txt

This assignment is to be done in pairs. Individual submissions are discouraged, but will be accepted. Only one member of the pair should submit. Work out who will submit ahead of time—duplicate submissions are extremely annoying to sort out.

Late submission is allowed up to 5 days (120 hours) after the deadline. A late penalty of 5% per day will be deducted from your total mark.

Discussion of assignment material with others is permitted, but you may not exchange or view each others’ (partial) solutions. The work submitted must be your own, in line with the University’s plagiarism policy. Note in particular that attempting to pass off AI writing (e.g. ChatGPT output) as your own still counts as plagiarism.

Background    In the lectures, we defined the set of traces (aka runs) for unlabelled transition systems. For example, if we ignore the labels on this transition system:

the set of traces starting from q0, which we will write Tr(q0), is the following:

{q0, q0q1, q0q1q2, q0q1q3, q0q1q3q4}

But the set of maximal traces, which we will write MTr(q0), is

{q0q1q2, q0q1q3q4}

For labelled transition systems, we are often less interested in what states we visit, and more interested in the labels of the transitions we take. To this end, we define the set of action traces starting from a state s, written ATr(s), to be the label sequences we can use to label the transitions of Tr(s). So in our example, we would have ATr(q0) = {λ, a, ab, ac, ad, ada}.

More formally, we define ATr(s) as follows:

where we use σ, τ to range over (possibly infinite) sequences, and where |σ| = ∞ if σ is infinite. Similarly, the maximal action traces MATr(s) are the label sequences we can use to label the transitions of MTr(s). So in the above example we have MATr(q0) = {ab, ac, ada}.

Problem 1                                                        (20 marks)

In the above example, there happened to be more action traces than traces, but that is not always the case. In the following, so refers to the initial state of whatever transition system you come up with.

Give examples of transition systems where the following is true:

(a) |Tr(s0)| = |ATr(s0)|                                                                          (4 marks)

(b) |Tr(s0)| > |ATr(s0)|                                                                          (4 marks)

(c) |MATr(s0)| = |ATr(s0)|                                                                      (4 marks)

(d) There are infinitely many states, but ATr(s0) is finite.                           (4 marks)

(e) ATr(s0) is infinite, but there are only finitely many states.                     (4 marks)

Problem 2                                        (40 marks)

Consider the following two labelled transitions M0 and M1, representing coffee machines:

The label $1 represents the machine receiving a coin, c represents the machine serving coffee in response to the coffee button being pressed, and similarly t represents the machine serving tea in response to the tea button being pressed.

(a) What is MATr(q0)? What is MATr(r0)?                                                                               (6 marks)

Now we want some coffee. Here’s a transition system representing a coffee buyer B:

We use the same alphabet to represent actions of the customer: $1 represents inserting a coin, c represents pressing the coffee button and obtaining coffee, and so t would represent pressing the tea button and obtaining tea.

Now that we have models of both the coffee buyer and the coffee machines, we can model how they interact. For that, we need to construct their synchronous product.

Definition 1 (Synchronous product) The synchronous product C0 k C1 of two labelled transition systems C0 = (S, →S,s0) and C1 = (T, →T, t0) is defined as:

where → is defined as follows for all s, t, α,s', t':

In words, the synchronous product allows only the transitions that are possible in both transition systems. If only one side is ready to proceed with an action, it can’t proceed. Intuitively, the $1 action in the transition system M0 || B represents a successful interaction between machine and buyer: the buyer inserts a coin, and the machine accepts it.

(b) Draw the state diagrams of M0 k B and M1 k B. Or if you prefer, explicitly enumerate all of their transitions. Feel free to leave out unreachable nodes from the diagram. (6 marks)

(c) In the transition system M0 k B, what is MATr((q0, b0))? In the transition system M1 k B, what is MATr((r0, b0))? (6 marks)

(d) Compare your answers to Questions (a) and (c). Is there a difference between M0 and M1 that is evident from one of the answers, but not the other? Why do you think that is? (10 marks)

(e) Define a safety property and a liveness property that, taken together, imply that our coffee drinker B gets appropriate service from the machine. (6 marks)

(f) Of the systems M0 k B and M1 k B, which ones satisfy your safety property? Which ones satisfy your liveness property? (6 marks)

Problem 3                                      (40 marks)

Read Section 4.1.4 (“Order of Commands”) of RFC 5321, which specifies how a session between a mail client and a mail server may proceed according to the SMTP protocol. A session is a structured interaction in which one or more parties exchange messages; in the case of SMTP, the purpose of a typical session is for the client to transmit e-mail to the server. The client tells the server what it wants to do by sending a sequence of protocol-specific commands. For our purposes, you don’t necessarily need to understand what the commands do, so you don’t have to read the rest of the RFC. But if you’re curious feel free to.

Define a DFA over the input alphabet

{DATA, EHLO, EXPN, HELP, MAIL, NOOP, RCPT, RSET, VRFY, QUIT}

that accepts exactly the admissible sequences of client-issued commands, as specified by Section 4.1.4 of the RFC. Ignore server responses and command parameters. Sometimes the server needs to make a decision about whether our command is acceptable based on the parameters; in such situations, assume the server will find anything we send acceptable.

Explain any design decisions you made in constructing the DFA, and any interpretative liberties you took. In particular, was there any point where you found the text of the RFC to be ambiguous? If so, how did you choose to interpret the ambiguous text?