MBT with LTS 1
===============================================================================
+Terminology:
+s0->s1 transition
+s0=>s1 transition composition
+s0=> executable sequence
+s0=/> non-executable sequence
+
+trace: sequence of possible
+reachable states: s after omega
+- s: state
+- omega: trace
+
+Representation
+- 4-tuple: (S, L, T, s0) States, Labels, Transition function, initial state
+- tree/graph
+- language/behaviour expression:
+ - := : assignment
+ - stop : termination
+ - ; : sequence
+ - label: transition input
+ - [] : choice
+ - ||| : parallel
+ - |[G]|: parallel synchronized on elements in G
+- equivalence from strong to weak
+ - isomorphism: need to observe tau
+ - bisimulation: infinite undo, copy and repeat
+ - failure trace: test with another lts and continue on failure
+ - testing trace: test LTS with another LTS
+ - completed trace: observe sequence and end
+ - trace: observe sequence
MBT with LTS 2
===============================================================================