Reference no: EM132214000

Assignment -

Consider the following definition of trees that expands on the variety already seen on homework assignments:

TREE ::= leaf<<N>>| node <<N x TREE x TREE>>

It says that a tree is either a leaf which has a numeric value, or it is a (binary) node which has a value and two sub-trees.

Here are some examples of trees:

Tree A can be described as node(4, leaf (5), leaf (9))

and tree B as node(1, node(2, leaf (3), leaf (5)), leaf (4))

1. Give the description of tree C in the same format.

Now consider the following function definitions:

2. Write axiomatic definitions for two functions: totalsum, which adds up all the numeric values in the tree; and maxsum, which returns the maximum sum of numeric values along a single branch of the tree from root to leaf. For example, the maxsum for tree C above is 2+3+5+7 = 17.

3. Prove the following by structural induction: ∀_t : TREE • maximum(t) ≤ totalsum(t)

Consider the following arcade game credit management system:

• The interface consists of a slot for depositing coins, a push button labeled "1", and a push button labeled "2".
• Up to two coins can be deposited, each coin being worth one credit. If there are two credits, no more coins will be accepted by the machine.
• A one-player game costs one credit, and can be initiated by pressing the "1" button when there is at least one credit.
• A two-player game costs two credits, and can be initiated by pressing the "2" button when there are two credits.
• While a game is in progress, coins are not accepted, and pressing the "1" and "2" buttons have no effect. The credit management system remains in the same state until the game is complete. Once the game is over, the system becomes active again.

The following define the set of states, the initial states, and the actions for a state machine that models this system:

S == [credits : {0, 1, 2}; game : {none, 1p, 2p}],

I = {s : S | credits = 0 Λ game = none};

A = {coin, 1_button, 2_button, game over}

The transitions of the system can be any set of transitions that accurately model the description given above of the machine's behaviour. If there is any ambiguity in the above description, there may thus be more than one possible set of transitions that accurately model the described behaviour.

Answer each of the following questions with respect to the above model.

1. Draw a transition diagram for the arcade system. You may name individual states if you wish. For each state, be sure to indicate clearly the values of all state variables. Don't forget to label transitions.

2. Do each of the following:

(a) Rewrite the set δ by enumeration (i.e., list all the triples). You may use the names you assigned to states in question (1) if you wish.

(b) Give the pre- and post-conditions of each action.

3. Answer each of the following:

(a) What happens if you press the 1_button when there are no credits?

(b) Can the game_over action fire if no game is in progress? How can you tell?

(c) What happens if you press the 2_button when a one player game is in progress?

(d) How many initial states are there in this system?

(e) Give the event-based trace of the execution in which a one player game, then a two player game are paid for (with no extra coins being inserted prior to each game) and then played, in that order.

4. Give an FSP specification of the arcade management system.

Consider the following enhanced arcade game credit management system:

• The interface consists of a slot for depositing coins, a push button labeled "1", a push button labeled "2", and a push button labelled "coin return".
• There is a minimum of zero credits, and a maximum of ten. Each coin deposited adds one credit, up to the maximum of ten. Once there are ten credits, any coin deposited will be returned.
• Pressing the "coin return" button at any point will set the credits to zero, and the appropriate number of coins will be returned. E.g., if the button is pressed when there are two credits, two coins should be returned.
• A one-player game costs one credit, and can be initiated by pressing the "1" button when there is at least one credit.
• A two-player game costs two credits, and can be initiated by pressing the "2" button when there are two credits.
• While a game is in progress, coins will be accepted, and the number of credits updates while the game is still in progress.
• While a game is in progress, the "coin return" button is enabled. Pressing the "coin return" button should not end the game.
• While a game is in progress, the "1" and "2" buttons are disabled. Pressing them does not change the state of the credit management system.

Here is the beginning of a Z specification for this system: GAME ::= none | one | two

1. Write an InitArcadeCreditSystem schema that defines the initial state for the system. Explain why this initial state is consistent with the state space invariant given above.

2. Write an operation CoinReturn that fires when the user presses the coin return button.

3. Write an operation 1_button that fires when the user presses the button labelled "1".

4. If the 1_button operation is not robust, use the schema calculus to make a robust version of the operation (be sure to define any auxiliary schemata you use in the process); if the operation is robust, explain why that is the case.

Note - Please adhere to deadline otherwise this whole exercise will be futile and the waste of money and time for me.

Attachment:- Assignment File.rar