FSM-based testing
===============================================================================
FSM: States, transitions, inputs, outputs
(S, s0, I, O, delta, lambda)
(States, initial, inputs, outputs, transition function, output function)

- Deterministic, complete, connected, reduced
- Tests length k only prove models with k extra states(k-complete)
- With resets
- W method
	- we test a state by testing that after reaching it the input/output is
	  good
- Transition tour, one loop all transitions
- Synchonizing, get always to a fixed state

- Compare with LTS:
	- has to be deterministic and complete
	- Only i/o alternation
	- not compositional
	- more intuitive
	- older theory

MBT with LTS 1
===============================================================================

MBT with LTS 2
===============================================================================

MBT with LTS 3
===============================================================================

MBT with LTS 4
===============================================================================


MBT with GAST
===============================================================================
Functional, black box, cycle detection, automatic generation, quickcheck,
quantification
- Property
- Model

MBT with SpecExplorer
===============================================================================