2 ===============================================================================
3 FSM: States, transitions, inputs, outputs
4 (S, s0, I, O, delta, lambda)
5 (States, initial, inputs, outputs, transition function, output function)
7 - Deterministic, complete, connected, reduced
8 - Tests length k only prove models with k extra states(k-complete)
11 - we test a state by testing that after reaching it the input/output is
13 - Transition tour, one loop all transitions
14 - Synchonizing, get always to a fixed state
17 - has to be deterministic and complete
18 - Only i/o alternation
24 ===============================================================================
27 s0=>s1 transition composition
28 s0=> executable sequence
29 s0=/> non-executable sequence
31 trace: sequence of possible
32 reachable states: s after omega
37 - 4-tuple: (S, L, T, s0) States, Labels, Transition function, initial state
39 - language/behaviour expression:
43 - label: transition input
46 - |[G]|: parallel synchronized on elements in G
47 - equivalence from strong to weak
48 - isomorphism: need to observe tau
49 - bisimulation: infinite undo, copy and repeat
50 - failure trace: test with another lts and continue on failure
51 - testing trace: test LTS with another LTS
52 - completed trace: observe sequence and end
53 - trace: observe sequence
56 ===============================================================================
59 ===============================================================================
62 ===============================================================================
66 ===============================================================================
67 Functional, black box, cycle detection, automatic generation, quickcheck,
73 ===============================================================================