[HD] EECS3342 F26 - 2026-11-03 (Tuesday) - Lecture 14

Overview

Jackie Wang develops inference-rule proof techniques for sequence obligations, distinguishing rules such as ORL, ORR1, ORR2, monotonicity, and arithmetic rewriting. Applying them to the M0 bridge-controller model reveals that two of four invariant-preservation obligations fail at the boundaries; adding guards n > 0 for ML in and n < d for ML out yields a revised model whose four obligations can be proved.

Key takeaways

Monotonicity is essential when an inference rule's hypotheses form only a subset of a sequence's hypotheses; remove the extras before matching the rule.
ORR1 and ORR2 apply to a disjunction in the goal and let a proof select one disjunct, whereas ORL handles a disjunction among the hypotheses and can split the proof into branches.
The original M0 model fails two boundary cases: decrementing from n = 0 violates natural-number status, and incrementing from n = d violates the capacity bound.
For the bridge controller, the valid repair is to guard ML in with n > 0 and ML out with n < d, rather than making n > 0 a global invariant that excludes empty-compound states.
Changing event guards requires regression checking: regenerate and prove all four obligations for two events and two invariants, including obligations that passed before the change.
Arithmetic rewrites can bridge syntactic mismatches between a goal and an inference rule, such as converting n − 1 ≤ d into a disjunction or n > 0 into 0 < n.

Chapters

0:00 Course Deadlines and Recap of Sequence Inference Rules

L3 is due the next day by midnight, and Written Test 2 is scheduled for November 18.
Jackie Wang reviews monotonicity as a way to discard irrelevant hypotheses before proving a sequence.
A sequence is built from predicates and a turnstile, while an inference rule relates sequences; they are related but not interchangeable.

4:04 ORR1 and ORR2: Choosing a Disjunctive Goal

ORR means the disjunction appears to the right of the turnstile, as part of the goal.
ORR1 proves the left disjunct P of a goal P or Q, while ORR2 proves the right disjunct Q.
A goal of P or Q requires establishing only one side, unlike ORL, which handles a disjunction among the hypotheses.

8:21 Justifying ORL with Propositional Equivalences

To justify ORL, translate its two antecedent sequences into P implies R and Q implies R, and its consequence into P or Q implies R.
Jackie derives the implication using implication rewriting, distributivity of disjunction over conjunction, and De Morgan's law.
The same method can test whether an unfamiliar inference rule is valid by translating its sequences into implications and checking the resulting logic.

18:42 Four Proof Obligations for M0 Invariant Preservation

The bridge-controller model M0 has two events, ML out and ML in, and two invariants, producing four preservation sequences.
Each sequence must be proved; an unprovable obligation indicates that the model may need to be changed.
The supplied inference-rule hints are useful during practice, but students should learn to select rules from the full rule set.

21:57 Using Monotonicity Before Applying the Natural-Number Rule

A sequence containing several hypotheses cannot directly use P2 when P2 requires only the hypothesis that n is a natural number.
Monotonicity removes unrelated hypotheses, leaving n ∈ N and the goal n + 1 ∈ N.
After the sequence matches P2 exactly, the natural-number successor obligation is proved.

25:29 Proving the Decrement Bound with Arithmetic and ORR1

The decrement obligation aims to prove n − 1 < d from n ≤ d, but the decrement rule's goal requires the strict inequality n − 1 < n.
Monotonicity first removes hypotheses that do not match the decrement rule.
Arithmetic rewrites n − 1 ≤ d as (n − 1 < d) or (n − 1 = d), then ORR1 keeps the left disjunct and the decrement rule completes the proof.

33:41 Why ORR Goal Rewriting Does Not Create a Branching Proof Tree

The decrement proof remains a single chain because ORR1 selects one side of a disjunction in the goal.
ORL applies when a disjunction is in the hypotheses to the left of the turnstile and can produce two separate proof branches.
Checking whether a conjunction or disjunction is left or right of the turnstile determines which inference rule applies.

36:41 Finding the Two Boundary Failures in M0

The obligation that n − 1 remains a natural number fails when n = 0, even though n itself is natural.
The obligation n + 1 ≤ d fails when n = d, since incrementing moves beyond the upper bound.
Monotonicity can strip away distracting hypotheses so a counterexample such as n = 0 or n = d clearly explains why an obligation is unprovable.

40:59 Deriving the Missing Preconditions for Decrement and Increment

The decrement event needs the additional condition n > 0 so its result remains a natural number.
The increment event needs n < d so its result stays within the capacity bound.
These are needed hypotheses for the failed obligations, but the proof alone does not determine where they belong in the model.

43:21 Why the Boundary Conditions Belong in Event Guards

Adding n > 0 as a new axiom is inappropriate because axioms depend on constants, while n is a variable.
Making n > 0 an invariant would wrongly exclude valid bridge states with no cars in the compound.
The suitable model change is to add n > 0 to the ML in guard and n < d to the ML out guard, matching when decrement and increment are enabled.

53:28 Regression Workflow for Revising the Bridge-Controller Model

The model-checking workflow generates proof obligations from M0, attempts to prove or disprove them, and uses failures to identify needed model changes.
After adding the two event guards, the revised model M0′ must have its proof obligations regenerated and checked again.
Because the number of events and invariants stays unchanged, M0′ still has four invariant-preservation sequences; further iterations may be needed if any still fail.

59:07 Rechecking All Four Obligations After Adding Guards

The new ML out guard n < d appears as an extra hypothesis in its generated sequences, and the ML in guard n > 0 appears in its sequences.
All four obligations are provable for M0′, making it correct with respect to invariant preservation.
The two obligations that were already provable in M0 still need to be checked after the model changes, rather than assumed to remain valid.

1:03:00 Proving the Revised Increment and Predecessor Obligations

For ML out, monotonicity keeps n < d and n + 1 ≤ d, matching the increment rule.
For ML in, the new n > 0 guard supplies the missing condition for the predecessor rule P2′ and proves n − 1 is natural.
The proof normalizes n > 0 to 0 < n with arithmetic before applying P2′; initialization and deadlock freedom remain as the next course topics.

Transcript excerpt

0:05 All right. So, nothing really special to announce, but just don't forget your L number three will be due tomorrow, I believe, uh by midnight. Just uh submit your best attempt. I'll give you a solution as usual. And then your written test number one, you can look up the calendar just to confirm. It's going to be November 18th in about two weeks time. >> November, huh? written test two. Absolutely. Thank you so much. I appreciate it. Yeah. And for your written test one, the result should be released. I'll try to do if I cannot do it before Thursday's class, I'll definitely do it Friday. But if you got any concern about the uh written test, you can always speak to me. But I'll definitely release the result. Okay. Okay. [snorts] I just need to verify

0:52 some result from the TA, then we should be good. It's definitely get uh getting very close to completing. Okay. And for your written test too, uh it's going to cover bridge controller. I'll release the guide and practice question about one week before the test as usual. So you can definitely expect that. And for exam, uh let's wait a little bit longer, right? So once we get a bit more closer to the exam, we'll talk more about the exam. Okay. Any questions? Okay. Okay. So just continue with the material. Okay. So let me just see here. Okay. I don't quite like here. So, sorry, let me fix it. All right. So, very quick recap from last Wednesday. So, we introduced the idea about inference rule which looks like this

1:41 right here. Right? So, we talk about this monotonicity uh inference rule. We're going to see many applications of that also again today and also in the subsequent lecture. So, the idea goes

This is the start of the transcript. Save this video free for the whole transcript, searchable and time-coded.

In this course

Related notes

Summary, takeaways, and chapters were generated by AI from the video's transcript and may contain errors. The video belongs to its creator, Jackie Wang.