* [[tutorial:model:vending_machine:start|Modelling with Finite State Machines: Vending machine]]
  * [[tutorial:method:petri_synthesis:start|Petri net synthesis: Concurrent vending machine]]
  * [[tutorial:model:dining_philosophers:start|Modelling with Petri nets: Dining philosophers]]
  * [[tutorial:model:distributed_mutual_exclusion:start|Modelling with STGs: Distributed Mutual Exclusion]]
  * [[tutorial:model:read_write_lock:start|Modelling with STGs: Writer-biased read/write lock]]
  * [[tutorial:model:phage_lambda:start|Modelling Genetic Regulatory Networks with STGs: Lysis-Lysogeny switch in Phage λ]]
  * [[tutorial:method:pipeline_wagging:start|Optimising asynchronous pipelines using wagging]]
  * [[tutorial:method:temporal_verification:start|Verification of temporal properties of asynchronous systems]]