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

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

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.