From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 21 Jan 2016 14:03:57 +0000 (+0100)
Subject: mbt slides1 done
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=07ef096f834c17ae167d8eadc127c04b9ea131f7;p=tt1516.git

mbt slides1 done
---

diff --git a/recap_mbt.txt b/recap_mbt.txt
index ded951e..b56d7c6 100644
--- 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
 ===============================================================================