Typowe projekty zabawka z TLA + są w linii:
- model kontrolera dźwigu: dźwig ma n drzwi i trzeba będzie modelować zarówno warunki zachowania i bezpieczeństwa, na przykład, że raz na górze winda już nie będzie się przesuwać, albo że nie powinniśmy mieć jednocześnie otwartych dwojga drzwi, a drzwi nie zostaną otwarte, gdy kabina nie znajduje się przed nim, i wiele innych.
- Sterownik sygnalizatorów świetlnych: na prostym przykładzie proste skrzyżowanie z wieloma ograniczeniami, takimi jak światła skierowane, jest zsynchronizowane, a jeśli jedna oś ma kolor zielony, inne mają kolor czerwony. Możesz zawęzić przedmiot, dodając wykrycie stanu ruchu i czasu.
- Model pralki: zwłaszcza szafki na drzwi i proste programy. Udowodnij, że nie ma sposobu, aby zamknąć drzwi, to jest zawsze istnieje rozwiązanie, które pozwoli ci uwolnić ciuchy (nawet jeśli są mokre) w ograniczonym czasie (musisz wziąć pod uwagę etap eliminacji wody), bez pobierania zbyt dużej ilości wody twoja podłoga.
W ogóle, ciekawe projekty dla lalek TLA + powinny łączyć stosunkowo proste zachowania i warunków strukturalnych i bezpieczeństwa, tak, że będzie w stanie zweryfikować zachowanie zdefiniowaną nie unieważnia warunki bezpieczeństwa.