Tutorial roadmap
Use this page when you are learning pyfcstm for the first time and want a small, observable success after each step. The global sidebar lists the tutorial pages directly; this roadmap is only the sibling guide that explains which page to read next, why that page belongs in the tutorial path, and where to leave the path when you need task recipes, explanations, or reference facts.
Role: this page is the Tutorial router for first-success learning. It gives a safe reading order, identifies the result each tutorial should produce, and keeps beginners from falling into reference-level detail too early.
Non-goals: this page is not the complete DSL reference, not a CLI option table, not the inspect schema, not a generated-template contract, and not the API map. When you need exact facts, use Reference map; when you already know the task, use How-to roadmap; when you need reasoning, use Explanation map.
How to read tutorial pages
Tutorial pages should teach one primary success path. They intentionally stop before every option, every edge case, or every diagnostic code. A tutorial is acceptable when it gives you an input, a command or short code fragment, visible output, and a next link that tells you where broader coverage lives.
The strongest signal that you should leave Tutorials is that your question has changed from “what is the first working path?” to “how do I repeat this in my own project?” or “what is the exact legal form?”. At that point, the sibling areas are more useful than another tour.
New-user path
Follow this route if you have not used pyfcstm before.
Start with Quick Start to prove that the installed command can simulate, inspect, generate, and export from one small file.
Read Write your first FCSTM DSL model to understand the source file shape behind that first run.
Choose the first feedback loop: FCSTM simulation first run if you want runtime behavior, or First inspect report if you want model structure and diagnostic feedback.
Read First generated runtime when you want generated Python output from the same model.
Finish the first learning loop with First diagram so the model can be explained with a diagram.
Treat Your First Bounded Model Check as the advanced capstone after you can already read an FCSTM model and one concrete runtime trace. It replaces one chosen event sequence with a bounded symbolic search over all allowed sequences.
Experienced-user path
Use this route if you already know the project shape and only need the tutorial that refreshes one workflow.
Already have an FCSTM file but do not trust it yet: jump to First inspect report and then to Diagnostics code reference.
Already have a valid model but need behavior evidence: jump to FCSTM simulation first run and then to Simulation tasks.
Already know the model and need output files: jump to First generated runtime or First diagram and then to the matching how-to page.
Already understand concrete traces and need evidence about every behavior up to a finite bound: finish with Your First Bounded Model Check.
Already need exact syntax, command options, or schema fields: skip tutorials and start at Reference map.
Maintainer path
Use this route when reviewing or extending tutorial material.
Confirm each tutorial has a realistic starting state and a single primary success path.
Confirm each command or code block has a short observable result rather than a long opaque script.
Confirm every tutorial states where it stops and links to the how-to, explanation, or reference page that owns the remaining depth.
Confirm Chinese and English tutorial pages teach the same capability and expose the same risk boundaries, even when the prose is not word-for-word identical.
Reader completion signals
After a tutorial, readers should be able to answer three questions.
What input file did I just run or read?
What did the output, state change, report, or diagram prove?
Where should I leave the tutorial when I need to repeat, look up, or explain the same behavior?
If those questions are still unclear, the tutorial needs a shorter output excerpt, a clearer result explanation, or a more explicit next link. If those questions are already clear, do not move reference tables into the tutorial; send the reader to the matching how-to guide, explanation, or reference page.
A tutorial may stay compact, but it must make the completed learning loop and the next document role visible.
Sibling tutorial cards
Quick start: Quick Start
Prerequisites: Python and the pyfcstm command are available, or you are ready
to follow Install pyfcstm first.
Outcome: you run the shortest end-to-end command chain over one traffic-light model and see simulation, inspect, generation, and PlantUML output families.
Non-goal: it does not explain every command option, every generated file, or the semantics behind state-machine execution.
Next step: read Write your first FCSTM DSL model when you want to understand the input file, or jump to CLI workflows when you only need repeatable command recipes.
DSL tutorial: Write your first FCSTM DSL model
Prerequisites: you have seen a tiny FCSTM file in the quick start and can edit a plain text file.
Outcome: you can build a small model with states, transitions, guards, lifecycle actions, and one deliberate repair step.
Non-goal: it is not the exhaustive grammar; legal forms, illegal forms, sugar expansion, and diagnostics live in DSL reference.
Next step: read FCSTM simulation first run to execute the model, or DSL semantics explanation to understand why those constructs mean what they mean.
Simulation tutorial: FCSTM simulation first run
Prerequisites: you have a valid sample model and want to observe active-state movement rather than only parse text.
Outcome: you can run a batch transcript or a short Python runtime loop and recognize the active path after cycles or events.
Non-goal: it does not catalog every REPL command, display setting, history format, or hot-start boundary.
Next step: use Simulation tasks for repeatable tasks and Simulation reference for exact command and API facts.
Inspect tutorial: First inspect report
Prerequisites: you have a model and want pyfcstm to report what it parsed, what it inferred, and which diagnostics can guide repair.
Outcome: you can produce human, JSON, and LLM-oriented inspect outputs and know why diagnostics can guide a human or an LLM back to source spans.
Non-goal: it does not enumerate every JSON field, diagnostic code, severity, or optional verification boundary.
Next step: use Inspect tasks for triage recipes, then Inspect report reference and Diagnostics code reference for exact lookup.
Generation tutorial: First generated runtime
Prerequisites: you have a valid model and want the packaged built-in Python template to produce files without hand-editing template internals.
Outcome: you can run pyfcstm generate --template python and inspect the
first generated runtime artifacts.
Non-goal: it does not teach custom template authoring, every built-in target contract, formatter policy, or renderer internals.
Next step: use Generation tasks for target-specific recipes, Template author tasks for authoring, and Template rendering explanation for the rendering pipeline.
Visualization tutorial: First diagram
Prerequisites: you have a valid model and want a diagram source or rendered artifact that explains structure to another reader.
Outcome: you can export PlantUML source, understand what the rendered example proves, and try the first detail presets.
Non-goal: it does not list every visualization option, renderer backend, suffix rule, or headless/CI boundary.
Next step: use Visualization tasks for diagram tasks and Visualization options reference for exact option behavior.
Bounded model checking: Your First Bounded Model Check
Prerequisites: you have completed the DSL tutorial and can interpret at least one concrete trace from Simulation or Inspect. You understand that a cycle can change both the active state and persistent variables.
Outcome: you replace one hand-picked execution with a bounded symbolic search, state a meaningful safety property, read a counterexample trace, repair the model, and understand why the repaired bounded result is not an unbounded proof.
Non-goal: it does not enumerate the FBMCQ grammar or derive every transition relation and property objective.
Next step: repeat practical checks with BMC Task Recipes, understand the mathematics through How FCSTM Becomes a Bounded Transition System, or look up exact query forms in FBMCQ Language Reference.
Where the tutorial path stops
Leave Tutorials deliberately when you need breadth or precision. Repeated operations belong in How-to Guides, design reasoning belongs in Explanations, and exact facts belong in Reference. That split keeps the first-success path short while still giving each capability a deeper owner.
Compatibility landing pages
The following old tutorial URLs remain reachable as compatibility landing notes. They protect old links and point to the current owner pages, but they are not part of the seven sibling tutorial cards above.