[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Maroš Orsák <maros.orsak159@xxxxxxxxx>*Date*: Fri, 13 Oct 2023 11:13:03 +0200*References*: <CAKxfy0uzWcRqDXJPmjyx-cWeNDwjykUzakcgHBB9Y2h=kupYeQ@mail.gmail.com> <CAKxfy0tNV5UnreVkoW8a1ms9n+bejK7RkmfgRj3Xbb3a3kk7eA@mail.gmail.com>

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]

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)

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

```

----------------- 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,Amirhosein Sayyadabdi--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?I really appreciate any help you can provide.Amirhosein SayyadabdiUniversity of Isfahan

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0tNV5UnreVkoW8a1ms9n%2BbejK7RkmfgRj3Xbb3a3kk7eA%40mail.gmail.com.

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAMd-2QsiwXshDO1Kt86K312OdYM_c94Lshg9T7GZOXDSK3gGcA%40mail.gmail.com.

**References**:**[tlaplus] TLA+ and Program Snippets***From:*Amirhosein Sayyadabdi

**[tlaplus] Re: TLA+ and Program Snippets***From:*Amirhosein Sayyadabdi

- Prev by Date:
**[tlaplus] Re: TLA+ and Program Snippets** - Next by Date:
**[tlaplus] Can I get the command line used by the toolbox?** - Previous by thread:
**[tlaplus] Re: TLA+ and Program Snippets** - Next by thread:
**[tlaplus] Can I get the command line used by the toolbox?** - Index(es):