mbt slides1 done

diff --git a/recap_mbt.txt b/recap_mbt.txt
index ded951e..b56d7c6 100644 (file)
--- a/recap_mbt.txt
+++ b/recap_mbt.txt
@@ -22,6 +22,35 @@ FSM: States, transitions, inputs, outputs
 
 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
 ===============================================================================