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

[Lee <fowler.lee8@xxxxxxxxx>]

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.