Skip to main content

Workflow Model and Proof Notebook

Build a small finite workflow analyzer and a proof notebook. Allow 6–9 hours after the labs. This is a mathematical model of a toy workflow, with no claim that it verifies a production service. Reuse your lab functions and write the closure loop yourself before consulting run_labs.py.

Model and implementation​

States are {0,1,2,3,4}. Transitions are (0,1),(1,2),(2,1),(2,3),(0,4). An ordered pair (a,b) means the workflow can move from a to b in one step.

  1. Begin with transitions plus all diagonal pairs. Repeatedly add the composition of the current relation with itself until no pair is added. Call the result R.
  2. Define E by aEb iff aRb and bRa. Compute its equivalence classes.
  3. Form a relation on classes: [a]≤[b] iff aRb. Prove it is well-defined before computing it from selected representatives. Produce a partial-order report.
  4. Consider state labels f(0)=0,f(1)=f(2)=1,f(3)=2,f(4)=3. Determine whether f induces a function on classes. Then change f(2) to 9 and explain the result.

Required mathematical argument​

Prove the loop returns the least reflexive-transitive relation containing the transitions. Establish that every inserted pair denotes a finite path, that any reflexive-transitive superset must contain every inserted pair, and that a fixed point is transitive. Prove termination using the number of still-absent pairs from the finite state product. Prove E is an equivalence relation and the quotient is a partial order. Show the label function descends to classes exactly when it is constant on every class. Separate these claims from a trace of this one fixture.

Calibration after your attempt​

R has 13 pairs: state 0 reaches all five states; states 1 and 2 each reach {1,2,3}; states 3 and 4 each reach only themselves. Classes are {0},{1,2},{3},{4}. Raw reachability fails antisymmetry at 1,2. The quotient covers are ({0},{1,2}),({1,2},{3}),({0},{4}); it has least class {0}, two maximal classes {3},{4}, and no greatest class. Its relation has eight pairs including diagonals.

To prove representative independence, if a'a, bb' and aRb, then a'RaRbRb' gives a'Rb' by transitivity. Reflexivity and transitivity descend directly; two classes related both ways must be the same E-class. For closure termination, 25−|R| is a nonnegative integer and decreases on each changing iteration. A fixed point satisfies R∘R⊆R. Combining two finite paths explains every added pair.

The original labels are constant on classes. The changed label assigns different values to 1 and 2, so no representative-independent class function follows. Choosing an arbitrary representative would hide that ambiguity rather than fix it.

Transfer and submission​

Add transition (3,1), then independently recompute classes, covers and label validity before running the code. Submit the old and new fixtures, deterministic output, proof notebook, one regression for a deliberate fault, and a short explanation of finite-test limits. Expected new classes are {0},{1,2,3},{4}; the quotient has covers from {0} to each other class. The original labels now fail constancy on {1,2,3}. Also explain the empty-state case on paper.

Ask a reviewer to select one proof step and one changed assumption. Save their feedback or mark external review pending. Carry the contract, proof and correction record into algorithm correctness, state-machine modeling and later capstone work.