13. Reasoning beyond one simulation

In this lesson: distinguish reachable and total envisionments, classify temporal properties, inspect signed-graph consistency, and add stronger qualitative knowledge without overstating what it proves.

Reachable versus total state spaces

Build the spring from Lesson 5:

import qrlib as qr
from qrlib import Qdir, TimeTag

spring = qr.Model("spring")
for name in ("x", "v", "a"):
    spring.variable(name, landmarks=("0",), unbounded=True)
spring.constrain(qr.Deriv("x", "v"))
spring.constrain(qr.Deriv("v", "a"))
spring.constrain(qr.Minus("x", "a"))

spring_initial = spring.state(
    time=TimeTag.POINT,
    x=("0", Qdir.INC),
    v=(("0", "+inf"), Qdir.STD),
    a=("0", Qdir.DEC),
)

Ordinary simulation explores what is reachable from that initial state. Attainable-envisionment mode merges equal reachable states into a graph:

attainable = qr.qsim(
    spring,
    spring_initial,
    config=qr.SimConfig(envisionment=True, discover_landmarks=False),
)

Total envisionment starts without an initial state and enumerates every constraint-consistent state in one region:

total = qr.envision(spring)
print(total.stats["states"], len(total.cycles()))

The reachable graph must embed in the total portrait, but the total portrait may contain equilibria and transient states unreachable from your chosen initial condition. A hard max_states limit raises an error: a silently partial “total” envisionment would be a contradiction in terms.

Temporal logic: classify or guide

Classify the existing reachable graph when the question is “does every behavior of this model satisfy the property?”:

from qrlib import guide
from qrlib.guide import F, G, mag

cycle_result = qr.qsim(spring, spring_initial)
returns_to_zero = G(F(mag("x", "==", "0")))
classification = guide.classify(cycle_result, returns_to_zero)
print(classification.universal)               # True

universal is the sound direction: because the graph soundly over-covers the real behaviors, a property that holds across all of them holds for the real system too. A non-empty satisfied set, by contrast, reports possible behaviors — a witness there is not a proof that any real behavior satisfies the property.

Use guide.guided when the temporal formula is part of the problem definition—an observation, boundary condition, or exogenous input—and you want it to prune generation. The generated graph then covers real behaviors conditioned on that formula.

Signed-graph consistency

The basic monotonicity checker asks whether all M+, M-, and Minus relationships admit one consistent assignment of orthant polarities:

from qrlib.analysis import monotonicity

sign_model = qr.Model("signed cycle")
for name in ("a", "b", "c"):
    sign_model.variable(name, landmarks=("0",), unbounded=True)
sign_model.constrain(qr.MPlus("a", "b"))
sign_model.constrain(qr.MPlus("b", "c"))
sign_model.constrain(qr.MMinus("c", "a"))

certificate = monotonicity.check_signed_graph(sign_model)
print(certificate.is_consistent)              # False
print([edge.kind for edge in certificate.conflict_cycle])

The returned negative cycle is a concrete structural conflict witness. A positive certificate is not a proof that a nonlinear vector field is a monotone dynamical system; it is only an orthant-consistency check over the declared signed relationships.

For multi-region models, check regions separately. Mutually exclusive positive and negative relationships may each be consistent in their own region even though their union is not.

Order-of-magnitude knowledge

Negligible(small, large) declares |small| < |large| throughout every region where it is active:

ordered = qr.Model("dominant sum")
for name in ("small", "large", "total"):
    ordered.variable(name, landmarks=("0",), unbounded=True)
ordered.constrain(qr.Add("small", "large", "total"))
ordered.constrain(qr.Negligible("small", "large"))
ordered.compile()

That inequality lets sign algebra resolve sums whose dominant operand is known. It is a global model assertion, not a floating-point “small enough” tolerance. Cyclic declarations such as Negligible(a, b) and Negligible(b, a) are contradictions.

Phase-space non-intersection

For an autonomous phase pair connected by Deriv(x, v), the optional phase filter rejects provable non-monotone returns across the same directed transversal:

phase_checked = qr.qsim(
    spring,
    spring_initial,
    config=qr.SimConfig(
        phase_pairs=(("x", "v"),),
    ),
)
print(phase_checked.stats["phase_filtered"])
print(phase_checked.stats["config_adjustments"])
# ['enabled landmark discovery for phase_pairs']

The declaration enables landmark discovery because the filter needs named turning points for its crossing comparisons. The filter acts only when landmark order proves a crossing conflict; unknown or unseparated crossings survive. It therefore strengthens QSIM without turning the library into a numeric reachability engine.

Choosing the right question

• Use qsim for futures reachable from an initial state.
• Use envision for the complete qualitative portrait of one region.
• Use guide.classify for temporal model checking of an existing graph.
• Use guide.guided to condition generation on a temporal specification.
• Use monotonicity checking for signed-graph contradictions.
• Use Negligible, energy, or phase filtering only when their premises are valid physical knowledge.

Exercises

1. Replace the final MMinus in the signed cycle with MPlus and inspect the polarity assignment.
2. Compare len(attainable.graph.nodes) with the number of nodes in total.
3. Compare behavior counts for the spring with and without phase_pairs, and inspect the phase-checked result's effective configuration and adjustment telemetry.

Next: 14. Composition, tensors, and scale →