Question 1:

In the context of software engineering, consider the Dining Philosophers Problem, where 4 philosophers
are sitting at a table, each with a plate of food and a fork placed between every two adjacent
philosophers. Each philosopher can either be thinking or eating. To eat, a philosopher must acquire both
the left and right forks. However, they must avoid deadlock, where all philosophers are holding one fork
and waiting for the other. Model the Dining Philosophers Problem using Petri Nets by:

1. Defining the places, transitions, and tokens that represent the philosophers, forks, and the actions of

thinking and eating.

Places:

 T1, T2, T3, T4: Represent the philosophers in the Thinking state.

 E1, E2, E3, E4: Represent the philosophers in the Eating state.

 F1, F2, F3, F4: Represent the availability of the forks between philosophers.

Transitions:

 TE1, TE2, TE3, and TE4 are transitions for acquiring both forks to proceed from the Thinking
state to the Eating state.

Tokens:

 Tokens are used to track the current state:

o A token in F1, F2, F3, or F4 means the corresponding fork is available.

o A token in T1, T2, T3, or T4 means the corresponding philosopher is thinking.

o A token in E1, E2, E3, or E4 means the corresponding philosopher is eating.

2. Illustrating how the Petri Net would handle the scenario for 4 philosophers while avoiding deadlock.
  Forks (F1, F2, F3, F4) are shared resources. A philosopher must acquire a token from both the
left and right fork places before transitioning to the eating state.

 Intermediate transitions (TE1, TE2, TE3, TE4) ensure that a philosopher cannot hold a fork
indefinitely without acquiring both forks. This avoids scenarios where all philosophers hold one
fork and wait for the other (deadlock).

Deadlock Prevention:

 The Petri Net imposes constraints through transition firing rules:

o A philosopher cannot transition to the eating state unless both forks are available.

o After eating, a philosopher must release both forks (returning tokens to F1, F2, F3, or
F4), allowing other philosophers to proceed.

3. Analyzing the state space of the Petri Net to identify potential deadlock situations and propose a
solution.

The current model could reach deadlock if:

 Each philosopher picks up their left fork simultaneously

 No right forks are available, leaving all philosophers waiting

The marking where deadlock occurs is:

M = {TE1: 1, TE2: 1, TE3: 1, TE4: 1}

Proposed Solution:

To prevent deadlock in this Petri Net, we use resource ordering. The idea is to impose a rule where each
process must acquire resources in a specific order, for example:

 Order of resources: TE1 < TE2 < TE3 < TE4.

 Process rule: Each process must request resources in this order, meaning no process can request
a higher-priority resource before acquiring the lower-priority ones.

Question 2:
Briefly explain the key concepts of Hoare Logic,including:

o Hoare Triple:
{P} C {Q}, where P is the precondition, C is the command, and Q is the post condition.
 P is the precondition (what must be true before executing the command)
 C is the command/program (the actual code to be executed)
 Q is the postcondition (what will be true after executing the command)

Preconditions and Postconditions

 Preconditions (P):

o Define the conditions that must hold before executing a piece of code.

o Ensure that the input or initial state is valid for the program to work correctly.

Postconditions (Q):

 Define the desired outcome or guarantees about the program's state after execution.

3. Invariants

Loop Invariants:

 Properties that remain true before and after each loop iteration

 Help prove loop correctness

 Must be:
o Initially true (before the loop starts)
o Preserved by each iteration (if true before, remains true after)

B. Consider the following simple program for calculating the sum of the first n positive integers:
sum := 0;

i := 1;

while (i &lt;= n) do {

sum := sum + i;

i := i + 1;

Your task is to:

State and Prove the Loop Invariant: Define an invariant that holds at the start and end of each iteration
of the loop, ensuring the program correctness.

1. Step-by-Step Verification:

o For each part of the program (initialization, loop condition, loop body), apply Hoare logic to verify that
the program satisfies its precondition, post condition, and loop invariant.

o Provide detailed explanations of how the program maintains correctness through each step of
execution, using Hoare logic.

Loop Invariant Proof for Sum Program

1. Loop Invariant Definition

Let's define our loop invariant P:

P ≡ sum = (i-1)(i)/2 ∧ i ≤ n+1

This invariant states that:

1. At any point, sum equals the sum of integers from 1 to i-1

2. i never exceeds n+1

2. Verification Steps

A. Initialization

{n ≥ 0}

sum := 0;

i := 1;

{P}

After initialization:

- sum = 0 = (1-1)(1)/2 = 0
- i = 1 ≤ n+1

Therefore, P holds after initialization.

B. Maintenance (Loop Body)

{P ∧ i ≤ n}

sum := sum + i;

i := i + 1;

{P}

Let's verify:

1. Before execution:

- sum = (i-1)(i)/2

- i ≤ n+1

2. After sum := sum + i:

sum = (i-1)(i)/2 + i

3. After i := i + 1:

sum = (i-2)(i-1)/2 + (i-1)

Simplify: sum = (i-1)(i)/2

New i ≤ n+1 (since old i ≤ n)

Therefore, P is maintained through the loop body.

C. Termination

Loop terminates when i > n

Combined with invariant i ≤ n+1, we know i = n+1

D. Correctness

When loop terminates:

- i = n+1

- sum = (i-1)(i)/2 = n(n+1)/2

3. Final Result

The program correctly computes sum = n(n+1)/2, which is the sum of first n positive integers.

4. Formal Hoare Triple

{n ≥ 0}
 sum := 0;

i := 1;

while (i ≤ n) do {

sum := sum + i;

i := i + 1;

{sum = n(n+1)/2}