TLA+ and Program Snippets

[Amirhosein Sayyadabdi]

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?

I really appreciate any help you can provide.

Amirhosein Sayyadabdi

University of Isfahan

[Amirhosein Sayyadabdi]

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,

Amirhosein Sayyadabdi

[Maroš Orsák]

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>>

[1] - https://lamport.azurewebsites.net/tla/book.html

[2] - https://github.com/tlaplus/Examples

[3] - https://www.hillelwayne.com/post/list-of-tla-examples/

Best regards,

Ing. Maros Orsak,

Senior Software Quality Enginner

pi 13. 10. 2023 o 10:48 Amirhosein Sayyadabdi <amir.ah...@gmail.com> napísal(a):

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0tNV5UnreVkoW8a1ms9n%2BbejK7RkmfgRj3Xbb3a3kk7eA%40mail.gmail.com.