EXPERIMENT 04 · FORWARD GENERATION
One mechanism.
Many ways through.
Review the rules. Choose the project state. Explore the ways to finish the refuge—and see what makes each plan possible.
One starting state can admit different work branches, resource allocations and task orders. Each retained plan carries its own justification.
A FICTIONAL CLIFFSIDE REFUGE
Explore the possibilities
Review or edit the mechanism and completion goal
Input tokens are consumed at a task’s start; outputs appear at its finish. The model declares all available tasks. Each task may occur at most once in this experiment. Resources, durations and goal conditions are assumptions to review.
| Task | Needs at start | Supplies at finish | Duration |
|---|
Editing this definition changes the supplied model. Select Generate plans to check it. No file or remote model is overwritten.
Ways to reach the goal
Work branches show which tasks an execution uses. Each plan below fixes a token-supply history and displays its earliest schedule. Different legal orders can describe the same plan witness.
Representative schedule
On a small screen, scroll sideways to see the full schedule. Keyboard: focus the chart and use the arrow keys.
Work structure
Why this plan is admitted
Follow the supplies through the execution
A wire carries a declared place type and token count. Separate resources remain separate supplies. Unused context passes through to the output.
Scroll sideways on a small screen; the supply table below retains every wire.
Typed composition and identity context
A marking records available tokens after completed atomic work. Choose a reachable state and ask which tasks can start together. This is a decision point with no ongoing timed work.
All enabled starts from this state
The state graph includes possible continuations after goal coverage. Plan generation stops each serial execution when it first covers the goal. These are different, explicitly stated views.
Keep three kinds of variation separate
- Choose a plan
- Select a different execution or allocation within the same model and starting state.
- Change the marking
- Vary available resources or initial conditions. A new state may enable different work or concurrency.
- Change the mechanism
- Revise what a task needs or supplies. This changes the engineering assumption, and requires its own review.
Exactness of a sequential-order language does not establish concurrency or timing equivalence. A work tree belongs to the selected witness; one tree need not represent every alternative.
Keep and revisit this model
Save a copy in this browser or download a portable model. Opening a saved copy recomputes its result; imported claims are never treated as verification.
No save made in this session.
From source methods to an inspectable result
A forward experiment
The mechanism supplies the choices. The search retains reachable states, joint starts and complete bounded branches. Typed supply histories then justify particular schedules. A tree is offered only when it preserves that witness’s dependency order.
The method draws on the foray’s highlighted Petri, categorical-composition and project-scheduling papers. See how each method is used.
What the checks mean
These are finite calculations under supplied assumptions, independently challenged by agents. They are not engineering approval, human-use validation or a general theorem about every Petri net.
Dates, durations and resources are illustrative. The search reports its bounds; a partial result is not evidence that no other plan exists.