Practical guide
Describe what must happen over time
A snapshot cannot tell you whether a request eventually receives a response. Linear temporal logic describes properties of a sequence of states.
Read the operators as obligations
| Formula | Meaning |
|---|---|
| G p | p holds at every position |
| F p | p holds now or at some later position |
| X p | p holds at the next position |
| p U q | q eventually holds, and p holds until then |
These operators let a property distinguish an immediate response from eventual progress. The SPIN LTL reference documents temporal syntax and its operators. Tool dialects differ, so inspect the formula accepted by your analyzer instead of transferring notation blindly.
Illustrative example: eventual acknowledgement
G (request -> F acknowledgement)
At every position with a request, an acknowledgement must occur then or later. This does not require a response within a deadline. It also does not say which acknowledgement belongs to which request. With multiple outstanding requests, one later acknowledgement could satisfy several boolean obligations unless the model preserves request identity.
Contrast a safety rule such as G !(writer_a_active & writer_b_active). A finite trace showing both writers active demonstrates a violation. Eventual progress needs a different argument: an unfinished prefix with no acknowledgement may simply not have run long enough.
Review traces before trusting the formula
| Sequence | What it shows |
|---|---|
| request, idle, acknowledgement | The request receives a response in this trace |
| request, idle, idle, end of capture | The finite capture does not settle unbounded eventuality |
| request followed by idle forever | An infinite behavior violating eventual acknowledgement |
A bounded response requirement needs an explicit timing model. Define the tick, scope, startup behavior and fairness assumptions. Assuming a worker is always eventually scheduled changes the behaviors being analyzed.
Use simulation as an inspection aid
Proof can simulate supported formulas over supplied signals. That helps a reviewer inspect a particular trace. A finite simulation is not universal model checking over every execution.
proof simulate "G (request -> F acknowledgement)" --signals traces.json --length 10
The signal file must use the command's supported schema; consult proof help simulate when creating it. No simulation result is asserted here.
Connect the formula to the real operation
Map signals to observable events and keep the correlation and timing assumptions with the requirement. Then choose model analysis and executed tests suited to that claim. A temporal formula that compiles but abstracts away the critical failure sequence can still be the wrong specification.
Follow the evidence
Write one satisfying trace and one violating trace before accepting a temporal formula.
Review one temporal property. Bring a satisfying trace and a feared failure sequence so we can assess whether the formula captures the timing and correlation that matter.
Inspect structured temporal requirements · Analyze all modeled behaviors