CIS 540: Spring 2014 Midterm

CIS 540: Spring 2014 Midterm
March 13, 2014
1. Reactions of this process is shown below:
Await dependencies:
Output y has no dependency
Output z depends on input x
The component is non-deterministic, since in some states two transitions are enabled due to the choose
construct in the assignment to z.
The component is input enabled as at least one transition is enabled for any input.
1
2. The ROBDD is shown below
3. To show that φ is not an inductive invariant:
Consider the state mode = on, x = 0. We can clearly see that the invariant φ is satised in this state.
However, the next state would be mode = of f, x = −1, in which the invariant fails. Therefore, we can
conclude that φ is not an inductive invariant of the system.
Consider a stronger invariant ψ given by (x ≥ 0) ∧ [(mode = on) → (x > 0)]. We can see that the
initial state .i.e. mode = of f, x = 0 satises this invariant. Now, we need to show that any transition
from a reachable state satises this invariant
Case 1: mode = of f, x = k, where k ≥ 0.
Any transition from this mode, would result in x = k + 1. Therefore the property is satised.
Case 2: mode = on, x = k, where k > 0. Note that the condition now has changed (greater than,
not greater than or equal) to accommodate the strengthening condition. The new state would be
mode = of f, x = k − 1. Since the minimum value of x in the previous state was 1, the minimum value
in the new state would be 0, which would still satisfy the property.
4. The transitions formula is shown below:
(a)
[(x < y) ∧ (x0 = x + y) ∧ (y 0 = y)] ∨ [¬(x < y) ∧ (x0 = x) ∧ (y 0 = y + 1)]
(b) Conj(A, T rans) = ([(x < y) ∧ (x0 = x + y) ∧ (y 0 = y)] ∨ [¬(x < y) ∧ (x0 = x) ∧ (y 0 = y + 1)]) ∧ (0 ≤
x ≤ 5)
We can split into two parts
i. (x < y) ∧ (x0 = x + y) ∧ (y 0 = y) ∧ (0 ≤ x ≤ 5)
Applying existential quantication on y,
(x < y 0 ) ∧ (x0 = x + y 0 ) ∧ (0 ≤ x ≤ 5)
Applying existential quantication on x,
(x0 < 2y 0 ) ∧ (0 ≤ x0 − y 0 ≤ 5)
2
After Renaming: (x < 2y) ∧ (0 ≤ x − y ≤ 5)
ii. ¬(x < y) ∧ (x0 = x) ∧ (y 0 = y + 1) ∧ (0 ≤ x ≤ 5)
Applying existential quantication on x,
¬(x0 < y) ∧ (y 0 = y + 1) ∧ (0 ≤ x0 ≤ 5),
Applying existential quantication on y,
¬(x0 < y 0 − 1) ∧ (0 ≤ x0 ≤ 5),
Simplifying and renaming,
(x + 1 ≥ y) ∧ (0 ≤ x ≤ 5)
Combining the two regions we get,
[(x < 2y) ∧ (0 ≤ x − y ≤ 5)] ∨ [(x + 1 ≥ y) ∧ (0 ≤ x ≤ 5)]
5. The asynchronous process is shown below
(a) No. It is not guaranteed that the value of x will eventually exceed 5(when only A2 is repeatedly
executed). We can see from the process description that, in order for x to eventually exceed 5,
the task A1 needs to be repeatedly executed. Note that A1 cannot be disabled by the execution
of A2. Therefore we need a weak fairness w.r.t A1 for x to exceed 5.
(b) There is no guarantee that the value of y will exceed 5.
We want the value of x to be greater than zero. To achieve this, the task A1 needs to execute at
least once. Therefore, we need weak fairness w.r.t A1 (As the task is always enabled) for the
value of y to exceed 5.
(c) It is not guaranteed that the two values become equal
We need a weak fairness w.r.t A1, for the two values to become equal. However, there is no
fairness that ensures that two values become equal after their values exceeds 1.
3
6. The process is shown below:
Validity: This property is not satised. Consider the execution shown below
1. temp := y.t&s (temp = 0)
2. temp := y.t&s (temp = 1)
3. dec2 := x (as temp is 1)
4. x = pref1
5. dec1 = pref1
In this case, even if pref 1 = pref 2 = 1, dec1 would be 1 and dec2 would be 0.
Wait Freedom: Since there are no loops, there is no place in which the processes can get stuck.
Therefore, wait freedom requirement is satised
Agreement: This is not satised. Consider the execution shown below
1. temp := y.t&s
(temp = 0)
2. temp := y.t&s (temp = 1)
3. dec2 := x (as temp is 1)
4. x = pref1
5. dec1 = pref1
In this execution, if pref 1 = 1, then the result would be dec1 = 1 and dec2 = 0.
4

Download Report