[tlaplus] Looking for Guidance on Getting Started with TLA+: Tips for a New Learner

[王圣予 <wshengyu3001@xxxxxxxxx>]

I’ve found that the fastest way to get familiar with a new tool is to practice and ask questions. After learning the basic TLA⁺ syntax, I started writing small examples. A bit of research showed that TLA⁺ is great at exploring the state space of concurrent programs, so I opened Rust Atomics and Locks and tried to model one of its simplest examples.

It shows a simple example in Chapter One:

```rust

use std::thread;

fn main() {
    let t1 = thread::spawn(f);
    let t2 = thread::spawn(f);

    println!("Hello from the main thread.");

    t1.join().unwrap();
    t2.join().unwrap();
}

fn f() {
    println!("Hello from another thread!");

    let id = thread::current().id();
    println!("This is my thread id: {id:?}");
}

```

I want to pretend that I have never learnt concurrent program and feel puzzle about the result of running this program 1000 times:

```
counts: 5
pattern:
Hello from the main thread.
Hello from another thread!
This is my thread id: ThreadId(3)
Hello from another thread!
This is my thread id: ThreadId(2)

counts: 930
pattern:
Hello from the main thread.
Hello from another thread!
This is my thread id: ThreadId(2)
Hello from another thread!
This is my thread id: ThreadId(3)

...

```

My first idea was to use the TLA⁺ model checker to explore the entire state space. However, I think TLA⁺ is designed to check whether all behaviors satisfy a specification, and simply defining an ideal sequence as the spec doesn’t give me the insight I’m looking for.

Given a simple example like this, how should I think about modeling it idiomatically in TLA⁺ so that I can explore the possible execution orders?

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/98a4015d-e154-4b7a-93a0-66f881f826d3n%40googlegroups.com.