hide x in SyncNor[in1, in2, out := set,ot, x] || SyncNor[in1, in2, out := x, reset, ot]not a correct implementation of an RS-Flip Flop?
Give a reactive modules solution for the above problem and for 4 philosophers that has the following properties:
predicate mutex is ~((pc1 = crit & pc2 = crit) | (pc2 = crit & pc3 = crit) | (pc3 = crit & pc4 = crit) | (pc4 = crit & pc1 = crit))First you have to succeed to parse, type check and construct the project window. Some of the programs are parsed, but the type checker might not detect a wrong name used instead of another name. This will crash the internal representation visitor (that assumes the program was type checked). Go gradually by commenting out parts of the program. Test your modules by simulating them. Alternatively, you might click the reach (mountains) button (you see how many states it has). Finally, test the judgments.
judgment mutex is System |= mutex
Your solution might not be fair, i.e., one of the philosopher may starve (never grab both forks). How should the data structure for the forks and the code for the philosopher be changed to assure fairness by construction? Explain in words.
Hints for the implementation in Reactive Modules
Consider two compatible modules P and Q.
(10p) Assume that the two modules have no private variables (privXP = privXQ = empty) and that the interface variables of one module are the external variables of the other module (intfXP = extlXQ and intfXQ = extlXP ). Then the two modules and the compound module have the same state space SP = SQ = SP||Q. Prove that the transition action of the compound module P||Q is the intersection of the transition actions of the two component modules, i.e., s ->P||Q t iff s ->P t and s ->Q t. What can you say about the initial states of the compound module?(10p) Assume that the two modules have no variables in common (XP intersected with XQ is empty). Then SP||Q = {(s1,s2) | s1 in SP and s2 in SQ}. Prove that the transition action of the compound module is the cartesian product of the transition actions of the two component modules, i.e., (s1,s2) ->P||Q (t1,t2) iff s1 ->P t1 and s2 ->Q t2. What can you say about the initial states of P||Q?
(10p) Now consider the general case. Consider two states s and t of the compound module P||Q. Prove that (1) s is in P||Q.sI iff s[XP] is in P.sI and s[XQ] is in Q.sI. (2) s ->P||Q t iff s[XP] ->P t[XP] and s[XQ] ->Q t[XQ].
Hint: Use in the argument the definition of a module (initial states and rounds) and of module composition.
Let G = (S, sI, t) be a symbolic representation of a finite transition graph and let f and postG be defined as in the class:postG (s) = (EX. s & t)[X / X']
f(s) = sI | postG (s)
where & and | are the boolean and and or operations, EX.s&t is existential quantification, i.e., exists(X, s&t)) and [X /X'] is renaming, i.e., rename(X',X). Show that:(10p) f is monotonic, | continuous and & continuous.
(10p) What is the least fixpoint mf and the greatest fixpoint nf ?(10p) Explain in words why the symbolic search algorithm can be viewed as a fixpoint computation? Which fixpoint does it compute?
Hints: You can identify & with intersection, | with union and => with subset. The empty set corresponds to false and the top set corresponds to true. Remember that a function f is:
monotonic: provided that P1 => P2 implies that f(P1) => f(P2)
| -continuous: provided that P1 => P2 =>... implies that f(|i Pi) = |i f(Pi)
&-continuous: provided that P1 <= P2 <=... implies that f(&i Pi) = &i f(Pi)
(10p) Give the initial predicate and the transition predicate for the Peterson's protocol P1 || P2
(10p) Simulate the symbolic search algorithm for checking that Peterson's protocol satisfies the mutual exclusion requirement. For each iteration of the repeat loop give the state predicate sR after quantifier elimination and simplification.
Let X = {x0,x1,y0,y1,o0,o1,c}.(10p) Choose an appropriate ordering of the variables and construct the BDD for addition such that the output o1o0 together with the carry bit c is the sum of the inputs x1x0 and y1y0.