# Re: [tlaplus] Re: TLA+ and Program Snippets

Hi Amirhosein,

I am also new to the Google group mailing list but I can describe my approach to learning TLA+:

1. I started with the book [1]
2. then I have moved to GitHub sources [2]
3. What I have found very useful is all the content from Hille Wayne [3]

and then when I grasped the first beginner phase of learning TLA+ I tried to experiment with the Chat-GPT 4 and generate such examples as you mentioned and I was impressed with the results.
A straightforward example of a recursive function model in TLA+


----------------- MODULE Factorial -----------------
EXTENDS Naturals

VARIABLES n, result

(* Recursive factorial function *)
RECURSIVE Fact(_)
Fact(x) ==
IF x = 0 THEN 1
ELSE x * Fact(x-1)

(* Initialization *)
Init ==
/\ n \in 0..5  (* We limit n to a small number for illustration purposes *)
/\ result = Fact(n)

(* Safety property: The result should be the factorial of n *)
Safety == result = Fact(n)

====================================================


Spec could be defined as Spec == Init /\ [][UNCHANGED <<n, result>>]_<<n, result>>

Best regards,

Ing. Maros Orsak,

Senior Software Quality Enginner

pi 13. 10. 2023 o 10:48 Amirhosein Sayyadabdi <amir.ahsa.2011@xxxxxxxxx> napísal(a):
I understand I may have asked a stupid question in my previous email, but any help would be appreciated. If Java snippets in TLA+ or PlusCal are not plausible or useless, then please help me understand how to define and manipulate complex data structures (for example, multi-dimensional arrays of structs) in either TLA+ or PlusCal.

Regards,

On Wed, Oct 11, 2023 at 6:15 AM Amirhosein Sayyadabdi <amir.ahsa.2011@xxxxxxxxx> wrote:
Hello everyone,

I am searching for examples of tiny program snippets (for example; Java classes, loops, inheritance, recursive functions, etc.) in TLA+ or PlusCal. Do you know if there is any particular source I can refer to?