Re: [tlaplus] Question: how to describe the network message from ewd687a/EWD687aPlusCal.tla in Rust?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Hi Lee,

I don't have time for a longer response, but you might find some inspiration from my Java implementation [1] of EWD998 (also distributed termination detection).

Markus

[1] https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/impl/src/EWD998.java

> On Jun 19, 2024, at 2:55 AM, Lee <fowler.lee8@xxxxxxxxx> wrote:
> 
> Hello All,
> 
> The following is a question about how to implement a certain piece of TLA+ in Rust, Python, Java Or Go (any language will do, I just need to get my head around it):
> 
> I am implementing the algorithm ewd687a/EWD687aPlusCal.tla from the Specifications listed on GitHub for the TLAExamples repo. I am having difficulty describing the TLA+ statement for the network in Rust (see below):
> 
> This is the statement in the spec and the part I find tricky is: msg->[snd \in Node |-> 0]: 
> 
> (* For every node we keep the following counters:
> - number of base messages received, per sending node
> - number of ack messages received *)
> network = [n \in Node |-> [msg |-> [snd \in Node |-> 0], ack |-> 0]]
> 
> My hope is to get some guidance on how one might describe the network as a struct in the form:
> 
> struct Message {
> from: Node,
> ack: u16, 
> }
> 
> #[derive(Debug, Clone)]
> pub struct Node {
> pub name: String,
> active: bool,
> node: Option<Rc<RefCell<Node>>>,
> message: u32,
> ack: u32,
> }
> 
> struct Network {
> network: VecDeque<Node>,
> status: Vec<Message>,
> termination_detection: bool,
> }
> ________________________________________
> I probably have it quite wrong so thank you for any tips you can provide.
> 
> King Greetings
> Lee F
> 
> -- 
> 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/4a42707b-1bcf-4b53-99c3-3c5eede1da4cn%40googlegroups.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/A4C3654D-FD8B-46EF-B3F2-A08036907F2D%40lemmster.de.