Chapter 02 — Discrete mathematics
Lesson map
Lesson 02 published. Map, example, EX003.
flowchart TD
N0["Learning outcomes and connection"]
N1["2.1 States, transitions and relations"]
N2["2.2 Invariants and logic"]
N3["2.3 Checking by search"]
N4["2.6 Common errors"]
N5["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5
N5 --> EX["Worked example"]
EX --> Q["Exercise EX003"]
Logical drawing
flowchart LR
N0["Learning outcomes and connection"]
N1["2.1 States, transitions and relations"]
N2["2.2 Invariants and logic"]
N3["2.3 Checking by search"]
N4["2.6 Common errors"]
N5["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> Q["EX003"]
[Learning outcomes and connection]
|
v
[2.1 States, transitions and relations]
|
v
[2.2 Invariants and logic]
|
v
[2.3 Checking by search]
|
v
[2.6 Common errors]
|
v
[Chapter synthesis]
|
v
[Worked example] --> [Exercise EX003]
Learning outcomes and connection
After this chapter you can (1) represent case states and permitted actions as a directed graph and a relation; (2) write invariants in propositional and first-order logic; (3) search a transition graph for paths that violate an invariant; and (4) express separation of duties as a set constraint. It prepares Chapter 25 (intake and authorisation design) and Chapter 31 (workflow orchestration).
2.1 States, transitions and relations
A response workflow has a finite set of states $S$ — for example new, triage, contain_req, approved, contained, recover, closed — and a transition relation $T \subseteq S \times S$. Each transition may be labelled with the roles allowed to perform it: a function $\rho : T \to 2^R$ where $R$ is the set of roles. This is a labelled directed graph. Questions an engineer must answer are graph questions: is closed reachable from every state (no dead ends)? Can contained be reached without passing approved? Is any state reachable that should not be?
2.2 Invariants and logic
An invariant is a property that must hold in every reachable state or on every path. "No containment without approval" is a path property: for every path $s_0 \ldots s_k$ with $s_k = \textit{contained}$, there is $i < k$ with $s_i = \textit{approved}$. Separation of duties is a set property: the roles that may request containment and the roles that may approve it must be disjoint, $\rho(\textit{triage},\textit{contain_req}) \cap \rho(\textit{contain_req},\textit{approved}) = \emptyset$. Writing these down precisely is the first defence against the most common workflow defect: an edge added "for convenience" that bypasses a gate. The classic principles of Saltzer and Schroeder (1975) — complete mediation, separation of privilege, least privilege — become checkable statements once the workflow is a graph.
2.3 Checking by search
To test the path invariant, delete the approved node and ask whether contained is still reachable from new. Breadth-first search answers in time linear in the number of edges. If it is reachable, every edge into contained from a state other than approved is a candidate violation.
On the HVSS graph from Lab 2, deleting approved still leaves the path new → triage → contain_req → contained, so the search reports it and points at the convenience edge. The same search, run after every change to the transition table, turns a review comment into a repeatable check that a build can fail on.
2.4 Worked example (synthetic): an approval graph at HVSS
HVSS's draft workflow has eight edges. A developer added contain_req → contained so that engineers could "act immediately in emergencies".
"""Lab 2 (synthetic): case-state transition relation and role authorisation invariant."""
from collections import deque
T = { # (from, to): roles allowed
("new","triage"):{"intake","analyst"}, ("triage","contain_req"):{"analyst"},
("contain_req","approved"):{"duty_manager"}, ("approved","contained"):{"engineer"},
("contained","recover"):{"engineer"}, ("recover","closed"):{"duty_manager"},
("triage","closed"):{"analyst"}, ("contain_req","contained"):{"engineer"}, # suspicious edge
}
def reachable(src, avoid):
seen, dq = {src}, deque([(src,[src])]); paths=[]
while dq:
s,p = dq.popleft()
if s=="contained": paths.append(p)
for (a,b) in T:
if a==s and b not in seen and b not in avoid:
seen.add(b); dq.append((b,p+[b]))
return paths
print("edges:", len(T))
bad = reachable("new", avoid={"approved"})
print("paths to 'contained' that skip 'approved':", bad)
for (a,b),r in sorted(T.items()):
if b=="contained" and a!="approved": print("violating edge:", a,"->",b,"roles",sorted(r))
# separation of duties: who requests may not approve
print("SoD holds:", not (T[("triage","contain_req")] & T[("contain_req","approved")]))
Expected output:
edges: 8
paths to 'contained' that skip 'approved': [['new', 'triage', 'contain_req', 'contained']]
violating edge: contain_req -> contained roles ['engineer']
SoD holds: True
The search finds the bypass path and names the edge. Separation of duties holds — analysts request, duty managers approve — but that is irrelevant if the approval state can be skipped. The engineering response is not to delete emergency action but to model it explicitly: an emergency_contain state with its own role set, a mandatory retrospective approval within a stated time and an audit event, so the invariant becomes "every containment is preceded by approval or followed by retrospective review within 60 minutes" and can still be checked.
2.5 Limits
Graph models check structure, not people's behaviour: a duty manager who approves everything satisfies the invariant. State explosion appears when states carry data (tenant, severity); then you check properties over a model abstraction and test the implementation separately (Chapter 30).
Removing the approved node also tells you nothing about how long a request waited there, or whether the approver read the evidence before saying yes. Those properties need timestamps and audit records from the running platform, which Chapter 30 tests against the implementation rather than against the abstract graph of eight edges.
2.6 Common errors
- Writing invariants in prose that cannot be checked.
- Checking only the "happy path".
- Treating role names as people: one person holding two roles defeats separation of duties.
At HVSS the third error is a staffing question rather than a modelling one. If the night duty manager also covers analyst shifts, the disjoint role sets in Lab 2 still print SoD holds: True, yet one person can both request and approve the same containment. The check has to run over the assignment of people to roles for each shift, not only over the role labels on the edges. Equally, a test suite that walks only new → triage → contain_req → approved → contained would never have exercised the bypass edge that the breadth-first search found.
Exercises — chapter 02
EX003 — Formalise. Objective: write precise invariants. Inputs: the eight edges of Lab 2. Steps: write in logic (a) no dead-end states except closed; (b) every path to closed that passes contained also passes recover; check (b) against the edge list. Expected evidence: two formulas and a verdict with a counterexample if false. Rubric: 3 = correct formulas and verdict; 2 = minor notation errors; 1 = prose only; 0 = none.
EX004 — Repair. Objective: restore the gate without losing emergency capability. Inputs: Lab 2. Steps: modify the transition table to add emergency_contain; extend the code to check the revised invariant; run it. Expected evidence: changed table, check code, output. Rubric: 3 = invariant checked and passing with emergency path present; 2 = model correct, check incomplete; 1 = edge simply deleted; 0 = none.
Chapter synthesis
A workflow is a labelled graph; authorisation rules are invariants over its paths and labels. State them in logic, check them by search and treat every convenience edge as a hypothesis of failure until the check passes.
Continue studying — chapter 02 of 50
← Chapter 01 · Course chapter index · Chapter 03 →
Continue to the next authored lesson.